ExponentialRemainder.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ExponentialBounds
6 
7 /-! # Exact finite exponential remainders and strip estimates
8 
9 The estimates are derived from explicit real-part gaps. The regular-polygon
10 gap and the global exclusion of other sectors are separate obligations.
11 -/
12 
13 namespace Komorebi.PaperIV
14 noncomputable section
15 
16 /-- Derivative jets of the actual normalized finite exponential remainder. -/
17 def finiteExponentialRemainder (s : Finset ℕ) (a : ℕ → ℂ) (b : ℂ)
18     (q : ℕ) (z : ℂ) : ℂ :=
19   ∑ l ∈ s, (a l - b) ^ q * Complex.exp ((a l - b) * z)
20 
21 theorem analyticAt_finiteExponentialRemainder (s : Finset ℕ) (a : ℕ → ℂ)
22     (b : ℂ) (q : ℕ) (z : ℂ) :
23     AnalyticAt ℂ (finiteExponentialRemainder s a b q) z := by
24   unfold finiteExponentialRemainder
25   fun_prop
26 
27 theorem hasDerivAt_finiteExponentialRemainder (s : Finset ℕ) (a : ℕ → ℂ)
28     (b : ℂ) (q : ℕ) (z : ℂ) :
29     HasDerivAt (finiteExponentialRemainder s a b q)
30       (finiteExponentialRemainder s a b (q + 1) z) z := by
31   have h := HasDerivAt.fun_sum (u := s) (fun l _ =>
32     (((hasDerivAt_id z).const_mul (a l - b)).cexp).const_mul ((a l - b) ^ q))
33   have he : (∑ l ∈ s, (a l - b) ^ q * (Complex.exp ((a l - b) * id z) * ((a l - b) * 1))) =
34       finiteExponentialRemainder s a b (q + 1) z := by
35     apply Finset.sum_congr rfl
36     intro l _
37     simp only [pow_succ, id_eq]
38     ring
39   rw [he] at h
40   convert h using 1 <;> rfl
41 
42 theorem iteratedDeriv_finiteExponentialRemainder (s : Finset ℕ) (a : ℕ → ℂ)
43     (b : ℂ) (q : ℕ) :
44     deriv^[q] (finiteExponentialRemainder s a b 0) =
45       finiteExponentialRemainder s a b q := by
46   induction q with
47   | zero => rfl
48   | succ q ih =>
49     rw [Function.iterate_succ_apply', ih]
50     exact funext (fun z => (hasDerivAt_finiteExponentialRemainder s a b q z).deriv)
51 
52 /-- All derivative orders satisfy an explicit uniform strip bound. -/
53 theorem finiteExponentialRemainder_strip_bound {s : Finset ℕ} {a : ℕ → ℂ}
54     {b : ℂ} {γ M A Y : ℝ} (hA : 0 ≤ A) (hM : 0 ≤ M)
55     (hgap : ∀ l ∈ s, (a l - b).re ≤ -γ)
56     (him : ∀ l ∈ s, |(a l - b).im| ≤ M)
57     (hnorm : ∀ l ∈ s, ‖a l - b‖ ≤ A)
58     {z : ℂ} (hx : 0 ≤ z.re) (hy : |z.im| ≤ Y) (q : ℕ) :
59     ‖finiteExponentialRemainder s a b q z‖ ≤
60       (s.card : ℝ) * A ^ q * Real.exp (-γ * z.re + M * Y) := by
61   have ht (l : ℕ) (hl : l ∈ s) :
62       ‖(a l - b) ^ q * Complex.exp ((a l - b) * z)‖ ≤
63         A ^ q * Real.exp (-γ * z.re + M * Y) := by
64     rw [norm_mul, norm_pow, Complex.norm_exp]
65     apply mul_le_mul (pow_le_pow_left₀ (norm_nonneg _) (hnorm l hl) q) _
66       (Real.exp_nonneg _) (pow_nonneg hA q)
67     apply Real.exp_le_exp.mpr
68     rw [Complex.mul_re]
69     have hreal := mul_le_mul_of_nonneg_right (hgap l hl) hx
70     have hib : -((a l - b).im * z.im) ≤ M * Y := by
71       calc
72         _ ≤ |(a l - b).im * z.im| := neg_le_abs _
73         _ = |(a l - b).im| * |z.im| := abs_mul _ _
74         _ ≤ M * Y := mul_le_mul (him l hl) hy (abs_nonneg _) hM
75     linarith
76   calc
77     _ ≤ ∑ l ∈ s, ‖(a l - b) ^ q * Complex.exp ((a l - b) * z)‖ := norm_sum_le _ _
78     _ ≤ ∑ _l ∈ s, A ^ q * Real.exp (-γ * z.re + M * Y) := Finset.sum_le_sum ht
79     _ = _ := by simp [mul_assoc]
80 
81 /-- Exact decomposition into two selected exponentials and the actual remainder. -/
82 theorem finite_two_term_normalization {s : Finset ℕ} {a : ℕ → ℂ}
83     {j k : ℕ} (hj : j ∈ s) (hk : k ∈ s) (hjk : j ≠ k) (z : ℂ) :
84     Complex.exp (-(a k * z)) * (∑ l ∈ s, Complex.exp (a l * z)) =
85       1 + Complex.exp ((a j - a k) * z) +
86         finiteExponentialRemainder ((s.erase j).erase k) a (a k) 0 z := by
87   have hk' : k ∈ s.erase j := Finset.mem_erase.mpr ⟨Ne.symm hjk, hk⟩
88   have hsum := Finset.sum_erase_add (s := s) (a := j) (f := fun l => Complex.exp (a l * z)) hj
89   have hsum' := Finset.sum_erase_add (s := s.erase j) (a := k)
90     (f := fun l => Complex.exp (a l * z)) hk'
91   rw [← hsum, ← hsum', mul_add, mul_add]
92   have he (v : ℂ) : Complex.exp (-(a k * z)) * Complex.exp (v * z) =
93       Complex.exp ((v - a k) * z) := by rw [← Complex.exp_add]; congr 1; ring
94   rw [he, he, sub_self, zero_mul, Complex.exp_zero]
95   rw [Finset.mul_sum]
96   have hs : (∑ l ∈ (s.erase j).erase k,
97       Complex.exp (-(a k * z)) * Complex.exp (a l * z)) =
98       finiteExponentialRemainder ((s.erase j).erase k) a (a k) 0 z := by
99     unfold finiteExponentialRemainder
100     simp only [pow_zero, one_mul, he]
101   rw [hs]
102   ring
103 
104 /-- Paper IV's normalized remainder, including every derivative jet. -/
105 def signedExponentialRemainder (N : ℕ) (omega rho : ℂ) (q : ℕ) (z : ℂ) : ℂ :=
106   finiteExponentialRemainder (((Finset.range N).erase 0).erase (N - 1))
107     (fun l => rho * omega ^ l) (rho * omega ^ (N - 1)) q z
108 
109 theorem signed_two_term_normalization {N : ℕ} (hN : 2 ≤ N)
110     (omega rho z : ℂ) :
111     (N : ℂ) * Complex.exp (-(rho * omega ^ (N - 1) * z)) *
112       entireSigned N 0 omega rho z =
113       1 + Complex.exp ((rho - rho * omega ^ (N - 1)) * z) +
114         signedExponentialRemainder N omega rho 0 z := by
115   rw [entireSigned_zero_eq_average]
116   have hn : (N : ℂ) ≠ 0 := by exact_mod_cast (show N ≠ 0 by omega)
117   have he : (N : ℂ) * Complex.exp (-(rho * omega ^ (N - 1) * z)) *
118       ((N : ℂ)⁻¹ * ∑ l ∈ Finset.range N, Complex.exp (rho * omega ^ l * z)) =
119       Complex.exp (-(rho * omega ^ (N - 1) * z)) *
120         ∑ l ∈ Finset.range N, Complex.exp (rho * omega ^ l * z) := by field_simp
121   rw [he]
122   simpa [signedExponentialRemainder] using finite_two_term_normalization
123     (a := fun l => rho * omega ^ l)
124     (Finset.mem_range.mpr (show 0 < N by omega))
125     (Finset.mem_range.mpr (show N - 1 < N by omega)) (show 0 ≠ N - 1 by omega) z
126 
127 /-- The normalized and original signed denominators have exactly the same zeros. -/
128 theorem signed_two_term_zero_iff {N : ℕ} (hN : 2 ≤ N) (omega rho z : ℂ) :
129     entireSigned N 0 omega rho z = 0 ↔
130       1 + Complex.exp ((rho - rho * omega ^ (N - 1)) * z) +
131         signedExponentialRemainder N omega rho 0 z = 0 := by
132   rw [← signed_two_term_normalization hN omega rho z]
133   have hn : (N : ℂ) ≠ 0 := by exact_mod_cast (show N ≠ 0 by omega)
134   simp [hn, Complex.exp_ne_zero]
135 
136 end
137 end Komorebi.PaperIV

Back to source controls