DerivativeGrowth.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SignedCorrectionCompletion
6 import KomorebiPaperIV.ZeroZetaConvergence
7 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter
12 open scoped Topology
13 
14 /-- A global exponential lower bound at every sufficiently large zero,
15 including every root-of-unity ray. -/
16 theorem canonicalSignedDenominator_derivative_lower_bound {N : ℕ} (hN : 3 ≤ N) :
17     ∃ A : ℝ, 0 < A ∧ ∃ R : ℝ, 0 < R ∧ ∀ z : ℂ,
18       R ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
19       A * Real.exp (Real.cos (Real.pi / N) * ‖z‖) ≤ ‖deriv (canonicalSignedDenominator N) z‖ := by
20   obtain ⟨B, _, M0, hM0⟩ := signedPositiveZero_derivative_asymptotic hN
21   have ht := (signedPositiveZero_tendsto_atTop (show 3 ≤ N from hN)).const_mul_atTop_of_neg
22     (neg_lt_zero.mpr (signedPolygonGap_pos hN))
23   have he := (Real.tendsto_exp_atBot.comp ht).const_mul B
24   simp only [mul_zero] at he
25   have hs := he.eventually (eventually_le_nhds (by norm_num : (0 : ℝ) < 1 / 2))
26   simp only [Function.comp_apply] at hs
27   obtain ⟨M1, hM1⟩ := eventually_atTop.mp hs
28   obtain ⟨M, hM, R, hR, hex⟩ := signedPositiveZero_unique_global_strings hN (max M0 M1)
29   let a := 2 * Real.sin (Real.pi / N) / N
30   have ha : 0 < a := div_pos (mul_pos (by norm_num) (signed_sine_pos (by omega))) (by exact_mod_cast (show 0 < N by omega))
31   refine ⟨a / 2, by positivity, R, hR, ?_⟩
32   intro z hz hz0
33   obtain ⟨p, hp, _⟩ := hex z hz hz0
34   have hm0 := le_trans (le_max_left M0 M1) (le_trans hM p.property)
35   have hm1 := le_trans (le_max_right M0 M1) (le_trans hM p.property)
36   have hb := (hM0 p.val.2 hm0).trans (hM1 p.val.2 hm1)
37   have hd : a / 2 * Real.exp (Real.cos (Real.pi / N) * signedPositiveZero N p.val.2) ≤
38       ‖deriv (canonicalSignedDenominator N) (signedPositiveZero N p.val.2 : ℂ)‖ := by
39     have hlow := (abs_le.mp hb).1
40     have hpos : 0 < a * Real.exp (Real.cos (Real.pi / N) * signedPositiveZero N p.val.2) := by positivity
41     have hq : (1 / 2 : ℝ) ≤ ‖deriv (canonicalSignedDenominator N) (signedPositiveZero N p.val.2 : ℂ)‖ /
42         (a * Real.exp (Real.cos (Real.pi / N) * signedPositiveZero N p.val.2)) := by dsimp [a]; linarith
43     have h := (le_div_iff₀ hpos).mp hq
44     nlinarith
45   rw [hp, signedPositiveZero_derivative_rotation (by omega)]
46   have hw := (canonicalPrimitiveRoot_isPrimitive (show 0 < N by omega)).norm'_eq_one (by omega)
47   simpa only [norm_mul, norm_inv, norm_pow, hw, one_pow, inv_one, one_mul,
48     Complex.norm_real, Real.norm_eq_abs, abs_of_pos (signedPositiveZero_pos (show 2 ≤ N by omega) _)] using hd
49 
50 /-- Exponential growth dominates any real power. The threshold is derived
51 from the actual denominator, not supplied as an analytic certificate. -/
52 theorem canonicalSignedDenominator_derivative_power_bound {N : ℕ} (hN : 3 ≤ N)
53     {q : ℕ} (hq : 0 < q) (t : ℝ) :
54     ∃ R : ℝ, 0 < R ∧ ∀ z : ℂ, R ≤ ‖z‖ → canonicalSignedDenominator N z = 0 →
55       1 / ‖deriv (canonicalSignedDenominator N) z‖ ^ q / ‖z‖ ^ t ≤ 1 / ‖z‖ ^ (2 : ℝ) := by
56   obtain ⟨A, hA, R0, hR0, hR0b⟩ := canonicalSignedDenominator_derivative_lower_bound hN
57   have hc : 0 < (q : ℝ) * Real.cos (Real.pi / N) := mul_pos (by exact_mod_cast hq) (signed_cosine_pos hN)
58   have he := (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (2 - t)
59     ((q : ℝ) * Real.cos (Real.pi / N)) hc).const_mul (1 / A ^ q)
60   simp only [mul_zero] at he
61   have hb := he.eventually (eventually_le_nhds (by norm_num : (0 : ℝ) < 1))
62   obtain ⟨R1, hR1⟩ := eventually_atTop.mp hb
63   refine ⟨max R0 R1, lt_of_lt_of_le hR0 (le_max_left _ _), ?_⟩
64   intro z hz hz0
65   have hzpos : 0 < ‖z‖ := lt_of_lt_of_le hR0 (le_trans (le_max_left _ _) hz)
66   have hd := hR0b z (le_trans (le_max_left _ _) hz) hz0
67   have hdpos : 0 < ‖deriv (canonicalSignedDenominator N) z‖ := lt_of_lt_of_le (by positivity) hd
68   have hdp := pow_le_pow_left₀ (by positivity : 0 ≤ A * Real.exp (Real.cos (Real.pi / N) * ‖z‖)) hd q
69   have hratio := hR1 ‖z‖ (le_trans (le_max_right _ _) hz)
70   have heq : (A * Real.exp (Real.cos (Real.pi / N) * ‖z‖)) ^ q =
71       A ^ q * Real.exp (((q : ℝ) * Real.cos (Real.pi / N)) * ‖z‖) := by
72     rw [mul_pow, ← Real.exp_nat_mul]
73     congr 2
74     ring
75   rw [heq] at hdp
76   have hinv := one_div_le_one_div_of_le (by positivity : 0 < A ^ q * Real.exp (((q : ℝ) * Real.cos (Real.pi / N)) * ‖z‖)) hdp
77   apply (div_le_div_of_nonneg_right hinv (Real.rpow_pos_of_pos hzpos t).le).trans
78   have hs : ‖z‖ ^ (2 - t) = ‖z‖ ^ (2 : ℝ) / ‖z‖ ^ t := Real.rpow_sub hzpos _ _
79   rw [hs] at hratio
80   rw [neg_mul, Real.exp_neg] at hratio
81   apply (le_div_iff₀ (Real.rpow_pos_of_pos hzpos 2)).mpr
82   convert hratio using 1
83   ring
84 
85 end
86 end Komorebi.PaperIV

Back to source controls