ZeroPerturbation.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroGeometry
6 import Mathlib.Analysis.Calculus.MeanValue
7 import Mathlib.Topology.MetricSpace.Contracting
8 
9 /-! # Local zeros of a perturbed two-exponential sum
10 
11 The zero existence and uniqueness step is proved by contraction of the actual
12 complex logarithm. No zero-counting or existence certificate is assumed.
13 -/
14 
15 namespace Komorebi.PaperIV
16 noncomputable section
17 open Metric
18 
19 theorem norm_one_add_lower_half {u : ℂ} (hu : ‖u‖ ≤ 1 / 2) :
20     (1 / 2 : ℝ) ≤ ‖1 + u‖ := by
21   have h := norm_sub_norm_le (1 : ℂ) (-u)
22   simp only [norm_one, norm_neg, sub_neg_eq_add] at h
23   linarith
24 
25 theorem log_one_add_lipschitz_half :
26     LipschitzOnWith 2 (fun u : ℂ => Complex.log (1 + u)) (closedBall 0 (1 / 2)) := by
27   apply (convex_closedBall (0 : ℂ) (1 / 2)).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
28     (f' := fun u => (1 + u)⁻¹)
29   · intro u hu
30     have hu' : ‖u‖ ≤ 1 / 2 := by simpa [mem_closedBall, dist_eq_norm] using hu
31     exact ((Complex.hasDerivAt_log (Complex.mem_slitPlane_of_norm_lt_one
32       (lt_of_le_of_lt hu' (by norm_num)))).comp_const_add 1 u).hasDerivWithinAt
33   · intro u hu
34     have hu' : ‖u‖ ≤ 1 / 2 := by simpa [mem_closedBall, dist_eq_norm] using hu
35     change ‖(1 + u)⁻¹‖ ≤ (2 : ℝ)
36     rw [norm_inv, inv_eq_one_div, div_le_iff₀ (lt_of_lt_of_le (by norm_num) (norm_one_add_lower_half hu'))]
37     linarith [norm_one_add_lower_half hu']
38 
39 /-- The actual logarithmic correction map. -/
40 def logarithmicZeroMap (a t : ℂ) (R : ℂ → ℂ) (z : ℂ) : ℂ :=
41   t + Complex.log (1 + R z) / a
42 
43 theorem logarithmicZeroMap_mapsTo {a t : ℂ} (ha : a ≠ 0) {R : ℂ → ℂ}
44     (hR : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R z‖ ≤ 1 / 2) :
45     Set.MapsTo (logarithmicZeroMap a t R) (closedBall t (1 / ‖a‖))
46       (closedBall t (1 / ‖a‖)) := by
47   intro z hz
48   rw [mem_closedBall, dist_eq_norm, logarithmicZeroMap, add_sub_cancel_left, norm_div]
49   apply (div_le_div_iff_of_pos_right (norm_pos_iff.mpr ha)).mpr
50   have h := Complex.norm_log_one_add_half_le_self (hR z hz)
51   linarith [hR z hz]
52 
53 theorem logarithmicZeroMap_lipschitz {a t : ℂ} (ha : a ≠ 0) {R R' : ℂ → ℂ}
54     (hR : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R z‖ ≤ 1 / 2)
55     (hd : ∀ z ∈ closedBall t (1 / ‖a‖), HasDerivAt R (R' z) z)
56     (hb : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R' z‖ ≤ ‖a‖ / 4) :
57     LipschitzOnWith (1 / 2) (logarithmicZeroMap a t R) (closedBall t (1 / ‖a‖)) := by
58   apply LipschitzOnWith.of_dist_le_mul
59   intro x hx y hy
60   have hxy := (convex_closedBall t (1 / ‖a‖)).norm_image_sub_le_of_norm_hasDerivWithin_le
61     (fun z hz => (hd z hz).hasDerivWithinAt) hb hy hx
62   have hl := log_one_add_lipschitz_half.dist_le_mul (R x)
63     (by simpa [mem_closedBall, dist_eq_norm] using hR x hx) (R y)
64     (by simpa [mem_closedBall, dist_eq_norm] using hR y hy)
65   simp only [NNReal.coe_ofNat, dist_eq_norm] at hl
66   simp only [dist_eq_norm, logarithmicZeroMap, add_sub_add_left_eq_sub,
67     ← sub_div, norm_div, NNReal.coe_div, NNReal.coe_one, NNReal.coe_ofNat]
68   apply (div_le_iff₀ (norm_pos_iff.mpr ha)).mpr
69   nlinarith
70 
71 theorem logarithmicZeroMap_fixed_iff {a t : ℂ} (ha : a ≠ 0)
72     (ht : Complex.exp (a * t) = -1) {R : ℂ → ℂ}
73     (hR : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R z‖ ≤ 1 / 2)
74     {z : ℂ} (hz : z ∈ closedBall t (1 / ‖a‖)) :
75     logarithmicZeroMap a t R z = z ↔ 1 + Complex.exp (a * z) + R z = 0 := by
76   have haN := norm_pos_iff.mpr ha
77   have hnorm : ‖a * (z - t)‖ ≤ 1 := by
78     rw [norm_mul]
79     have hz' : ‖z - t‖ ≤ 1 / ‖a‖ := by simpa [mem_closedBall, dist_eq_norm] using hz
80     calc _ ≤ ‖a‖ * (1 / ‖a‖) := mul_le_mul_of_nonneg_left hz' (norm_nonneg a)
81          _ = 1 := by field_simp
82   have he : Complex.exp (a * z) = -Complex.exp (a * (z - t)) := by
83     rw [show a * z = a * t + a * (z - t) by ring, Complex.exp_add, ht]
84     ring
85   have hne : 1 + R z ≠ 0 := norm_pos_iff.mp
86     (lt_of_lt_of_le (by norm_num) (norm_one_add_lower_half (hR z hz)))
87   constructor
88   · intro hf
89     have hlog : Complex.log (1 + R z) = a * (z - t) := by
90       unfold logarithmicZeroMap at hf
91       field_simp at hf
92       linear_combination hf
93     have hh := Complex.exp_log hne
94     rw [hlog] at hh
95     rw [he, hh]
96     ring
97   · intro hf
98     have hh : Complex.exp (a * (z - t)) = 1 + R z := by
99       rw [he] at hf
100       linear_combination -hf
101     have hi : |(a * (z - t)).im| ≤ 1 :=
102       (Complex.abs_im_le_norm _).trans hnorm
103     have hl := Complex.log_exp (x := a * (z - t))
104       (by have := (abs_le.mp hi).1; linarith [Real.two_le_pi])
105       (by have := (abs_le.mp hi).2; linarith [Real.two_le_pi])
106     rw [hh] at hl
107     unfold logarithmicZeroMap
108     rw [hl]
109     field_simp
110     ring
111 
112 /-- A small differentiable remainder creates exactly one zero in the local disk. -/
113 theorem perturbed_exponential_unique_zero {a t : ℂ} (ha : a ≠ 0)
114     (ht : Complex.exp (a * t) = -1) {R R' : ℂ → ℂ}
115     (hR : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R z‖ ≤ 1 / 2)
116     (hd : ∀ z ∈ closedBall t (1 / ‖a‖), HasDerivAt R (R' z) z)
117     (hb : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R' z‖ ≤ ‖a‖ / 4) :
118     ∃! z : ℂ, z ∈ closedBall t (1 / ‖a‖) ∧ 1 + Complex.exp (a * z) + R z = 0 := by
119   have hm := logarithmicZeroMap_mapsTo ha hR
120   have hl := logarithmicZeroMap_lipschitz ha hR hd hb
121   have hc : ContractingWith (1 / 2) (hm.restrict (logarithmicZeroMap a t R)
122       (closedBall t (1 / ‖a‖)) (closedBall t (1 / ‖a‖))) :=
123     ⟨by norm_num, hl.mapsToRestrict hm⟩
124   obtain ⟨z, hz, hf, _⟩ := ContractingWith.exists_fixedPoint'
125     isClosed_closedBall.isComplete hm hc
126     (show t ∈ closedBall t (1 / ‖a‖) by simp)
127     (edist_ne_top t (logarithmicZeroMap a t R t))
128   refine ⟨z, ⟨hz, (logarithmicZeroMap_fixed_iff ha ht hR hz).mp hf⟩, ?_⟩
129   intro y hy
130   have hfy := (logarithmicZeroMap_fixed_iff ha ht hR hy.1).mpr hy.2
131   have hdist := hl.dist_le_mul y hy.1 z hz
132   rw [hfy, hf] at hdist
133   have hzero : dist y z = 0 := by
134     simp only [NNReal.coe_div, NNReal.coe_one, NNReal.coe_ofNat] at hdist
135     nlinarith [dist_nonneg (x := y) (y := z)]
136   exact dist_eq_zero.mp hzero
137 
138 /-- An explicit displacement bound for every zero in the local disk. -/
139 theorem perturbed_exponential_zero_distance {a t : ℂ} (ha : a ≠ 0)
140     (ht : Complex.exp (a * t) = -1) {R : ℂ → ℂ} {ε : ℝ} (hε : ε ≤ 1 / 2)
141     (hR : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R z‖ ≤ ε)
142     {z : ℂ} (hz : z ∈ closedBall t (1 / ‖a‖))
143     (hzero : 1 + Complex.exp (a * z) + R z = 0) :
144     ‖z - t‖ ≤ (3 / 2 : ℝ) * ε / ‖a‖ := by
145   have hf := (logarithmicZeroMap_fixed_iff ha ht (fun w hw => (hR w hw).trans hε) hz).mpr hzero
146   have he : z - t = Complex.log (1 + R z) / a := by
147     unfold logarithmicZeroMap at hf
148     linear_combination -hf
149   rw [he, norm_div]
150   apply div_le_div_of_nonneg_right _ (norm_nonneg a)
151   exact (Complex.norm_log_one_add_half_le_self ((hR z hz).trans hε)).trans
152     (mul_le_mul_of_nonneg_left (hR z hz) (by norm_num))
153 
154 /-- The displacement estimate retains the actual remainder value at the zero. -/
155 theorem perturbed_exponential_pointwise_distance {a t : ℂ} (ha : a ≠ 0)
156     (ht : Complex.exp (a * t) = -1) {R : ℂ → ℂ}
157     (hR : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R z‖ ≤ 1 / 2)
158     {z : ℂ} (hz : z ∈ closedBall t (1 / ‖a‖))
159     (hzero : 1 + Complex.exp (a * z) + R z = 0) :
160     ‖z - t‖ ≤ (3 / 2 : ℝ) * ‖R z‖ / ‖a‖ := by
161   have hf := (logarithmicZeroMap_fixed_iff ha ht hR hz).mpr hzero
162   have he : z - t = Complex.log (1 + R z) / a := by
163     unfold logarithmicZeroMap at hf
164     linear_combination -hf
165   rw [he, norm_div]
166   exact div_le_div_of_nonneg_right (Complex.norm_log_one_add_half_le_self (hR z hz)) (norm_nonneg a)
167 
168 theorem hasDerivAt_perturbed_exponential (a : ℂ) {R : ℂ → ℂ} {z Rz' : ℂ}
169     (hd : HasDerivAt R Rz' z) :
170     HasDerivAt (fun w => 1 + Complex.exp (a * w) + R w)
171       (a * Complex.exp (a * z) + Rz') z := by
172   have h := ((((hasDerivAt_id z).const_mul a).cexp).const_add 1).add hd
173   have he : Complex.exp (a * id z) * (a * 1) + Rz' = a * Complex.exp (a * z) + Rz' := by
174     simp only [id_eq, mul_one]
175     ring
176   rw [he] at h
177   convert h using 1 <;> rfl
178 
179 /-- The derivative cannot vanish at the localized zero. -/
180 theorem perturbed_exponential_zero_derivative_lower {a : ℂ} {R : ℂ → ℂ}
181     {z Rz' : ℂ} (hzero : 1 + Complex.exp (a * z) + R z = 0)
182     (hR : ‖R z‖ ≤ 1 / 2) (hb : ‖Rz'‖ ≤ ‖a‖ / 4) :
183     ‖a‖ / 4 ≤ ‖a * Complex.exp (a * z) + Rz'‖ := by
184   have he : Complex.exp (a * z) = -(1 + R z) := by linear_combination hzero
185   have hn : ‖a‖ / 2 ≤ ‖a * Complex.exp (a * z)‖ := by
186     rw [he, norm_mul, norm_neg]
187     have := mul_le_mul_of_nonneg_left (norm_one_add_lower_half hR) (norm_nonneg a)
188     linarith
189   have h := norm_sub_norm_le (a * Complex.exp (a * z)) (-Rz')
190   simp only [norm_neg, sub_neg_eq_add] at h
191   linarith
192 
193 /-- Analytic multiplicity one follows from the quantified derivative bound. -/
194 theorem perturbed_exponential_zero_order_one {a : ℂ} (ha : a ≠ 0)
195     {R : ℂ → ℂ} {z : ℂ} (hRanalytic : AnalyticAt ℂ R z)
196     (hzero : 1 + Complex.exp (a * z) + R z = 0)
197     (hR : ‖R z‖ ≤ 1 / 2) (hb : ‖deriv R z‖ ≤ ‖a‖ / 4) :
198     analyticOrderAt (fun w => 1 + Complex.exp (a * w) + R w) z = 1 := by
199   have hf : AnalyticAt ℂ (fun w => 1 + Complex.exp (a * w) + R w) z := by fun_prop
200   apply hf.analyticOrderAt_eq_one_of_zero_deriv_ne_zero hzero
201   rw [(hasDerivAt_perturbed_exponential a hRanalytic.differentiableAt.hasDerivAt).deriv]
202   apply norm_pos_iff.mp
203   exact lt_of_lt_of_le (div_pos (norm_pos_iff.mpr ha) (by norm_num))
204     (perturbed_exponential_zero_derivative_lower hzero hR hb)
205 
206 /-- The derivative asymptotic is an exact finite error estimate at a zero. -/
207 theorem perturbed_exponential_derivative_error {a : ℂ} {R : ℂ → ℂ}
208     {z Rz' : ℂ} (hzero : 1 + Complex.exp (a * z) + R z = 0) :
209     ‖(a * Complex.exp (a * z) + Rz') + a‖ ≤ ‖a‖ * ‖R z‖ + ‖Rz'‖ := by
210   have he : (a * Complex.exp (a * z) + Rz') + a = -(a * R z) + Rz' := by
211     linear_combination a * hzero
212   rw [he]
213   simpa [norm_mul] using norm_add_le (-(a * R z)) Rz'
214 
215 theorem norm_log_one_add_sub_self_half {u : ℂ} (hu : ‖u‖ ≤ 1 / 2) :
216     ‖Complex.log (1 + u) - u‖ ≤ ‖u‖ ^ 2 := by
217   have hinv : (1 - ‖u‖)⁻¹ ≤ 2 := by
218     rw [inv_eq_one_div, div_le_iff₀ (by linarith)]
219     linarith
220   have h := Complex.norm_log_one_add_sub_self_le (lt_of_le_of_lt hu (by norm_num))
221   nlinarith [mul_le_mul_of_nonneg_left hinv (sq_nonneg ‖u‖)]
222 
223 /-- The leading displacement formula with an explicit quadratic error bound. -/
224 theorem perturbed_exponential_first_correction {a t : ℂ} (ha : a ≠ 0)
225     (ht : Complex.exp (a * t) = -1) {R R' : ℂ → ℂ} {ε L : ℝ} (hε : ε ≤ 1 / 2)
226     (hR : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R z‖ ≤ ε)
227     (hd : ∀ z ∈ closedBall t (1 / ‖a‖), HasDerivAt R (R' z) z)
228     (hb : ∀ z ∈ closedBall t (1 / ‖a‖), ‖R' z‖ ≤ L)
229     {z : ℂ} (hz : z ∈ closedBall t (1 / ‖a‖))
230     (hzero : 1 + Complex.exp (a * z) + R z = 0) :
231     ‖z - t - R t / a‖ ≤ (ε ^ 2 + L * ((3 / 2 : ℝ) * ε / ‖a‖)) / ‖a‖ := by
232   have htmem : t ∈ closedBall t (1 / ‖a‖) := by simp
233   have hL : 0 ≤ L := (norm_nonneg _).trans (hb t htmem)
234   have hf := (logarithmicZeroMap_fixed_iff ha ht (fun w hw => (hR w hw).trans hε) hz).mpr hzero
235   have he : z - t - R t / a = (Complex.log (1 + R z) - R t) / a := by
236     unfold logarithmicZeroMap at hf
237     linear_combination -hf
238   rw [he, norm_div]
239   apply div_le_div_of_nonneg_right _ (norm_nonneg a)
240   have hlog := norm_log_one_add_sub_self_half ((hR z hz).trans hε)
241   have hLip := (convex_closedBall t (1 / ‖a‖)).norm_image_sub_le_of_norm_hasDerivWithin_le
242     (fun w hw => (hd w hw).hasDerivWithinAt) hb htmem hz
243   have hdist := perturbed_exponential_zero_distance ha ht hε hR hz hzero
244   calc
245     _ ≤ ‖Complex.log (1 + R z) - R z‖ + ‖R z - R t‖ := norm_sub_le_norm_sub_add_norm_sub ..
246     _ ≤ ε ^ 2 + L * ((3 / 2 : ℝ) * ε / ‖a‖) := by
247       apply add_le_add
248       · exact hlog.trans (pow_le_pow_left₀ (norm_nonneg _) (hR z hz) 2)
249       · exact hLip.trans (mul_le_mul_of_nonneg_left hdist hL)
250 
251 end
252 end Komorebi.PaperIV

Back to source controls