DyadicTranslation.lean

1 import PaperXI.DyadicGauss
2 
3 noncomputable section
4 set_option autoImplicit false
5 namespace PaperXI.Dyadic
6 open scoped BigOperators Classical
7 variable {ι κ : Type*} [Fintype ι] [Fintype κ]
8 
9 def pairing (v x : ι → F2 × F2) : F2 :=
10   ∑ i, ((v i).1 * (x i).2 + (v i).2 * (x i).1)
11 
12 def translate (a v : ι → F2 × F2) : ι → F2 × F2 :=
13   fun i => ((a i).1 + (v i).2, (a i).2 + (v i).1)
14 
15 theorem quadratic_translate (a v x : ι → F2 × F2) :
16     quadratic (translate a v) x = quadratic a x + pairing v x := by
17   simp only [quadratic, pairing, ← Finset.sum_add_distrib]
18   apply Finset.sum_congr rfl
19   intro i _
20   simp only [plane, translate]
21   ring
22 
23 theorem arf_translate (a v : ι → F2 × F2) :
24     arf (translate a v) = arf a + quadratic a v := by
25   simp only [arf, quadratic, ← Finset.sum_add_distrib]
26   apply Finset.sum_congr rfl
27   intro i _
28   simp only [plane, translate]
29   ring
30 
31 theorem gauss_translate (a v : ι → F2 × F2) :
32     (∑ x, sign (quadratic (translate a v) x)) =
33       sign (quadratic a v) * ∑ x, sign (quadratic a x) := by
34   rw [gauss_sum, gauss_sum, arf_translate, sign_add]
35   ring
36 
37 theorem arf_orthogonal (a : ι → F2 × F2) (b : κ → F2 × F2) :
38     arf (Sum.elim a b) = arf a + arf b := by
39   simp [arf, Fintype.sum_sum_type]
40 
41 theorem gauss_orthogonal (a : ι → F2 × F2) (b : κ → F2 × F2) :
42     (∑ x, sign (quadratic (Sum.elim a b) x)) =
43       (∑ x, sign (quadratic a x)) * ∑ x, sign (quadratic b x) := by
44   calc
45     _ = sign (arf (Sum.elim a b)) * 2 ^ Fintype.card (ι ⊕ κ) := by
46       convert gauss_sum (Sum.elim a b) using 1
47       apply Finset.sum_congr
48       · ext x
49         simp
50       · intro x _
51         rfl
52     _ = _ := by
53       rw [gauss_sum a, gauss_sum b, arf_orthogonal, sign_add]
54       simp only [Fintype.card_sum, pow_add]
55       ring
56 
57 theorem sign_orthogonal (a : ι → F2 × F2) (b : κ → F2 × F2) :
58     sign (arf (Sum.elim a b)) = sign (arf a) * sign (arf b) := by
59   rw [arf_orthogonal, sign_add]
60 
61 @[simp] theorem arf_zero : arf (0 : ι → F2 × F2) = 0 := by
62   simp [arf]
63 
64 def anisotropic (i : ι) : ι → F2 × F2 := Pi.single i (1, 1)
65 
66 theorem arf_anisotropic (i : ι) : arf (anisotropic i) = 1 := by
67   classical
68   unfold arf
69   calc
70     _ = ∑ j, if j = i then (1 : F2) else 0 := by
71       apply Finset.sum_congr rfl
72       intro j _
73       by_cases h : j = i <;> simp [anisotropic, h]
74     _ = 1 := by simp
75 
76 theorem opposite_gauss (i : ι) :
77     (∑ x, sign (quadratic (anisotropic i) x)) =
78       -(∑ x, sign (quadratic (0 : ι → F2 × F2) x)) := by
79   rw [gauss_sum, gauss_sum, arf_anisotropic, arf_zero, sign_zero, sign_one]
80   ring
81 
82 theorem both_arf [Nonempty ι] :
83     (∃ a : ι → F2 × F2, arf a = 0) ∧ (∃ a : ι → F2 × F2, arf a = 1) := by
84   constructor
85   · exact ⟨0, arf_zero⟩
86   · obtain ⟨i⟩ := ‹Nonempty ι›
87     exact ⟨anisotropic i, arf_anisotropic i⟩
88 
89 end PaperXI.Dyadic

Back to source controls