DyadicRefinement.lean

1 import PaperXI.DyadicCoordinates
2 import PaperXI.DyadicTranslation
3 
4 /-! Translation and opposite phases for all refinements of the actual
5 coordinate symplectic form, with the Arf value evaluated on basis vectors. -/
6 noncomputable section
7 set_option autoImplicit false
8 namespace PaperXI.DyadicRefinement
9 open scoped BigOperators Classical
10 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates
11 variable {ι : Type*} [Fintype ι]
12 
13 def basisArf (q : Refinement (symplectic (ι := ι))) : F2 :=
14   ∑ i, q.value (firstAxis i) * q.value (secondAxis i)
15 
16 @[simp] theorem basisArf_coordinateRefinement (a : ι → F2 × F2) :
17     basisArf (coordinateRefinement a) = arf a := by
18   simp [basisArf, coordinateRefinement, arf]
19 
20 theorem translation_refinement (q : Refinement (symplectic (ι := ι)))
21     (v : ι → F2 × F2) :
22     addLinear q (symplectic v) =
23       coordinateRefinement (translate (refinementCoefficients q) v) := by
24   ext x
25   change q.value x + symplectic v x = quadratic _ x
26   rw [refinement_coordinate_formula, quadratic_translate]
27   rfl
28 
29 theorem arf_translation (q : Refinement (symplectic (ι := ι)))
30     (v : ι → F2 × F2) :
31     basisArf (addLinear q (symplectic v)) = basisArf q + q.value v := by
32   rw [translation_refinement, basisArf_coordinateRefinement, arf_translate,
33     refinement_arf_basis_formula, ← refinement_coordinate_formula]
34   rfl
35 
36 theorem opposite_refinements (i : ι) :
37     ∃ q r : Refinement (symplectic (ι := ι)),
38       basisArf q = 0 ∧ basisArf r = 1 ∧
39       (∑ x, sign (r.value x)) = -(∑ x, sign (q.value x)) := by
40   refine ⟨coordinateRefinement 0, coordinateRefinement (anisotropic i), ?_, ?_, ?_⟩
41   · simp
42   · simp [arf_anisotropic]
43   · exact opposite_gauss i
44 
45 theorem sign_eq_neg_one_pow (t : F2) : sign t = (-1 : ℤ) ^ t.val := by
46   fin_cases t <;> decide
47 
48 end PaperXI.DyadicRefinement

Back to source controls