CyclicSeries.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.RingTheory.PowerSeries.Basic
7 import Mathlib.Algebra.BigOperators.Ring.Finset
8 import Mathlib.Algebra.BigOperators.Fin
9 import Mathlib.Tactic
10 
11 /-!
12 # Cyclic coefficient projectors
13 
14 The analytic root-of-unity average in Paper IV acts on formal coefficients by
15 retaining one congruence class. This foundation is adapted from Paper IV v1.0.0
16 CyclicFilters.lean; the inherited proof is explicitly identified in the census.  This file takes that coefficient action as the
17 formal definition and proves the projector laws without convergence hypotheses.
18 -/
19 
20 namespace KomorebiPaperV.CyclicSeries
21 
22 open scoped PowerSeries
23 
24 noncomputable section
25 
26 variable {R : Type*} [CommSemiring R]
27 
28 /-- The formal cyclic projector retaining degrees congruent to `j` modulo `N`. -/
29 def cyclicProjector (N j : ℕ) (f : R⟦X⟧) : R⟦X⟧ :=
30   PowerSeries.mk fun n => if n % N = j % N then PowerSeries.coeff n f else 0
31 
32 @[simp]
33 theorem coeff_cyclicProjector (N j n : ℕ) (f : R⟦X⟧) :
34     PowerSeries.coeff n (cyclicProjector N j f) =
35       if n % N = j % N then PowerSeries.coeff n f else 0 := by
36   simp [cyclicProjector]
37 
38 theorem cyclicProjector_idempotent (N j : ℕ) (f : R⟦X⟧) :
39     cyclicProjector N j (cyclicProjector N j f) = cyclicProjector N j f := by
40   ext n
41   by_cases h : n % N = j % N <;> simp [h]
42 
43 theorem cyclicProjector_orthogonal {N i j : ℕ} (hij : i % N ≠ j % N) (f : R⟦X⟧) :
44     cyclicProjector N i (cyclicProjector N j f) = 0 := by
45   ext n
46   by_cases hi : n % N = i % N
47   · have hj : n % N ≠ j % N := fun h => hij (hi.symm.trans h)
48     simp only [coeff_cyclicProjector, hi, hij, ↓reduceIte, map_zero]
49   · simp [hi]
50 
51 theorem cyclicProjector_eq_zero_of_residue_ne {N j n : ℕ} (h : n % N ≠ j % N)
52     (f : R⟦X⟧) :
53     PowerSeries.coeff n (cyclicProjector N j f) = 0 := by
54   simp [h]
55 
56 theorem cyclicProjector_eq_of_mod_eq {N i j : ℕ} (hij : i % N = j % N) (f : R⟦X⟧) :
57     cyclicProjector N i f = cyclicProjector N j f := by
58   ext n
59   simp only [coeff_cyclicProjector]
60   rw [hij]
61 
62 theorem cyclicProjector_add (N j : ℕ) (f g : R⟦X⟧) :
63     cyclicProjector N j (f + g) = cyclicProjector N j f + cyclicProjector N j g := by
64   ext n
65   by_cases h : n % N = j % N <;> simp [h]
66 
67 theorem cyclicProjector_sum {I : Type*} (N j : ℕ) (s : Finset I) (f : I → R⟦X⟧) :
68     cyclicProjector N j (∑ i ∈ s, f i) = ∑ i ∈ s, cyclicProjector N j (f i) := by
69   classical
70   induction s using Finset.induction_on with
71   | empty =>
72       ext n
73       simp [cyclicProjector]
74   | @insert a s ha ih =>
75       rw [Finset.sum_insert ha, Finset.sum_insert ha, cyclicProjector_add, ih]
76 
77 /-- The `N` residue projectors resolve the identity. -/
78 theorem sum_cyclicProjector {N : ℕ} (hN : 0 < N) (f : R⟦X⟧) :
79     (∑ j ∈ Finset.range N, cyclicProjector N j f) = f := by
80   ext n
81   rw [map_sum]
82   rw [Finset.sum_eq_single (n % N)]
83   · simp [Nat.mod_eq_of_lt (Nat.mod_lt n hN)]
84   · intro j hj hne
85     have hjN : j < N := Finset.mem_range.mp hj
86     have hmod : j % N = j := Nat.mod_eq_of_lt hjN
87     have hres : n % N ≠ j % N := by simpa [hmod] using hne.symm
88     simp [hres]
89   · exact fun hmem => (hmem (Finset.mem_range.mpr (Nat.mod_lt n hN))).elim
90 
91 /-- Multiplying two pure packets adds their labels modulo `N`. -/
92 theorem cyclicProjector_product_packet (N i j : ℕ) (f g : R⟦X⟧) :
93     cyclicProjector N ((i + j) % N)
94         (cyclicProjector N i f * cyclicProjector N j g) =
95       cyclicProjector N i f * cyclicProjector N j g := by
96   ext n
97   by_cases hn : n % N = (i + j) % N
98   · simp [hn]
99   · simp only [coeff_cyclicProjector, hn, Nat.mod_mod, ↓reduceIte]
100     symm
101     rw [PowerSeries.coeff_mul]
102     apply Finset.sum_eq_zero
103     intro p hp
104     by_cases hi : p.1 % N = i % N
105     · by_cases hj : p.2 % N = j % N
106       · exfalso
107         apply hn
108         have hpadd : p.1 + p.2 = n := Finset.mem_antidiagonal.mp hp
109         calc
110           n % N = (p.1 + p.2) % N := by rw [hpadd]
111           _ = (p.1 % N + p.2 % N) % N := Nat.add_mod _ _ _
112           _ = (i % N + j % N) % N := by rw [hi, hj]
113           _ = (i + j) % N := (Nat.add_mod i j N).symm
114       · simp [hj]
115     · simp [hi]
116 
117 /-- A projector with any other label kills a pure packet product. -/
118 theorem cyclicProjector_product_other {N i j k : ℕ}
119     (hk : k % N ≠ (i + j) % N) (f g : R⟦X⟧) :
120     cyclicProjector N k (cyclicProjector N i f * cyclicProjector N j g) = 0 := by
121   rw [← cyclicProjector_product_packet N i j f g]
122   apply cyclicProjector_orthogonal (R := R)
123   simpa using hk
124 
125 /-- The full cyclic product law, expressed as a finite double packet sum. -/
126 theorem cyclic_product_law {N : ℕ} (hN : 0 < N) (k : ℕ) (f g : R⟦X⟧) :
127     cyclicProjector N k (f * g) =
128       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
129         if (i + j) % N = k % N then
130           cyclicProjector N i f * cyclicProjector N j g
131         else 0 := by
132   calc
133     cyclicProjector N k (f * g) =
134         cyclicProjector N k
135           ((∑ i ∈ Finset.range N, cyclicProjector N i f) *
136             (∑ j ∈ Finset.range N, cyclicProjector N j g)) := by
137       rw [sum_cyclicProjector hN, sum_cyclicProjector hN]
138     _ = ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
139           if (i + j) % N = k % N then
140             cyclicProjector N i f * cyclicProjector N j g
141           else 0 := by
142       rw [Finset.sum_mul]
143       simp_rw [Finset.mul_sum]
144       rw [cyclicProjector_sum]
145       apply Finset.sum_congr rfl
146       intro i hi
147       rw [cyclicProjector_sum]
148       apply Finset.sum_congr rfl
149       intro j hj
150       by_cases hlabel : (i + j) % N = k % N
151       · simp only [hlabel, ↓reduceIte]
152         rw [cyclicProjector_eq_of_mod_eq (i := k) (j := (i + j) % N)
153           (by simpa using hlabel.symm)]
154         exact cyclicProjector_product_packet N i j f g
155       · simp only [hlabel, ↓reduceIte]
156         exact cyclicProjector_product_other (R := R) (fun h => hlabel h.symm) f g
157 
158 /-- A product of pure residue packets stays in the sum residue, including the empty product. -/
159 theorem pure_finite_product {I : Type*} (N : ℕ) (s : Finset I) (i : I → ℕ)
160     (f : I → R⟦X⟧) (hf : ∀ a ∈ s, cyclicProjector N (i a) (f a) = f a) :
161     cyclicProjector N (∑ a ∈ s, i a) (∏ a ∈ s, f a) = ∏ a ∈ s, f a := by
162   classical
163   induction s using Finset.induction_on with
164   | empty =>
165     simp only [Finset.sum_empty, Finset.prod_empty]
166     ext n
167     by_cases hn : n = 0 <;> simp [PowerSeries.coeff_one, hn]
168   | @insert a s ha ih =>
169     have hfa := hf a (Finset.mem_insert_self a s)
170     have hfs := ih (fun b hb => hf b (Finset.mem_insert_of_mem hb))
171     rw [Finset.sum_insert ha, Finset.prod_insert ha]
172     have h := cyclicProjector_product_packet N (i a) (∑ b ∈ s, i b) (f a) (∏ b ∈ s, f b)
173     rw [hfa, hfs] at h
174     simpa only [cyclicProjector, Nat.mod_mod] using h
175 
176 /-- Projecting a pure finite product either retains it or kills it. -/
177 theorem project_finite_product {I : Type*} (N k : ℕ) (s : Finset I) (i : I → ℕ)
178     (f : I → R⟦X⟧) (hf : ∀ a ∈ s, cyclicProjector N (i a) (f a) = f a) :
179     cyclicProjector N k (∏ a ∈ s, f a) =
180       if (∑ a ∈ s, i a) % N = k % N then ∏ a ∈ s, f a else 0 := by
181   classical
182   have hp := pure_finite_product N s i f hf
183   by_cases h : (∑ a ∈ s, i a) % N = k % N
184   · rw [ite_eq_left h, ← cyclicProjector_eq_of_mod_eq h]
185     exact hp
186   · rw [ite_eq_right h, ← hp]
187     exact cyclicProjector_orthogonal (Ne.symm h) _
188 
189 theorem sum_fin_projector {N : ℕ} (hN : 0 < N) (f : R⟦X⟧) :
190     (∑ i : Fin N, cyclicProjector N i.val f) = f := by
191   exact (Fin.sum_univ_eq_sum_range (fun j => cyclicProjector N j f) N).trans
192     (sum_cyclicProjector hN f)
193 
194 /-- The literal q-tuple power formula, including q = 0. -/
195 theorem cyclic_power_law {N : ℕ} (hN : 0 < N) (k q : ℕ) (f : R⟦X⟧) :
196     cyclicProjector N k (f ^ q) =
197       ∑ i : Fin q → Fin N, if (∑ a, (i a).val) % N = k % N then
198         ∏ a, cyclicProjector N (i a).val f else 0 := by
199   classical
200   have hex : f ^ q = ∑ i : Fin q → Fin N, ∏ a, cyclicProjector N (i a).val f := by
201     have h := Fintype.sum_pow (fun i : Fin N => cyclicProjector N i.val f) q
202     rw [sum_fin_projector hN] at h
203     exact h
204   rw [hex, cyclicProjector_sum]
205   apply Finset.sum_congr rfl
206   intro i _
207   exact project_finite_product N k Finset.univ (fun a => (i a).val)
208     (fun a => cyclicProjector N (i a).val f)
209     (fun a _ => cyclicProjector_idempotent N (i a).val f)
210 
211 end
212 
213 end KomorebiPaperV.CyclicSeries

Back to source controls