DyadicGauss.lean

1 import Mathlib.Data.ZMod.Basic
2 import Mathlib.Algebra.BigOperators.Ring.Finset
3 import Mathlib.Tactic
4 
5 /-! Dyadic quadratic refinements in explicit symplectic coordinates. -/
6 noncomputable section
7 set_option autoImplicit false
8 namespace PaperXI.Dyadic
9 open scoped BigOperators
10 abbrev F2 := ZMod 2
11 
12 def sign (t : F2) : ℤ := if t = 0 then 1 else -1
13 
14 @[simp] theorem sign_zero : sign 0 = 1 := by simp [sign]
15 @[simp] theorem sign_one : sign 1 = -1 := by norm_num [sign]
16 
17 theorem sign_add (a b : F2) : sign (a + b) = sign a * sign b := by
18   fin_cases a <;> fin_cases b <;> decide
19 
20 theorem sign_injective : Function.Injective sign := by
21   intro a b
22   fin_cases a <;> fin_cases b <;> intro h
23   · rfl
24   · change (1 : ℤ) = -1 at h
25     omega
26   · change (-1 : ℤ) = 1 at h
27     omega
28   · rfl
29 
30 theorem sign_sum {ι : Type*} (s : Finset ι) (f : ι → F2) :
31     sign (∑ i ∈ s, f i) = ∏ i ∈ s, sign (f i) := by
32   classical
33   induction s using Finset.induction_on with
34   | empty => simp
35   | @insert a s ha ih => simp [ha, sign_add, ih]
36 
37 def plane (a x : F2 × F2) : F2 := x.1 * x.2 + a.1 * x.1 + a.2 * x.2
38 
39 theorem plane_gauss (a : F2 × F2) :
40     (∑ x : F2 × F2, sign (plane a x)) = sign (a.1 * a.2) * 2 := by
41   rcases a with ⟨a, b⟩
42   fin_cases a <;> fin_cases b <;> decide
43 
44 open scoped Classical
45 variable {ι : Type*} [Fintype ι]
46 
47 def quadratic (a x : ι → F2 × F2) : F2 := ∑ i, plane (a i) (x i)
48 
49 def arf (a : ι → F2 × F2) : F2 := ∑ i, (a i).1 * (a i).2
50 
51 theorem gauss_sum (a : ι → F2 × F2) :
52     (∑ x, sign (quadratic a x)) = sign (arf a) * 2 ^ Fintype.card ι := by
53   classical
54   simp only [quadratic, sign_sum]
55   rw [← Fintype.prod_sum (fun (i : ι) (x : F2 × F2) => sign (plane (a i) x))]
56   simp_rw [plane_gauss]
57   rw [Finset.prod_mul_distrib, ← sign_sum]
58   simp [arf]
59 
60 end PaperXI.Dyadic

Back to source controls