NormalizedExactOrder.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.NormalizedOrder
6 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 theorem log_growth_ratio_of_polynomial_exp_bounds {M : ℝ → ℝ} {p B C : ℝ} (j : ℕ)
14     (hp : 0 < p) (hB : 0 < B) (hC : 0 < C)
15     (hb : ∀ᶠ R in atTop,
16       Real.exp (R ^ p) / (C * (R ^ p) ^ j) ≤ M R ∧ M R ≤ B * Real.exp (R ^ p)) :
17     Tendsto (fun R : ℝ => Real.log (M R) / R ^ p) atTop (𝓝 1) := by
18   have ht := tendsto_rpow_atTop hp
19   have hlog : Tendsto (fun R : ℝ => Real.log (R ^ p) / R ^ p) atTop (𝓝 0) := by
20     have h : Tendsto (fun x : ℝ => Real.log x / x) atTop (𝓝 0) := by
21       simpa using (isLittleO_log_rpow_atTop (by norm_num : (0 : ℝ) < 1)).tendsto_div_nhds_zero
22     exact h.comp ht
23   have hl : Tendsto (fun R : ℝ => 1 - Real.log C / R ^ p - (j : ℝ) * (Real.log (R ^ p) / R ^ p))
24       atTop (𝓝 1) := by
25     simpa using (tendsto_const_nhds.sub (tendsto_const_nhds.div_atTop ht)).sub (hlog.const_mul (j : ℝ))
26   have hu : Tendsto (fun R : ℝ => 1 + Real.log B / R ^ p) atTop (𝓝 1) := by
27     simpa using tendsto_const_nhds.add (tendsto_const_nhds.div_atTop ht)
28   apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hl hu
29   · filter_upwards [hb, eventually_gt_atTop (0 : ℝ)] with R hR hpos
30     have ht0 : 0 < R ^ p := Real.rpow_pos_of_pos hpos p
31     have hden : 0 < C * (R ^ p) ^ j := mul_pos hC (pow_pos ht0 j)
32     have h := Real.log_le_log (div_pos (Real.exp_pos _) hden) hR.1
33     rw [Real.log_div (Real.exp_ne_zero _) hden.ne', Real.log_exp,
34       Real.log_mul hC.ne' (pow_ne_zero j ht0.ne'), Real.log_pow] at h
35     have hh := div_le_div_of_nonneg_right h ht0.le
36     convert hh using 1
37     field_simp
38     ring
39   · filter_upwards [hb, eventually_gt_atTop (0 : ℝ)] with R hR hpos
40     have ht0 : 0 < R ^ p := Real.rpow_pos_of_pos hpos p
41     have hm : 0 < M R := (div_pos (Real.exp_pos _) (mul_pos hC (pow_pos ht0 j))).trans_le hR.1
42     have h := Real.log_le_log hm hR.2
43     rw [Real.log_mul hB.ne' (Real.exp_ne_zero _), Real.log_exp] at h
44     have hh := div_le_div_of_nonneg_right h ht0.le
45     convert hh using 1
46     field_simp
47     ring
48 
49 theorem entireTransfer_positive_ray_lower {N : ℕ} (hN : 0 < N) (j : ℕ)
50     {ω : ℂ} (hω : IsPrimitiveRoot ω N) :
51     ∀ᶠ r : ℝ in atTop, Real.exp r / (2 * N) ≤ ‖entireTransfer N j ω 1 r‖ := by
52   have ht := (entireTransfer_positive_ray hN j hω).norm
53   have hh := ht.eventually (eventually_ge_nhds (by norm_num : (1 / 2 : ℝ) < ‖(1 : ℂ)‖))
54   filter_upwards [hh] with r hr
55   have hn : (0 : ℝ) < N := by exact_mod_cast hN
56   simp only [norm_mul, Complex.norm_natCast, Complex.norm_exp, Complex.neg_re, Complex.ofReal_re] at hr
57   have he : ‖entireTransfer N j ω 1 r‖ =
58       (Real.exp r / N) * ((N : ℝ) * Real.exp (-r) * ‖entireTransfer N j ω 1 r‖) := by
59     rw [Real.exp_neg]
60     field_simp
61   rw [he]
62   have hmul := mul_le_mul_of_nonneg_left hr (le_of_lt (div_pos (Real.exp_pos r) hn))
63   convert! hmul using 1
64   ring
65 
66 theorem entireNormalizedSection_maximum_bounds {N j : ℕ} (hN : 0 < N) (hj : j < N) :
67     ∀ᶠ R : ℝ in atTop,
68       Real.exp (R ^ (1 / (N : ℝ))) / (2 * N * (R ^ (1 / (N : ℝ))) ^ j) ≤
69         diskMaximumModulus (entireNormalizedSection N j) R ∧
70       diskMaximumModulus (entireNormalizedSection N j) R ≤
71         (j.factorial : ℝ) * Real.exp (R ^ (1 / (N : ℝ))) := by
72   have hp : 0 < 1 / (N : ℝ) := by positivity
73   have ht := tendsto_rpow_atTop hp
74   have hc : Continuous (entireNormalizedSection N j) :=
75     (show Differentiable ℂ (entireNormalizedSection N j) from fun z =>
76       (analyticAt_entireNormalizedSection hN j z).differentiableAt).continuous
77   filter_upwards [ht.eventually (entireTransfer_positive_ray_lower hN j (canonicalPrimitiveRoot_isPrimitive hN)),
78     eventually_gt_atTop (0 : ℝ)] with R hlow hR
79   let t : ℝ := R ^ (1 / (N : ℝ))
80   have ht0 : 0 < t := Real.rpow_pos_of_pos hR _
81   have hpow : t ^ N = R := by simpa only [t, one_div] using Real.rpow_inv_natCast_pow hR.le hN.ne'
82   have he := congrArg norm (entireNormalizedSection_transfer hN hj
83     (canonicalPrimitiveRoot_isPrimitive hN) (t : ℂ))
84   simp only [norm_mul, norm_pow, Complex.norm_real, Real.norm_eq_abs, abs_of_pos ht0,
85     Complex.norm_natCast] at he
86   have hf : (1 : ℝ) ≤ j.factorial := by exact_mod_cast Nat.one_le_iff_ne_zero.mpr j.factorial_ne_zero
87   constructor
88   · have hcoeff : Real.exp t / (2 * N) ≤
89         ‖entireNormalizedSection N j ((t : ℂ) ^ N)‖ * t ^ j := by
90       rw [he]
91       exact hlow.trans (le_mul_of_one_le_left (norm_nonneg _) hf)
92     have hdiv := (div_le_iff₀ (pow_pos ht0 j)).mpr hcoeff
93     have hmax := norm_le_diskMaximumModulus hc (z := (t : ℂ) ^ N) (r := R)
94       (by simp [norm_pow, Complex.norm_real, Real.norm_eq_abs, abs_of_pos ht0, hpow])
95     have hdiv' : Real.exp t / (2 * N * t ^ j) ≤ ‖entireNormalizedSection N j ((t : ℂ) ^ N)‖ := by
96       simpa only [div_div] using hdiv
97     exact hdiv'.trans hmax
98   · apply diskMaximumModulus_le hR.le
99     intro w hw
100     exact (entireNormalizedSection_norm_le hN j w).trans
101       (mul_le_mul_of_nonneg_left (Real.exp_le_exp.mpr (Real.rpow_le_rpow (norm_nonneg _) hw hp.le)) (by positivity))
102 
103 theorem entireNormalizedSection_growth_limit {N j : ℕ} (hN : 0 < N) (hj : j < N) :
104     Tendsto (fun R : ℝ => Real.log (diskMaximumModulus (entireNormalizedSection N j) R) /
105       R ^ (1 / (N : ℝ))) atTop (𝓝 1) :=
106   log_growth_ratio_of_polynomial_exp_bounds j (by positivity) (by positivity) (by positivity)
107     (entireNormalizedSection_maximum_bounds hN hj)
108 
109 /-- Exact order, including the N=1 case; no coefficient-order formula is assumed. -/
110 theorem entireNormalizedSection_order_exact {N j : ℕ} (hN : 0 < N) (hj : j < N) :
111     entireGrowthOrder (entireNormalizedSection N j) = 1 / (N : ℝ) :=
112   (order_ratio_of_log_growth (entireNormalizedSection_growth_limit hN hj)).limsup_eq
113 
114 end
115 end Komorebi.PaperIV

Back to source controls