CanonicalProductMultiplicity.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.FullCanonicalProduct
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 
11 /-- A general normally convergent reciprocal product, also used after deleting
12 all copies of a single zero. -/
13 def reciprocalProduct {ι : Type*} (a : ι → ℂ) (w : ℂ) : ℂ := ∏' i, (1 - w / a i)
14 
15 theorem reciprocalProduct_locally_uniform {ι : Type*} (a : ι → ℂ)
16     (hs : Summable (fun i => 1 / ‖a i‖)) :
17     HasProdLocallyUniformlyOn (fun i w => 1 - w / a i) (reciprocalProduct a) univ := by
18   apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_univ
19   intro K _ hK
20   obtain ⟨B, hB⟩ := hK.isBounded.exists_norm_le
21   have h := (hs.mul_left B).hasProdUniformlyOn_one_add hK
22     (f := fun i w => -w / a i) (Eventually.of_forall (fun i w hw => ?_)) (fun _ => by fun_prop)
23   · simpa only [reciprocalProduct, neg_div, ← sub_eq_add_neg] using! h
24   · rw [norm_div, norm_neg, mul_one_div]
25     exact div_le_div_of_nonneg_right (hB w hw) (norm_nonneg _)
26 
27 theorem reciprocalProduct_entire {ι : Type*} (a : ι → ℂ)
28     (hs : Summable (fun i => 1 / ‖a i‖)) : Differentiable ℂ (reciprocalProduct a) := by
29   apply differentiableOn_univ.mp
30   apply (reciprocalProduct_locally_uniform a hs).differentiableOn _ isOpen_univ
31   apply Eventually.of_forall
32   intro S
33   have h : DifferentiableOn ℂ (fun w : ℂ => ∏ i ∈ S, (1 - w / a i)) univ :=
34     DifferentiableOn.fun_finsetProd (fun _ _ => by fun_prop)
35   simpa only [Finset.prod_fn] using h
36 
37 theorem reciprocalProduct_ne_zero {ι : Type*} (a : ι → ℂ)
38     (hs : Summable (fun i => 1 / ‖a i‖)) (ha : ∀ i, a i ≠ 0)
39     {w : ℂ} (hw : ∀ i, w ≠ a i) : reciprocalProduct a w ≠ 0 := by
40   have h := tprod_one_add_ne_zero_of_summable (f := fun i => -w / a i) (fun i => ?_)
41     (by simpa only [norm_div, norm_neg, mul_one_div] using hs.mul_left ‖w‖)
42   · simpa only [reciprocalProduct, neg_div, ← sub_eq_add_neg] using! h
43   · rw [neg_div, ← sub_eq_add_neg, sub_ne_zero]
44     intro he
45     exact hw i ((div_eq_one_iff_eq (ha i)).mp he.symm)
46 
47 def zeroIndexFiberEquiv (f : ℂ → ℂ) (z : {z : ℂ // f z = 0}) :
48     Fin (analyticOrderNatAt f z) ≃ {i : ZeroMultiplicityIndex f // i.1 = z} where
49   toFun k := ⟨⟨z, k⟩, rfl⟩
50   invFun i := by
51     rcases i with ⟨⟨w, k⟩, h⟩
52     cases h
53     exact k
54   left_inv _ := rfl
55   right_inv i := by
56     rcases i with ⟨⟨w, k⟩, h⟩
57     cases h
58     rfl
59 
60 def otherZeroProduct (f : ℂ → ℂ) (z : {z : ℂ // f z = 0}) (w : ℂ) : ℂ :=
61   reciprocalProduct (fun i : {i : ZeroMultiplicityIndex f // i.1 ≠ z} => indexedZero i.val) w
62 
63 theorem otherZeroProduct_entire {f : ℂ → ℂ} (hs : ZeroPowerSummable f 1)
64     (z : {z : ℂ // f z = 0}) : Differentiable ℂ (otherZeroProduct f z) :=
65   reciprocalProduct_entire _ ((zeroMultiplicity_reciprocal_summable hs).subtype _)
66 
67 theorem otherZeroProduct_ne_zero_at_zero {f : ℂ → ℂ} (hs : ZeroPowerSummable f 1)
68     (hf0 : f 0 ≠ 0) (z : {z : ℂ // f z = 0}) : otherZeroProduct f z z ≠ 0 := by
69   apply reciprocalProduct_ne_zero _ ((zeroMultiplicity_reciprocal_summable hs).subtype _)
70     (fun i => indexedZero_ne_zero hf0 i.val)
71   intro i he
72   apply i.property
73   exact Subtype.ext he.symm
74 
75 /-- The factor at one distinct zero has exactly the prescribed multiplicity. -/
76 theorem fullCanonicalProduct_factor_at_zero {f : ℂ → ℂ} (hs : ZeroPowerSummable f 1)
77     (z : {z : ℂ // f z = 0}) (w : ℂ) :
78     fullCanonicalProduct f w = (1 - w / (z : ℂ)) ^ analyticOrderNatAt f z * otherZeroProduct f z w := by
79   have hm := fullCanonicalProduct_factors_summable hs w
80   let S : Set (ZeroMultiplicityIndex f) := {i | i.1 = z}
81   have he := Multipliable.tprod_mul_tprod_compl
82     (f := fun i : ZeroMultiplicityIndex f => 1 - w / indexedZero i) (s := S)
83     (multipliable_one_sub_of_summable (hm.subtype S))
84     (multipliable_one_sub_of_summable (hm.subtype (Sᶜ)))
85   have hfiber : (∏' _k : Fin (analyticOrderNatAt f z), (1 - w / (z : ℂ))) =
86       ∏' i : S, (1 - w / indexedZero i.val) :=
87     (zeroIndexFiberEquiv f z).tprod_eq (fun i => 1 - w / indexedZero i.val)
88   have hf : (∏' i : S, (1 - w / indexedZero i.val)) =
89       (1 - w / (z : ℂ)) ^ analyticOrderNatAt f z := by
90     simpa only [tprod_fintype, Finset.prod_const,
91       Finset.card_univ, Fintype.card_fin] using hfiber.symm
92   rw [hf] at he
93   exact he.symm
94 
95 theorem linear_zero_factor_order {z : ℂ} (hz : z ≠ 0) :
96     analyticOrderAt (fun w : ℂ => 1 - w / z) z = 1 := by
97   apply (show AnalyticAt ℂ (fun w : ℂ => 1 - w / z) z by fun_prop).analyticOrderAt_eq_one_of_zero_deriv_ne_zero
98   · rw [div_self hz, sub_self]
99   · have hd := ((hasDerivAt_id z).div_const z).const_sub 1
100     erw [hd.deriv]
101     exact neg_ne_zero.mpr (one_div_ne_zero hz)
102 
103 theorem fullCanonicalProduct_order_at_zero {f : ℂ → ℂ} (hs : ZeroPowerSummable f 1)
104     (hf0 : f 0 ≠ 0) (z : {z : ℂ // f z = 0}) :
105     analyticOrderAt (fullCanonicalProduct f) z = (analyticOrderNatAt f z : ℕ∞) := by
106   have hz : (z : ℂ) ≠ 0 := by intro h; apply hf0; simpa only [h] using z.property
107   have he : fullCanonicalProduct f =
108       (fun w : ℂ => (1 - w / (z : ℂ)) ^ analyticOrderNatAt f z) * otherZeroProduct f z :=
109     funext (fullCanonicalProduct_factor_at_zero hs z)
110   rw [he, analyticOrderAt_mul (by fun_prop) ((otherZeroProduct_entire hs z).analyticAt z)]
111   have ho := ((otherZeroProduct_entire hs z).analyticAt z).analyticOrderAt_eq_zero.mpr
112     (otherZeroProduct_ne_zero_at_zero hs hf0 z)
113   rw [ho, add_zero]
114   erw [analyticOrderAt_pow (f := fun w : ℂ => 1 - w / (z : ℂ)) (by fun_prop)]
115   rw [linear_zero_factor_order hz]
116   simp only [nsmul_one]
117 
118 theorem fullCanonicalProduct_same_orders {f : ℂ → ℂ} (hf : Differentiable ℂ f)
119     (hs : ZeroPowerSummable f 1) (hf0 : f 0 ≠ 0) (z : ℂ) :
120     analyticOrderAt (fullCanonicalProduct f) z = analyticOrderAt f z := by
121   by_cases hz : f z = 0
122   · have h := fullCanonicalProduct_order_at_zero hs hf0 ⟨z, hz⟩
123     simpa only [Nat.cast_analyticOrderNatAt (entire_analyticOrderAt_ne_top (fun w => hf.analyticAt w) hf0 z)] using h
124   · rw [((fullCanonicalProduct_entire hs).analyticAt z).analyticOrderAt_eq_zero.mpr
125       (fun h => hz ((fullCanonicalProduct_zero_iff hf hs hf0 z).mp h)),
126       (hf.analyticAt z).analyticOrderAt_eq_zero.mpr hz]
127 
128 theorem entireReducedDenominator_full_product_same_orders {N : ℕ} (hN : 2 ≤ N) (z : ℂ) :
129     analyticOrderAt (fullCanonicalProduct (entireReducedDenominator N)) z =
130       analyticOrderAt (entireReducedDenominator N) z :=
131   fullCanonicalProduct_same_orders
132     (fun z => (analyticAt_entireReducedDenominator (by omega) z).differentiableAt)
133     (entireReducedDenominator_reciprocal_zeros_summable hN)
134     (by rw [entireReducedDenominator_zero]; exact one_ne_zero) z
135 
136 end
137 end Komorebi.PaperIV

Back to source controls