SignedCorrectionCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedRealPhase
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Metric Filter
10 open scoped Topology
11 
12 def signedLeadingCorrection (N m : ℕ) : ℂ :=
13   signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0
14     (signedZeroCenter N m : ℂ) / signedZeroFrequency N
15 
16 theorem signedLeadingCorrection_eq_real_quotient {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
17     signedLeadingCorrection N m = -canonicalSignedDenominator N (signedZeroCenter N m : ℂ) /
18       (signedDerivativeMainTerm N m (signedZeroCenter N m) : ℂ) := by
19   have ha := signedZeroFrequency_ne_zero hN
20   have hP := signedNormalizationFactor_ne_zero (show 0 < N by omega) (signedZeroCenter N m : ℂ)
21   have hl := signed_derivative_leading_phase hN m (signedZeroCenter N m)
22   simp only [sub_self, mul_zero, neg_zero, Complex.ofReal_zero, zero_mul, Complex.exp_zero, mul_one] at hl
23   have hn := signed_two_term_normalization hN
24     (canonicalPrimitiveRoot N) (canonicalSignedRoot N) (signedZeroCenter N m : ℂ)
25   change signedNormalizationFactor N (signedZeroCenter N m : ℂ) *
26     canonicalSignedDenominator N (signedZeroCenter N m : ℂ) =
27       1 + Complex.exp (signedZeroFrequency N * (signedZeroCenter N m : ℂ)) + _ at hn
28   rw [signedZeroCenter_cancellation hN, add_neg_cancel, zero_add] at hn
29   rw [signedLeadingCorrection, ← hn, ← hl]
30   field_simp
31 
32 theorem signedLeadingCorrection_real {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
33     (signedLeadingCorrection N m).im = 0 := by
34   rw [signedLeadingCorrection_eq_real_quotient hN]
35   simp [Complex.div_im, entireSigned_canonical_real (show 0 < N by omega)
36     (show 0 < N by omega), canonicalSignedDenominator]
37 
38 theorem signedRemainderEnvelope_center_tendsto_zero {N : ℕ} (hN : 3 ≤ N) :
39     Tendsto (fun m => signedRemainderEnvelope N (signedZeroCenter N m)) atTop (𝓝 0) := by
40   have ht := (signedZeroCenter_tendsto_atTop (show 2 ≤ N by omega)).const_mul_atTop_of_neg
41     (neg_lt_zero.mpr (signedPolygonGap_pos hN))
42   have he := (Real.tendsto_exp_atBot.comp ht).const_mul (signedRemainderScale N)
43   simpa only [mul_zero, signedRemainderEnvelope, Function.comp_apply] using he
44 
45 /-- The leading displacement, now specialized to the actual named zeros, with
46 its real correction and the full quadratic exponential error. -/
47 theorem signedPositiveZero_first_correction {N : ℕ} (hN : 3 ≤ N) :
48     (∀ m, (signedLeadingCorrection N m).im = 0) ∧
49     ∃ C : ℝ, 0 < C ∧ ∃ M : ℕ, ∀ m ≥ M,
50       ‖(signedPositiveZero N m : ℂ) - (signedZeroCenter N m : ℂ) - signedLeadingCorrection N m‖ ≤
51         C * Real.exp (-(2 * signedPolygonGap N) * signedZeroCenter N m) := by
52   refine ⟨signedLeadingCorrection_real (by omega), ?_⟩
53   obtain ⟨_, _, M0, hM0⟩ := signedPositiveZero_local_strings hN
54   have hs := (signedRemainderEnvelope_center_tendsto_zero hN).eventually
55     (eventually_le_nhds (by norm_num : (0 : ℝ) < 1 / 2))
56   obtain ⟨M1, hM1⟩ := eventually_atTop.mp hs
57   let C := ((1 + 3 / ‖signedZeroFrequency N‖) / ‖signedZeroFrequency N‖) * signedRemainderScale N ^ 2
58   have hS : 0 < signedRemainderScale N := by
59     simpa only [signedRemainderEnvelope, mul_zero, Real.exp_zero, mul_one] using signedRemainderEnvelope_pos hN 0
60   have ha : 0 < ‖signedZeroFrequency N‖ := norm_pos_iff.mpr (signedZeroFrequency_ne_zero (by omega))
61   refine ⟨C, by dsimp [C]; positivity, max M0 M1, ?_⟩
62   intro m hm
63   have hx := (hM0 m (le_trans (le_max_left M0 M1) hm)).1
64   have hb := canonicalSignedDenominator_first_correction hN (signedZeroCenter_ge_radius (by omega) m)
65     (signedZeroCenter_cancellation (by omega) m) (hM1 m (le_trans (le_max_right M0 M1) hm)) hx.2.2 hx.2.1
66   rw [signedRemainderEnvelope_sq] at hb
67   simpa only [signedLeadingCorrection, C, mul_assoc] using hb
68 
69 /-- A phase perturbation estimate with no small-angle side condition. -/
70 theorem norm_real_phase_sub_one_le (x : ℝ) :
71     ‖Complex.exp ((x : ℂ) * Complex.I) - 1‖ ≤ |x| := by
72   rw [mul_comm (x : ℂ), Complex.norm_exp_I_mul_ofReal_sub_one, Real.norm_eq_abs, abs_mul]
73   have h := (Real.abs_sin_le_abs (x := x / 2))
74   rw [abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 2)] at h
75   norm_num only [abs_of_pos (by norm_num : (0 : ℝ) < 2)]
76   linarith
77 
78 theorem relative_error_through_unit_phase {d b p : ℂ} (hb : b ≠ 0) (hp : ‖p‖ = 1) :
79     ‖d / b - 1‖ ≤ ‖d / (b * p) - 1‖ + ‖p - 1‖ := by
80   have hp0 : p ≠ 0 := by intro h; simp [h] at hp
81   have he : d / b - 1 = (d / (b * p) - 1) * p + (p - 1) := by field_simp; ring
82   rw [he]
83   exact (norm_add_le _ _).trans_eq (by rw [norm_mul, hp, mul_one])
84 
85 /-- Exact alternating-sign derivative asymptotics, in the original denominator
86 and at its actual real zeros. -/
87 theorem signedPositiveZero_signed_derivative_asymptotic {N : ℕ} (hN : 3 ≤ N) :
88     ∃ C : ℝ, 0 < C ∧ ∃ M : ℕ, ∀ m ≥ M,
89       ‖deriv (canonicalSignedDenominator N) (signedPositiveZero N m : ℂ) /
90         (signedDerivativeMainTerm N m (signedPositiveZero N m) : ℂ) - 1‖ ≤
91         C * Real.exp (-signedPolygonGap N * signedPositiveZero N m) := by
92   obtain ⟨C0, hC0, M, hM⟩ := signedPositiveZero_local_strings hN
93   let B := (‖signedZeroFrequency N‖ + 2) / ‖signedZeroFrequency N‖
94   let S := signedRemainderScale N
95   let r := 1 / ‖signedZeroFrequency N‖
96   let T := B * S + Real.sin (Real.pi / N) * C0
97   have hB : 0 < B := div_pos (by positivity) (norm_pos_iff.mpr (signedZeroFrequency_ne_zero (by omega)))
98   have hS : 0 < S := by
99     simpa only [signedRemainderEnvelope, mul_zero, Real.exp_zero, mul_one] using signedRemainderEnvelope_pos hN 0
100   have hT : 0 < T := add_pos (mul_pos hB hS) (mul_pos (signed_sine_pos (by omega)) hC0)
101   refine ⟨T * Real.exp (signedPolygonGap N * r), by positivity, M, ?_⟩
102   intro m hm
103   let x := signedPositiveZero N m
104   let t := signedZeroCenter N m
105   let p := Complex.exp ((-(Real.sin (Real.pi / N) * (x - t)) : ℝ) * Complex.I)
106   have hp : ‖p‖ = 1 := Complex.norm_exp_ofReal_mul_I _
107   have hx := (hM m hm).1
108   have hdelta : |x - t| ≤ r := by
109     simpa only [mem_closedBall, dist_eq_norm, ← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs] using hx.2.2
110   have hphase : ‖p - 1‖ ≤ Real.sin (Real.pi / N) * |x - t| := by
111     have h := norm_real_phase_sub_one_le (-(Real.sin (Real.pi / N) * (x - t)))
112     simpa only [abs_neg, abs_mul, abs_of_pos (signed_sine_pos (show 2 ≤ N by omega))] using h
113   have hrelative := canonicalSignedDenominator_relative_derivative_error hN
114     (signedZeroCenter_ge_radius (by omega) m) hx.2.2 hx.2.1
115   have hcombine := relative_error_through_unit_phase (d := deriv (canonicalSignedDenominator N) (x : ℂ))
116     (Complex.ofReal_ne_zero.mpr (signedDerivativeMainTerm_ne_zero (show 2 ≤ N by omega) m x)) hp
117   rw [← signed_derivative_leading_phase (by omega) m x] at hcombine
118   have hsmall : ‖deriv (canonicalSignedDenominator N) (x : ℂ) /
119       (signedDerivativeMainTerm N m x : ℂ) - 1‖ ≤ T * Real.exp (-signedPolygonGap N * t) := by
120     apply hcombine.trans
121     have hc := (hM m hm).2.2.1
122     dsimp [T, B, S, signedRemainderEnvelope, x, t] at *
123     nlinarith [mul_le_mul_of_nonneg_left hc (signed_sine_pos (by omega : 2 ≤ N)).le]
124   have he : Real.exp (-signedPolygonGap N * t) ≤
125       Real.exp (signedPolygonGap N * r) * Real.exp (-signedPolygonGap N * x) := by
126     rw [← Real.exp_add]
127     apply Real.exp_le_exp.mpr
128     have hd := (le_abs_self (x - t)).trans hdelta
129     nlinarith [signedPolygonGap_pos hN]
130   exact hsmall.trans (by simpa only [mul_assoc] using mul_le_mul_of_nonneg_left he hT.le)
131 
132 /-- The asymptotic sign is an actual eventual sign, not only a modulus claim. -/
133 theorem signedPositiveZero_eventual_derivative_sign {N : ℕ} (hN : 3 ≤ N) :
134     ∃ M : ℕ, ∀ m ≥ M,
135       0 < (-1 : ℝ) ^ (m + 1) *
136         (deriv (canonicalSignedDenominator N) (signedPositiveZero N m : ℂ)).re := by
137   obtain ⟨C, _, M0, hM0⟩ := signedPositiveZero_signed_derivative_asymptotic hN
138   have ht := (signedPositiveZero_tendsto_atTop hN).const_mul_atTop_of_neg
139     (neg_lt_zero.mpr (signedPolygonGap_pos hN))
140   have he := (Real.tendsto_exp_atBot.comp ht).const_mul C
141   simp only [mul_zero] at he
142   have hs := he.eventually (eventually_le_nhds (by norm_num : (0 : ℝ) < 1 / 2))
143   obtain ⟨M1, hM1⟩ := eventually_atTop.mp hs
144   refine ⟨max M0 M1, ?_⟩
145   intro m hm
146   let x := signedPositiveZero N m
147   let d := deriv (canonicalSignedDenominator N) (x : ℂ)
148   let b := signedDerivativeMainTerm N m x
149   have hb0 : b ≠ 0 := signedDerivativeMainTerm_ne_zero (by omega) m x
150   have hb := (hM0 m (le_trans (le_max_left _ _) hm)).trans
151     (hM1 m (le_trans (le_max_right _ _) hm))
152   have hdreal : d = (d.re : ℂ) := by
153     apply Complex.ext
154     · rfl
155     · exact canonicalSignedDenominator_derivative_real (by omega) x
156   change ‖d / (b : ℂ) - 1‖ ≤ (1 / 2 : ℝ) at hb
157   rw [hdreal, ← Complex.ofReal_div, ← Complex.ofReal_one, ← Complex.ofReal_sub,
158     Complex.norm_real, Real.norm_eq_abs] at hb
159   have hq : 0 < d.re / b := by have h := (abs_le.mp hb).1; linarith
160   have hmul : 0 < d.re * b := by
161     have heq : d.re * b = (d.re / b) * b ^ 2 := by field_simp
162     rw [heq]
163     exact mul_pos hq (sq_pos_of_ne_zero hb0)
164   have hspos := signedDerivativeScale_pos (show 2 ≤ N by omega) x
165   have h : 0 < ((-1 : ℝ) ^ (m + 1) * d.re) * signedDerivativeScale N x := by
166     dsimp [b, signedDerivativeMainTerm] at hmul
167     nlinarith
168   exact (mul_pos_iff_of_pos_right hspos).mp h
169 
170 end
171 end Komorebi.PaperIV

Back to source controls