ZeroZetaConvergence.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.FullZeroSummability
6 import Mathlib.Analysis.Complex.SummableUniformlyOn
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 def weightedDirichletTerm {ι : Type*} (w : ι → ℕ) (r : ι → ℝ) (i : ι) (s : ℂ) : ℂ :=
14   (w i : ℂ) * Complex.exp (-s * (Real.log (r i) : ℂ))
15 
16 theorem weightedDirichletTerm_norm {ι : Type*} (w : ι → ℕ) (r : ι → ℝ)
17     (hr : ∀ i, 0 < r i) (i : ι) (s : ℂ) :
18     ‖weightedDirichletTerm w r i s‖ = (w i : ℝ) / r i ^ s.re := by
19   rw [weightedDirichletTerm, norm_mul, Complex.norm_natCast, Complex.norm_exp]
20   simp only [Complex.mul_re, Complex.neg_re, Complex.neg_im, Complex.ofReal_re,
21     Complex.ofReal_im, mul_zero, sub_zero]
22   rw [Real.rpow_def_of_pos (hr i), div_eq_mul_inv, ← Real.exp_neg]
23   congr 2
24   ring
25 
26 theorem weightedDirichletTerm_differentiable {ι : Type*} (w : ι → ℕ) (r : ι → ℝ) (i : ι) :
27     Differentiable ℂ (weightedDirichletTerm w r i) := by
28   unfold weightedDirichletTerm
29   fun_prop
30 
31 theorem weightedDirichletTerm_strip_bound {ι : Type*} (w : ι → ℕ) (r : ι → ℝ)
32     (hr : ∀ i, 0 < r i) {a b : ℝ} {s : ℂ} (ha : a ≤ s.re) (hb : s.re ≤ b) (i : ι) :
33     ‖weightedDirichletTerm w r i s‖ ≤ (w i : ℝ) / r i ^ a + (w i : ℝ) / r i ^ b := by
34   rw [weightedDirichletTerm_norm w r hr]
35   simp only [Real.rpow_def_of_pos (hr i), div_eq_mul_inv, ← Real.exp_neg]
36   have hw := Nat.cast_nonneg (α := ℝ) (w i)
37   by_cases hl : 0 ≤ Real.log (r i)
38   · have he : Real.exp (-(Real.log (r i) * s.re)) ≤ Real.exp (-(Real.log (r i) * a)) := by
39       apply Real.exp_le_exp.mpr
40       nlinarith
41     exact (mul_le_mul_of_nonneg_left he hw).trans (le_add_of_nonneg_right (by positivity))
42   · have he : Real.exp (-(Real.log (r i) * s.re)) ≤ Real.exp (-(Real.log (r i) * b)) := by
43       apply Real.exp_le_exp.mpr
44       nlinarith
45     exact (mul_le_mul_of_nonneg_left he hw).trans (le_add_of_nonneg_left (by positivity))
46 
47 /-- A direct Weierstrass test on bounded vertical strips. Both sides of the
48 unit circle are controlled, so small radii require no implicit omission. -/
49 theorem weightedDirichlet_locally_uniform {ι : Type*} (w : ι → ℕ) (r : ι → ℝ)
50     (hr : ∀ i, 0 < r i) (c : ℝ)
51     (hs : ∀ t : ℝ, c < t → Summable (fun i => (w i : ℝ) / r i ^ t)) :
52     HasSumLocallyUniformlyOn (weightedDirichletTerm w r)
53       (fun s => ∑' i, weightedDirichletTerm w r i s) {s : ℂ | c < s.re} := by
54   apply hasSumLocallyUniformlyOn_of_of_forall_exists_nhds
55   intro s hs0
56   change c < s.re at hs0
57   let a := (c + s.re) / 2
58   let b := s.re + 1
59   have ha : c < a := by dsimp [a]; linarith [hs0]
60   have hb : c < b := by dsimp [b]; linarith [hs0]
61   let U : Set ℂ := {z | a < z.re ∧ z.re < b}
62   have hU : IsOpen U := (isOpen_lt continuous_const Complex.continuous_re).inter
63     (isOpen_lt Complex.continuous_re continuous_const)
64   have hsU : s ∈ U := by constructor <;> dsimp [a, b] <;> linarith [hs0]
65   refine ⟨U, mem_nhdsWithin_of_mem_nhds (hU.mem_nhds hsU), ?_⟩
66   apply hasSumUniformlyOn_iff_tendstoUniformlyOn.mpr
67   apply tendstoUniformlyOn_tsum ((hs a ha).add (hs b hb))
68   intro i z hz
69   exact weightedDirichletTerm_strip_bound w r hr hz.1.le hz.2.le i
70 
71 theorem weightedDirichlet_differentiableOn {ι : Type*} (w : ι → ℕ) (r : ι → ℝ)
72     (hr : ∀ i, 0 < r i) (c : ℝ)
73     (hs : ∀ t : ℝ, c < t → Summable (fun i => (w i : ℝ) / r i ^ t)) :
74     DifferentiableOn ℂ (fun s => ∑' i, weightedDirichletTerm w r i s) {s : ℂ | c < s.re} := by
75   apply (weightedDirichlet_locally_uniform w r hr c hs).summableLocallyUniformlyOn.differentiableOn
76     (isOpen_lt continuous_const Complex.continuous_re)
77   intro i s _
78   exact weightedDirichletTerm_differentiable w r i s
79 
80 /-- The exact absolute zero-zeta summand from the manuscript. -/
81 def absoluteZeroZetaTerm (f : ℂ → ℂ) (z : {z : ℂ // f z = 0}) (s : ℂ) : ℂ :=
82   weightedDirichletTerm (fun z : {z : ℂ // f z = 0} => analyticOrderNatAt f z)
83     (fun z => ‖(z : ℂ)‖) z s
84 
85 def absoluteZeroZeta (f : ℂ → ℂ) (s : ℂ) : ℂ := ∑' z, absoluteZeroZetaTerm f z s
86 
87 theorem zero_norm_pos_of_value_at_zero {f : ℂ → ℂ} (hf : f 0 ≠ 0)
88     (z : {z : ℂ // f z = 0}) : 0 < ‖(z : ℂ)‖ := by
89   apply norm_pos_iff.mpr
90   intro hz
91   have h := z.property
92   rw [hz] at h
93   exact hf h
94 
95 theorem absoluteZeroZetaTerm_norm {f : ℂ → ℂ} (hf : f 0 ≠ 0)
96     (z : {z : ℂ // f z = 0}) (s : ℂ) :
97     ‖absoluteZeroZetaTerm f z s‖ = (analyticOrderNatAt f z : ℝ) / ‖(z : ℂ)‖ ^ s.re :=
98   weightedDirichletTerm_norm _ _ (zero_norm_pos_of_value_at_zero hf) z s
99 
100 theorem absoluteZeroZeta_summable_norm_iff {f : ℂ → ℂ} (hf : f 0 ≠ 0) (s : ℂ) :
101     Summable (fun z => ‖absoluteZeroZetaTerm f z s‖) ↔ ZeroPowerSummable f s.re := by
102   simp only [absoluteZeroZetaTerm_norm hf, ZeroPowerSummable]
103 
104 theorem absoluteZeroZeta_locally_uniform {f : ℂ → ℂ} (hf : f 0 ≠ 0) (c : ℝ)
105     (hs : ∀ t, c < t → ZeroPowerSummable f t) :
106     HasSumLocallyUniformlyOn (absoluteZeroZetaTerm f) (absoluteZeroZeta f)
107       {s : ℂ | c < s.re} :=
108   weightedDirichlet_locally_uniform _ _ (zero_norm_pos_of_value_at_zero hf) c hs
109 
110 theorem absoluteZeroZeta_differentiableOn {f : ℂ → ℂ} (hf : f 0 ≠ 0) (c : ℝ)
111     (hs : ∀ t, c < t → ZeroPowerSummable f t) :
112     DifferentiableOn ℂ (absoluteZeroZeta f) {s : ℂ | c < s.re} :=
113   weightedDirichlet_differentiableOn _ _ (zero_norm_pos_of_value_at_zero hf) c hs
114 
115 /-- Exact absolute abscissa, including divergence on and to the left of the boundary. -/
116 theorem canonicalSignedDenominator_zeta_absolute_convergence {N : ℕ} (hN : 2 ≤ N) (s : ℂ) :
117     Summable (fun z => ‖absoluteZeroZetaTerm (canonicalSignedDenominator N) z s‖) ↔ 1 < s.re := by
118   rw [absoluteZeroZeta_summable_norm_iff (by rw [canonicalSignedDenominator_zero (by omega)]; exact one_ne_zero)]
119   exact canonicalSignedDenominator_zero_power_summable_iff hN s.re
120 
121 theorem canonicalSignedDenominator_zeta_locally_uniform {N : ℕ} (hN : 2 ≤ N) :
122     HasSumLocallyUniformlyOn (absoluteZeroZetaTerm (canonicalSignedDenominator N))
123       (absoluteZeroZeta (canonicalSignedDenominator N)) {s : ℂ | 1 < s.re} := by
124   apply absoluteZeroZeta_locally_uniform (by rw [canonicalSignedDenominator_zero (by omega)]; exact one_ne_zero)
125   intro t ht
126   exact (canonicalSignedDenominator_zero_power_summable_iff hN t).mpr ht
127 
128 theorem canonicalSignedDenominator_zeta_holomorphic {N : ℕ} (hN : 2 ≤ N) :
129     DifferentiableOn ℂ (absoluteZeroZeta (canonicalSignedDenominator N)) {s : ℂ | 1 < s.re} := by
130   apply absoluteZeroZeta_differentiableOn (by rw [canonicalSignedDenominator_zero (by omega)]; exact one_ne_zero)
131   intro t ht
132   exact (canonicalSignedDenominator_zero_power_summable_iff hN t).mpr ht
133 
134 theorem entireReducedDenominator_zeta_absolute_convergence {N : ℕ} (hN : 2 ≤ N) (s : ℂ) :
135     Summable (fun z => ‖absoluteZeroZetaTerm (entireReducedDenominator N) z s‖) ↔ 1 / (N : ℝ) < s.re := by
136   rw [absoluteZeroZeta_summable_norm_iff (by rw [entireReducedDenominator_zero]; exact one_ne_zero)]
137   exact entireReducedDenominator_zero_power_summable_iff hN s.re
138 
139 theorem entireReducedDenominator_zeta_locally_uniform {N : ℕ} (hN : 2 ≤ N) :
140     HasSumLocallyUniformlyOn (absoluteZeroZetaTerm (entireReducedDenominator N))
141       (absoluteZeroZeta (entireReducedDenominator N)) {s : ℂ | 1 / (N : ℝ) < s.re} := by
142   apply absoluteZeroZeta_locally_uniform (by rw [entireReducedDenominator_zero]; exact one_ne_zero)
143   intro t ht
144   exact (entireReducedDenominator_zero_power_summable_iff hN t).mpr ht
145 
146 theorem entireReducedDenominator_zeta_holomorphic {N : ℕ} (hN : 2 ≤ N) :
147     DifferentiableOn ℂ (absoluteZeroZeta (entireReducedDenominator N)) {s : ℂ | 1 / (N : ℝ) < s.re} := by
148   apply absoluteZeroZeta_differentiableOn (by rw [entireReducedDenominator_zero]; exact one_ne_zero)
149   intro t ht
150   exact (entireReducedDenominator_zero_power_summable_iff hN t).mpr ht
151 
152 end
153 end Komorebi.PaperIV

Back to source controls