EntireQuotientGrowth.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.SublinearExponentialRigidity
6 import Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
7 import Mathlib.Analysis.Complex.Harmonic.Poisson
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter Metric Real ValueDistribution
12 open scoped Topology
13 
14 theorem entire_logCounting_poles_zero {f : ℂ → ℂ} (hf : Differentiable ℂ f) :
15     logCounting f ⊤ = 0 := by
16   have ha : AnalyticOnNhd ℂ f univ := fun z _ => hf.analyticAt z
17   rw [logCounting_top, negPart_eq_zero.mpr (MeromorphicOn.AnalyticOnNhd.divisor_nonneg ha)]
18   simp
19 
20 theorem entire_normalized_proximity_inv_le {f : ℂ → ℂ}
21     (hf : Differentiable ℂ f) (h0 : f 0 = 1) {R : ℝ} (hR : 1 ≤ R) :
22     proximity f⁻¹ ⊤ R ≤ proximity f ⊤ R := by
23   have hm : Meromorphic f := fun z => (hf.analyticAt z).meromorphicAt
24   have ht := (hf.analyticAt 0).meromorphicTrailingCoeffAt_of_ne_zero (by rw [h0]; exact one_ne_zero)
25   have he := characteristic_sub_characteristic_inv_le (R := R) hm
26   rw [ht, h0, norm_one, log_one, abs_zero, max_self] at he
27   have heq := abs_nonpos_iff.mp he
28   simp only [characteristic, Pi.add_apply, entire_logCounting_poles_zero hf, Pi.zero_apply, add_zero] at heq
29   have hn := logCounting_nonneg (f := f⁻¹) (e := ⊤) hR
30   linarith
31 
32 theorem entire_eventually_codiscrete_ne_zero {f : ℂ → ℂ}
33     (hf : Differentiable ℂ f) (h0 : f 0 ≠ 0) :
34     ∀ᶠ z in codiscrete ℂ, f z ≠ 0 := by
35   have hm : MeromorphicOn f univ := fun z _ => (hf.analyticAt z).meromorphicAt
36   have hh := hm.eventually_codiscreteWithin_apply_ne_zero (fun z _ => ?_)
37   · simpa only [Filter.codiscrete] using hh
38   · rw [(hf.analyticAt z).meromorphicOrderAt_eq,
39       ← Nat.cast_analyticOrderNatAt (entire_analyticOrderAt_ne_top (fun w => hf.analyticAt w) h0 z),
40       ENat.map_natCast]
41     exact WithTop.coe_ne_top
42 
43 /-- Jensen's formula controls a normalized entire quotient using only upper
44 growth of numerator and denominator, including circles through their zeros. -/
45 theorem entire_quotient_proximity_le {f P Q : ℂ → ℂ}
46     (hf : Differentiable ℂ f) (hP : Differentiable ℂ P)
47     (hP0 : P 0 = 1) (he : ∀ z, P z * Q z = f z)
48     {R : ℝ} (hR : 1 ≤ R) :
49     proximity Q ⊤ R ≤ proximity f ⊤ R + proximity P ⊤ R := by
50   have hm : Meromorphic f := fun z => (hf.analyticAt z).meromorphicAt
51   have hp : Meromorphic P := fun z => (hP.analyticAt z).meromorphicAt
52   have heq : Q =ᶠ[codiscrete ℂ] f * P⁻¹ := by
53     filter_upwards [entire_eventually_codiscrete_ne_zero hP (by rw [hP0]; exact one_ne_zero)] with z hz
54     change Q z = f z * (P z)⁻¹
55     rw [← he z]
56     field_simp
57   rw [proximity_congr_codiscrete heq (by linarith)]
58   exact (proximity_mul_top_le hm hp.inv R).trans
59     (add_le_add_right (entire_normalized_proximity_inv_le hP hP0 hR) _)
60 
61 /-- A Poisson-kernel estimate on the half-radius disk. -/
62 theorem entire_re_le_three_proximity_exp {g : ℂ → ℂ} (hg : Differentiable ℂ g)
63     {R : ℝ} (hR : 0 < R) {z : ℂ} (hz : ‖z‖ < R / 2) :
64     (g z).re ≤ 3 * proximity (fun w => Complex.exp (g w)) ⊤ R := by
65   let K : ℂ → ℝ := fun w => (herglotzRieszKernel 0 z w).re
66   have hzR : z ∈ ball (0 : ℂ) R := by
67     rw [mem_ball_zero_iff]; linarith
68   have hK : ContinuousOn K (sphere 0 |R|) :=
69     Complex.continuous_re.comp_continuousOn
70       (continuousOn_herglotzRieszKernel_sphere (by
71         rw [abs_of_pos hR, mem_sphere_zero_iff_norm]; intro heq; linarith))
72   have hh : InnerProductSpace.HarmonicOnNhd (fun w => (g w).re) (closedBall 0 R) :=
73     fun w _ => (hg.analyticAt w).harmonicAt_re
74   have he := hh.circleAverage_re_herglotzRieszKernel_smul hzR
75   change circleAverage (fun w => K w * (g w).re) 0 R = (g z).re at he
76   have hi : CircleIntegrable (fun w => K w * (g w).re) 0 R :=
77     (hK.mul (Complex.continuous_re.comp hg.continuous).continuousOn).circleIntegrable'
78   have hj : CircleIntegrable (fun w => 3 * max 0 (g w).re) 0 R := by
79     exact (continuous_const.mul (continuous_const.max (Complex.continuous_re.comp hg.continuous))).continuousOn.circleIntegrable'
80   have hm := circleAverage_mono hi hj (fun w hw => ?_)
81   · rw [he] at hm
82     simpa only [proximity_top, Complex.norm_exp, posLog, log_exp,
83       ← smul_eq_mul, circleAverage_fun_smul] using hm
84   · have hw' : w ∈ sphere (0 : ℂ) R := by rwa [abs_of_pos hR] at hw
85     have hu := re_herglotzRieszKernel_le hw' hzR
86     have hl := le_re_herglotzRieszKernel hw' hzR
87     simp only [sub_zero] at hu hl
88     have hd : 0 < R - ‖z‖ := by linarith
89     have hk3 : K w ≤ 3 := by
90       simpa only [K, herglotzRieszKernel, sub_zero] using
91         hu.trans ((div_le_iff₀ hd).mpr (show R + ‖z‖ ≤ 3 * (R - ‖z‖) by linarith))
92     have hk0 : 0 ≤ K w := by
93       have hd2 : 0 ≤ R + ‖z‖ := by positivity
94       simpa only [K, herglotzRieszKernel, sub_zero] using (div_nonneg hd.le hd2).trans hl
95     exact (mul_le_mul_of_nonneg_left (le_max_right 0 _) hk0).trans
96       (mul_le_mul_of_nonneg_right hk3 (le_max_left 0 _))
97 
98 theorem entire_proximity_le_of_growth {f : ℂ → ℂ} (hf : Differentiable ℂ f)
99     {R B : ℝ} (hB : 0 ≤ B) (hb : ∀ z ∈ sphere (0 : ℂ) |R|, ‖f z‖ ≤ exp B) :
100     proximity f ⊤ R ≤ B := by
101   rw [proximity_top]
102   apply circleAverage_mono_on_of_le_circle
103     ((show MeromorphicOn f (sphere 0 |R|) from fun z _ => (hf.analyticAt z).meromorphicAt).circleIntegrable_posLog_norm)
104   intro z hz
105   rw [posLog, max_le_iff]
106   refine ⟨hB, ?_⟩
107   by_cases h : f z = 0
108   · simpa [h] using hB
109   · exact (log_le_iff_le_exp (norm_pos_iff.mpr h)).mpr (hb z hz)
110 
111 /-- Sublinear growth of two entire factors eliminates a normalized exponential
112 factor. All estimates are derived from circle means, even when a circle meets zeros. -/
113 theorem entire_sublinear_factor_rigidity {f P g : ℂ → ℂ}
114     (hf : Differentiable ℂ f) (hP : Differentiable ℂ P) (hg : Differentiable ℂ g)
115     (hP0 : P 0 = 1) (hg0 : g 0 = 0)
116     (he : ∀ z, P z * Complex.exp (g z) = f z)
117     {C s : ℝ} (hC : 0 ≤ C) (hs : s < 1)
118     (hbound : ∀ R : ℝ, 1 ≤ R → ∀ z : ℂ, ‖z‖ ≤ R →
119       ‖f z‖ ≤ exp (C * R ^ s) ∧ ‖P z‖ ≤ exp (C * R ^ s)) : g = 0 := by
120   let M : ℝ → ℝ := fun R => 1 + 6 * C * (2 * R) ^ s
121   apply entire_realPart_sublinear_constant hg hg0 (M := M)
122   · filter_upwards [eventually_ge_atTop (1 : ℝ)] with R hR
123     dsimp [M]
124     positivity
125   · have ht : Tendsto (fun R : ℝ => R ^ (s - 1)) atTop (𝓝 0) := by
126       simpa only [neg_sub] using tendsto_rpow_neg_atTop (show 0 < 1 - s by linarith)
127     have heq : (fun R => M R / R) =ᶠ[atTop]
128         (fun R => R⁻¹ + (6 * C * (2 : ℝ) ^ s) * R ^ (s - 1)) := by
129       filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
130       dsimp [M]
131       rw [Real.mul_rpow (by norm_num) hR.le, Real.rpow_sub hR, Real.rpow_one]
132       ring
133     have hlim : Tendsto (fun R : ℝ => R⁻¹ + (6 * C * (2 : ℝ) ^ s) * R ^ (s - 1)) atTop (𝓝 0) := by
134       simpa only [mul_zero, add_zero] using tendsto_inv_atTop_zero.add (ht.const_mul (6 * C * (2 : ℝ) ^ s))
135     exact hlim.congr' heq.symm
136   · filter_upwards [eventually_ge_atTop (1 : ℝ)] with R hR z hz
137     have hR0 : 0 < R := by linarith
138     have h2R : 1 ≤ 2 * R := by linarith
139     have hzb : ‖z‖ < (2 * R) / 2 := by linarith
140     have hgrowth := entire_re_le_three_proximity_exp hg (by linarith : 0 < 2 * R) hzb
141     have hp := entire_quotient_proximity_le hf hP hP0 he h2R
142     have hb : 0 ≤ C * (2 * R) ^ s := mul_nonneg hC (Real.rpow_nonneg (by linarith) _)
143     have hbF := entire_proximity_le_of_growth hf (R := 2 * R) hb (fun w hw => ?_)
144     have hbP := entire_proximity_le_of_growth hP (R := 2 * R) hb (fun w hw => ?_)
145     · dsimp [M]
146       linarith
147     all_goals
148       rw [abs_of_pos (by linarith : 0 < 2 * R), mem_sphere_zero_iff_norm] at hw
149       first | exact (hbound (2 * R) h2R w hw.le).1 | exact (hbound (2 * R) h2R w hw.le).2
150 
151 end
152 end Komorebi.PaperIV

Back to source controls