DerivativeWeightedZeta.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.DerivativeGrowth
6 import KomorebiPaperIV.BranchedDirichlet
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 /-- Exactly the simple zeros: possible multiple exceptional zeros are omitted,
14 as specified by the manuscript's definition. -/
15 abbrev SimpleZeros (f : ℂ → ℂ) := {z : ℂ // f z = 0 ∧ deriv f z ≠ 0}
16 
17 def SimpleZeros.toZero {f : ℂ → ℂ} (z : SimpleZeros f) : {z : ℂ // f z = 0} :=
18   ⟨z.val, z.property.1⟩
19 
20 theorem SimpleZeros.toZero_injective (f : ℂ → ℂ) :
21     Function.Injective (SimpleZeros.toZero (f := f)) := by
22   intro a b h
23   exact Subtype.ext (congrArg (fun z : {z : ℂ // f z = 0} => z.val) h)
24 
25 theorem SimpleZeros.order_one {f : ℂ → ℂ} (hf : ∀ z, AnalyticAt ℂ f z) (z : SimpleZeros f) :
26     analyticOrderNatAt f z.val = 1 := by
27   rw [analyticOrderNatAt, (hf z.val).analyticOrderAt_eq_one_of_zero_deriv_ne_zero
28     z.property.1 z.property.2]
29   rfl
30 
31 theorem canonicalSignedDenominator_simple_zero_power_summable {N : ℕ} (hN : 2 ≤ N)
32     {t : ℝ} (ht : 1 < t) :
33     Summable (fun z : SimpleZeros (canonicalSignedDenominator N) => 1 / ‖z.val‖ ^ t) := by
34   have h := (canonicalSignedDenominator_zero_power_summable_iff hN t).mpr ht
35   have hi := h.comp_injective (SimpleZeros.toZero_injective (canonicalSignedDenominator N))
36   change Summable (fun z : SimpleZeros (canonicalSignedDenominator N) =>
37     (analyticOrderNatAt (canonicalSignedDenominator N) z.val : ℝ) / ‖z.val‖ ^ t) at hi
38   convert hi using 1
39   funext z
40   rw [SimpleZeros.order_one (f := canonicalSignedDenominator N)
41     (fun w => analyticAt_entireSigned N 0 _ _ w) z, Nat.cast_one]
42 
43 theorem simple_logarithm_re {f : ℂ → ℂ} (L : SimpleZeros f → ℂ)
44     (hL : ∀ z, Complex.exp (L z) = z.val) (z : SimpleZeros f) :
45     (L z).re = Real.log ‖z.val‖ := by
46   have h := congrArg norm (hL z)
47   rw [Complex.norm_exp] at h
48   rw [← h, Real.log_exp]
49 
50 def derivativeZeroWeight (N q : ℕ) (z : SimpleZeros (canonicalSignedDenominator N)) : ℂ :=
51   (deriv (canonicalSignedDenominator N) z.val ^ q)⁻¹
52 
53 theorem derivativeZeroWeight_norm (N q : ℕ) (z : SimpleZeros (canonicalSignedDenominator N)) :
54     ‖derivativeZeroWeight N q z‖ = 1 / ‖deriv (canonicalSignedDenominator N) z.val‖ ^ q := by
55   simp only [derivativeZeroWeight, norm_inv, norm_pow, one_div]
56 
57 /-- Every real polynomial weight is summable against the derivative decay,
58 including the finite exceptional simple zeros. -/
59 theorem derivativeZeroWeight_power_summable {N q : ℕ} (hN : 3 ≤ N) (hq : 0 < q) (t : ℝ) :
60     Summable (fun z : SimpleZeros (canonicalSignedDenominator N) =>
61       ‖derivativeZeroWeight N q z‖ / ‖z.val‖ ^ t) := by
62   have hs := canonicalSignedDenominator_simple_zero_power_summable (show 2 ≤ N by omega)
63     (show (1 : ℝ) < 2 by norm_num)
64   apply hs.of_norm_bounded_eventually
65   obtain ⟨R, _, hR⟩ := canonicalSignedDenominator_derivative_power_bound hN hq t
66   have hf : ((fun z : SimpleZeros (canonicalSignedDenominator N) => z.val) ⁻¹'
67       zeroDisk (canonicalSignedDenominator N) R).Finite :=
68     (canonicalSignedDenominator_zeroDisk_finite (show 0 < N by omega) R).preimage
69       Subtype.val_injective.injOn
70   have hb : ∀ᶠ z : SimpleZeros (canonicalSignedDenominator N) in cofinite, R ≤ ‖z.val‖ := by
71     apply eventually_cofinite.mpr
72     apply hf.subset
73     intro z hz
74     exact ⟨(not_le.mp hz).le, z.property.1⟩
75   filter_upwards [hb] with z hz
76   rw [Real.norm_eq_abs, abs_of_nonneg (by positivity), derivativeZeroWeight_norm]
77   exact hR z.val hz z.property.1
78 
79 theorem canonicalSignedDenominator_two_derivative_norm {z : ℂ}
80     (hz : canonicalSignedDenominator 2 z = 0) : ‖deriv (canonicalSignedDenominator 2) z‖ = 1 := by
81   have he : canonicalSignedDenominator 2 = Complex.cos := funext
82     (entireSigned_two_eq_cos (canonicalPrimitiveRoot_isPrimitive (by norm_num : 0 < 2))
83       (canonicalSignedRoot_pow (by norm_num : 0 < 2)))
84   rw [he, Complex.deriv_cos, norm_neg]
85   rw [he] at hz
86   have hs := Complex.sin_sq_add_cos_sq z
87   rw [hz, zero_pow (by norm_num : (2 : ℕ) ≠ 0), add_zero] at hs
88   have hn := congrArg norm hs
89   rw [norm_pow, norm_one] at hn
90   nlinarith [norm_nonneg (Complex.sin z)]
91 
92 theorem derivativeZeroWeight_two_power_summable (q : ℕ) {t : ℝ} (ht : 1 < t) :
93     Summable (fun z : SimpleZeros (canonicalSignedDenominator 2) =>
94       ‖derivativeZeroWeight 2 q z‖ / ‖z.val‖ ^ t) := by
95   convert canonicalSignedDenominator_simple_zero_power_summable (by norm_num : 2 ≤ 2) ht using 1
96   funext z
97   simp only [derivativeZeroWeight_norm, canonicalSignedDenominator_two_derivative_norm z.property.1,
98     one_pow, div_one]
99 
100 def derivativeWeightedZeroZetaTerm (N q : ℕ)
101     (L : SimpleZeros (canonicalSignedDenominator N) → ℂ)
102     (z : SimpleZeros (canonicalSignedDenominator N)) (s : ℂ) : ℂ :=
103   branchedDirichletTerm (derivativeZeroWeight N q) L z s
104 
105 def derivativeWeightedZeroZeta (N q : ℕ)
106     (L : SimpleZeros (canonicalSignedDenominator N) → ℂ) (s : ℂ) : ℂ :=
107   ∑' z, derivativeWeightedZeroZetaTerm N q L z s
108 
109 theorem derivativeWeightedZeroZetaTerm_eq (N q : ℕ)
110     (L : SimpleZeros (canonicalSignedDenominator N) → ℂ)
111     (z : SimpleZeros (canonicalSignedDenominator N)) (s : ℂ) :
112     derivativeWeightedZeroZetaTerm N q L z s =
113       Complex.exp (-s * L z) / deriv (canonicalSignedDenominator N) z.val ^ q := by
114   unfold derivativeWeightedZeroZetaTerm branchedDirichletTerm derivativeZeroWeight
115   ring
116 
117 theorem derivativeWeightedZeroZeta_summable_norm {N q : ℕ} (hN : 3 ≤ N) (hq : 0 < q)
118     (L : SimpleZeros (canonicalSignedDenominator N) → ℂ)
119     (hL : ∀ z, Complex.exp (L z) = z.val)
120     {B : ℝ} (hB : 0 ≤ B) (harg : ∀ z, |(L z).im| ≤ B) (s : ℂ) :
121     Summable (fun z => ‖derivativeWeightedZeroZetaTerm N q L z s‖) := by
122   apply branchedDirichlet_summable_norm (derivativeZeroWeight N q) L (fun z => ‖z.val‖)
123     _ (simple_logarithm_re L hL) hB harg s (derivativeZeroWeight_power_summable hN hq s.re)
124   intro z
125   exact zero_norm_pos_of_value_at_zero
126     (by rw [canonicalSignedDenominator_zero (by omega)]; exact one_ne_zero) z.toZero
127 
128 theorem derivativeWeightedZeroZeta_two_summable_norm (q : ℕ)
129     (L : SimpleZeros (canonicalSignedDenominator 2) → ℂ)
130     (hL : ∀ z, Complex.exp (L z) = z.val)
131     {B : ℝ} (hB : 0 ≤ B) (harg : ∀ z, |(L z).im| ≤ B) {s : ℂ} (hs : 1 < s.re) :
132     Summable (fun z => ‖derivativeWeightedZeroZetaTerm 2 q L z s‖) := by
133   apply branchedDirichlet_summable_norm (derivativeZeroWeight 2 q) L (fun z => ‖z.val‖)
134     _ (simple_logarithm_re L hL) hB harg s (derivativeZeroWeight_two_power_summable q hs)
135   intro z
136   exact zero_norm_pos_of_value_at_zero
137     (by rw [canonicalSignedDenominator_zero (by norm_num : 0 < 2)]; exact one_ne_zero) z.toZero
138 
139 /-- Paper IV 14.8, N≥3: the actual derivative-weighted series is locally
140 uniformly convergent on the whole plane and has an entire sum. -/
141 theorem derivativeWeightedZeroZeta_entire {N q : ℕ} (hN : 3 ≤ N) (hq : 0 < q)
142     (L : SimpleZeros (canonicalSignedDenominator N) → ℂ)
143     (hL : ∀ z, Complex.exp (L z) = z.val)
144     {B : ℝ} (hB : 0 ≤ B) (harg : ∀ z, |(L z).im| ≤ B) :
145     HasSumLocallyUniformlyOn (derivativeWeightedZeroZetaTerm N q L)
146       (derivativeWeightedZeroZeta N q L) univ ∧
147     Differentiable ℂ (derivativeWeightedZeroZeta N q L) := by
148   apply branchedDirichlet_entire (derivativeZeroWeight N q) L (fun z => ‖z.val‖)
149     _ (simple_logarithm_re L hL) hB harg (derivativeZeroWeight_power_summable hN hq)
150   intro z
151   exact zero_norm_pos_of_value_at_zero
152     (by rw [canonicalSignedDenominator_zero (by omega)]; exact one_ne_zero) z.toZero
153 
154 /-- Paper IV 14.8, N=2: local uniform convergence and holomorphy on Re(s)>1,
155 with arbitrary bounded logarithmic arguments. -/
156 theorem derivativeWeightedZeroZeta_two_holomorphic (q : ℕ)
157     (L : SimpleZeros (canonicalSignedDenominator 2) → ℂ)
158     (hL : ∀ z, Complex.exp (L z) = z.val)
159     {B : ℝ} (hB : 0 ≤ B) (harg : ∀ z, |(L z).im| ≤ B) :
160     HasSumLocallyUniformlyOn (derivativeWeightedZeroZetaTerm 2 q L)
161       (derivativeWeightedZeroZeta 2 q L) {s : ℂ | 1 < s.re} ∧
162     DifferentiableOn ℂ (derivativeWeightedZeroZeta 2 q L) {s : ℂ | 1 < s.re} := by
163   apply branchedDirichlet_halfplane (derivativeZeroWeight 2 q) L (fun z => ‖z.val‖)
164     _ (simple_logarithm_re L hL) hB harg 1 (fun t ht => derivativeZeroWeight_two_power_summable q ht)
165   intro z
166   exact zero_norm_pos_of_value_at_zero
167     (by rw [canonicalSignedDenominator_zero (by norm_num : 0 < 2)]; exact one_ne_zero) z.toZero
168 
169 end
170 end Komorebi.PaperIV

Back to source controls