HadamardIdentification.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.EntireQuotientGrowth
6 import KomorebiPaperIV.CanonicalProductGrowth
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 /-- The actual quotient is identically one. No growth certificate is assumed:
14 the zero-power bounds, product estimate and Jensen-Poisson estimate prove it. -/
15 theorem entireReducedDenominator_quotient_eq_one {N : ℕ} (hN : 2 ≤ N) :
16     canonicalProductQuotient (entireReducedDenominator N) = 1 := by
17   obtain ⟨hQ, hn, h0, he⟩ := entireReducedDenominator_product_quotient hN
18   obtain ⟨g, hg, hg0, hgexp⟩ := entire_normalized_exists_log hQ hn h0
19   obtain ⟨C, hC, hbound⟩ := entireReducedDenominator_and_product_growth hN
20   have hf : Differentiable ℂ (entireReducedDenominator N) :=
21     fun z => (analyticAt_entireReducedDenominator (by omega) z).differentiableAt
22   have hP := fullCanonicalProduct_entire (entireReducedDenominator_reciprocal_zeros_summable hN)
23   have hgz : g = 0 := entire_sublinear_factor_rigidity hf hP hg
24     (fullCanonicalProduct_zero _) hg0 (fun z => by rw [hgexp]; exact he z)
25     hC (by norm_num : (3 / 4 : ℝ) < 1) hbound
26   funext z
27   rw [← hgexp z, hgz]
28   exact Complex.exp_zero
29 
30 /-- The complete genus-zero Hadamard product for every N ≥ 2, including all
31 exceptional zeros repeated according to their analytic multiplicities. -/
32 theorem entireReducedDenominator_eq_fullCanonicalProduct {N : ℕ} (hN : 2 ≤ N) :
33     entireReducedDenominator N = fullCanonicalProduct (entireReducedDenominator N) := by
34   funext z
35   have he := (entireReducedDenominator_product_quotient hN).2.2.2 z
36   rw [entireReducedDenominator_quotient_eq_one hN, Pi.one_apply, mul_one] at he
37   exact he.symm
38 
39 /-- Full statement of Theorem 12.1: equality and convergence uniformly on
40 each compact subset for the product over the entire zero multiset. -/
41 theorem entireReducedDenominator_hadamard_uniform {N : ℕ} (hN : 2 ≤ N)
42     {K : Set ℂ} (hK : IsCompact K) :
43     HasProdUniformlyOn
44       (fun (i : ZeroMultiplicityIndex (entireReducedDenominator N)) w => 1 - w / indexedZero i)
45       (entireReducedDenominator N) K := by
46   simpa only [← entireReducedDenominator_eq_fullCanonicalProduct hN] using
47     fullCanonicalProduct_uniform_on_compact
48       (entireReducedDenominator_reciprocal_zeros_summable hN) hK
49 
50 theorem canonicalSignedDenominator_hadamard {N : ℕ} (hN : 2 ≤ N) (z : ℂ) :
51     canonicalSignedDenominator N z =
52       ∏' i : ZeroMultiplicityIndex (entireReducedDenominator N), (1 - z ^ N / indexedZero i) := by
53   calc
54     _ = entireReducedDenominator N (z ^ N) := canonicalSignedDenominator_eq_reduced_power (by omega) z
55     _ = fullCanonicalProduct (entireReducedDenominator N) (z ^ N) :=
56       congrFun (entireReducedDenominator_eq_fullCanonicalProduct hN) _
57     _ = _ := rfl
58 
59 end
60 end Komorebi.PaperIV

Back to source controls