ZeroLatticeComparison.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ExponentialZetaComparison
6 import KomorebiPaperIV.HurwitzLattice
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 theorem positiveZetaTerm_mul {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (s : ℂ) :
14     positiveZetaTerm (x * y) s = positiveZetaTerm x s * positiveZetaTerm y s := by
15   simp only [positiveZetaTerm, Real.log_mul hx.ne' hy.ne', Complex.ofReal_add, mul_add,
16     Complex.exp_add]
17 
18 theorem positiveZetaTerm_eq_cpow {x : ℝ} (hx : 0 < x) (s : ℂ) :
19     positiveZetaTerm x s = 1 / (x : ℂ) ^ s := by
20   rw [one_div, Complex.cpow_def_of_ne_zero (Complex.ofReal_ne_zero.mpr hx.ne'),
21     ← Complex.exp_neg, ← Complex.ofReal_log hx.le]
22   unfold positiveZetaTerm
23   congr 1
24   ring
25 
26 theorem positiveZetaTerm_norm {x : ℝ} (hx : 0 < x) (s : ℂ) :
27     ‖positiveZetaTerm x s‖ = 1 / x ^ s.re := by
28   simpa only [weightedDirichletTerm, Nat.cast_one, one_mul, positiveZetaTerm] using
29     weightedDirichletTerm_norm (fun _ : Unit => 1) (fun _ => x) (fun _ => hx) () s
30 
31 theorem positiveZetaTerm_lattice_hasSum {A : ℝ} (hA : 0 < A) (s : ℂ) (hs : 1 < s.re) :
32     HasSum (fun m : ℕ => positiveZetaTerm (A * ((m : ℝ) + 1 / 2)) s)
33       (hurwitzLatticeModel A 1 s) := by
34   have h := (HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re
35     (show (1 / 2 : ℝ) ∈ Icc 0 1 by constructor <;> norm_num) hs).mul_left (positiveZetaTerm A s)
36   convert! h using 1
37   · funext m
38     rw [positiveZetaTerm_mul hA (by positivity), positiveZetaTerm_eq_cpow (x := (m : ℝ) + 1 / 2) (by positivity)]
39     push_cast
40     rfl
41   · simp only [hurwitzLatticeModel, Nat.cast_one, one_mul, positiveZetaTerm]
42 
43 theorem signedZeroCenter_positive {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
44     0 < signedZeroCenter N m := by
45   unfold signedZeroCenter
46   exact mul_pos (div_pos Real.pi_pos (signed_sine_pos hN)) (by positivity)
47 
48 theorem signedZeroCenter_reciprocal_square_summable {N : ℕ} (hN : 2 ≤ N) :
49     Summable (fun m => 1 / signedZeroCenter N m ^ (2 : ℝ)) := by
50   have h := (positiveZetaTerm_lattice_hasSum
51     (div_pos Real.pi_pos (signed_sine_pos hN)) (2 : ℂ) (by norm_num)).summable.norm
52   change Summable (fun m => ‖positiveZetaTerm (signedZeroCenter N m) (2 : ℂ)‖) at h
53   simpa only [positiveZetaTerm_norm (signedZeroCenter_positive hN _), show (2 : ℂ).re = (2 : ℝ) by rfl] using! h
54 
55 theorem SignedZeroEnumeration.root_tendsto_atTop {N : ℕ} (hN : 2 ≤ N)
56     (e : SignedZeroEnumeration N) : Tendsto e.root atTop atTop := by
57   exact (e.root_equivalent_lattice hN).symm.tendsto_atTop
58     ((tendsto_natCast_atTop_atTop (R := ℝ)).const_mul_atTop
59       (div_pos Real.pi_pos (signed_sine_pos hN)))
60 
61 def SignedZeroEnumeration.latticeCorrection {N : ℕ} (e : SignedZeroEnumeration N) (s : ℂ) : ℂ :=
62   ∑' m, exponentialZetaDifference e.root (fun j => signedZeroCenter N (j + e.offset)) m s
63 
64 theorem SignedZeroEnumeration.latticeCorrection_locally_uniform {N : ℕ} (hN : 2 ≤ N)
65     (e : SignedZeroEnumeration N) :
66     HasSumLocallyUniformlyOn
67       (exponentialZetaDifference e.root (fun j => signedZeroCenter N (j + e.offset)))
68       e.latticeCorrection univ := by
69   obtain ⟨C, hC, γ, hγ, hdisp⟩ := e.displacement
70   apply exponentialZetaDifference_locally_uniform
71     (fun m => signedZeroCenter_positive hN _) (e.root_tendsto_atTop hN)
72     ((signedZeroCenter_tendsto_atTop hN).comp (tendsto_add_atTop_nat e.offset))
73     ((signedZeroCenter_reciprocal_square_summable hN).comp_injective (fun _ _ h => Nat.add_right_cancel h))
74     hC hγ
75   exact Eventually.of_forall hdisp
76 
77 theorem SignedZeroEnumeration.latticeCorrection_entire {N : ℕ} (hN : 2 ≤ N)
78     (e : SignedZeroEnumeration N) : Differentiable ℂ e.latticeCorrection := by
79   apply differentiableOn_univ.mp
80   exact (e.latticeCorrection_locally_uniform hN).summableLocallyUniformlyOn.differentiableOn
81     isOpen_univ (fun m s _ => exponentialZetaDifference_entire _ _ m s)
82 
83 theorem SignedZeroEnumeration.positiveZetaTerm_summable {N : ℕ} (hN : 2 ≤ N)
84     (e : SignedZeroEnumeration N) {s : ℂ} (hs : 1 < s.re) :
85     Summable (fun m => positiveZetaTerm (e.root m) s) := by
86   apply Summable.of_norm
87   simp only [positiveZetaTerm_norm (e.positive _)]
88   exact (e.root_reciprocal_rpow_summable_iff hN _).mpr hs
89 
90 def SignedZeroEnumeration.latticePrefix {N : ℕ} (e : SignedZeroEnumeration N) (s : ℂ) : ℂ :=
91   ∑ m ∈ Finset.range e.offset, positiveZetaTerm (signedZeroCenter N m) s
92 
93 theorem SignedZeroEnumeration.latticePrefix_entire {N : ℕ} (e : SignedZeroEnumeration N) :
94     Differentiable ℂ e.latticePrefix := by
95   unfold SignedZeroEnumeration.latticePrefix
96   exact Differentiable.fun_sum (fun m _ => positiveZetaTerm_entire _)
97 
98 /-- Equality with the unshifted Hurwitz model; the finite prefix is retained. -/
99 theorem SignedZeroEnumeration.root_zeta_eq_model {N : ℕ} (hN : 2 ≤ N)
100     (e : SignedZeroEnumeration N) {s : ℂ} (hs : 1 < s.re) :
101     (∑' m, positiveZetaTerm (e.root m) s) =
102       hurwitzLatticeModel (Real.pi / Real.sin (Real.pi / N)) 1 s +
103         e.latticeCorrection s - e.latticePrefix s := by
104   have hmodel := positiveZetaTerm_lattice_hasSum
105     (div_pos Real.pi_pos (signed_sine_pos hN)) s hs
106   have hsum := hmodel.summable
107   have htail := hsum.comp_injective (fun _ _ h => Nat.add_right_cancel h :
108     Function.Injective (fun m : ℕ => m + e.offset))
109   have hc : e.latticeCorrection s = (∑' m, positiveZetaTerm (e.root m) s) -
110       ∑' m, positiveZetaTerm (signedZeroCenter N (m + e.offset)) s :=
111     (e.positiveZetaTerm_summable hN hs).tsum_sub htail
112   have hp := hsum.sum_add_tsum_nat_add e.offset
113   rw [hmodel.tsum_eq] at hp
114   change e.latticePrefix s + (∑' m, positiveZetaTerm (signedZeroCenter N (m + e.offset)) s) = _ at hp
115   rw [hc]
116   linear_combination hp
117 
118 end
119 end Komorebi.PaperIV

Back to source controls