BreakQuadratic.lean

1 import PaperXI.DyadicAbstractOrthogonal
2 import Mathlib.LinearAlgebra.Dimension.Constructions
3 
4 /-! Actual finite orthogonal products of dyadic quadratic refinements.
5 The index type may be empty and the factors may have dimension zero. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.BreakQuadratic
9 open scoped BigOperators Classical
10 open PaperXI.Dyadic PaperXI.DyadicAffine
11 
12 variable {ι : Type*} [Fintype ι] {V : ι → Type*}
13   [∀ i, AddCommGroup (V i)] [∀ i, Module F2 (V i)]
14 
15 /-- The actual sum of the component bilinear forms on a dependent product. -/
16 def form (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2) :
17     (∀ i, V i) →ₗ[F2] (∀ i, V i) →ₗ[F2] F2 where
18   toFun x :=
19     { toFun := fun y => ∑ i, b i (x i) (y i)
20       map_add' := by intro y z; simp [Finset.sum_add_distrib]
21       map_smul' := by intro a y; simp [Finset.mul_sum] }
22   map_add' := by intro x y; ext z; simp [Finset.sum_add_distrib]
23   map_smul' := by intro a x; ext y; simp [Finset.mul_sum]
24 
25 @[simp] theorem form_apply (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
26     (x y : ∀ i, V i) : form b x y = ∑ i, b i (x i) (y i) := rfl
27 
28 theorem form_alternating (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
29     (ha : ∀ i x, b i x x = 0) (x : ∀ i, V i) : form b x x = 0 := by
30   simp [ha]
31 
32 theorem form_single_right (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
33     (x : ∀ i, V i) (j : ι) (y : V j) :
34     form b x (Pi.single j y) = b j (x j) y := by
35   classical
36   rw [form_apply, Finset.sum_eq_single j]
37   · simp
38   · intro i _ hij
39     simp [Pi.single_eq_of_ne hij]
40   · simp
41 
42 theorem form_nondegenerate (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
43     (hn : ∀ i x, (∀ y, b i x y = 0) → x = 0)
44     (x : ∀ i, V i) (hx : ∀ y, form b x y = 0) : x = 0 := by
45   funext i
46   apply hn i (x i)
47   intro y
48   simpa only [form_single_right] using hx (Pi.single i y)
49 
50 /-- The quadratic refinement is the actual sum of the supplied refinements. -/
51 def refinement (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
52     (q : ∀ i, Refinement (b i)) : Refinement (form b) where
53   value x := ∑ i, (q i).value (x i)
54   polar x y := by
55     simp only [Pi.add_apply, Refinement.polar, form_apply, Finset.sum_add_distrib]
56 
57 @[simp] theorem refinement_apply (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
58     (q : ∀ i, Refinement (b i)) (x : ∀ i, V i) :
59     (refinement b q).value x = ∑ i, (q i).value (x i) := rfl
60 
61 /-- The explicit polar identity identifies the total refinement, not merely
62 its alternating form. -/
63 theorem refinement_polar (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
64     (q : ∀ i, Refinement (b i)) (x y : ∀ i, V i) :
65     (refinement b q).value (x + y) =
66       (refinement b q).value x + (refinement b q).value y + form b x y :=
67   (refinement b q).polar x y
68 
69 /-- The literal Gauss sum of a finite product is the product of the literal
70 component Gauss sums. No nondegeneracy or dimension hypothesis is needed. -/
71 theorem gauss_sum_product [∀ i, Fintype (V i)]
72     (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2) (q : ∀ i, Refinement (b i)) :
73     (∑ x : (∀ i, V i), sign ((refinement b q).value x)) =
74       ∏ i, ∑ x : V i, sign ((q i).value x) := by
75   simp only [refinement_apply, sign_sum]
76   exact (Fintype.prod_sum (fun i x => sign ((q i).value x))).symm
77 
78 variable [∀ i, FiniteDimensional F2 (V i)]
79 
80 omit [Fintype ι] in
81 /-- Each nondegenerate alternating factor has the actual even dimension. -/
82 theorem finrank_eq_twice_half (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
83     (ha : ∀ i x, b i x x = 0)
84     (hn : ∀ i x, (∀ y, b i x y = 0) → x = 0) (i : ι) :
85     Module.finrank F2 (V i) = 2 * (Module.finrank F2 (V i) / 2) := by
86   obtain ⟨r, hr⟩ := SymplecticCoordinates.even_finrank (b i) (ha i) (hn i)
87   omega
88 
89 /-- The positive square-root normalization uses the sum of actual
90 half-dimensions, including the empty sum. -/
91 theorem half_finrank_product (b : ∀ i, V i →ₗ[F2] V i →ₗ[F2] F2)
92     (ha : ∀ i x, b i x x = 0)
93     (hn : ∀ i x, (∀ y, b i x y = 0) → x = 0) :
94     Module.finrank F2 (∀ i, V i) / 2 =
95       ∑ i, Module.finrank F2 (V i) / 2 := by
96   rw [Module.finrank_pi_fintype]
97   have h : (∑ i, Module.finrank F2 (V i)) =
98       2 * ∑ i, Module.finrank F2 (V i) / 2 := by
99     rw [Finset.mul_sum]
100     exact Finset.sum_congr rfl (fun i _ => finrank_eq_twice_half b ha hn i)
101   rw [h]
102   omega
103 
104 end PaperXI.BreakQuadratic

Back to source controls