TranslationAverage.lean

1 import PaperXI.FiniteAverage
2 import Mathlib.LinearAlgebra.Dimension.Finrank
3 import Mathlib.LinearAlgebra.Pi
4 
5 /-! The translation representation and its rank-one constant-function projector. -/
6 set_option autoImplicit false
7 set_option maxHeartbeats 600000
8 noncomputable section
9 open scoped BigOperators
10 namespace PaperXI.TranslationAverage
11 variable {X : Type*} [AddCommGroup X] [Fintype X]
12 
13 def translation : Representation ℂ (Multiplicative X) (X → ℂ) where
14   toFun x :=
15     { toFun := fun f u => f (u + x.toAdd)
16       map_add' := by intros; rfl
17       map_smul' := by intros; rfl }
18   map_one' := by ext f u; simp
19   map_mul' x y := by ext f u; simp [add_assoc]
20 
21 omit [Fintype X] in
22 @[simp] theorem translation_apply (x : Multiplicative X) (f : X → ℂ) (u : X) :
23     translation x f u = f (u + x.toAdd) := rfl
24 
25 def mean (f : X → ℂ) : ℂ := (Fintype.card X : ℂ)⁻¹ * ∑ u : X, f u
26 
27 def constantSubmodule : Submodule ℂ (X → ℂ) :=
28   LinearMap.range (LinearMap.const (R := ℂ) (ι := X) (M₂ := ℂ))
29 
30 omit [AddCommGroup X] [Fintype X] in
31 theorem mem_constantSubmodule (f : X → ℂ) :
32     f ∈ constantSubmodule ↔ ∃ c : ℂ, ∀ u, f u = c := by
33   constructor
34   · rintro ⟨c, hc⟩
35     exact ⟨c, fun u => (congrFun hc u).symm⟩
36   · rintro ⟨c, hc⟩
37     exact ⟨c, funext fun u => (hc u).symm⟩
38 
39 theorem average_apply (f : X → ℂ) (u : X) :
40     FiniteAverage.average (translation (X := X)) f u = mean f := by
41   simp only [FiniteAverage.average_apply, Pi.smul_apply, Finset.sum_apply,
42     translation_apply, smul_eq_mul, mean]
43   rw [Fintype.card_multiplicative]
44   congr 1
45   rw [Function.Bijective.sum_comp Multiplicative.toAdd.bijective (fun x : X => f (u + x))]
46   exact Function.Bijective.sum_comp (AddGroup.addLeft_bijective u) f
47 
48 theorem range_eq :
49     LinearMap.range (FiniteAverage.average (translation (X := X))) = constantSubmodule := by
50   ext f
51   constructor
52   · rintro ⟨g, rfl⟩
53     exact (mem_constantSubmodule _).2 ⟨mean g, average_apply g⟩
54   · intro hf
55     rcases (mem_constantSubmodule f).1 hf with ⟨c, hc⟩
56     refine ⟨f, FiniteAverage.fixes _ ?_⟩
57     intro g
58     ext u
59     simp only [translation_apply, hc]
60 
61 theorem finrank_range :
62     Module.finrank ℂ (LinearMap.range (FiniteAverage.average (translation (X := X)))) = 1 := by
63   rw [range_eq]
64   have hinj : Function.Injective (LinearMap.const (R := ℂ) (ι := X) (M₂ := ℂ)) := by
65     intro a b h
66     exact congrFun h 0
67   change Module.finrank ℂ (LinearMap.range (LinearMap.const (R := ℂ) (ι := X) (M₂ := ℂ))) = 1
68   rw [LinearMap.finrank_range_of_inj hinj, Module.finrank_self]
69 
70 /-- The standard finite-sum Hermitian pairing on the function model. -/
71 def pairing (f g : X → ℂ) : ℂ := ∑ u : X, star (f u) * g u
72 
73 theorem pairing_translation (x : Multiplicative X) (f g : X → ℂ) :
74     pairing (translation x f) (translation x g) = pairing f g := by
75   simp only [pairing, translation_apply]
76   exact Function.Bijective.sum_comp (AddGroup.addRight_bijective x.toAdd)
77     (fun u => star (f u) * g u)
78 
79 theorem pairing_self_adjoint (f g : X → ℂ) :
80     pairing (FiniteAverage.average (translation (X := X)) f) g =
81       pairing f (FiniteAverage.average (translation (X := X)) g) := by
82   simp only [pairing, average_apply, mean, star_mul, star_inv₀, star_natCast,
83     star_sum, Finset.mul_sum, Finset.sum_mul]
84   rw [Finset.sum_comm]
85   apply Finset.sum_congr rfl
86   intro u hu
87   apply Finset.sum_congr rfl
88   intro v hv
89   ring
90 
91 theorem residual_orthogonal (f : X → ℂ) {g : X → ℂ}
92     (hg : g ∈ constantSubmodule) :
93     pairing (f - FiniteAverage.average (translation (X := X)) f) g = 0 := by
94   have hfix : FiniteAverage.average (translation (X := X)) g = g := by
95     have hr : g ∈ LinearMap.range (FiniteAverage.average (translation (X := X))) := by rwa [range_eq]
96     apply FiniteAverage.fixes
97     rwa [FiniteAverage.range_eq] at hr
98   have hsub (a b c : X → ℂ) : pairing (a-b) c = pairing a c - pairing b c := by
99     simp [pairing, star_sub, sub_mul, Finset.sum_sub_distrib]
100   rw [hsub, pairing_self_adjoint, hfix, sub_self]
101 
102 end PaperXI.TranslationAverage

Back to source controls