DyadicOrthogonal.lean

1 import PaperXI.DyadicBasis
2 import PaperXI.DyadicTranslation
3 import Mathlib.LinearAlgebra.BilinearMap
4 
5 noncomputable section
6 set_option autoImplicit false
7 namespace PaperXI.DyadicOrthogonal
8 open scoped BigOperators Classical
9 open PaperXI.Dyadic PaperXI.DyadicAffine PaperXI.DyadicCoordinates
10 variable {V W ι κ : Type*} [AddCommGroup V] [Module F2 V]
11   [AddCommGroup W] [Module F2 W] [Fintype ι] [Fintype κ]
12 variable (b : V →ₗ[F2] V →ₗ[F2] F2) (c : W →ₗ[F2] W →ₗ[F2] F2)
13 
14 def form : (V × W) →ₗ[F2] (V × W) →ₗ[F2] F2 :=
15   b.compl₁₂ (LinearMap.fst F2 V W) (LinearMap.fst F2 V W) +
16   c.compl₁₂ (LinearMap.snd F2 V W) (LinearMap.snd F2 V W)
17 
18 @[simp] theorem form_apply (x y : V × W) : form b c x y = b x.1 y.1 + c x.2 y.2 := rfl
19 
20 def refinement (q : Refinement b) (r : Refinement c) : Refinement (form b c) where
21   value x := q.value x.1 + r.value x.2
22   polar x y := by
23     simp only [Prod.fst_add, Prod.snd_add, q.polar, r.polar, form_apply]
24     ring
25 
26 variable {b c}
27 
28 theorem gauss_product [Fintype V] [Fintype W] (q : Refinement b) (r : Refinement c) :
29     (∑ x, sign ((refinement b c q r).value x)) =
30       (∑ x, sign (q.value x)) * ∑ y, sign (r.value y) := by
31   simp only [refinement, sign_add, Fintype.sum_prod_type, Finset.mul_sum,
32     Finset.sum_mul]
33   exact Finset.sum_comm
34 
35 def coordinates (e : V ≃ₗ[F2] (ι → F2 × F2))
36     (f : W ≃ₗ[F2] (κ → F2 × F2)) :
37     (V × W) ≃ₗ[F2] ((ι ⊕ κ) → F2 × F2) :=
38   (e.prodCongr f).trans (LinearEquiv.sumArrowLequivProdArrow ι κ F2 (F2 × F2)).symm
39 
40 theorem coordinates_form (e : V ≃ₗ[F2] (ι → F2 × F2))
41     (f : W ≃ₗ[F2] (κ → F2 × F2))
42     (he : ∀ x y, b x y = symplectic (e x) (e y))
43     (hf : ∀ x y, c x y = symplectic (f x) (f y)) (x y : V × W) :
44     form b c x y = symplectic (coordinates e f x) (coordinates e f y) := by
45   rw [form_apply, he, hf]
46   simp [symplectic_apply, coordinates, Fintype.sum_sum_type]
47 
48 theorem arf_add [Fintype V] [Fintype W]
49     (e : V ≃ₗ[F2] (ι → F2 × F2)) (f : W ≃ₗ[F2] (κ → F2 × F2))
50     (he : ∀ x y, b x y = symplectic (e x) (e y))
51     (hf : ∀ x y, c x y = symplectic (f x) (f y))
52     (q : Refinement b) (r : Refinement c) :
53     PaperXI.DyadicBasis.basisArf (coordinates e f) (refinement b c q r) =
54       PaperXI.DyadicBasis.basisArf e q + PaperXI.DyadicBasis.basisArf f r := by
55   apply sign_injective
56   apply mul_right_cancel₀ (pow_ne_zero (Fintype.card ι + Fintype.card κ)
57     (by norm_num : (2 : ℤ) ≠ 0))
58   have h := PaperXI.DyadicBasis.gauss_sum (coordinates e f) (coordinates_form e f he hf)
59     (refinement b c q r)
60   rw [gauss_product, PaperXI.DyadicBasis.gauss_sum e he,
61     PaperXI.DyadicBasis.gauss_sum f hf] at h
62   rw [Fintype.card_sum] at h
63   rw [sign_add, pow_add]
64   rw [pow_add] at h
65   linear_combination -h
66 
67 theorem normalized_sign_product [Fintype V] [Fintype W]
68     (e : V ≃ₗ[F2] (ι → F2 × F2)) (f : W ≃ₗ[F2] (κ → F2 × F2))
69     (he : ∀ x y, b x y = symplectic (e x) (e y))
70     (hf : ∀ x y, c x y = symplectic (f x) (f y))
71     (q : Refinement b) (r : Refinement c) :
72     sign (PaperXI.DyadicBasis.basisArf (coordinates e f) (refinement b c q r)) =
73       sign (PaperXI.DyadicBasis.basisArf e q) * sign (PaperXI.DyadicBasis.basisArf f r) := by
74   rw [arf_add e f he hf, sign_add]
75 
76 end PaperXI.DyadicOrthogonal

Back to source controls