SignedDerivativeAsymptotics.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedZeroOrbits
6 import KomorebiPaperIV.SignedZeroCorrection
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Metric
11 
12 /-- The exact nonvanishing factor used in the two-term normalization. -/
13 def signedNormalizationFactor (N : ℕ) (z : ℂ) : ℂ :=
14   (N : ℂ) * Complex.exp (-(canonicalSignedVertex N (N - 1) * z))
15 
16 theorem signedNormalizationFactor_ne_zero {N : ℕ} (hN : 0 < N) (z : ℂ) :
17     signedNormalizationFactor N z ≠ 0 :=
18   mul_ne_zero (by exact_mod_cast hN.ne') (Complex.exp_ne_zero _)
19 
20 /-- At a denominator zero, the product-rule term containing the denominator
21 vanishes, leaving the actual derivative of the original entire function. -/
22 theorem canonicalSignedDenominator_derivative_normalization {N : ℕ} (hN : 3 ≤ N)
23     {z : ℂ} (hz : canonicalSignedDenominator N z = 0) :
24     signedNormalizationFactor N z * deriv (canonicalSignedDenominator N) z =
25       signedZeroFrequency N * Complex.exp (signedZeroFrequency N * z) +
26         signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 1 z := by
27   let R := signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 0
28   let G := fun w : ℂ => 1 + Complex.exp (signedZeroFrequency N * w) + R w
29   have hP : AnalyticAt ℂ (signedNormalizationFactor N) z := by
30     unfold signedNormalizationFactor; fun_prop
31   have hD : AnalyticAt ℂ (canonicalSignedDenominator N) z := analyticAt_entireSigned _ _ _ _ _
32   have hp := hP.differentiableAt.hasDerivAt.mul hD.differentiableAt.hasDerivAt
33   have hR : HasDerivAt R
34       (signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 1 z) z :=
35     hasDerivAt_finiteExponentialRemainder _ _ _ 0 z
36   have hg := hasDerivAt_perturbed_exponential (signedZeroFrequency N) hR
37   have he : (fun w => signedNormalizationFactor N w * canonicalSignedDenominator N w) = G := by
38     funext w
39     exact signed_two_term_normalization (by omega) _ _ w
40   change HasDerivAt (fun w => signedNormalizationFactor N w * canonicalSignedDenominator N w) _ z at hp
41   rw [he, hz, mul_zero, zero_add] at hp
42   have hh := hp.unique hg
43   simpa only [mul_comm] using hh
44 
45 /-- A relative derivative estimate for the original denominator. Its leading
46 term is `-a/P(z)`, where `a=2 i sin(pi/N)` and `P` is the exact prefactor. -/
47 theorem canonicalSignedDenominator_relative_derivative_error {N : ℕ} (hN : 3 ≤ N)
48     {t : ℝ} (ht : 1 / ‖signedZeroFrequency N‖ ≤ t) {z : ℂ}
49     (hz : z ∈ closedBall (t : ℂ) (1 / ‖signedZeroFrequency N‖))
50     (hz0 : canonicalSignedDenominator N z = 0) :
51     ‖deriv (canonicalSignedDenominator N) z /
52       (-signedZeroFrequency N / signedNormalizationFactor N z) - 1‖ ≤
53       ((‖signedZeroFrequency N‖ + 2) / ‖signedZeroFrequency N‖) * signedRemainderEnvelope N t := by
54   have ha := signedZeroFrequency_ne_zero (show 2 ≤ N by omega)
55   have hP := signedNormalizationFactor_ne_zero (show 0 < N by omega) z
56   have hnorm := canonicalSignedDenominator_derivative_normalization hN hz0
57   have hb := canonicalSignedDenominator_normalized_derivative_error hN ht hz hz0
58   have he : deriv (canonicalSignedDenominator N) z /
59       (-signedZeroFrequency N / signedNormalizationFactor N z) - 1 =
60       -((signedZeroFrequency N * Complex.exp (signedZeroFrequency N * z) +
61         signedExponentialRemainder N (canonicalPrimitiveRoot N) (canonicalSignedRoot N) 1 z) +
62           signedZeroFrequency N) / signedZeroFrequency N := by
63     rw [← hnorm]
64     field_simp
65     ring
66   rw [he, norm_div, norm_neg]
67   calc
68     _ ≤ ((‖signedZeroFrequency N‖ + 2) * signedRemainderEnvelope N t) /
69         ‖signedZeroFrequency N‖ := div_le_div_of_nonneg_right hb (norm_nonneg _)
70     _ = _ := by ring
71 
72 /-- At a real point the leading derivative modulus is exactly the manuscript's
73 `(2 sin(pi/N)/N) exp(cos(pi/N) t)` scale. -/
74 theorem signed_derivative_leading_norm {N : ℕ} (hN : 3 ≤ N) (t : ℝ) :
75     ‖-signedZeroFrequency N / signedNormalizationFactor N (t : ℂ)‖ =
76       (2 * Real.sin (Real.pi / N) / N) * Real.exp (Real.cos (Real.pi / N) * t) := by
77   have hn : (N : ℝ) ≠ 0 := by exact_mod_cast (show N ≠ 0 by omega)
78   rw [norm_div, norm_neg, signedZeroFrequency_norm (by omega)]
79   unfold signedNormalizationFactor
80   rw [norm_mul, Complex.norm_natCast, Complex.norm_exp, Complex.neg_re, Complex.mul_re,
81     Complex.ofReal_re, Complex.ofReal_im, mul_zero, sub_zero,
82     canonicalSignedVertex_last_re (by omega), Real.exp_neg]
83   field_simp
84 
85 /-- The relative estimate also controls the modulus of the actual derivative. -/
86 theorem canonicalSignedDenominator_derivative_modulus_error {N : ℕ} (hN : 3 ≤ N)
87     {t x : ℝ} (ht : 1 / ‖signedZeroFrequency N‖ ≤ t)
88     (hx : (x : ℂ) ∈ closedBall (t : ℂ) (1 / ‖signedZeroFrequency N‖))
89     (hx0 : canonicalSignedDenominator N (x : ℂ) = 0) :
90     |‖deriv (canonicalSignedDenominator N) (x : ℂ)‖ /
91         ((2 * Real.sin (Real.pi / N) / N) * Real.exp (Real.cos (Real.pi / N) * x)) - 1| ≤
92       ((‖signedZeroFrequency N‖ + 2) / ‖signedZeroFrequency N‖) * signedRemainderEnvelope N t := by
93   have hb := canonicalSignedDenominator_relative_derivative_error hN ht hx hx0
94   have hh := abs_norm_sub_norm_le
95     (deriv (canonicalSignedDenominator N) (x : ℂ) /
96       (-signedZeroFrequency N / signedNormalizationFactor N (x : ℂ))) (1 : ℂ)
97   rw [norm_div, norm_one, signed_derivative_leading_norm hN] at hh
98   exact hh.trans hb
99 
100 end
101 end Komorebi.PaperIV

Back to source controls