FullCanonicalProduct.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.FullZeroSummability
6 import Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
7 import Mathlib.Analysis.Complex.LocallyUniformLimit
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter
12 
13 /-- Every distinct zero occurs exactly its analytic multiplicity many times. -/
14 def ZeroMultiplicityIndex (f : ℂ → ℂ) :=
15   Σ z : {z : ℂ // f z = 0}, Fin (analyticOrderNatAt f z)
16 
17 def indexedZero {f : ℂ → ℂ} (i : ZeroMultiplicityIndex f) : ℂ := i.1.val
18 
19 def fullCanonicalProduct (f : ℂ → ℂ) (w : ℂ) : ℂ :=
20   ∏' i : ZeroMultiplicityIndex f, (1 - w / indexedZero i)
21 
22 theorem zeroMultiplicity_reciprocal_summable {f : ℂ → ℂ} (hf : ZeroPowerSummable f 1) :
23     Summable (fun i : ZeroMultiplicityIndex f => 1 / ‖indexedZero i‖) := by
24   apply (summable_sigma_of_nonneg (fun i : ZeroMultiplicityIndex f => by positivity)).mpr
25   constructor
26   · intro z
27     exact (hasSum_fintype _).summable
28   · simpa only [indexedZero, tsum_fintype, Finset.sum_const, Finset.card_univ,
29       Fintype.card_fin, nsmul_eq_mul, mul_one_div, ZeroPowerSummable, Real.rpow_one] using hf
30 
31 theorem fullCanonicalProduct_factors_summable {f : ℂ → ℂ} (hf : ZeroPowerSummable f 1) (w : ℂ) :
32     Summable (fun i : ZeroMultiplicityIndex f => ‖w / indexedZero i‖) := by
33   simpa only [norm_div, mul_one_div] using (zeroMultiplicity_reciprocal_summable hf).mul_left ‖w‖
34 
35 theorem fullCanonicalProduct_multipliable {f : ℂ → ℂ} (hf : ZeroPowerSummable f 1) (w : ℂ) :
36     Multipliable (fun i : ZeroMultiplicityIndex f => 1 - w / indexedZero i) :=
37   multipliable_one_sub_of_summable (fullCanonicalProduct_factors_summable hf w)
38 
39 theorem fullCanonicalProduct_uniform_on_compact {f : ℂ → ℂ} (hf : ZeroPowerSummable f 1)
40     {K : Set ℂ} (hK : IsCompact K) :
41     HasProdUniformlyOn (fun (i : ZeroMultiplicityIndex f) w => 1 - w / indexedZero i)
42       (fullCanonicalProduct f) K := by
43   obtain ⟨B, hB⟩ := hK.isBounded.exists_norm_le
44   have h := ((zeroMultiplicity_reciprocal_summable hf).mul_left B).hasProdUniformlyOn_one_add hK
45     (f := fun (i : ZeroMultiplicityIndex f) w => -w / indexedZero i)
46     (Eventually.of_forall (fun i w hw => ?_)) (fun _ => by fun_prop)
47   · simpa only [fullCanonicalProduct, neg_div, ← sub_eq_add_neg] using! h
48   · rw [norm_div, norm_neg, mul_one_div]
49     exact div_le_div_of_nonneg_right (hB w hw) (norm_nonneg _)
50 
51 theorem fullCanonicalProduct_locally_uniform {f : ℂ → ℂ} (hf : ZeroPowerSummable f 1) :
52     HasProdLocallyUniformlyOn (fun (i : ZeroMultiplicityIndex f) w => 1 - w / indexedZero i)
53       (fullCanonicalProduct f) univ := by
54   apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_univ
55   intro K _ hK
56   exact fullCanonicalProduct_uniform_on_compact hf hK
57 
58 theorem fullCanonicalProduct_entire {f : ℂ → ℂ} (hf : ZeroPowerSummable f 1) :
59     Differentiable ℂ (fullCanonicalProduct f) := by
60   apply differentiableOn_univ.mp
61   apply (fullCanonicalProduct_locally_uniform hf).differentiableOn _ isOpen_univ
62   apply Eventually.of_forall
63   intro S
64   have h : DifferentiableOn ℂ (fun w : ℂ => ∏ i ∈ S, (1 - w / indexedZero i)) univ :=
65     DifferentiableOn.fun_finsetProd (fun _ _ => by fun_prop)
66   simpa only [Finset.prod_fn] using h
67 
68 theorem fullCanonicalProduct_zero (f : ℂ → ℂ) : fullCanonicalProduct f 0 = 1 := by
69   simp [fullCanonicalProduct]
70 
71 theorem fullCanonicalProduct_ne_zero {f : ℂ → ℂ} (hf : ZeroPowerSummable f 1)
72     (hf0 : f 0 ≠ 0) {w : ℂ} (hw : ∀ i : ZeroMultiplicityIndex f, w ≠ indexedZero i) :
73     fullCanonicalProduct f w ≠ 0 := by
74   have h := tprod_one_add_ne_zero_of_summable
75     (f := fun i : ZeroMultiplicityIndex f => -w / indexedZero i) (fun i => ?_)
76     (by simpa only [neg_div, norm_neg] using fullCanonicalProduct_factors_summable hf w)
77   · simpa only [fullCanonicalProduct, neg_div, ← sub_eq_add_neg] using! h
78   · rw [neg_div, ← sub_eq_add_neg, sub_ne_zero]
79     intro he
80     apply hw i
81     apply (div_eq_one_iff_eq ?_).mp he.symm
82     intro hz
83     apply hf0
84     have he := i.1.property
85     change f (indexedZero i) = 0 at he
86     rw [hz] at he
87     exact he
88 
89 theorem fullCanonicalProduct_zero_iff_index {f : ℂ → ℂ} (hf : ZeroPowerSummable f 1)
90     (hf0 : f 0 ≠ 0) (w : ℂ) :
91     fullCanonicalProduct f w = 0 ↔ ∃ i : ZeroMultiplicityIndex f, w = indexedZero i := by
92   constructor
93   · intro hz
94     by_contra h
95     push Not at h
96     exact fullCanonicalProduct_ne_zero hf hf0 h hz
97   · rintro ⟨i, rfl⟩
98     apply tprod_of_exists_eq_zero
99     refine ⟨i, ?_⟩
100     rw [div_self, sub_self]
101     intro hz
102     apply hf0
103     have he := i.1.property
104     change f (indexedZero i) = 0 at he
105     rw [hz] at he
106     exact he
107 
108 theorem indexedZero_ne_zero {f : ℂ → ℂ} (hf0 : f 0 ≠ 0) (i : ZeroMultiplicityIndex f) :
109     indexedZero i ≠ 0 := by
110   intro h
111   apply hf0
112   have he := i.1.property
113   change f (indexedZero i) = 0 at he
114   rwa [h] at he
115 
116 theorem entire_zero_multiplicity_pos {f : ℂ → ℂ} (hf : Differentiable ℂ f)
117     (hf0 : f 0 ≠ 0) {w : ℂ} (hw : f w = 0) : 0 < analyticOrderNatAt f w := by
118   apply ENat.toNat_pos
119   · exact (hf.analyticAt w).analyticOrderAt_ne_zero.mpr hw
120   · exact entire_analyticOrderAt_ne_top (fun z => hf.analyticAt z) hf0 w
121 
122 theorem fullCanonicalProduct_zero_iff {f : ℂ → ℂ} (hf : Differentiable ℂ f)
123     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (w : ℂ) :
124     fullCanonicalProduct f w = 0 ↔ f w = 0 := by
125   rw [fullCanonicalProduct_zero_iff_index hs hf0]
126   constructor
127   · rintro ⟨i, rfl⟩
128     exact i.1.property
129   · intro hw
130     exact ⟨⟨⟨w, hw⟩, ⟨0, entire_zero_multiplicity_pos hf hf0 hw⟩⟩, rfl⟩
131 
132 theorem zeroMultiplicityIndex_countable {f : ℂ → ℂ} (hs : ZeroPowerSummable f 1)
133     (hf0 : f 0 ≠ 0) : Countable (ZeroMultiplicityIndex f) := by
134   have hc := (zeroMultiplicity_reciprocal_summable hs).countable_support
135   have he : Function.support (fun i : ZeroMultiplicityIndex f => 1 / ‖indexedZero i‖) = univ := by
136     ext i
137     simp only [Function.mem_support, mem_univ, iff_true]
138     exact one_div_ne_zero (norm_ne_zero_iff.mpr (indexedZero_ne_zero hf0 i))
139   rw [he] at hc
140   exact countable_univ_iff.mp hc
141 
142 /-- The complete product includes every exceptional zero with its actual multiplicity. -/
143 theorem entireReducedDenominator_full_product_properties {N : ℕ} (hN : 2 ≤ N) :
144     Differentiable ℂ (fullCanonicalProduct (entireReducedDenominator N)) ∧
145     fullCanonicalProduct (entireReducedDenominator N) 0 = 1 ∧
146     (∀ w, fullCanonicalProduct (entireReducedDenominator N) w = 0 ↔ entireReducedDenominator N w = 0) ∧
147     Countable (ZeroMultiplicityIndex (entireReducedDenominator N)) := by
148   have hs := entireReducedDenominator_reciprocal_zeros_summable hN
149   have h0 : entireReducedDenominator N 0 ≠ 0 := by rw [entireReducedDenominator_zero]; exact one_ne_zero
150   refine ⟨fullCanonicalProduct_entire hs, fullCanonicalProduct_zero _, ?_, zeroMultiplicityIndex_countable hs h0⟩
151   exact fullCanonicalProduct_zero_iff (fun z => (analyticAt_entireReducedDenominator (by omega) z).differentiableAt) hs h0
152 
153 end
154 end Komorebi.PaperIV

Back to source controls