EntireBridge.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.FiniteAnalytic
6 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
7 
8 /-!
9 # Pointwise entire realization
10 
11 Finite exponential sums are entire. Their absolutely convergent Taylor series
12 are identified with the existing formal transfer and signed sections below.
13 The definitions do not assume any convergence or differential equation.
14 -/
15 
16 namespace Komorebi.PaperIV
17 open scoped PowerSeries
18 noncomputable section
19 
20 /-- The kth derivative expression of a finite exponential sum. -/
21 def exponentialSumJet (N : ℕ) (w a : ℕ → ℂ) (k : ℕ) (z : ℂ) : ℂ :=
22   ∑ l ∈ Finset.range N, w l * a l ^ k * Complex.exp (a l * z)
23 
24 theorem analyticAt_exponentialSumJet (N : ℕ) (w a : ℕ → ℂ) (k : ℕ) (z : ℂ) :
25     AnalyticAt ℂ (exponentialSumJet N w a k) z := by
26   unfold exponentialSumJet
27   fun_prop
28 
29 theorem hasDerivAt_exponentialSumJet (N : ℕ) (w a : ℕ → ℂ) (k : ℕ) (z : ℂ) :
30     HasDerivAt (exponentialSumJet N w a k) (exponentialSumJet N w a (k + 1) z) z := by
31   have h := HasDerivAt.fun_sum (u := Finset.range N) (fun l _ =>
32     (((hasDerivAt_id z).const_mul (a l)).cexp).const_mul (w l * a l ^ k))
33   have hd : (∑ l ∈ Finset.range N,
34       w l * a l ^ k * (Complex.exp (a l * id z) * (a l * 1))) =
35       exponentialSumJet N w a (k + 1) z := by
36     apply Finset.sum_congr rfl
37     intro l _
38     simp only [pow_succ, id_eq]
39     ring
40   rw [hd] at h
41   convert h using 1 <;> rfl
42 
43 theorem iteratedDeriv_exponentialSum (N : ℕ) (w a : ℕ → ℂ) (k : ℕ) :
44     deriv^[k] (exponentialSumJet N w a 0) = exponentialSumJet N w a k := by
45   induction k with
46   | zero => rfl
47   | succ k ih =>
48     rw [Function.iterate_succ_apply', ih]
49     exact funext (fun z => (hasDerivAt_exponentialSumJet N w a k z).deriv)
50 
51 /-- A finite exponential sum whose exponents satisfy `a^N = c` solves the
52 corresponding scalar constant-coefficient ODE everywhere. -/
53 theorem exponentialSum_ode (N : ℕ) (w a : ℕ → ℂ) (c : ℂ)
54     (ha : ∀ l ∈ Finset.range N, a l ^ N = c) (z : ℂ) :
55     deriv^[N] (exponentialSumJet N w a 0) z =
56       c * exponentialSumJet N w a 0 z := by
57   rw [iteratedDeriv_exponentialSum, exponentialSumJet, exponentialSumJet,
58     Finset.mul_sum]
59   apply Finset.sum_congr rfl
60   intro l hl
61   rw [ha l hl]
62   simp only [pow_zero]
63   ring
64 
65 /-- The pointwise Fourier average for the transfer section. -/
66 def entireTransfer (N j : ℕ) (omega lambda : ℂ) (z : ℂ) : ℂ :=
67   (N : ℂ)⁻¹ *
68     ∑ l ∈ Finset.range N,
69       ((omega ^ j)⁻¹) ^ l * Complex.exp ((lambda * omega ^ l) * z)
70 
71 theorem analyticAt_entireTransfer (N j : ℕ) (omega lambda z : ℂ) :
72     AnalyticAt ℂ (entireTransfer N j omega lambda) z := by
73   unfold entireTransfer
74   fun_prop
75 
76 theorem entireTransfer_eq_exponentialSum (N j : ℕ) (omega lambda : ℂ) :
77     entireTransfer N j omega lambda =
78       exponentialSumJet N (fun l => (N : ℂ)⁻¹ * ((omega ^ j)⁻¹) ^ l)
79         (fun l => lambda * omega ^ l) 0 := by
80   funext z
81   simp [entireTransfer, exponentialSumJet, Finset.mul_sum, mul_assoc]
82 
83 /-- Convergence to the pointwise function of exactly the formal coefficients
84 already used in the root-filter formalization. -/
85 theorem hasSum_finiteRootAverage (N j : ℕ) (omega lambda z : ℂ) :
86     HasSum (fun n =>
87       PowerSeries.coeff n (finiteRootAverage N j omega
88         (PowerSeries.rescale lambda (PowerSeries.exp ℂ))) * z ^ n)
89       (entireTransfer N j omega lambda z) := by
90   have h := (hasSum_sum (s := Finset.range N) (fun l _ =>
91     (NormedSpace.expSeries_div_hasSum_exp ((lambda * omega ^ l) * z)).mul_left
92       (((omega ^ j)⁻¹) ^ l))).mul_left ((N : ℂ)⁻¹)
93   rw [← Complex.exp_eq_exp_ℂ] at h
94   apply h.congr_fun
95   intro n
96   simp only [finiteRootAverage, PowerSeries.coeff_C_mul, map_sum,
97     PowerSeries.coeff_rescale, PowerSeries.coeff_exp]
98   rw [mul_assoc, Finset.sum_mul]
99   congr 1
100   apply Finset.sum_congr rfl
101   intro l _
102   simp [mul_pow]
103   ring
104 
105 /-- The analytic transfer function is the sum of its formal transfer series. -/
106 theorem hasSum_entireTransfer {N j : ℕ} (hN : 0 < N) (hj : j < N)
107     {omega : ℂ} (homega : IsPrimitiveRoot omega N) (lambda z : ℂ) :
108     HasSum (fun n => PowerSeries.coeff n (transferSection N j lambda) * z ^ n)
109       (entireTransfer N j omega lambda z) := by
110   simpa only [finiteRootAverage_rescale_exp_eq_transferSection hN hj homega]
111     using hasSum_finiteRootAverage N j omega lambda z
112 
113 theorem entireTransfer_eq_tsum {N j : ℕ} (hN : 0 < N) (hj : j < N)
114     {omega : ℂ} (homega : IsPrimitiveRoot omega N) (lambda z : ℂ) :
115     entireTransfer N j omega lambda z =
116       ∑' n, PowerSeries.coeff n (transferSection N j lambda) * z ^ n :=
117   (hasSum_entireTransfer hN hj homega lambda z).tsum_eq.symm
118 
119 /-- Independence of the chosen primitive root follows from the actual series. -/
120 theorem entireTransfer_independent_root {N j : ℕ} (hN : 0 < N) (hj : j < N)
121     {omega eta : ℂ} (homega : IsPrimitiveRoot omega N)
122     (heta : IsPrimitiveRoot eta N) (lambda z : ℂ) :
123     entireTransfer N j omega lambda z = entireTransfer N j eta lambda z := by
124   exact (hasSum_entireTransfer hN hj homega lambda z).unique
125     (hasSum_entireTransfer hN hj heta lambda z)
126 
127 theorem entireTransfer_ode {N : ℕ} {omega : ℂ}
128     (homega : IsPrimitiveRoot omega N) (j : ℕ) (lambda z : ℂ) :
129     deriv^[N] (entireTransfer N j omega lambda) z =
130       lambda ^ N * entireTransfer N j omega lambda z := by
131   rw [entireTransfer_eq_exponentialSum]
132   apply exponentialSum_ode
133   intro l _
134   rw [mul_pow, ← pow_mul, Nat.mul_comm l N, pow_mul, homega.pow_eq_one]
135   simp
136 
137 /-- Pointwise signed section using any chosen Nth root of minus one. -/
138 def entireSigned (N j : ℕ) (omega rho : ℂ) (z : ℂ) : ℂ :=
139   (rho ^ j)⁻¹ * entireTransfer N j omega rho z
140 
141 theorem analyticAt_entireSigned (N j : ℕ) (omega rho z : ℂ) :
142     AnalyticAt ℂ (entireSigned N j omega rho) z := by
143   exact analyticAt_const.mul (analyticAt_entireTransfer N j omega rho z)
144 
145 /-- Exact entire realization of the signed formal series. -/
146 theorem hasSum_entireSigned {N j : ℕ} (hN : 0 < N) (hj : j < N)
147     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
148     (z : ℂ) :
149     HasSum (fun n => PowerSeries.coeff n (signedSection (R := ℂ) N j) * z ^ n)
150       (entireSigned N j omega rho z) := by
151   have h := (hasSum_entireTransfer hN hj homega rho z).mul_left ((rho ^ j)⁻¹)
152   rw [signedSection_eq_inv_pow_mul_transferSection hN hj hrho]
153   simpa only [entireSigned, PowerSeries.coeff_C_mul, mul_assoc] using h
154 
155 theorem entireSigned_eq_tsum {N j : ℕ} (hN : 0 < N) (hj : j < N)
156     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
157     (z : ℂ) :
158     entireSigned N j omega rho z =
159       ∑' n, PowerSeries.coeff n (signedSection (R := ℂ) N j) * z ^ n :=
160   (hasSum_entireSigned hN hj homega hrho z).tsum_eq.symm
161 
162 theorem entireSigned_independent_roots {N j : ℕ} (hN : 0 < N) (hj : j < N)
163     {omega eta rho sigma : ℂ} (homega : IsPrimitiveRoot omega N)
164     (heta : IsPrimitiveRoot eta N) (hrho : rho ^ N = -1) (hsigma : sigma ^ N = -1)
165     (z : ℂ) :
166     entireSigned N j omega rho z = entireSigned N j eta sigma z :=
167   (hasSum_entireSigned hN hj homega hrho z).unique
168     (hasSum_entireSigned hN hj heta hsigma z)
169 
170 /-- The denominator's pointwise finite exponential representation. -/
171 theorem entireSigned_zero_eq_average (N : ℕ) (omega rho z : ℂ) :
172     entireSigned N 0 omega rho z =
173       (N : ℂ)⁻¹ * ∑ l ∈ Finset.range N, Complex.exp ((rho * omega ^ l) * z) := by
174   simp [entireSigned, entireTransfer]
175 
176 /-- Exact derivative/Taylor-coefficient correspondence at the origin. -/
177 theorem entireTransfer_derivative_at_zero {N j : ℕ} (hN : 0 < N) (hj : j < N)
178     {omega : ℂ} (homega : IsPrimitiveRoot omega N) (lambda : ℂ) (k : ℕ) :
179     deriv^[k] (entireTransfer N j omega lambda) 0 =
180       (k.factorial : ℂ) * PowerSeries.coeff k (transferSection N j lambda) := by
181   rw [entireTransfer_eq_exponentialSum, iteratedDeriv_exponentialSum]
182   rw [← finiteRootAverage_rescale_exp_eq_transferSection hN hj homega lambda]
183   simp only [exponentialSumJet, mul_zero, Complex.exp_zero, mul_one,
184     finiteRootAverage, PowerSeries.coeff_C_mul, map_sum, PowerSeries.coeff_rescale,
185     PowerSeries.coeff_exp]
186   rw [Finset.mul_sum, Finset.mul_sum]
187   apply Finset.sum_congr rfl
188   intro l _
189   simp only [mul_pow, map_inv₀, map_natCast, one_div]
190   have hk : (k.factorial : ℂ) ≠ 0 := by exact_mod_cast k.factorial_ne_zero
191   field_simp
192 
193 /-- The initial derivative matrix is genuinely diagonal for the entire functions. -/
194 theorem entireTransfer_initial_data {N j k : ℕ} (hN : 0 < N)
195     (hj : j < N) (hk : k < N) {omega : ℂ} (homega : IsPrimitiveRoot omega N)
196     (lambda : ℂ) :
197     deriv^[k] (entireTransfer N j omega lambda) 0 =
198       if k = j then lambda ^ j else 0 := by
199   rw [entireTransfer_derivative_at_zero hN hj homega, coeff_transferSection]
200   have hfac : (k.factorial : ℂ) ≠ 0 := by exact_mod_cast k.factorial_ne_zero
201   by_cases h : k = j
202   · subst k
203     simp [transferSectionCoeff, Nat.mod_eq_of_lt hk]
204     field_simp
205   · simp [transferSectionCoeff, Nat.mod_eq_of_lt hk, h]
206 
207 theorem entireSigned_eq_exponentialSum (N j : ℕ) (omega rho : ℂ) :
208     entireSigned N j omega rho =
209       exponentialSumJet N
210         (fun l => (rho ^ j)⁻¹ * (N : ℂ)⁻¹ * ((omega ^ j)⁻¹) ^ l)
211         (fun l => rho * omega ^ l) 0 := by
212   funext z
213   simp [entireSigned, entireTransfer, exponentialSumJet, Finset.mul_sum, mul_assoc]
214 
215 theorem entireSigned_ode {N : ℕ} {omega rho : ℂ}
216     (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1) (j : ℕ) (z : ℂ) :
217     deriv^[N] (entireSigned N j omega rho) z = -entireSigned N j omega rho z := by
218   rw [entireSigned_eq_exponentialSum]
219   have h := exponentialSum_ode N
220     (fun l => (rho ^ j)⁻¹ * (N : ℂ)⁻¹ * ((omega ^ j)⁻¹) ^ l)
221     (fun l => rho * omega ^ l) (-1) (by
222       intro l _
223       rw [mul_pow, ← pow_mul, Nat.mul_comm l N, pow_mul, homega.pow_eq_one, hrho]
224       simp) z
225   simpa using h
226 
227 theorem entireSigned_derivative_eq_scaled_transfer (N j k : ℕ) (omega rho z : ℂ) :
228     deriv^[k] (entireSigned N j omega rho) z =
229       (rho ^ j)⁻¹ * deriv^[k] (entireTransfer N j omega rho) z := by
230   rw [entireSigned_eq_exponentialSum, entireTransfer_eq_exponentialSum,
231     iteratedDeriv_exponentialSum, iteratedDeriv_exponentialSum]
232   simp [exponentialSumJet, Finset.mul_sum, mul_assoc]
233 
234 theorem entireSigned_initial_data {N j k : ℕ} (hN : 0 < N)
235     (hj : j < N) (hk : k < N) {omega rho : ℂ} (homega : IsPrimitiveRoot omega N)
236     (hrho : rho ^ N = -1) :
237     deriv^[k] (entireSigned N j omega rho) 0 = if k = j then 1 else 0 := by
238   have hr : rho ≠ 0 := by
239     intro h
240     simp [h, hN.ne'] at hrho
241   rw [entireSigned_derivative_eq_scaled_transfer,
242     entireTransfer_initial_data hN hj hk homega]
243   split_ifs <;> simp [pow_ne_zero j hr]
244 
245 end
246 end Komorebi.PaperIV

Back to source controls