CyclicFilters.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.RingTheory.PowerSeries.Basic
7 
8 /-!
9 # Cyclic coefficient projectors
10 
11 The analytic root-of-unity average in Paper IV acts on formal coefficients by
12 retaining one congruence class.  This file takes that coefficient action as the
13 formal definition and proves the projector laws without convergence hypotheses.
14 -/
15 
16 namespace Komorebi.PaperIV
17 
18 open scoped PowerSeries
19 
20 noncomputable section
21 
22 variable {R : Type*} [CommSemiring R]
23 
24 /-- The formal cyclic projector retaining degrees congruent to `j` modulo `N`. -/
25 def cyclicProjector (N j : ℕ) (f : R⟦X⟧) : R⟦X⟧ :=
26   PowerSeries.mk fun n => if n % N = j % N then PowerSeries.coeff n f else 0
27 
28 @[simp]
29 theorem coeff_cyclicProjector (N j n : ℕ) (f : R⟦X⟧) :
30     PowerSeries.coeff n (cyclicProjector N j f) =
31       if n % N = j % N then PowerSeries.coeff n f else 0 := by
32   simp [cyclicProjector]
33 
34 theorem cyclicProjector_idempotent (N j : ℕ) (f : R⟦X⟧) :
35     cyclicProjector N j (cyclicProjector N j f) = cyclicProjector N j f := by
36   ext n
37   by_cases h : n % N = j % N <;> simp [h]
38 
39 theorem cyclicProjector_orthogonal {N i j : ℕ} (hij : i % N ≠ j % N) (f : R⟦X⟧) :
40     cyclicProjector N i (cyclicProjector N j f) = 0 := by
41   ext n
42   by_cases hi : n % N = i % N
43   · have hj : n % N ≠ j % N := fun h => hij (hi.symm.trans h)
44     simp only [coeff_cyclicProjector, hi, hij, ↓reduceIte, map_zero]
45   · simp [hi]
46 
47 theorem cyclicProjector_eq_zero_of_residue_ne {N j n : ℕ} (h : n % N ≠ j % N)
48     (f : R⟦X⟧) :
49     PowerSeries.coeff n (cyclicProjector N j f) = 0 := by
50   simp [h]
51 
52 theorem cyclicProjector_eq_of_mod_eq {N i j : ℕ} (hij : i % N = j % N) (f : R⟦X⟧) :
53     cyclicProjector N i f = cyclicProjector N j f := by
54   ext n
55   simp only [coeff_cyclicProjector]
56   rw [hij]
57 
58 theorem cyclicProjector_add (N j : ℕ) (f g : R⟦X⟧) :
59     cyclicProjector N j (f + g) = cyclicProjector N j f + cyclicProjector N j g := by
60   ext n
61   by_cases h : n % N = j % N <;> simp [h]
62 
63 theorem cyclicProjector_sum {I : Type*} (N j : ℕ) (s : Finset I) (f : I → R⟦X⟧) :
64     cyclicProjector N j (∑ i ∈ s, f i) = ∑ i ∈ s, cyclicProjector N j (f i) := by
65   classical
66   induction s using Finset.induction_on with
67   | empty =>
68       ext n
69       simp [cyclicProjector]
70   | @insert a s ha ih =>
71       rw [Finset.sum_insert ha, Finset.sum_insert ha, cyclicProjector_add, ih]
72 
73 /-- The `N` residue projectors resolve the identity. -/
74 theorem sum_cyclicProjector {N : ℕ} (hN : 0 < N) (f : R⟦X⟧) :
75     (∑ j ∈ Finset.range N, cyclicProjector N j f) = f := by
76   ext n
77   rw [map_sum]
78   rw [Finset.sum_eq_single (n % N)]
79   · simp [Nat.mod_eq_of_lt (Nat.mod_lt n hN)]
80   · intro j hj hne
81     have hjN : j < N := Finset.mem_range.mp hj
82     have hmod : j % N = j := Nat.mod_eq_of_lt hjN
83     have hres : n % N ≠ j % N := by simpa [hmod] using hne.symm
84     simp [hres]
85   · exact fun hmem => (hmem (Finset.mem_range.mpr (Nat.mod_lt n hN))).elim
86 
87 /-- Multiplying two pure packets adds their labels modulo `N`. -/
88 theorem cyclicProjector_product_packet (N i j : ℕ) (f g : R⟦X⟧) :
89     cyclicProjector N ((i + j) % N)
90         (cyclicProjector N i f * cyclicProjector N j g) =
91       cyclicProjector N i f * cyclicProjector N j g := by
92   ext n
93   by_cases hn : n % N = (i + j) % N
94   · simp [hn]
95   · simp only [coeff_cyclicProjector, hn, Nat.mod_mod, ↓reduceIte]
96     symm
97     rw [PowerSeries.coeff_mul]
98     apply Finset.sum_eq_zero
99     intro p hp
100     by_cases hi : p.1 % N = i % N
101     · by_cases hj : p.2 % N = j % N
102       · exfalso
103         apply hn
104         have hpadd : p.1 + p.2 = n := Finset.mem_antidiagonal.mp hp
105         calc
106           n % N = (p.1 + p.2) % N := by rw [hpadd]
107           _ = (p.1 % N + p.2 % N) % N := Nat.add_mod _ _ _
108           _ = (i % N + j % N) % N := by rw [hi, hj]
109           _ = (i + j) % N := (Nat.add_mod i j N).symm
110       · simp [hj]
111     · simp [hi]
112 
113 /-- A projector with any other label kills a pure packet product. -/
114 theorem cyclicProjector_product_other {N i j k : ℕ}
115     (hk : k % N ≠ (i + j) % N) (f g : R⟦X⟧) :
116     cyclicProjector N k (cyclicProjector N i f * cyclicProjector N j g) = 0 := by
117   rw [← cyclicProjector_product_packet N i j f g]
118   apply cyclicProjector_orthogonal (R := R)
119   simpa using hk
120 
121 /-- The full cyclic product law, expressed as a finite double packet sum. -/
122 theorem cyclic_product_law {N : ℕ} (hN : 0 < N) (k : ℕ) (f g : R⟦X⟧) :
123     cyclicProjector N k (f * g) =
124       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
125         if (i + j) % N = k % N then
126           cyclicProjector N i f * cyclicProjector N j g
127         else 0 := by
128   calc
129     cyclicProjector N k (f * g) =
130         cyclicProjector N k
131           ((∑ i ∈ Finset.range N, cyclicProjector N i f) *
132             (∑ j ∈ Finset.range N, cyclicProjector N j g)) := by
133       rw [sum_cyclicProjector hN, sum_cyclicProjector hN]
134     _ = ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
135           if (i + j) % N = k % N then
136             cyclicProjector N i f * cyclicProjector N j g
137           else 0 := by
138       rw [Finset.sum_mul]
139       simp_rw [Finset.mul_sum]
140       rw [cyclicProjector_sum]
141       apply Finset.sum_congr rfl
142       intro i hi
143       rw [cyclicProjector_sum]
144       apply Finset.sum_congr rfl
145       intro j hj
146       by_cases hlabel : (i + j) % N = k % N
147       · simp only [hlabel, ↓reduceIte]
148         rw [cyclicProjector_eq_of_mod_eq (i := k) (j := (i + j) % N)
149           (by simpa using hlabel.symm)]
150         exact cyclicProjector_product_packet N i j f g
151       · simp only [hlabel, ↓reduceIte]
152         exact cyclicProjector_product_other (R := R) (fun h => hlabel h.symm) f g
153 
154 end
155 
156 end Komorebi.PaperIV

Back to source controls