SharpGrowth.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.DominantExponential
6 import KomorebiPaperIV.CanonicalProductGrowth
7 import Mathlib.Topology.Order.LiminfLimsup
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter Metric
12 open scoped Topology
13 
14 /-- Maximum modulus on the closed disk. -/
15 def diskMaximumModulus (f : ℂ → ℂ) (r : ℝ) : ℝ :=
16   sSup ((fun z => ‖f z‖) '' closedBall 0 r)
17 
18 /-- Growth order in the usual maximum-modulus normalization. -/
19 def entireGrowthOrder (f : ℂ → ℂ) : ℝ :=
20   limsup (fun r : ℝ => Real.log (Real.log (diskMaximumModulus f r)) / Real.log r) atTop
21 
22 /-- Exponential type for functions of order one. -/
23 def entireExponentialType (f : ℂ → ℂ) : ℝ :=
24   limsup (fun r : ℝ => Real.log (diskMaximumModulus f r) / r) atTop
25 
26 theorem norm_le_diskMaximumModulus {f : ℂ → ℂ} (hf : Continuous f)
27     {z : ℂ} {r : ℝ} (hz : ‖z‖ ≤ r) : ‖f z‖ ≤ diskMaximumModulus f r :=
28   le_csSup ((isCompact_closedBall (0 : ℂ) r).bddAbove_image hf.norm.continuousOn)
29     (mem_image_of_mem _ (mem_closedBall_zero_iff.mpr hz))
30 
31 theorem diskMaximumModulus_le {f : ℂ → ℂ} {r B : ℝ} (hr : 0 ≤ r)
32     (hf : ∀ z : ℂ, ‖z‖ ≤ r → ‖f z‖ ≤ B) : diskMaximumModulus f r ≤ B := by
33   apply csSup_le
34   · exact ⟨‖f 0‖, mem_image_of_mem _ (mem_closedBall_self hr)⟩
35   · rintro _ ⟨z, hz, rfl⟩
36     exact hf z (mem_closedBall_zero_iff.mp hz)
37 
38 /-- Sharp logarithmic growth follows from matching exponential bounds. -/
39 theorem log_growth_ratio_of_exp_bounds {M : ℝ → ℝ} {p C : ℝ}
40     (hp : 0 < p) (hC : 0 < C)
41     (hb : ∀ᶠ r in atTop, Real.exp (r ^ p) / C ≤ M r ∧ M r ≤ Real.exp (r ^ p)) :
42     Tendsto (fun r : ℝ => Real.log (M r) / r ^ p) atTop (𝓝 1) := by
43   have hl : Tendsto (fun r : ℝ => 1 - Real.log C / r ^ p) atTop (𝓝 1) := by
44     simpa using tendsto_const_nhds.sub (tendsto_const_nhds.div_atTop (tendsto_rpow_atTop hp))
45   apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hl tendsto_const_nhds
46   · filter_upwards [hb, eventually_gt_atTop (0 : ℝ)] with r hr hpos
47     have hm : 0 < M r := (div_pos (Real.exp_pos _) hC).trans_le hr.1
48     have h := Real.log_le_log (div_pos (Real.exp_pos _) hC) hr.1
49     rw [Real.log_div (Real.exp_ne_zero _) hC.ne', Real.log_exp] at h
50     apply (le_div_iff₀ (Real.rpow_pos_of_pos hpos _)).mpr
51     have hne : r ^ p ≠ 0 := (Real.rpow_pos_of_pos hpos p).ne'
52     field_simp
53     nlinarith
54   · filter_upwards [hb, eventually_gt_atTop (0 : ℝ)] with r hr hpos
55     have hm : 0 < M r := (div_pos (Real.exp_pos _) hC).trans_le hr.1
56     apply (div_le_one (Real.rpow_pos_of_pos hpos _)).mpr
57     exact (Real.log_le_iff_le_exp hm).mpr hr.2
58 
59 /-- The logarithmic ratio limit also proves the exact growth-order limit. -/
60 theorem order_ratio_of_log_growth {M : ℝ → ℝ} {p : ℝ}
61     (h : Tendsto (fun r : ℝ => Real.log (M r) / r ^ p) atTop (𝓝 1)) :
62     Tendsto (fun r : ℝ => Real.log (Real.log (M r)) / Real.log r) atTop (𝓝 p) := by
63   have hlog : Tendsto (fun r : ℝ => Real.log (Real.log (M r) / r ^ p)) atTop (𝓝 0) := by
64     simpa only [Real.log_one] using! (Real.continuousAt_log (by norm_num : (1 : ℝ) ≠ 0)).tendsto.comp h
65   have hlim : Tendsto (fun r : ℝ => p + Real.log (Real.log (M r) / r ^ p) / Real.log r) atTop (𝓝 p) := by
66     simpa using tendsto_const_nhds.add (hlog.div_atTop Real.tendsto_log_atTop)
67   apply hlim.congr'
68   filter_upwards [eventually_gt_atTop (1 : ℝ), h.eventually (eventually_gt_nhds (by norm_num : (0 : ℝ) < 1))] with r hr hratio
69   have hr0 : 0 < r := by linarith
70   have hpow : 0 < r ^ p := Real.rpow_pos_of_pos hr0 p
71   have hm : 0 < Real.log (M r) := (div_pos_iff_of_pos_right hpow).mp hratio
72   rw [Real.log_div hm.ne' hpow.ne', Real.log_rpow hr0]
73   field_simp [(Real.log_pos hr).ne']
74   ring
75 
76 /-- A concrete lower bound on a vertex-facing ray, derived from the proved limit. -/
77 theorem canonicalSignedDenominator_ray_lower {N : ℕ} (hN : 0 < N) :
78     ∀ᶠ r : ℝ in atTop,
79       Real.exp r / (2 * N) ≤
80         ‖canonicalSignedDenominator N ((r : ℂ) * star (canonicalSignedVertex N 0))‖ := by
81   have ht := (canonicalSignedDenominator_dominant_ray hN hN).norm
82   have hh : ∀ᶠ r : ℝ in atTop,
83       (1 / 2 : ℝ) ≤ ‖(N : ℂ) * Complex.exp (-(r : ℂ)) *
84         canonicalSignedDenominator N ((r : ℂ) * star (canonicalSignedVertex N 0))‖ := by
85     exact (ht.eventually (eventually_ge_nhds (by norm_num : (1 / 2 : ℝ) < ‖(1 : ℂ)‖)))
86   filter_upwards [hh] with r hr
87   have hn : (0 : ℝ) < N := by exact_mod_cast hN
88   simp only [norm_mul, Complex.norm_natCast, Complex.norm_exp, Complex.neg_re, Complex.ofReal_re] at hr
89   have he : ‖canonicalSignedDenominator N ((r : ℂ) * star (canonicalSignedVertex N 0))‖ =
90       (Real.exp r / N) * ((N : ℝ) * Real.exp (-r) *
91         ‖canonicalSignedDenominator N ((r : ℂ) * star (canonicalSignedVertex N 0))‖) := by
92     rw [Real.exp_neg]
93     field_simp
94   rw [he]
95   have hmul := mul_le_mul_of_nonneg_left hr (le_of_lt (div_pos (Real.exp_pos r) hn))
96   convert! hmul using 1
97   ring
98 
99 /-- The actual denominator maximum has matching exponential bounds. -/
100 theorem canonicalSignedDenominator_maximum_bounds {N : ℕ} (hN : 0 < N) :
101     ∀ᶠ r : ℝ in atTop, Real.exp r / (2 * N) ≤ diskMaximumModulus (canonicalSignedDenominator N) r ∧
102       diskMaximumModulus (canonicalSignedDenominator N) r ≤ Real.exp r := by
103   have hc : Continuous (canonicalSignedDenominator N) :=
104     (show Differentiable ℂ (canonicalSignedDenominator N) from fun z =>
105       (analyticAt_entireSigned N 0 (canonicalPrimitiveRoot N) (canonicalSignedRoot N) z).differentiableAt).continuous
106   filter_upwards [canonicalSignedDenominator_ray_lower hN, eventually_ge_atTop (0 : ℝ)] with r hr hr0
107   constructor
108   · exact hr.trans (norm_le_diskMaximumModulus hc (by simp [norm_canonicalSignedVertex, abs_of_nonneg hr0]))
109   · exact diskMaximumModulus_le hr0 (fun z hz =>
110       (norm_entireSigned_zero_le hN (canonicalPrimitiveRoot_isPrimitive hN) (canonicalSignedRoot_pow hN) z).trans
111         (Real.exp_le_exp.mpr hz))
112 
113 theorem canonicalSignedDenominator_type_limit {N : ℕ} (hN : 0 < N) :
114     Tendsto (fun r : ℝ => Real.log (diskMaximumModulus (canonicalSignedDenominator N) r) / r) atTop (𝓝 1) := by
115   simpa using log_growth_ratio_of_exp_bounds (p := 1) (by norm_num)
116     (show (0 : ℝ) < 2 * N by positivity)
117     (by simpa using canonicalSignedDenominator_maximum_bounds hN)
118 
119 theorem canonicalSignedDenominator_order_limit {N : ℕ} (hN : 0 < N) :
120     Tendsto (fun r : ℝ => Real.log (Real.log (diskMaximumModulus (canonicalSignedDenominator N) r)) / Real.log r)
121       atTop (𝓝 1) :=
122   order_ratio_of_log_growth (by simpa using canonicalSignedDenominator_type_limit hN)
123 
124 theorem canonicalSignedDenominator_order_one {N : ℕ} (hN : 0 < N) :
125     entireGrowthOrder (canonicalSignedDenominator N) = 1 :=
126   (canonicalSignedDenominator_order_limit hN).limsup_eq
127 
128 theorem canonicalSignedDenominator_type_one {N : ℕ} (hN : 0 < N) :
129     entireExponentialType (canonicalSignedDenominator N) = 1 :=
130   (canonicalSignedDenominator_type_limit hN).limsup_eq
131 
132 /-- Passing to w=z^N transfers the sharp bound to the reduced entire function. -/
133 theorem entireReducedDenominator_maximum_bounds {N : ℕ} (hN : 0 < N) :
134     ∀ᶠ r : ℝ in atTop,
135       Real.exp (r ^ (1 / (N : ℝ))) / (2 * N) ≤ diskMaximumModulus (entireReducedDenominator N) r ∧
136       diskMaximumModulus (entireReducedDenominator N) r ≤ Real.exp (r ^ (1 / (N : ℝ))) := by
137   have hn : (0 : ℝ) < N := by exact_mod_cast hN
138   have hp : 0 < 1 / (N : ℝ) := one_div_pos.mpr hn
139   have ht := tendsto_rpow_atTop hp
140   have hc : Continuous (entireReducedDenominator N) :=
141     (show Differentiable ℂ (entireReducedDenominator N) from fun z =>
142       (analyticAt_entireReducedDenominator hN z).differentiableAt).continuous
143   filter_upwards [ht.eventually (canonicalSignedDenominator_ray_lower hN),
144     eventually_ge_atTop (0 : ℝ)] with r hr hr0
145   let z : ℂ := (r ^ (1 / (N : ℝ)) : ℝ) * star (canonicalSignedVertex N 0)
146   have hz : ‖z‖ = r ^ (1 / (N : ℝ)) := by
147     simp [z, norm_canonicalSignedVertex, abs_of_nonneg (Real.rpow_nonneg hr0 _)]
148   have hw : ‖z ^ N‖ = r := by
149     rw [norm_pow, hz, one_div, Real.rpow_inv_natCast_pow hr0 hN.ne']
150   constructor
151   · have hlow := norm_le_diskMaximumModulus hc (le_of_eq hw)
152     rw [← canonicalSignedDenominator_eq_reduced_power hN] at hlow
153     exact hr.trans hlow
154   · apply diskMaximumModulus_le hr0
155     intro w hw
156     exact (entireReducedDenominator_norm_le hN w).trans
157       (Real.exp_le_exp.mpr (Real.rpow_le_rpow (norm_nonneg _) hw hp.le))
158 
159 theorem entireReducedDenominator_growth_limit {N : ℕ} (hN : 0 < N) :
160     Tendsto (fun r : ℝ => Real.log (diskMaximumModulus (entireReducedDenominator N) r) / r ^ (1 / (N : ℝ)))
161       atTop (𝓝 1) :=
162   log_growth_ratio_of_exp_bounds (by positivity) (by positivity) (entireReducedDenominator_maximum_bounds hN)
163 
164 theorem entireReducedDenominator_order_limit {N : ℕ} (hN : 0 < N) :
165     Tendsto (fun r : ℝ => Real.log (Real.log (diskMaximumModulus (entireReducedDenominator N) r)) / Real.log r)
166       atTop (𝓝 (1 / (N : ℝ))) :=
167   order_ratio_of_log_growth (entireReducedDenominator_growth_limit hN)
168 
169 /-- The complete order assertion of Proposition 11.2. -/
170 theorem entireReducedDenominator_order_exact {N : ℕ} (hN : 0 < N) :
171     entireGrowthOrder (entireReducedDenominator N) = 1 / (N : ℝ) :=
172   (entireReducedDenominator_order_limit hN).limsup_eq
173 
174 end
175 end Komorebi.PaperIV

Back to source controls