CanonicalProductGrowth.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.FullCanonicalProduct
6 import Mathlib.Analysis.MeanInequalitiesPow
7 import Mathlib.Analysis.Complex.Polynomial.Basic
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter
12 open scoped Topology
13 
14 theorem log_one_add_le_rpow_div {x s : ℝ} (hx : 0 ≤ x) (hs : 0 < s) (hs1 : s ≤ 1) :
15     Real.log (1 + x) ≤ x ^ s / s := by
16   have h := Real.log_le_sub_one_of_pos (Real.rpow_pos_of_pos (by linarith : 0 < 1 + x) s)
17   rw [Real.log_rpow (by linarith)] at h
18   have hp := Real.rpow_add_le_add_rpow (a := 1) (b := x) zero_le_one hx hs.le hs1
19   rw [Real.one_rpow] at hp
20   apply (le_div_iff₀ hs).mpr
21   nlinarith
22 
23 theorem zeroMultiplicity_reciprocal_rpow_summable {f : ℂ → ℂ} {s : ℝ}
24     (hf : ZeroPowerSummable f s) :
25     Summable (fun i : ZeroMultiplicityIndex f => 1 / ‖indexedZero i‖ ^ s) := by
26   apply (summable_sigma_of_nonneg (fun i : ZeroMultiplicityIndex f => by positivity)).mpr
27   constructor
28   · intro z
29     exact (hasSum_fintype _).summable
30   · simpa only [indexedZero, tsum_fintype, Finset.sum_const, Finset.card_univ,
31       Fintype.card_fin, nsmul_eq_mul, mul_one_div, ZeroPowerSummable] using hf
32 
33 def reciprocalPowerMass (f : ℂ → ℂ) (s : ℝ) : ℝ :=
34   ∑' i : ZeroMultiplicityIndex f, 1 / ‖indexedZero i‖ ^ s
35 
36 theorem reciprocalPowerMass_nonneg (f : ℂ → ℂ) (s : ℝ) : 0 ≤ reciprocalPowerMass f s :=
37   tsum_nonneg (fun _ => by positivity)
38 
39 /-- A genus-zero product inherits every summable reciprocal exponent below one. -/
40 theorem fullCanonicalProduct_growth {f : ℂ → ℂ} {s : ℝ}
41     (hf : ZeroPowerSummable f 1) (hfs : ZeroPowerSummable f s)
42     (hs : 0 < s) (hs1 : s ≤ 1) (w : ℂ) :
43     ‖fullCanonicalProduct f w‖ ≤
44       Real.exp ((reciprocalPowerMass f s / s) * ‖w‖ ^ s) := by
45   have hm := zeroMultiplicity_reciprocal_rpow_summable hfs
46   have hsum : Summable (fun i : ZeroMultiplicityIndex f => ‖w / indexedZero i‖ ^ s) := by
47     simpa only [norm_div, Real.div_rpow (norm_nonneg _) (norm_nonneg _), mul_one_div] using
48       hm.mul_left (‖w‖ ^ s)
49   have he : (∑' i : ZeroMultiplicityIndex f, ‖w / indexedZero i‖ ^ s) =
50       ‖w‖ ^ s * reciprocalPowerMass f s := by
51     unfold reciprocalPowerMass
52     rw [← tsum_mul_left]
53     apply tsum_congr
54     intro i
55     rw [norm_div, Real.div_rpow (norm_nonneg _) (norm_nonneg _), mul_one_div]
56   have ht := (continuous_norm.tendsto (fullCanonicalProduct f w)).comp
57     (fullCanonicalProduct_multipliable hf w).hasProd
58   apply le_of_tendsto ht
59   apply Eventually.of_forall
60   intro S
61   calc
62     ‖∏ i ∈ S, (1 - w / indexedZero i)‖ ≤ ∏ i ∈ S, Real.exp (‖w / indexedZero i‖ ^ s / s) := by
63       rw [norm_prod]
64       apply Finset.prod_le_prod (fun _ _ => norm_nonneg _)
65       intro i _
66       apply (norm_sub_le _ _).trans
67       rw [norm_one]
68       exact (Real.log_le_iff_le_exp (by positivity)).mp
69         (log_one_add_le_rpow_div (norm_nonneg _) hs hs1)
70     _ = Real.exp ((∑ i ∈ S, ‖w / indexedZero i‖ ^ s) / s) := by
71       rw [← Real.exp_sum, Finset.sum_div]
72     _ ≤ Real.exp ((∑' i : ZeroMultiplicityIndex f, ‖w / indexedZero i‖ ^ s) / s) := by
73       apply Real.exp_le_exp.mpr
74       apply div_le_div_of_nonneg_right _ hs.le
75       exact hsum.sum_le_tsum S (fun _ _ => Real.rpow_nonneg (norm_nonneg _) _)
76     _ = Real.exp ((reciprocalPowerMass f s / s) * ‖w‖ ^ s) := by
77       rw [he]
78       congr 1
79       ring
80 
81 /-- The reduced denominator has the explicit order-1/N upper bound. -/
82 theorem entireReducedDenominator_norm_le {N : ℕ} (hN : 0 < N) (w : ℂ) :
83     ‖entireReducedDenominator N w‖ ≤ Real.exp (‖w‖ ^ (1 / (N : ℝ))) := by
84   obtain ⟨z, rfl⟩ := IsAlgClosed.exists_pow_nat_eq w hN
85   rw [← canonicalSignedDenominator_eq_reduced_power hN, norm_pow, one_div,
86     Real.pow_rpow_inv_natCast (norm_nonneg z) hN.ne']
87   exact norm_entireSigned_zero_le hN (canonicalPrimitiveRoot_isPrimitive hN)
88     (canonicalSignedRoot_pow hN) z
89 
90 /-- One fixed sublinear exponent works for every N ≥ 2, for both entire factors. -/
91 theorem entireReducedDenominator_and_product_growth {N : ℕ} (hN : 2 ≤ N) :
92     ∃ C : ℝ, 0 ≤ C ∧ ∀ R : ℝ, 1 ≤ R → ∀ w : ℂ, ‖w‖ ≤ R →
93       ‖entireReducedDenominator N w‖ ≤ Real.exp (C * R ^ (3 / 4 : ℝ)) ∧
94       ‖fullCanonicalProduct (entireReducedDenominator N) w‖ ≤ Real.exp (C * R ^ (3 / 4 : ℝ)) := by
95   have hN0 : 0 < N := by omega
96   have hn : (2 : ℝ) ≤ N := by exact_mod_cast hN
97   have hn0 : (0 : ℝ) < N := by positivity
98   have he : 1 / (N : ℝ) < (3 / 4 : ℝ) := (div_lt_iff₀ hn0).mpr (by linarith)
99   have hs := (entireReducedDenominator_zero_power_summable_iff hN (3 / 4)).mpr he
100   let B := reciprocalPowerMass (entireReducedDenominator N) (3 / 4) / (3 / 4)
101   have hB : 0 ≤ B := div_nonneg (reciprocalPowerMass_nonneg _ _) (by norm_num)
102   refine ⟨1 + B, by positivity, fun R hR w hw => ?_⟩
103   have hRp : 0 ≤ R ^ (3 / 4 : ℝ) := Real.rpow_nonneg (by linarith) _
104   constructor
105   · apply (entireReducedDenominator_norm_le hN0 w).trans
106     apply Real.exp_le_exp.mpr
107     calc
108       ‖w‖ ^ (1 / (N : ℝ)) ≤ R ^ (1 / (N : ℝ)) :=
109         Real.rpow_le_rpow (norm_nonneg _) hw (by positivity)
110       _ ≤ R ^ (3 / 4 : ℝ) := Real.rpow_le_rpow_of_exponent_le hR he.le
111       _ ≤ (1 + B) * R ^ (3 / 4 : ℝ) := by nlinarith
112   · apply (fullCanonicalProduct_growth (entireReducedDenominator_reciprocal_zeros_summable hN)
113       hs (by norm_num) (by norm_num) w).trans
114     apply Real.exp_le_exp.mpr
115     change B * ‖w‖ ^ (3 / 4 : ℝ) ≤ _
116     calc
117       _ ≤ B * R ^ (3 / 4 : ℝ) := mul_le_mul_of_nonneg_left
118         (Real.rpow_le_rpow (norm_nonneg _) hw (by norm_num)) hB
119       _ ≤ (1 + B) * R ^ (3 / 4 : ℝ) := by nlinarith
120 
121 end
122 end Komorebi.PaperIV

Back to source controls