JensenZeroGrowth.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.EntireQuotientGrowth
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter Metric Real MeromorphicOn
10 open scoped Topology Classical
11 
12 theorem finite_sum_le_finsum_nonneg {α : Type*} {g : α → ℤ}
13     (hg : (Function.support g).Finite) (h0 : ∀ x, 0 ≤ g x) (S : Finset α) :
14     ∑ x ∈ S, g x ≤ ∑ᶠ x, g x := by
15   have he : (∑ᶠ x, g x) = ∑ x ∈ S ∪ hg.toFinset, g x := by
16     apply finsum_eq_sum_of_support_subset
17     intro x hx
18     exact Finset.mem_union_right S (hg.mem_toFinset.mpr hx)
19   rw [he]
20   exact Finset.sum_le_sum_of_subset_of_nonneg Finset.subset_union_left (fun x _ _ => h0 x)
21 
22 theorem entire_divisor_eq_orderNat {f : ℂ → ℂ} (hf : Differentiable ℂ f)
23     (h0 : f 0 ≠ 0) {R : ℝ} {z : ℂ} (hz : ‖z‖ ≤ R) :
24     divisor f (closedBall 0 R) z = (analyticOrderNatAt f z : ℤ) := by
25   have ha : AnalyticOnNhd ℂ f (closedBall 0 R) := fun w _ => hf.analyticAt w
26   rw [ha.divisor_apply (by simpa using hz),
27     ← Nat.cast_analyticOrderNatAt (entire_analyticOrderAt_ne_top (fun w => hf.analyticAt w) h0 z),
28     ENat.map_natCast]
29   rfl
30 
31 theorem entire_zero_finite_weight_growth {f : ℂ → ℂ} (hf : Differentiable ℂ f)
32     (h0 : f 0 = 1) {C p : ℝ} (hC : 0 ≤ C)
33     (hgrowth : ∀ R : ℝ, 1 ≤ R → ∀ z : ℂ, ‖z‖ ≤ R → ‖f z‖ ≤ exp (C * R ^ p))
34     {R : ℝ} (hR : 1 ≤ R) (S : Finset ℂ) (hS : ∀ z ∈ S, ‖z‖ ≤ R) :
35     (∑ z ∈ S, (analyticOrderNatAt f z : ℝ)) ≤ (C * (2 : ℝ) ^ p / log 2) * R ^ p := by
36   have hr : 0 < R := by linarith
37   have ha : AnalyticOnNhd ℂ f (closedBall 0 |2 * R|) := fun z _ => hf.analyticAt z
38   have hne : f 0 ≠ 0 := by rw [h0]; exact one_ne_zero
39   have hj := ha.sum_divisor_le (r := R) (M := exp (C * (2 * R) ^ p))
40     (by simpa only [abs_of_pos hr] using hr)
41     (by rw [abs_of_pos hr, abs_of_pos (by positivity : 0 < 2 * R)]; linarith)
42     (Real.one_le_exp_iff.mpr (by positivity)) hne (fun z hz => ?_)
43   · have haR : AnalyticOnNhd ℂ f (closedBall 0 R) := fun z _ => hf.analyticAt z
44     have hs : (∑ z ∈ S, (analyticOrderNatAt f z : ℤ)) ≤ ∑ᶠ z, divisor f (closedBall 0 R) z := by
45       calc
46         _ = ∑ z ∈ S, divisor f (closedBall 0 R) z :=
47           Finset.sum_congr rfl (fun z hz => (entire_divisor_eq_orderNat hf hne (hS z hz)).symm)
48         _ ≤ _ := finite_sum_le_finsum_nonneg
49           ((divisor f (closedBall 0 R)).finiteSupport (isCompact_closedBall ..))
50           (fun z => haR.divisor_nonneg z) S
51     have hsR : (Int.cast (∑ z ∈ S, (analyticOrderNatAt f z : ℤ)) : ℝ) ≤
52         Int.cast (∑ᶠ z, divisor f (closedBall 0 R) z) := Int.cast_le.mpr hs
53     simp only [Int.cast_sum, Int.cast_natCast] at hsR
54     rw [abs_of_pos hr, h0, norm_one, div_one, log_exp,
55       mul_div_cancel_right₀ (2 : ℝ) hr.ne', Real.mul_rpow (by norm_num) hr.le] at hj
56     calc
57       _ ≤ C * ((2 : ℝ) ^ p * R ^ p) / log 2 := hsR.trans hj
58       _ = _ := by ring
59   · rw [abs_of_pos (by positivity : 0 < 2 * R), mem_sphere_zero_iff_norm] at hz
60     exact hgrowth (2 * R) (by linarith) z hz.le
61 
62 theorem entire_zero_subtype_weight_growth {f : ℂ → ℂ} (hf : Differentiable ℂ f)
63     (h0 : f 0 = 1) {C p : ℝ} (hC : 0 ≤ C)
64     (hgrowth : ∀ R : ℝ, 1 ≤ R → ∀ z : ℂ, ‖z‖ ≤ R → ‖f z‖ ≤ exp (C * R ^ p))
65     {R : ℝ} (hR : 1 ≤ R) (S : Finset {z : ℂ // f z = 0}) (hS : ∀ z ∈ S, ‖(z : ℂ)‖ ≤ R) :
66     (∑ z ∈ S, (analyticOrderNatAt f z : ℝ)) ≤ (C * (2 : ℝ) ^ p / log 2) * R ^ p := by
67   let e : {z : ℂ // f z = 0} ↪ ℂ := ⟨Subtype.val, Subtype.val_injective⟩
68   have h := entire_zero_finite_weight_growth hf h0 hC hgrowth hR (S.map e) (by
69     intro z hz
70     obtain ⟨u, hu, rfl⟩ := Finset.mem_map.mp hz
71     exact hS u hu)
72   simpa only [Finset.sum_map, e, Function.Embedding.coeFn_mk] using h
73 
74 theorem entire_zero_bounded_finite {f : ℂ → ℂ} (hf : Differentiable ℂ f)
75     (h0 : f 0 ≠ 0) (R : ℝ) :
76     {z : {z : ℂ // f z = 0} | ‖(z : ℂ)‖ ≤ R}.Finite := by
77   have ha : AnalyticOnNhd ℂ f univ := fun z _ => hf.analyticAt z
78   have hn : ¬ EqOn f 0 univ := fun h => h0 (h (mem_univ (0 : ℂ)))
79   have he := (ha.eqOn_zero_or_eventually_ne_zero_of_preconnected isPreconnected_univ).resolve_left hn
80   have hk := (codiscreteWithin_mono (subset_univ (closedBall (0 : ℂ) R))) he
81   have hc := (isCompact_closedBall (0 : ℂ) R).finite_sdiff_of_mem_codiscreteWithin hk
82   apply Set.Finite.of_finite_image (f := fun z : {z : ℂ // f z = 0} => (z : ℂ)) _ Subtype.val_injective.injOn
83   exact hc.subset (by rintro z ⟨u, hu, rfl⟩; exact ⟨by simpa using hu, fun hn => hn u.property⟩)
84 
85 end
86 end Komorebi.PaperIV

Back to source controls