NormalizedProduct.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.NormalizedGrowth
6 import KomorebiPaperIV.SublinearHadamard
7 import KomorebiPaperIV.AnalyticTaylorAlgebra
8 import KomorebiPaperIV.ThetaZeroBell
9 
10 namespace Komorebi.PaperIV
11 noncomputable section
12 open Set Filter
13 open scoped Topology
14 
15 /-- The full genus-zero product for every normalized residue section. -/
16 theorem entireNormalizedSection_hadamard {N : ℕ} (hN : 2 ≤ N) (j : ℕ) :
17     entireNormalizedSection N j = fullCanonicalProduct (entireNormalizedSection N j) := by
18   have hN0 : 0 < N := by omega
19   apply entire_sublinear_growth_hadamard
20     (fun z => (analyticAt_entireNormalizedSection hN0 j z).differentiableAt)
21     (entireNormalizedSection_zero N j) (normalizedSectionGrowthConstant_pos j).le (by positivity)
22     _ (entireNormalizedSection_disk_growth hN0 j)
23   have hn : (1 : ℝ) < N := by exact_mod_cast (show 1 < N by omega)
24   exact (div_lt_one (by positivity : (0 : ℝ) < N)).mpr hn
25 
26 theorem entireNormalizedSection_hadamard_uniform {N : ℕ} (hN : 2 ≤ N) (j : ℕ)
27     {K : Set ℂ} (hK : IsCompact K) :
28     HasProdUniformlyOn (fun (i : ZeroMultiplicityIndex (entireNormalizedSection N j)) w =>
29       1 - w / indexedZero i) (entireNormalizedSection N j) K := by
30   have hn : (1 : ℝ) < N := by exact_mod_cast (show 1 < N by omega)
31   have hs := entireNormalizedSection_zeroPowerSummable (show 0 < N by omega) j
32     ((div_lt_one (by positivity : (0 : ℝ) < N)).mpr hn)
33   simpa only [← entireNormalizedSection_hadamard hN j] using fullCanonicalProduct_uniform_on_compact hs hK
34 
35 theorem analyticTaylorSeries_entireNormalizedSection {N : ℕ} (hN : 0 < N) (j : ℕ) :
36     analyticTaylorSeries (entireNormalizedSection N j) = normalizedResidueSection (K := ℂ) N j := by
37   ext n
38   rw [analyticTaylorSeries_coeff, analyticTaylorCoefficient, entireNormalizedSection_iteratedDeriv_zero hN,
39     coeff_normalizedResidueSection]
40   have hn : (n.factorial : ℂ) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
41   field_simp
42 
43 end
44 end Komorebi.PaperIV

Back to source controls