SublinearHadamard.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.WeightedGrowthSummability
6 import KomorebiPaperIV.CanonicalProductGrowth
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 /-- A normalized entire function with sublinear power growth equals the product
14 over its actual zeros, with multiplicities. Convergence is proved from growth. -/
15 theorem entire_sublinear_growth_hadamard {f : ℂ → ℂ} (hf : Differentiable ℂ f)
16     (h0 : f 0 = 1) {C p : ℝ} (hC : 0 ≤ C) (hp : 0 ≤ p) (hp1 : p < 1)
17     (hgrowth : ∀ R : ℝ, 1 ≤ R → ∀ z : ℂ, ‖z‖ ≤ R → ‖f z‖ ≤ Real.exp (C * R ^ p)) :
18     f = fullCanonicalProduct f := by
19   let q : ℝ := (p + 1) / 2
20   have hq : 0 < q := by dsimp [q]; linarith
21   have hpq : p < q := by dsimp [q]; linarith
22   have hq1 : q < 1 := by dsimp [q]; linarith
23   have hs := entire_growth_zeroPowerSummable hf h0 hC hp hp1 hgrowth
24   have hsq := entire_growth_zeroPowerSummable hf h0 hC hp hpq hgrowth
25   have hn : f 0 ≠ 0 := by simp [h0]
26   have hQ := canonicalProductQuotient_entire hf hs hn
27   obtain ⟨g, hg, hg0, he⟩ := entire_normalized_exists_log hQ
28     (canonicalProductQuotient_ne_zero hf hs hn) (by rw [canonicalProductQuotient_zero hf hs, h0])
29   let B := reciprocalPowerMass f q / q
30   have hB : 0 ≤ B := div_nonneg (reciprocalPowerMass_nonneg _ _) hq.le
31   have hzero : g = 0 := entire_sublinear_factor_rigidity hf (fullCanonicalProduct_entire hs)
32     hg (fullCanonicalProduct_zero f) hg0 (fun z => by rw [he]; exact fullCanonicalProduct_times_quotient hf hs hn z)
33     (show 0 ≤ C + B by positivity) hq1 (by
34       intro R hR z hz
35       have hRp : 0 ≤ R ^ q := Real.rpow_nonneg (by linarith) _
36       constructor
37       · apply (hgrowth R hR z hz).trans
38         apply Real.exp_le_exp.mpr
39         calc
40           _ ≤ C * R ^ q := mul_le_mul_of_nonneg_left (Real.rpow_le_rpow_of_exponent_le hR hpq.le) hC
41           _ ≤ (C + B) * R ^ q := by nlinarith
42       · apply (fullCanonicalProduct_growth hs hsq hq hq1.le z).trans
43         apply Real.exp_le_exp.mpr
44         change B * ‖z‖ ^ q ≤ _
45         calc
46           _ ≤ B * R ^ q := mul_le_mul_of_nonneg_left (Real.rpow_le_rpow (norm_nonneg _) hz hq.le) hB
47           _ ≤ (C + B) * R ^ q := by nlinarith)
48   funext z
49   have h := fullCanonicalProduct_times_quotient hf hs hn z
50   rw [← he z, hzero] at h
51   simpa using h.symm
52 
53 end
54 end Komorebi.PaperIV

Back to source controls