DyadicCoordinates.lean

1 import PaperXI.DyadicAffine
2 import PaperXI.DyadicGauss
3 import Mathlib.LinearAlgebra.Pi
4 
5 /-! Every quadratic refinement in symplectic coordinates has unique linear
6 coefficients. This identifies all refinements, not only a chosen family. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.DyadicCoordinates
10 open scoped BigOperators Classical
11 open PaperXI.Dyadic PaperXI.DyadicAffine
12 
13 variable {ι : Type*} [Fintype ι]
14 
15 def symplectic : (ι → F2 × F2) →ₗ[F2] (ι → F2 × F2) →ₗ[F2] F2 where
16   toFun x :=
17     { toFun := fun y => ∑ i, ((x i).1 * (y i).2 + (x i).2 * (y i).1)
18       map_add' := by
19         intro y z
20         simp only [Pi.add_apply, Prod.fst_add, Prod.snd_add]
21         rw [← Finset.sum_add_distrib]
22         apply Finset.sum_congr rfl
23         intro i hi
24         ring
25       map_smul' := by
26         intro r y
27         change (∑ i, ((x i).1 * (r * (y i).2) + (x i).2 * (r * (y i).1))) =
28           r * (∑ i, ((x i).1 * (y i).2 + (x i).2 * (y i).1))
29         rw [Finset.mul_sum]
30         apply Finset.sum_congr rfl
31         intro i hi
32         ring }
33   map_add' := by
34     intro x z
35     apply LinearMap.ext
36     intro y
37     change (∑ i, (((x + z) i).1 * (y i).2 + ((x + z) i).2 * (y i).1)) =
38       (∑ i, ((x i).1 * (y i).2 + (x i).2 * (y i).1)) +
39       (∑ i, ((z i).1 * (y i).2 + (z i).2 * (y i).1))
40     rw [← Finset.sum_add_distrib]
41     apply Finset.sum_congr rfl
42     intro i hi
43     simp only [Pi.add_apply, Prod.fst_add, Prod.snd_add]
44     ring
45   map_smul' := by
46     intro r x
47     apply LinearMap.ext
48     intro y
49     change (∑ i, ((r * (x i).1) * (y i).2 + (r * (x i).2) * (y i).1)) =
50       r * (∑ i, ((x i).1 * (y i).2 + (x i).2 * (y i).1))
51     rw [Finset.mul_sum]
52     apply Finset.sum_congr rfl
53     intro i hi
54     ring
55 
56 @[simp] theorem symplectic_apply (x y : ι → F2 × F2) :
57     symplectic x y = ∑ i, ((x i).1 * (y i).2 + (x i).2 * (y i).1) := rfl
58 
59 theorem quadratic_polar (a x y : ι → F2 × F2) :
60     quadratic a (x + y) = quadratic a x + quadratic a y + symplectic x y := by
61   simp only [quadratic, plane, Pi.add_apply, Prod.fst_add, Prod.snd_add,
62     symplectic_apply, ← Finset.sum_add_distrib]
63   apply Finset.sum_congr rfl
64   intro i hi
65   ring
66 
67 def coordinateRefinement (a : ι → F2 × F2) : Refinement (symplectic (ι := ι)) where
68   value := quadratic a
69   polar := quadratic_polar a
70 
71 def firstAxis (i : ι) : ι → F2 × F2 := Pi.single i (1, 0)
72 def secondAxis (i : ι) : ι → F2 × F2 := Pi.single i (0, 1)
73 
74 omit [Fintype ι] in
75 theorem single_axes (i : ι) (z : F2 × F2) :
76     Pi.single i z = z.1 • firstAxis i + z.2 • secondAxis i := by
77   ext j <;> by_cases h : j = i <;> simp [firstAxis, secondAxis, h]
78 
79 def linearCoefficients (l : (ι → F2 × F2) →ₗ[F2] F2) : ι → F2 × F2 :=
80   fun i => (l (firstAxis i), l (secondAxis i))
81 
82 theorem linear_coordinate_formula (l : (ι → F2 × F2) →ₗ[F2] F2)
83     (x : ι → F2 × F2) :
84     l x = ∑ i, ((linearCoefficients l i).1 * (x i).1 +
85       (linearCoefficients l i).2 * (x i).2) := by
86   conv_lhs => rw [← Finset.univ_sum_single x]
87   rw [map_sum]
88   apply Finset.sum_congr rfl
89   intro i hi
90   rw [single_axes, map_add, map_smul, map_smul]
91   simp [linearCoefficients, mul_comm]
92 
93 @[simp] theorem quadratic_firstAxis (a : ι → F2 × F2) (i : ι) :
94     quadratic a (firstAxis i) = (a i).1 := by
95   unfold quadratic
96   rw [Finset.sum_eq_single i]
97   · simp [plane, firstAxis]
98   · intro j hj hji
99     simp [plane, firstAxis, Pi.single_eq_of_ne hji]
100   · simp
101 
102 @[simp] theorem quadratic_secondAxis (a : ι → F2 × F2) (i : ι) :
103     quadratic a (secondAxis i) = (a i).2 := by
104   unfold quadratic
105   rw [Finset.sum_eq_single i]
106   · simp [plane, secondAxis]
107   · intro j hj hji
108     simp [plane, secondAxis, Pi.single_eq_of_ne hji]
109   · simp
110 
111 def refinementCoefficients (q : Refinement (symplectic (ι := ι))) : ι → F2 × F2 :=
112   linearCoefficients (linearDifference q (coordinateRefinement 0))
113 
114 theorem refinement_coordinate_formula (q : Refinement (symplectic (ι := ι)))
115     (x : ι → F2 × F2) : q.value x = quadratic (refinementCoefficients q) x := by
116   have h := linear_coordinate_formula (linearDifference q (coordinateRefinement 0)) x
117   simp only [linearDifference_apply, coordinateRefinement] at h
118   dsimp only [refinementCoefficients]
119   simp only [quadratic, plane, Pi.zero_apply, Prod.fst_zero, Prod.snd_zero,
120     zero_mul, add_zero] at h ⊢
121   simp only [Finset.sum_add_distrib] at h ⊢
122   dsimp only [coordinateRefinement] at h ⊢
123   linear_combination h
124 
125 @[simp] theorem refinementCoefficients_coordinateRefinement (a : ι → F2 × F2) :
126     refinementCoefficients (coordinateRefinement a) = a := by
127   ext i <;> simp [refinementCoefficients, linearCoefficients, coordinateRefinement]
128 
129 /-- Complete parameterization of all refinements in symplectic coordinates. -/
130 def coordinateEquiv : (ι → F2 × F2) ≃ Refinement (symplectic (ι := ι)) where
131   toFun := coordinateRefinement
132   invFun := refinementCoefficients
133   left_inv := refinementCoefficients_coordinateRefinement
134   right_inv q := by
135     ext x
136     exact (refinement_coordinate_formula q x).symm
137 
138 @[simp] theorem refinementCoefficients_apply
139     (q : Refinement (symplectic (ι := ι))) (i : ι) :
140     refinementCoefficients q i = (q.value (firstAxis i), q.value (secondAxis i)) := by
141   simp [refinementCoefficients, linearCoefficients, coordinateRefinement]
142 
143 /-- The coefficient Arf value is precisely the sum of products of values on
144 the paired symplectic basis vectors. -/
145 theorem arf_basis_formula (a : ι → F2 × F2) :
146     arf a = ∑ i, quadratic a (firstAxis i) * quadratic a (secondAxis i) := by
147   simp [arf]
148 
149 theorem refinement_arf_basis_formula (q : Refinement (symplectic (ι := ι))) :
150     arf (refinementCoefficients q) =
151       ∑ i, q.value (firstAxis i) * q.value (secondAxis i) := by
152   simp [arf]
153 
154 /-- Gauss evaluation for every actual refinement of the coordinate form. -/
155 theorem refinement_gauss_sum (q : Refinement (symplectic (ι := ι))) :
156     (∑ x, sign (q.value x)) =
157       sign (∑ i, q.value (firstAxis i) * q.value (secondAxis i)) *
158         2 ^ Fintype.card ι := by
159   simp_rw [refinement_coordinate_formula q]
160   rw [gauss_sum, arf_basis_formula]
161 
162 end PaperXI.DyadicCoordinates

Back to source controls