ReducedCanonicalProduct.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroSequenceAsymptotics
6 import Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
7 import Mathlib.Analysis.Complex.LocallyUniformLimit
8 
9 /-! The genus-zero product over the constructed positive tail is entire.
10 This file does not assert its equality with the reduced denominator: the finite
11 exceptional factor and the zero-free quotient still need to be identified. -/
12 namespace Komorebi.PaperIV
13 noncomputable section
14 open Filter Set
15 
16 def reducedTailProduct (N M : ℕ) (w : ℂ) : ℂ :=
17   ∏' m : ℕ, (1 - w / (reducedPositiveZero N (m + M) : ℂ))
18 
19 theorem reducedPositiveZero_pos {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
20     0 < reducedPositiveZero N m := pow_pos (signedPositiveZero_pos hN m) N
21 
22 theorem reducedTail_reciprocal_summable {N : ℕ} (hN : 3 ≤ N) (M : ℕ) :
23     Summable (fun m => 1 / reducedPositiveZero N (m + M)) :=
24   (summable_nat_add_iff M).mpr (reducedPositiveZero_reciprocal_summable hN)
25 
26 theorem reducedTail_factors_norm_summable {N : ℕ} (hN : 3 ≤ N) (M : ℕ) (w : ℂ) :
27     Summable (fun m => ‖w / (reducedPositiveZero N (m + M) : ℂ)‖) := by
28   simpa only [norm_div, Complex.norm_real, Real.norm_eq_abs,
29     abs_of_pos (reducedPositiveZero_pos (by omega : 2 ≤ N) _), mul_one_div] using
30     (reducedTail_reciprocal_summable hN M).mul_left ‖w‖
31 
32 theorem reducedTailProduct_multipliable {N : ℕ} (hN : 3 ≤ N) (M : ℕ) (w : ℂ) :
33     Multipliable (fun m => 1 - w / (reducedPositiveZero N (m + M) : ℂ)) :=
34   multipliable_one_sub_of_summable (reducedTail_factors_norm_summable hN M w)
35 
36 theorem reducedTailProduct_uniform_on_compact {N : ℕ} (hN : 3 ≤ N) (M : ℕ)
37     {K : Set ℂ} (hK : IsCompact K) :
38     HasProdUniformlyOn (fun m w => 1 - w / (reducedPositiveZero N (m + M) : ℂ))
39       (reducedTailProduct N M) K := by
40   obtain ⟨B, hB⟩ := hK.isBounded.exists_norm_le
41   have hs := (reducedTail_reciprocal_summable hN M).mul_left B
42   have hh := hs.hasProdUniformlyOn_nat_one_add hK
43     (f := fun (m : ℕ) (w : ℂ) => -w / (reducedPositiveZero N (m + M) : ℂ))
44     (Filter.Eventually.of_forall (fun m w hw => ?_)) (fun _ => by fun_prop)
45   · simpa only [reducedTailProduct, neg_div, ← sub_eq_add_neg] using! hh
46   · rw [norm_div, norm_neg, Complex.norm_real, Real.norm_eq_abs,
47       abs_of_pos (reducedPositiveZero_pos (by omega : 2 ≤ N) _), mul_one_div]
48     exact div_le_div_of_nonneg_right (hB w hw) (le_of_lt (reducedPositiveZero_pos (by omega) _))
49 
50 theorem reducedTailProduct_locally_uniform {N : ℕ} (hN : 3 ≤ N) (M : ℕ) :
51     HasProdLocallyUniformlyOn (fun m w => 1 - w / (reducedPositiveZero N (m + M) : ℂ))
52       (reducedTailProduct N M) univ := by
53   apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_univ
54   intro K _ hK
55   exact reducedTailProduct_uniform_on_compact hN M hK
56 
57 theorem analyticAt_reducedTailProduct {N : ℕ} (hN : 3 ≤ N) (M : ℕ) (w : ℂ) :
58     AnalyticAt ℂ (reducedTailProduct N M) w := by
59   have he : ∀ s : Finset ℕ, DifferentiableOn ℂ
60       (fun w : ℂ => ∏ m ∈ s, (1 - w / (reducedPositiveZero N (m + M) : ℂ))) univ := by
61     intro s
62     exact DifferentiableOn.fun_finsetProd (fun _ _ => by fun_prop)
63   have hd := (reducedTailProduct_locally_uniform hN M).differentiableOn
64     (Filter.Eventually.of_forall (fun s => by simpa only [Finset.prod_fn] using he s)) isOpen_univ
65   exact (differentiableOn_univ.mp hd).analyticAt w
66 
67 @[simp] theorem reducedTailProduct_zero (N M : ℕ) : reducedTailProduct N M 0 = 1 := by
68   simp [reducedTailProduct]
69 
70 theorem reducedTailProduct_ne_zero {N : ℕ} (hN : 3 ≤ N) (M : ℕ) {w : ℂ}
71     (hw : ∀ m : ℕ, w ≠ (reducedPositiveZero N (m + M) : ℂ)) :
72     reducedTailProduct N M w ≠ 0 := by
73   have hs : Summable (fun m => ‖-w / (reducedPositiveZero N (m + M) : ℂ)‖) := by
74     simpa only [neg_div, norm_neg] using reducedTail_factors_norm_summable hN M w
75   have hh := tprod_one_add_ne_zero_of_summable (f := fun m => -w / (reducedPositiveZero N (m + M) : ℂ))
76     (fun m => ?_) hs
77   · simpa only [reducedTailProduct, neg_div, ← sub_eq_add_neg] using! hh
78   · rw [neg_div, ← sub_eq_add_neg, sub_ne_zero]
79     intro h
80     apply hw m
81     exact (div_eq_one_iff_eq (Complex.ofReal_ne_zero.mpr (ne_of_gt (reducedPositiveZero_pos (by omega) _)))).mp h.symm
82 
83 /-- The convergent product has exactly the chosen sequence entries as zeros. -/
84 theorem reducedTailProduct_zero_iff {N : ℕ} (hN : 3 ≤ N) (M : ℕ) (w : ℂ) :
85     reducedTailProduct N M w = 0 ↔ ∃ m : ℕ, w = (reducedPositiveZero N (m + M) : ℂ) := by
86   constructor
87   · intro hz
88     by_contra h
89     push Not at h
90     exact reducedTailProduct_ne_zero hN M h hz
91   · rintro ⟨m, rfl⟩
92     apply tprod_of_exists_eq_zero
93     refine ⟨m, ?_⟩
94     rw [div_self (Complex.ofReal_ne_zero.mpr (ne_of_gt (reducedPositiveZero_pos (by omega) _))), sub_self]
95 
96 end
97 end Komorebi.PaperIV

Back to source controls