FiniteFieldAverage.lean

1 import Mathlib.Algebra.Ring.GeomSum
2 import Mathlib.LinearAlgebra.Projection
3 import Mathlib.Tactic.Abel
4 
5 /-! Actual finite-order averages and their fixed/moving decomposition over a field.
6 The construction uses the invertibility of the order scalar, with no initial
7 complementary decomposition or finite-dimensionality assumption. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.FiniteFieldAverage
11 
12 open scoped BigOperators
13 variable {F V : Type*} [Field F] [AddCommGroup V] [Module F V]
14 
15 /-- The actual difference from the identity. -/
16 def difference (g : V ≃ₗ[F] V) : Module.End F V := g.toLinearMap - LinearMap.id
17 
18 /-- The literal finite-order averaging map. -/
19 def average (g : V ≃ₗ[F] V) (m : ℕ) : Module.End F V :=
20   (m : F)⁻¹ • ∑ j ∈ Finset.range m, g.toLinearMap ^ j
21 
22 /-- The literal weighted companion to the finite-order average. -/
23 def companion (g : V ≃ₗ[F] V) (m : ℕ) : Module.End F V :=
24   (m : F)⁻¹ • ∑ j ∈ Finset.range m, (j : F) • g.toLinearMap ^ j
25 
26 @[simp] theorem difference_apply (g : V ≃ₗ[F] V) (v : V) : difference g v = g v - v := rfl
27 
28 @[simp] theorem average_apply (g : V ≃ₗ[F] V) (m : ℕ) (v : V) :
29     average g m v = (m : F)⁻¹ • ∑ j ∈ Finset.range m, (g.toLinearMap ^ j) v := by
30   simp [average, LinearMap.sum_apply]
31 
32 @[simp] theorem companion_apply (g : V ≃ₗ[F] V) (m : ℕ) (v : V) :
33     companion g m v = (m : F)⁻¹ • ∑ j ∈ Finset.range m, (j : F) • (g.toLinearMap ^ j) v := by
34   simp [companion, LinearMap.sum_apply]
35 
36 /-- The weighted geometric identity before imposing finite order. -/
37 theorem weighted_identity (f : Module.End F V) (m : ℕ) :
38     (f - 1) * (∑ j ∈ Finset.range m, (j : F) • f ^ j) =
39       (m : F) • f ^ m - (∑ j ∈ Finset.range m, f ^ j) - (f ^ m - 1) := by
40   induction m with
41   | zero => simp
42   | succ m ih =>
43     rw [Finset.sum_range_succ, mul_add, ih, mul_smul_comm, sub_mul,
44       one_mul, ← pow_succ']
45     simp only [Finset.sum_range_succ, Nat.cast_add, Nat.cast_one,
46       add_smul, one_smul, smul_sub]
47     abel
48 
49 /-- A finite-order equality of automorphisms is the corresponding equality of endomorphisms. -/
50 theorem power_eq_one (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1) :
51     g.toLinearMap ^ m = 1 := by
52   ext v
53   have h := congrArg (fun e : V ≃ₗ[F] V => e v) hpow
54   simpa only [LinearEquiv.pow_apply, LinearEquiv.coe_one, Function.id_def, Module.End.pow_apply,
55     Module.End.one_apply, LinearEquiv.coe_coe] using h
56 
57 /-- The average annihilates the moving difference. -/
58 theorem average_mul_difference (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1) :
59     average g m * difference g = 0 := by
60   change ((m : F)⁻¹ • ∑ j ∈ Finset.range m, g.toLinearMap ^ j) * (g.toLinearMap - 1) = 0
61   rw [smul_mul_assoc, geom_sum_mul, power_eq_one g m hpow]
62   simp
63 
64 /-- The image of the average consists of fixed vectors. -/
65 theorem difference_mul_average (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1) :
66     difference g * average g m = 0 := by
67   change (g.toLinearMap - 1) * ((m : F)⁻¹ • ∑ j ∈ Finset.range m, g.toLinearMap ^ j) = 0
68   rw [mul_smul_comm, mul_geom_sum, power_eq_one g m hpow]
69   simp
70 
71 /-- The companion constructs the moving part of each actual vector. -/
72 theorem moving_identity (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
73     (hm : (m : F) ≠ 0) : difference g * companion g m = 1 - average g m := by
74   change (g.toLinearMap - 1) * ((m : F)⁻¹ • ∑ j ∈ Finset.range m, (j : F) • g.toLinearMap ^ j) = _
75   rw [mul_smul_comm, weighted_identity, power_eq_one g m hpow]
76   simp [average, smul_sub, smul_smul, hm]
77 
78 /-- Fixed vectors are fixed by every nonnegative power of the actual action. -/
79 theorem power_fixes (g : V ≃ₗ[F] V) {v : V} (hv : g v = v) (j : ℕ) :
80     (g.toLinearMap ^ j) v = v := by
81   induction j with
82   | zero => rfl
83   | succ j ih => rw [pow_succ']; change g ((g.toLinearMap ^ j) v) = v; rw [ih, hv]
84 
85 /-- The average is the identity on the actual fixed space. -/
86 theorem average_fixes (g : V ≃ₗ[F] V) (m : ℕ) (hm : (m : F) ≠ 0)
87     {v : V} (hv : v ∈ LinearMap.ker (difference g)) : average g m v = v := by
88   have hgv : g v = v := sub_eq_zero.mp hv
89   rw [average_apply]
90   simp only [power_fixes g hgv, Finset.sum_const, Finset.card_range]
91   rw [← Nat.cast_smul_eq_nsmul F, smul_smul, inv_mul_cancel₀ hm, one_smul]
92 
93 /-- The range of the actual average is precisely the fixed space. -/
94 theorem range_average (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
95     (hm : (m : F) ≠ 0) : LinearMap.range (average g m) = LinearMap.ker (difference g) := by
96   ext v
97   constructor
98   · rintro ⟨x, rfl⟩
99     exact LinearMap.congr_fun (difference_mul_average g m hpow) x
100   · intro hv
101     exact ⟨v, average_fixes g m hm hv⟩
102 
103 /-- The kernel of the actual average is precisely the moving space. -/
104 theorem ker_average (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
105     (hm : (m : F) ≠ 0) : LinearMap.ker (average g m) = LinearMap.range (difference g) := by
106   ext v
107   constructor
108   · intro hv
109     refine ⟨companion g m v, ?_⟩
110     have h := LinearMap.congr_fun (moving_identity g m hpow hm) v
111     change difference g (companion g m v) = v - average g m v at h
112     simpa only [show average g m v = 0 from hv, sub_zero] using h
113   · rintro ⟨x, rfl⟩
114     exact LinearMap.congr_fun (average_mul_difference g m hpow) x
115 
116 /-- The actual finite-order average is idempotent. -/
117 theorem idempotent (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
118     (hm : (m : F) ≠ 0) : average g m * average g m = average g m := by
119   ext v
120   apply average_fixes g m hm
121   exact LinearMap.congr_fun (difference_mul_average g m hpow) v
122 
123 /-- The fixed and moving subspaces are complementary, without a finite-dimensionality premise. -/
124 theorem isCompl (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
125     (hm : (m : F) ≠ 0) :
126     IsCompl (LinearMap.ker (difference g)) (LinearMap.range (difference g)) := by
127   have hP : IsIdempotentElem (average g m) := idempotent g m hpow hm
128   simpa only [range_average g m hpow hm, ker_average g m hpow hm] using LinearMap.IsIdempotentElem.isCompl hP
129 
130 /-- The genuine fixed/moving decomposition maps the pair to its sum in the original space. -/
131 def decomposition (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
132     (hm : (m : F) ≠ 0) :
133     (LinearMap.ker (difference g) × LinearMap.range (difference g)) ≃ₗ[F] V :=
134   Submodule.prodEquivOfIsCompl _ _ (isCompl g m hpow hm)
135 
136 @[simp] theorem decomposition_apply (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
137     (hm : (m : F) ≠ 0)
138     (x : LinearMap.ker (difference g) × LinearMap.range (difference g)) :
139     decomposition g m hpow hm x = x.1.val + x.2.val := rfl
140 
141 /-- The fixed coordinate of the inverse decomposition is the literal finite average. -/
142 theorem decomposition_symm_fst (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
143     (hm : (m : F) ≠ 0) (v : V) :
144     ((decomposition g m hpow hm).symm v).1.val = average g m v := by
145   let x := (decomposition g m hpow hm).symm v
146   have hsum : x.1.val + x.2.val = v := (decomposition g m hpow hm).apply_symm_apply v
147   have hfixed := average_fixes g m hm x.1.property
148   have hmoving : average g m x.2.val = 0 := by
149     exact (SetLike.ext_iff.mp (ker_average g m hpow hm) x.2.val).mpr x.2.property
150   have h := congrArg (average g m) hsum
151   simpa only [map_add, hfixed, hmoving, add_zero] using h
152 
153 /-- The moving coordinate is the actual remainder after averaging. -/
154 theorem decomposition_symm_snd (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1)
155     (hm : (m : F) ≠ 0) (v : V) :
156     ((decomposition g m hpow hm).symm v).2.val = v - average g m v := by
157   have hsum := (decomposition g m hpow hm).apply_symm_apply v
158   rw [decomposition_apply, decomposition_symm_fst] at hsum
159   exact eq_sub_of_add_eq' hsum
160 
161 /-- Composing the average with the finite-order action does not change it. -/
162 theorem average_mul_action (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1) :
163     average g m * g.toLinearMap = average g m := by
164   have h := average_mul_difference g m hpow
165   change average g m * (g.toLinearMap - 1) = 0 at h
166   rw [mul_sub, mul_one] at h
167   exact sub_eq_zero.mp h
168 
169 /-- The finite-order action fixes the average pointwise. -/
170 theorem action_mul_average (g : V ≃ₗ[F] V) (m : ℕ) (hpow : g ^ m = 1) :
171     g.toLinearMap * average g m = average g m := by
172   have h := difference_mul_average g m hpow
173   change (g.toLinearMap - 1) * average g m = 0 at h
174   rw [sub_mul, one_mul] at h
175   exact sub_eq_zero.mp h
176 
177 /-- Any two admissible order exponents give the same actual fixed-space projector. -/
178 theorem average_independent (g : V ≃ₗ[F] V) (m n : ℕ)
179     (hgm : g ^ m = 1) (hgn : g ^ n = 1) (hm : (m : F) ≠ 0) (hn : (n : F) ≠ 0) :
180     average g m = average g n := by
181   apply LinearMap.IsIdempotentElem.ext (idempotent g m hgm hm) (idempotent g n hgn hn)
182   constructor
183   · rw [range_average g m hgm hm, range_average g n hgn hn]
184   · rw [ker_average g m hgm hm, ker_average g n hgn hn]
185 
186 end PaperXI.FiniteFieldAverage

Back to source controls