WeightedGrowthSummability.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.JensenZeroGrowth
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Real
10 open scoped Classical
11 set_option maxHeartbeats 800000
12 
13 /-- Weighted counting bounds imply convergence above the counting exponent. -/
14 theorem weighted_growth_summable_large {ι : Type*} {x w : ι → ℝ} {C p q : ℝ}
15     (hx : ∀ i, 1 ≤ x i) (hw : ∀ i, 0 ≤ w i) (hC : 0 ≤ C)
16     (hp : 0 ≤ p) (hpq : p < q)
17     (hg : ∀ R : ℝ, 1 ≤ R → ∀ S : Finset ι, (∀ i ∈ S, x i ≤ R) →
18       ∑ i ∈ S, w i ≤ C * R ^ p) : Summable (fun i => w i / (x i) ^ q) := by
19   let shell : ι → ℕ := fun i => ⌊log (x i)⌋₊
20   let g : ℕ → ℝ := fun n => (C * exp p) * exp (p - q) ^ n
21   have hgs : Summable g := (summable_geometric_of_lt_one (exp_pos _).le
22     (exp_lt_one_iff.mpr (sub_neg.mpr hpq))).mul_left (C * exp p)
23   have hg0 : ∀ n, 0 ≤ g n := fun n => by dsimp [g]; positivity
24   apply summable_of_sum_le (fun i => div_nonneg (hw i) (rpow_nonneg (by linarith [hx i]) _))
25     (c := ∑' n, g n)
26   intro S
27   have hfiber (n : ℕ) : ∑ i ∈ S.filter (fun i => shell i = n), w i / (x i) ^ q ≤ g n := by
28     let T := S.filter (fun i => shell i = n)
29     have hlog (i : ι) (hi : i ∈ T) : (n : ℝ) ≤ log (x i) ∧ log (x i) < (n : ℝ) + 1 := by
30       have he : shell i = n := (Finset.mem_filter.mp hi).2
31       constructor
32       · simpa only [shell, he] using Nat.floor_le (log_nonneg (hx i))
33       · simpa only [shell, he] using Nat.lt_floor_add_one (log (x i))
34     have hupper : ∀ i ∈ T, x i ≤ exp ((n : ℝ) + 1) := by
35       intro i hi
36       rw [← exp_log (by linarith [hx i] : 0 < x i)]
37       exact (exp_lt_exp.mpr (hlog i hi).2).le
38     have hsum := hg (exp ((n : ℝ) + 1)) (one_le_exp (by positivity)) T hupper
39     calc
40       _ ≤ ∑ i ∈ T, w i * exp (-(q * (n : ℝ))) := by
41         apply Finset.sum_le_sum
42         intro i hi
43         rw [rpow_def_of_pos (by linarith [hx i] : 0 < x i), div_eq_mul_inv, ← exp_neg]
44         apply mul_le_mul_of_nonneg_left _ (hw i)
45         apply exp_le_exp.mpr
46         nlinarith [(hlog i hi).1]
47       _ = (∑ i ∈ T, w i) * exp (-(q * (n : ℝ))) := (Finset.sum_mul ..).symm
48       _ ≤ (C * exp ((n : ℝ) + 1) ^ p) * exp (-(q * (n : ℝ))) :=
49         mul_le_mul_of_nonneg_right hsum (exp_pos _).le
50       _ = g n := by
51         dsimp [g]
52         rw [← exp_mul, mul_assoc, ← exp_add, ← exp_nat_mul, mul_assoc, ← exp_add]
53         congr 2
54         ring
55   calc
56     _ = ∑ n ∈ S.image shell, ∑ i ∈ S.filter (fun i => shell i = n), w i / (x i) ^ q :=
57       (Finset.sum_fiberwise_of_maps_to (fun i hi => Finset.mem_image_of_mem shell hi) _).symm
58     _ ≤ ∑ n ∈ S.image shell, g n := Finset.sum_le_sum (fun n _ => hfiber n)
59     _ ≤ ∑' n, g n := hgs.sum_le_tsum _ (fun n _ => hg0 n)
60 
61 theorem weighted_growth_summable {ι : Type*} {x w : ι → ℝ} {C p q : ℝ}
62     (hw : ∀ i, 0 ≤ w i) (hC : 0 ≤ C) (hp : 0 ≤ p) (hpq : p < q)
63     (hsmall : {i | x i < 1}.Finite)
64     (hg : ∀ R : ℝ, 1 ≤ R → ∀ S : Finset ι, (∀ i ∈ S, x i ≤ R) →
65       ∑ i ∈ S, w i ≤ C * R ^ p) : Summable (fun i => w i / (x i) ^ q) := by
66   apply (summable_subtype_and_compl (s := {i | x i < 1})).mp
67   refine ⟨hsmall.summable (fun i => w i / (x i) ^ q), ?_⟩
68   apply weighted_growth_summable_large (ι := {i // ¬ x i < 1})
69     (x := fun i => x i.val) (w := fun i => w i.val) (C := C) (p := p)
70     (fun i => le_of_not_gt i.property) (fun i => hw i) hC hp hpq
71   intro R hR S hS
72   let e : {i // ¬ x i < 1} ↪ ι := ⟨Subtype.val, Subtype.val_injective⟩
73   have h := hg R hR (S.map e) (by
74     intro i hi
75     obtain ⟨v, hv, rfl⟩ := Finset.mem_map.mp hi
76     exact hS v hv)
77   simpa only [Finset.sum_map, e, Function.Embedding.coeFn_mk] using h
78 
79 theorem entire_growth_zeroPowerSummable {f : ℂ → ℂ} (hf : Differentiable ℂ f)
80     (h0 : f 0 = 1) {C p q : ℝ} (hC : 0 ≤ C) (hp : 0 ≤ p) (hpq : p < q)
81     (hg : ∀ R : ℝ, 1 ≤ R → ∀ z : ℂ, ‖z‖ ≤ R → ‖f z‖ ≤ exp (C * R ^ p)) :
82     ZeroPowerSummable f q := by
83   have hne : f 0 ≠ 0 := by simp [h0]
84   apply weighted_growth_summable (C := C * 2 ^ p / log 2) (p := p)
85   · intro z; positivity
86   · exact div_nonneg (mul_nonneg hC (rpow_nonneg (by norm_num) _)) (log_pos (by norm_num)).le
87   · exact hp
88   · exact hpq
89   · exact (entire_zero_bounded_finite hf hne 1).subset (fun z hz => show ‖(z : ℂ)‖ ≤ 1 from le_of_lt hz)
90   · intro R hR S hS
91     exact entire_zero_subtype_weight_growth hf h0 hC hg hR S hS
92 
93 end
94 end Komorebi.PaperIV

Back to source controls