PointwiseFilters.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.EntireBridge
6 import KomorebiPaperIV.ZeroMomentLogarithm
7 
8 namespace Komorebi.PaperIV
9 open scoped Topology PowerSeries
10 open Set
11 noncomputable section
12 
13 /-- The manuscript's finite root average, acting on actual functions. -/
14 def pointwiseRootAverage (N j : ℕ) (omega : ℂ) (f : ℂ → ℂ) (z : ℂ) : ℂ :=
15   (N : ℂ)⁻¹ * ∑ l ∈ Finset.range N, ((omega ^ j)⁻¹) ^ l * f (omega ^ l * z)
16 
17 theorem root_weight_sum {N : ℕ} (hN : 0 < N) {omega : ℂ}
18     (ho : IsPrimitiveRoot omega N) (j n : ℕ) :
19     ∑ l ∈ Finset.range N, ((omega ^ j)⁻¹) ^ l * (omega ^ l) ^ n =
20       if n % N = j % N then (N : ℂ) else 0 := by
21   let b := (omega ^ j)⁻¹ * omega ^ n
22   have ho0 := ho.ne_zero hN.ne'
23   have ht (l : ℕ) : ((omega ^ j)⁻¹) ^ l * (omega ^ l) ^ n = b ^ l := by
24     simp only [b, ← pow_mul, mul_pow]
25     rw [Nat.mul_comm l n]
26   simp_rw [ht]
27   have hb : b = 1 ↔ n % N = j % N := by
28     rw [show b = (omega ^ j)⁻¹ * omega ^ n from rfl,
29       inv_mul_eq_one₀ (pow_ne_zero j ho0), eq_comm]
30     simpa only [ho.eq_orderOf, Nat.ModEq] using
31       (ho.isOfFinOrder hN.ne').pow_eq_pow_iff_modEq (n := n) (m := j)
32   have hp : b ^ N = 1 := by
33     simp only [b, mul_pow, inv_pow, ← pow_mul]
34     rw [mul_comm j N, mul_comm n N, pow_mul, pow_mul, ho.pow_eq_one]
35     simp
36   split_ifs with h
37   · simp [hb.mpr h]
38   · have hn : b ≠ 1 := fun he => h (hb.mp he)
39     have he : (b - 1) * ∑ l ∈ Finset.range N, b ^ l = 0 := by
40       rw [mul_geom_sum, hp, sub_self]
41     exact (mul_eq_zero.mp he).resolve_left (sub_ne_zero.mpr hn)
42 
43 theorem mapsTo_root_pow {omega : ℂ} {s : Set ℂ}
44     (hs : MapsTo (fun z => omega * z) s s) (l : ℕ) :
45     MapsTo (fun z => omega ^ l * z) s s := by
46   induction l with
47   | zero => intro z hz; simpa using hz
48   | succ l ih =>
49     intro z hz
50     simpa [pow_succ', mul_assoc] using hs (ih hz)
51 
52 theorem pointwiseRootAverage_covariant {N : ℕ} (hN : 0 < N) {omega : ℂ}
53     (ho : IsPrimitiveRoot omega N) (j : ℕ) (f : ℂ → ℂ) (z : ℂ) :
54     pointwiseRootAverage N j omega f (omega * z) =
55       omega ^ j * pointwiseRootAverage N j omega f z := by
56   let a := (omega ^ j)⁻¹
57   let g := fun l : ℕ => a ^ l * f (omega ^ l * z)
58   have haN : a ^ N = 1 := by
59     simp only [a, inv_pow, ← pow_mul]
60     rw [Nat.mul_comm j N, pow_mul, ho.pow_eq_one]
61     simp
62   have hg : g N = g 0 := by simp [g, haN, ho.pow_eq_one]
63   have hshift : (∑ l ∈ Finset.range N, g (l + 1)) = ∑ l ∈ Finset.range N, g l := by
64     have h := Finset.sum_range_succ' g N
65     rw [Finset.sum_range_succ, hg] at h
66     exact (add_right_cancel h).symm
67   have ht (l : ℕ) : a ^ l * f (omega ^ l * (omega * z)) = omega ^ j * g (l + 1) := by
68     rw [show omega ^ l * (omega * z) = omega ^ (l + 1) * z by rw [pow_succ]; ring]
69     dsimp [g]
70     rw [pow_succ]
71     have hc : omega ^ j * a = 1 := mul_inv_cancel₀ (pow_ne_zero j (ho.ne_zero hN.ne'))
72     calc
73       _ = (omega ^ j * a) * (a ^ l * f (omega ^ (l + 1) * z)) := by rw [hc]; ring
74       _ = _ := by ring
75   unfold pointwiseRootAverage
76   change (N : ℂ)⁻¹ * (∑ l ∈ Finset.range N, a ^ l * f (omega ^ l * (omega * z))) = _
77   simp_rw [ht]
78   rw [← Finset.mul_sum, hshift]
79   dsimp [g, a]
80   ring
81 
82 theorem pointwiseRootAverage_of_covariant {N : ℕ} (hN : 0 < N) {omega : ℂ}
83     (ho : IsPrimitiveRoot omega N) {s : Set ℂ}
84     (hs : MapsTo (fun z => omega * z) s s) (j k : ℕ) (f : ℂ → ℂ)
85     (hf : ∀ z ∈ s, f (omega * z) = omega ^ k * f z) {z : ℂ} (hz : z ∈ s) :
86     pointwiseRootAverage N j omega f z =
87       if k % N = j % N then f z else 0 := by
88   have hp (l : ℕ) : f (omega ^ l * z) = (omega ^ l) ^ k * f z := by
89     induction l with
90     | zero => simp
91     | succ l ih =>
92       rw [pow_succ', mul_assoc, hf _ (mapsTo_root_pow hs l hz), ih, mul_pow]
93       ring
94   unfold pointwiseRootAverage
95   simp_rw [hp, ← mul_assoc]
96   rw [← Finset.sum_mul, root_weight_sum hN ho]
97   split_ifs <;> simp [Nat.cast_ne_zero.mpr hN.ne']
98 
99 theorem pointwiseRootAverage_projector {N : ℕ} (hN : 0 < N) {omega : ℂ}
100     (ho : IsPrimitiveRoot omega N) (i j : ℕ) (f : ℂ → ℂ) (z : ℂ) :
101     pointwiseRootAverage N i omega (pointwiseRootAverage N j omega f) z =
102       if j % N = i % N then pointwiseRootAverage N j omega f z else 0 := by
103   exact pointwiseRootAverage_of_covariant hN ho (mapsTo_univ _ _) i j _
104     (fun w _ => pointwiseRootAverage_covariant hN ho j f w) (mem_univ z)
105 
106 theorem pointwiseRootAverage_resolution {N : ℕ} (hN : 0 < N) {omega : ℂ}
107     (ho : IsPrimitiveRoot omega N) (f : ℂ → ℂ) (z : ℂ) :
108     (∑ j ∈ Finset.range N, pointwiseRootAverage N j omega f z) = f z := by
109   have hw (l : ℕ) : (∑ j ∈ Finset.range N, ((omega ^ j)⁻¹) ^ l) =
110       if l % N = 0 then (N : ℂ) else 0 := by
111     have h := root_weight_sum hN ho l 0
112     simp only [pow_zero, mul_one, Nat.zero_mod] at h
113     convert h using 1
114     · apply Finset.sum_congr rfl
115       intro j _
116       simp only [← inv_pow, ← pow_mul]
117       rw [Nat.mul_comm]
118     · simp [eq_comm]
119   unfold pointwiseRootAverage
120   rw [← Finset.mul_sum, Finset.sum_comm]
121   simp_rw [← Finset.sum_mul, hw]
122   rw [Finset.sum_eq_single 0]
123   · simp [Nat.cast_ne_zero.mpr hN.ne']
124   · intro l hl hl0
125     simp [Nat.mod_eq_of_lt (Finset.mem_range.mp hl), hl0]
126   · simp [hN]
127 
128 theorem differentiableOn_pointwiseRootAverage {N : ℕ} (j : ℕ) (omega : ℂ)
129     {s : Set ℂ} (hs : MapsTo (fun z => omega * z) s s)
130     {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f s) :
131     DifferentiableOn ℂ (pointwiseRootAverage N j omega f) s := by
132   apply DifferentiableOn.const_mul
133   apply DifferentiableOn.fun_sum
134   intro l _
135   apply DifferentiableOn.const_mul
136   exact hf.comp (by fun_prop) (mapsTo_root_pow hs l)
137 
138 theorem pointwiseRootAverage_range_iff {N : ℕ} (hN : 0 < N) {omega : ℂ}
139     (ho : IsPrimitiveRoot omega N) {s : Set ℂ}
140     (hs : MapsTo (fun z => omega * z) s s) (j : ℕ) {f : ℂ → ℂ}
141     (hf : DifferentiableOn ℂ f s) :
142     (∃ g : ℂ → ℂ, DifferentiableOn ℂ g s ∧ EqOn (pointwiseRootAverage N j omega g) f s) ↔
143       ∀ z ∈ s, f (omega * z) = omega ^ j * f z := by
144   constructor
145   · rintro ⟨g, _, hg⟩ z hz
146     rw [← hg (hs hz), ← hg hz]
147     exact pointwiseRootAverage_covariant hN ho j g z
148   · intro hc
149     refine ⟨f, hf, fun z hz => ?_⟩
150     simpa using pointwiseRootAverage_of_covariant hN ho hs j j f hc hz
151 
152 theorem pointwiseRootAverage_sum {I : Type*} (s : Finset I)
153     (N j : ℕ) (omega : ℂ) (f : I → ℂ → ℂ) (z : ℂ) :
154     pointwiseRootAverage N j omega (fun w => ∑ i ∈ s, f i w) z =
155       ∑ i ∈ s, pointwiseRootAverage N j omega (f i) z := by
156   unfold pointwiseRootAverage
157   simp_rw [Finset.mul_sum]
158   rw [Finset.sum_comm]
159 
160 theorem pointwiseRootAverage_product {N : ℕ} (hN : 0 < N) {omega : ℂ}
161     (ho : IsPrimitiveRoot omega N) (k : ℕ) (f g : ℂ → ℂ) (z : ℂ) :
162     pointwiseRootAverage N k omega (fun w => f w * g w) z =
163       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
164         if (i + j) % N = k % N then
165           pointwiseRootAverage N i omega f z * pointwiseRootAverage N j omega g z
166         else 0 := by
167   have he : (fun w => f w * g w) =
168       (fun w => ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
169         pointwiseRootAverage N i omega f w * pointwiseRootAverage N j omega g w) := by
170     funext w
171     rw [← Finset.sum_mul_sum, pointwiseRootAverage_resolution hN ho,
172       pointwiseRootAverage_resolution hN ho]
173   rw [he, pointwiseRootAverage_sum]
174   apply Finset.sum_congr rfl
175   intro i _
176   rw [pointwiseRootAverage_sum]
177   apply Finset.sum_congr rfl
178   intro j _
179   apply pointwiseRootAverage_of_covariant hN ho (mapsTo_univ _ _)
180   · intro w _
181     rw [pointwiseRootAverage_covariant hN ho, pointwiseRootAverage_covariant hN ho, pow_add]
182     ring
183   · exact mem_univ z
184 
185 theorem pointwiseRootAverage_hasSum {N : ℕ} (hN : 0 < N) {omega : ℂ}
186     (ho : IsPrimitiveRoot omega N) (j : ℕ) (a : ℕ → ℂ) (f : ℂ → ℂ) (z : ℂ)
187     (hf : ∀ l ∈ Finset.range N, HasSum (fun n => a n * (omega ^ l * z) ^ n)
188       (f (omega ^ l * z))) :
189     HasSum (fun n => (if n % N = j % N then a n else 0) * z ^ n)
190       (pointwiseRootAverage N j omega f z) := by
191   have h := (hasSum_sum (fun l hl => (hf l hl).mul_left (((omega ^ j)⁻¹) ^ l))).mul_left ((N : ℂ)⁻¹)
192   apply h.congr_fun
193   intro n
194   simp only [mul_pow]
195   have ht (l : ℕ) : ((omega ^ j)⁻¹) ^ l * (a n * ((omega ^ l) ^ n * z ^ n)) =
196       (((omega ^ j)⁻¹) ^ l * (omega ^ l) ^ n) * (a n * z ^ n) := by ring
197   simp_rw [ht]
198   rw [← Finset.sum_mul, root_weight_sum hN ho]
199   split_ifs <;> simp [Nat.cast_ne_zero.mpr hN.ne']
200 
201 end
202 end Komorebi.PaperIV

Back to source controls