NormalizedGrowth.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.NormalizedEntire
6 import KomorebiPaperIV.WeightedGrowthSummability
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter Real
11 open scoped Topology
12 
13 theorem entireNormalizedSection_norm_le {N : ℕ} (hN : 0 < N) (j : ℕ) (w : ℂ) :
14     ‖entireNormalizedSection N j w‖ ≤ (j.factorial : ℝ) * exp (‖w‖ ^ (1 / (N : ℝ))) := by
15   let t := ‖w‖ ^ (1 / (N : ℝ))
16   have ht : 0 ≤ t := rpow_nonneg (norm_nonneg _) _
17   have htN : t ^ N = ‖w‖ := by
18     dsimp [t]; rw [one_div, rpow_inv_natCast_pow (norm_nonneg _) hN.ne']
19   have hi : Function.Injective (fun n : ℕ => N * n) := fun a b h => Nat.mul_left_cancel hN h
20   have hs := (Real.summable_pow_div_factorial t).comp_injective hi
21   have hle := (hasSum_entireNormalizedSection hN j w).norm_le_of_bounded
22     (hs.hasSum.mul_left (j.factorial : ℝ)) (fun n => ?_)
23   · apply hle.trans
24     apply mul_le_mul_of_nonneg_left _ (by positivity)
25     calc
26       _ ≤ ∑' n : ℕ, t ^ n / (n.factorial : ℝ) := tsum_comp_le_tsum_of_inj
27         (Real.summable_pow_div_factorial t) (fun n => by positivity) hi
28       _ = exp t := by simpa only [Real.exp_eq_exp_ℝ] using (NormedSpace.expSeries_div_hasSum_exp t).tsum_eq
29   · simp only [norm_mul, norm_div, norm_pow, Complex.norm_natCast, Function.comp_apply]
30     rw [← htN, pow_mul]
31     calc
32       _ = (j.factorial : ℝ) * (t ^ (N * n) / ((N * n + j).factorial : ℝ)) := by rw [pow_mul]; ring
33       _ ≤ (j.factorial : ℝ) * (t ^ (N * n) / ((N * n).factorial : ℝ)) := by
34         apply mul_le_mul_of_nonneg_left _ (by positivity)
35         apply div_le_div_of_nonneg_left (pow_nonneg ht _) (by positivity)
36         exact_mod_cast Nat.factorial_le (Nat.le_add_right (N * n) j)
37       _ = _ := by rw [pow_mul]
38 
39 def normalizedSectionGrowthConstant (j : ℕ) : ℝ := 1 + log (j.factorial : ℝ)
40 
41 theorem normalizedSectionGrowthConstant_pos (j : ℕ) : 0 < normalizedSectionGrowthConstant j := by
42   have hj : (1 : ℝ) ≤ j.factorial := by exact_mod_cast Nat.factorial_pos j
43   have := log_nonneg hj
44   unfold normalizedSectionGrowthConstant
45   linarith
46 
47 theorem entireNormalizedSection_disk_growth {N : ℕ} (hN : 0 < N) (j : ℕ)
48     (R : ℝ) (hR : 1 ≤ R) (w : ℂ) (hw : ‖w‖ ≤ R) :
49     ‖entireNormalizedSection N j w‖ ≤
50       exp (normalizedSectionGrowthConstant j * R ^ (1 / (N : ℝ))) := by
51   have hj : (1 : ℝ) ≤ j.factorial := by exact_mod_cast Nat.factorial_pos j
52   have hp : 0 ≤ 1 / (N : ℝ) := by positivity
53   have hpow : 1 ≤ R ^ (1 / (N : ℝ)) := one_le_rpow hR hp
54   apply (entireNormalizedSection_norm_le hN j w).trans
55   calc
56     _ ≤ (j.factorial : ℝ) * exp (R ^ (1 / (N : ℝ))) := mul_le_mul_of_nonneg_left
57       (exp_le_exp.mpr (rpow_le_rpow (norm_nonneg _) hw hp)) (by positivity)
58     _ = exp (log (j.factorial : ℝ) + R ^ (1 / (N : ℝ))) := by rw [exp_add, exp_log (by positivity)]
59     _ ≤ _ := by apply exp_le_exp.mpr; unfold normalizedSectionGrowthConstant; nlinarith [log_nonneg hj]
60 
61 theorem entireNormalizedSection_zeroPowerSummable {N : ℕ} (hN : 0 < N) (j : ℕ)
62     {q : ℝ} (hq : 1 / (N : ℝ) < q) : ZeroPowerSummable (entireNormalizedSection N j) q :=
63   entire_growth_zeroPowerSummable
64     (fun w => (analyticAt_entireNormalizedSection hN j w).differentiableAt)
65     (entireNormalizedSection_zero N j) (normalizedSectionGrowthConstant_pos j).le (by positivity)
66     hq (entireNormalizedSection_disk_growth hN j)
67 
68 end
69 end Komorebi.PaperIV

Back to source controls