BranchZetaContinuation.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroZetaContinuation
6 import KomorebiPaperIV.BranchedDirichlet
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 /-- A chosen logarithm at each distinct zero, with the actual multiplicity. -/
14 def branchedZeroZetaTerm (f : ℂ → ℂ) (L : {z : ℂ // f z = 0} → ℂ)
15     (z : {z : ℂ // f z = 0}) (s : ℂ) : ℂ :=
16   (analyticOrderNatAt f z : ℂ) * Complex.exp (-s * L z)
17 
18 def branchedZeroZeta (f : ℂ → ℂ) (L : {z : ℂ // f z = 0} → ℂ) (s : ℂ) : ℂ :=
19   ∑' z, branchedZeroZetaTerm f L z s
20 
21 theorem branchedZeroZetaTerm_entire (f : ℂ → ℂ) (L : {z : ℂ // f z = 0} → ℂ)
22     (z : {z : ℂ // f z = 0}) : Differentiable ℂ (branchedZeroZetaTerm f L z) := by
23   unfold branchedZeroZetaTerm
24   fun_prop
25 
26 /-- This support condition allows every logarithm choice on the finite exceptional
27 set, and requires the real logarithm on the proved positive tail. The results
28 below hold for arbitrary exceptional values, hence in particular for logarithms. -/
29 def RealLogOnReducedTail {N : ℕ} (hN : 2 ≤ N)
30     (L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) : Prop :=
31   ∀ m, L ((canonicalZeroEnumeration hN).reducedZero (by omega) m) =
32     (Real.log ‖((canonicalZeroEnumeration hN).reducedRoot m)‖ : ℂ)
33 
34 def reducedBranchCorrection {N : ℕ} (hN : 2 ≤ N)
35     (L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) (s : ℂ) : ℂ :=
36   ∑' z : ↥((range ((canonicalZeroEnumeration hN).reducedZero (by omega)))ᶜ),
37     (branchedZeroZetaTerm (entireReducedDenominator N) L z.val s -
38       absoluteZeroZetaTerm (entireReducedDenominator N) z.val s)
39 
40 theorem reducedBranchCorrection_entire {N : ℕ} (hN : 2 ≤ N)
41     (L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) :
42     Differentiable ℂ (reducedBranchCorrection hN L) := by
43   unfold reducedBranchCorrection
44   exact finite_subtype_tsum_entire ((canonicalZeroEnumeration hN).reducedZero_finite_complement (by omega))
45     (fun z s => branchedZeroZetaTerm (entireReducedDenominator N) L z s -
46       absoluteZeroZetaTerm (entireReducedDenominator N) z s)
47     (fun z => (branchedZeroZetaTerm_entire _ _ z).sub (absoluteZeroZetaTerm_entire _ z))
48 
49 theorem branchedZeroZetaTerm_eq_absolute_on_tail {N : ℕ} (hN : 2 ≤ N)
50     {L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ}
51     (hL : RealLogOnReducedTail hN L) (m : ℕ) (s : ℂ) :
52     branchedZeroZetaTerm (entireReducedDenominator N) L
53       ((canonicalZeroEnumeration hN).reducedZero (by omega) m) s =
54     absoluteZeroZetaTerm (entireReducedDenominator N)
55       ((canonicalZeroEnumeration hN).reducedZero (by omega) m) s := by
56   simp only [branchedZeroZetaTerm, absoluteZeroZetaTerm, weightedDirichletTerm, hL m]
57   rfl
58 
59 theorem branchedReducedZeta_summable {N : ℕ} (hN : 2 ≤ N)
60     {L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ}
61     (hL : RealLogOnReducedTail hN L) {s : ℂ} (hs : 1 / (N : ℝ) < s.re) :
62     Summable (fun z => branchedZeroZetaTerm (entireReducedDenominator N) L z s) := by
63   let e := canonicalZeroEnumeration hN
64   have hc := e.reducedZero_finite_complement (by omega)
65   have ha := ((entireReducedDenominator_zeta_absolute_convergence hN s).mpr hs).of_norm
66   have hr : Summable (fun z : range (e.reducedZero (by omega)) =>
67       branchedZeroZetaTerm (entireReducedDenominator N) L z.val s) := by
68     apply (ha.subtype _).congr
69     intro z
70     change absoluteZeroZetaTerm (entireReducedDenominator N) z.val s =
71       branchedZeroZetaTerm (entireReducedDenominator N) L z.val s
72     obtain ⟨m, hm⟩ := z.property
73     rw [← hm]
74     exact (branchedZeroZetaTerm_eq_absolute_on_tail hN hL m s).symm
75   have he := hc.summable_compl_iff (f := fun z => branchedZeroZetaTerm (entireReducedDenominator N) L z s)
76   rw [compl_compl] at he
77   exact he.mp hr
78 
79 theorem branchedReducedZeta_eq_absolute_add_entire {N : ℕ} (hN : 2 ≤ N)
80     {L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ}
81     (hL : RealLogOnReducedTail hN L) {s : ℂ} (hs : 1 / (N : ℝ) < s.re) :
82     branchedZeroZeta (entireReducedDenominator N) L s =
83       absoluteZeroZeta (entireReducedDenominator N) s + reducedBranchCorrection hN L s := by
84   let e := canonicalZeroEnumeration hN
85   have ha := ((entireReducedDenominator_zeta_absolute_convergence hN s).mpr hs).of_norm
86   have hb := branchedReducedZeta_summable hN hL hs
87   have hea := tsum_injection_add_complement (e.reducedZero (by omega)) (e.reducedZero_injective (by omega)) ha
88   have heb := tsum_injection_add_complement (e.reducedZero (by omega)) (e.reducedZero_injective (by omega)) hb
89   have hc : reducedBranchCorrection hN L s =
90       (∑' z : ↥((range (e.reducedZero (by omega)))ᶜ), branchedZeroZetaTerm (entireReducedDenominator N) L z.val s) -
91       ∑' z : ↥((range (e.reducedZero (by omega)))ᶜ), absoluteZeroZetaTerm (entireReducedDenominator N) z.val s :=
92     (hb.subtype _).tsum_sub (ha.subtype _)
93   have htail : (fun m => branchedZeroZetaTerm (entireReducedDenominator N) L (e.reducedZero (by omega) m) s) =
94       (fun m => absoluteZeroZetaTerm (entireReducedDenominator N) (e.reducedZero (by omega) m) s) := by
95     funext m
96     exact branchedZeroZetaTerm_eq_absolute_on_tail hN hL m s
97   rw [htail] at heb
98   change _ = branchedZeroZeta (entireReducedDenominator N) L s at heb
99   change _ = absoluteZeroZeta (entireReducedDenominator N) s at hea
100   rw [hc]
101   linear_combination hea - heb
102 
103 def branchedReducedZetaContinuation {N : ℕ} (hN : 2 ≤ N)
104     (L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) (s : ℂ) : ℂ :=
105   reducedZetaContinuation hN s + reducedBranchCorrection hN L s
106 
107 theorem branchedReducedZetaContinuation_eq {N : ℕ} (hN : 2 ≤ N)
108     {L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ}
109     (hL : RealLogOnReducedTail hN L) {s : ℂ} (hs : 1 / (N : ℝ) < s.re) :
110     branchedZeroZeta (entireReducedDenominator N) L s = branchedReducedZetaContinuation hN L s := by
111   rw [branchedReducedZeta_eq_absolute_add_entire hN hL hs, entireReducedDenominator_zeta_eq_hurwitz hN hs]
112   rfl
113 
114 theorem branchedReducedZetaContinuation_meromorphic {N : ℕ} (hN : 2 ≤ N)
115     (L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) (s : ℂ) :
116     MeromorphicAt (branchedReducedZetaContinuation hN L) s :=
117   (reducedZetaContinuation_meromorphic hN s).add
118     ((reducedBranchCorrection_entire hN L).analyticAt s).meromorphicAt
119 
120 theorem branchedReducedZetaContinuation_holomorphic_off_pole {N : ℕ} (hN : 2 ≤ N)
121     (L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) {s : ℂ}
122     (hs : s ≠ 1 / (N : ℂ)) : DifferentiableAt ℂ (branchedReducedZetaContinuation hN L) s :=
123   (reducedZetaContinuation_holomorphic_off_pole hN hs).add (reducedBranchCorrection_entire hN L s)
124 
125 theorem branchedReducedZetaContinuation_residue {N : ℕ} (hN : 2 ≤ N)
126     (L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) :
127     Tendsto (fun s : ℂ => (s - 1 / (N : ℂ)) * branchedReducedZetaContinuation hN L s)
128       (𝓝[≠] (1 / (N : ℂ))) (𝓝 ((Real.sin (Real.pi / N) / (N * Real.pi) : ℝ) : ℂ)) :=
129   entire_add_preserves_residue (reducedBranchCorrection_entire hN L) (reducedZetaContinuation_residue hN)
130 
131 theorem branchedReducedZetaContinuation_simple_pole {N : ℕ} (hN : 2 ≤ N)
132     (L : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) :
133     meromorphicOrderAt (branchedReducedZetaContinuation hN L) (1 / (N : ℂ)) = (-1 : ℤ) := by
134   apply meromorphicOrderAt_eq_neg_one_of_residue (branchedReducedZetaContinuation_meromorphic hN L _)
135     (fun s hs => branchedReducedZetaContinuation_holomorphic_off_pole hN L hs) _
136     (branchedReducedZetaContinuation_residue hN L)
137   apply Complex.ofReal_ne_zero.mpr
138   exact ne_of_gt (div_pos (signed_sine_pos hN) (mul_pos (by exact_mod_cast (show 0 < N by omega)) Real.pi_pos))
139 
140 /-- Any two allowed choices have an entire difference of continuations. -/
141 theorem branchedReducedZetaContinuation_difference_entire {N : ℕ} (hN : 2 ≤ N)
142     (L M : {z : ℂ // entireReducedDenominator N z = 0} → ℂ) :
143     Differentiable ℂ (fun s => branchedReducedZetaContinuation hN L s -
144       branchedReducedZetaContinuation hN M s) := by
145   have he : (fun s => branchedReducedZetaContinuation hN L s - branchedReducedZetaContinuation hN M s) =
146       (fun s => reducedBranchCorrection hN L s - reducedBranchCorrection hN M s) := by
147     funext s
148     unfold branchedReducedZetaContinuation
149     ring
150   rw [he]
151   exact (reducedBranchCorrection_entire hN L).sub (reducedBranchCorrection_entire hN M)
152 
153 end
154 end Komorebi.PaperIV

Back to source controls