ZeroZetaContinuation.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroZetaDecomposition
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 open scoped Topology
11 
12 def reducedZetaCorrection {N : ℕ} (hN : 2 ≤ N) (s : ℂ) : ℂ :=
13   let e := canonicalZeroEnumeration hN
14   e.reducedExceptionZeta (by omega) s + e.latticeCorrection ((N : ℂ) * s) -
15     e.latticePrefix ((N : ℂ) * s)
16 
17 def absoluteZetaCorrection {N : ℕ} (hN : 2 ≤ N) (s : ℂ) : ℂ :=
18   let e := canonicalZeroEnumeration hN
19   e.absoluteExceptionZeta (by omega) s + (N : ℂ) * e.latticeCorrection s -
20     (N : ℂ) * e.latticePrefix s
21 
22 theorem reducedZetaCorrection_entire {N : ℕ} (hN : 2 ≤ N) :
23     Differentiable ℂ (reducedZetaCorrection hN) := by
24   unfold reducedZetaCorrection
25   exact ((canonicalZeroEnumeration hN).reducedExceptionZeta_entire (by omega)).add
26     (((canonicalZeroEnumeration hN).latticeCorrection_entire hN).comp (by fun_prop)) |>.sub
27       (((canonicalZeroEnumeration hN).latticePrefix_entire).comp (by fun_prop))
28 
29 theorem absoluteZetaCorrection_entire {N : ℕ} (hN : 2 ≤ N) :
30     Differentiable ℂ (absoluteZetaCorrection hN) := by
31   unfold absoluteZetaCorrection
32   exact ((canonicalZeroEnumeration hN).absoluteExceptionZeta_entire (by omega)).add
33     (((canonicalZeroEnumeration hN).latticeCorrection_entire hN).const_mul _) |>.sub
34       (((canonicalZeroEnumeration hN).latticePrefix_entire).const_mul _)
35 
36 /-- The manuscript's reduced formula, with its entire correction constructed
37 from the proved zero enumeration and actual exceptional zeros. -/
38 theorem entireReducedDenominator_zeta_eq_hurwitz {N : ℕ} (hN : 2 ≤ N)
39     {s : ℂ} (hs : 1 / (N : ℝ) < s.re) :
40     absoluteZeroZeta (entireReducedDenominator N) s =
41       hurwitzLatticeModel (Real.pi / Real.sin (Real.pi / N)) N s + reducedZetaCorrection hN s := by
42   let e := canonicalZeroEnumeration hN
43   have hsN : 1 < ((N : ℂ) * s).re := by
44     simp only [Complex.mul_re, Complex.natCast_re, Complex.natCast_im, zero_mul, sub_zero]
45     exact (div_lt_iff₀ (by exact_mod_cast (show 0 < N by omega) : (0 : ℝ) < N)).mp hs |>.trans_eq (mul_comm _ _)
46   rw [e.reducedZeta_decomposition hN hs, e.root_zeta_eq_model hN hsN]
47   simp only [hurwitzLatticeModel, Nat.cast_one, one_mul, reducedZetaCorrection]
48   dsimp [e]
49   ring
50 
51 theorem canonicalSignedDenominator_zeta_eq_hurwitz {N : ℕ} (hN : 2 ≤ N)
52     {s : ℂ} (hs : 1 < s.re) :
53     absoluteZeroZeta (canonicalSignedDenominator N) s =
54       (N : ℂ) * hurwitzLatticeModel (Real.pi / Real.sin (Real.pi / N)) 1 s +
55         absoluteZetaCorrection hN s := by
56   let e := canonicalZeroEnumeration hN
57   rw [e.absoluteZeta_decomposition hN hs, e.root_zeta_eq_model hN hs]
58   dsimp [absoluteZetaCorrection, e]
59   ring
60 
61 def reducedZetaContinuation {N : ℕ} (hN : 2 ≤ N) (s : ℂ) : ℂ :=
62   hurwitzLatticeModel (Real.pi / Real.sin (Real.pi / N)) N s + reducedZetaCorrection hN s
63 
64 def absoluteZetaContinuation {N : ℕ} (hN : 2 ≤ N) (s : ℂ) : ℂ :=
65   (N : ℂ) * hurwitzLatticeModel (Real.pi / Real.sin (Real.pi / N)) 1 s + absoluteZetaCorrection hN s
66 
67 theorem reducedZetaContinuation_meromorphic {N : ℕ} (hN : 2 ≤ N) (s : ℂ) :
68     MeromorphicAt (reducedZetaContinuation hN) s :=
69   (hurwitzLatticeModel_meromorphicAt _ _ s).add
70     ((reducedZetaCorrection_entire hN).analyticAt s).meromorphicAt
71 
72 theorem absoluteZetaContinuation_meromorphic {N : ℕ} (hN : 2 ≤ N) (s : ℂ) :
73     MeromorphicAt (absoluteZetaContinuation hN) s :=
74   ((MeromorphicAt.const (N : ℂ) s).mul (hurwitzLatticeModel_meromorphicAt _ _ s)).add
75     ((absoluteZetaCorrection_entire hN).analyticAt s).meromorphicAt
76 
77 theorem reducedZetaContinuation_holomorphic_off_pole {N : ℕ} (hN : 2 ≤ N)
78     {s : ℂ} (hs : s ≠ 1 / (N : ℂ)) : DifferentiableAt ℂ (reducedZetaContinuation hN) s :=
79   (hurwitzLatticeModel_differentiableAt (by omega) hs).add (reducedZetaCorrection_entire hN s)
80 
81 theorem absoluteZetaContinuation_holomorphic_off_pole {N : ℕ} (hN : 2 ≤ N)
82     {s : ℂ} (hs : s ≠ 1) : DifferentiableAt ℂ (absoluteZetaContinuation hN) s := by
83   have h : s ≠ 1 / ((1 : ℕ) : ℂ) := by simpa using hs
84   exact ((hurwitzLatticeModel_differentiableAt (by norm_num : 0 < (1 : ℕ)) h).const_mul _).add
85     (absoluteZetaCorrection_entire hN s)
86 
87 theorem entire_add_preserves_residue {f Q : ℂ → ℂ} {p r : ℂ}
88     (hQ : Differentiable ℂ Q)
89     (h : Tendsto (fun s => (s - p) * f s) (𝓝[≠] p) (𝓝 r)) :
90     Tendsto (fun s => (s - p) * (f s + Q s)) (𝓝[≠] p) (𝓝 r) := by
91   have ht : Tendsto (fun s => (s - p) * Q s) (𝓝[≠] p) (𝓝 0) := by
92     simpa only [sub_self, zero_mul] using
93       ((show Continuous (fun s => (s - p) * Q s) from (continuous_id.sub continuous_const).mul hQ.continuous).tendsto p).mono_left nhdsWithin_le_nhds
94   simpa only [mul_add, add_zero] using h.add ht
95 
96 theorem reducedZetaContinuation_residue {N : ℕ} (hN : 2 ≤ N) :
97     Tendsto (fun s : ℂ => (s - 1 / (N : ℂ)) * reducedZetaContinuation hN s)
98       (𝓝[≠] (1 / (N : ℂ))) (𝓝 ((Real.sin (Real.pi / N) / (N * Real.pi) : ℝ) : ℂ)) := by
99   have h := entire_add_preserves_residue (reducedZetaCorrection_entire hN)
100     (hurwitzLatticeModel_residue (div_pos Real.pi_pos (signed_sine_pos hN)) (show 0 < N by omega))
101   convert h using 1
102   congr 1
103   push_cast
104   field_simp
105 
106 theorem absoluteZetaContinuation_residue {N : ℕ} (hN : 2 ≤ N) :
107     Tendsto (fun s : ℂ => (s - 1) * absoluteZetaContinuation hN s)
108       (𝓝[≠] 1) (𝓝 ((N * Real.sin (Real.pi / N) / Real.pi : ℝ) : ℂ)) := by
109   have h := (hurwitzLatticeModel_residue (div_pos Real.pi_pos (signed_sine_pos hN))
110     (show 0 < (1 : ℕ) by norm_num)).const_mul (N : ℂ)
111   simp only [Nat.cast_one, one_div_one, one_mul] at h
112   have h' : Tendsto (fun s : ℂ => (s - 1) *
113       ((N : ℂ) * hurwitzLatticeModel (Real.pi / Real.sin (Real.pi / N)) 1 s))
114       (𝓝[≠] 1) (𝓝 ((N * Real.sin (Real.pi / N) / Real.pi : ℝ) : ℂ)) := by
115     convert h using 1
116     · funext s; ring
117     · congr 1; push_cast; field_simp
118   exact entire_add_preserves_residue (absoluteZetaCorrection_entire hN) h'
119 
120 theorem reducedZetaContinuation_simple_pole {N : ℕ} (hN : 2 ≤ N) :
121     meromorphicOrderAt (reducedZetaContinuation hN) (1 / (N : ℂ)) = (-1 : ℤ) := by
122   apply meromorphicOrderAt_eq_neg_one_of_residue (reducedZetaContinuation_meromorphic hN _)
123     (fun s hs => reducedZetaContinuation_holomorphic_off_pole hN hs) _ (reducedZetaContinuation_residue hN)
124   apply Complex.ofReal_ne_zero.mpr
125   exact ne_of_gt (div_pos (signed_sine_pos hN) (mul_pos (by exact_mod_cast (show 0 < N by omega)) Real.pi_pos))
126 
127 theorem absoluteZetaContinuation_simple_pole {N : ℕ} (hN : 2 ≤ N) :
128     meromorphicOrderAt (absoluteZetaContinuation hN) 1 = (-1 : ℤ) := by
129   apply meromorphicOrderAt_eq_neg_one_of_residue (absoluteZetaContinuation_meromorphic hN _)
130     (fun s hs => absoluteZetaContinuation_holomorphic_off_pole hN hs) _ (absoluteZetaContinuation_residue hN)
131   apply Complex.ofReal_ne_zero.mpr
132   exact ne_of_gt (div_pos (mul_pos (by exact_mod_cast (show 0 < N by omega)) (signed_sine_pos hN)) Real.pi_pos)
133 
134 end
135 end Komorebi.PaperIV

Back to source controls