SublinearExponentialRigidity.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.CanonicalProductQuotient
6 import Mathlib.Analysis.Complex.HasPrimitives
7 import Mathlib.Analysis.Complex.BorelCaratheodory
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter Metric
12 open scoped Topology
13 
14 /-- A normalized entire function without zeros has an entire logarithm,
15 constructed by integrating its logarithmic derivative. -/
16 theorem entire_normalized_exists_log {f : ℂ → ℂ} (hf : Differentiable ℂ f)
17     (hn : ∀ z, f z ≠ 0) (h0 : f 0 = 1) :
18     ∃ g : ℂ → ℂ, Differentiable ℂ g ∧ g 0 = 0 ∧ ∀ z, Complex.exp (g z) = f z := by
19   have hd : Differentiable ℂ (fun z => deriv f z / f z) := by
20     intro z
21     exact (hf.analyticAt z).deriv.differentiableAt.div (hf z) (hn z)
22   obtain ⟨g, hg0, hg⟩ := hd.isExactOn_univ.with_val_at 0 0
23   have hg' : Differentiable ℂ g := fun z => (hg z (mem_univ z)).differentiableAt
24   have hH : ∀ z, HasDerivAt (fun w => f w * Complex.exp (-g w)) 0 z := by
25     intro z
26     convert! ((hf z).hasDerivAt).mul ((hg z (mem_univ z)).neg.cexp) using 1
27     field_simp [hn z]
28     ring
29   have he : ∀ z, f z * Complex.exp (-g z) = 1 := by
30     intro z
31     have h := is_const_of_deriv_eq_zero (fun w => (hH w).differentiableAt)
32       (fun w => (hH w).deriv) z 0
33     simpa only [hg0, h0, neg_zero, Complex.exp_zero, one_mul] using h
34   refine ⟨g, hg', hg0, fun z => ?_⟩
35   have h := he z
36   rw [Complex.exp_neg, ← div_eq_mul_inv] at h
37   exact ((div_eq_one_iff_eq (Complex.exp_ne_zero _)).mp h).symm
38 
39 /-- Borel-Carathéodory turns a sublinear bound on real parts into rigidity.
40 The bound is uniform throughout each disk, not merely along one ray. -/
41 theorem entire_realPart_sublinear_constant {g : ℂ → ℂ} (hg : Differentiable ℂ g)
42     (h0 : g 0 = 0) {M : ℝ → ℝ}
43     (hp : ∀ᶠ R in atTop, 0 < M R)
44     (hM : Tendsto (fun R => M R / R) atTop (𝓝 0))
45     (hb : ∀ᶠ R in atTop, ∀ w : ℂ, ‖w‖ < R → (g w).re ≤ M R) : g = 0 := by
46   funext z
47   have hb' : ∀ᶠ R in atTop, ‖g z‖ ≤ 2 * (M R / R) * ‖z‖ / (1 - ‖z‖ / R) := by
48     filter_upwards [hp, hb, eventually_gt_atTop (‖z‖ + 1)] with R hRp hRb hR
49     have hR0 : 0 < R := by linarith [norm_nonneg z]
50     have h := Complex.borelCaratheodory_zero hRp hg.differentiableOn
51       (fun w hw => hRb w (mem_ball_zero_iff.mp hw)) hR0
52       (mem_ball_zero_iff.mpr (by linarith)) h0
53     convert h using 1
54     field_simp
55   have hsmall : Tendsto (fun R : ℝ => ‖z‖ / R) atTop (𝓝 0) := by
56     simpa only [div_eq_mul_inv, mul_zero] using (tendsto_inv_atTop_zero.const_mul ‖z‖)
57   have ht : Tendsto (fun R => 2 * (M R / R) * ‖z‖ / (1 - ‖z‖ / R)) atTop (𝓝 0) := by
58     simpa only [mul_zero, zero_mul, sub_zero, zero_div] using!
59       ((hM.const_mul 2).mul_const ‖z‖).div (tendsto_const_nhds.sub hsmall) (by norm_num)
60   exact norm_eq_zero.mp (le_antisymm (ge_of_tendsto ht hb') (norm_nonneg _))
61 
62 /-- The remaining Hadamard reduction can use any proved uniform sublinear
63 log-norm bound for the normalized zero-free quotient. -/
64 theorem entire_zeroFree_sublinear_logNorm_eq_one {f : ℂ → ℂ}
65     (hf : Differentiable ℂ f) (hn : ∀ z, f z ≠ 0) (h0 : f 0 = 1) {M : ℝ → ℝ}
66     (hp : ∀ᶠ R in atTop, 0 < M R)
67     (hM : Tendsto (fun R => M R / R) atTop (𝓝 0))
68     (hb : ∀ᶠ R in atTop, ∀ w : ℂ, ‖w‖ < R → Real.log ‖f w‖ ≤ M R) :
69     f = 1 := by
70   obtain ⟨g, hg, hg0, he⟩ := entire_normalized_exists_log hf hn h0
71   have hre : ∀ z, (g z).re = Real.log ‖f z‖ := by
72     intro z
73     rw [← he z, Complex.norm_exp, Real.log_exp]
74   have hgzero : g = 0 := entire_realPart_sublinear_constant hg hg0 hp hM (by
75     filter_upwards [hb] with R hR w hw
76     rw [hre]
77     exact hR w hw)
78   funext z
79   rw [← he z, hgzero]
80   exact Complex.exp_zero
81 
82 theorem entireReducedDenominator_product_quotient_has_log {N : ℕ} (hN : 2 ≤ N) :
83     ∃ g : ℂ → ℂ, Differentiable ℂ g ∧ g 0 = 0 ∧
84       ∀ z, Complex.exp (g z) * fullCanonicalProduct (entireReducedDenominator N) z = entireReducedDenominator N z := by
85   obtain ⟨hd, hn, h0, he⟩ := entireReducedDenominator_product_quotient hN
86   obtain ⟨g, hg, hg0, hgexp⟩ := entire_normalized_exists_log hd hn h0
87   exact ⟨g, hg, hg0, fun z => by rw [hgexp, mul_comm]; exact he z⟩
88 
89 end
90 end Komorebi.PaperIV

Back to source controls