HurwitzLattice.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import Mathlib.NumberTheory.LSeries.HurwitzZeta
6 import Mathlib.Analysis.Meromorphic.Order
7 import Mathlib.Analysis.Complex.RemovableSingularity
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter Complex
12 open scoped Topology
13 
14 /-- The entire remainder in Mathlib's regularized Hurwitz representation. -/
15 def hurwitzRegularPart (a : UnitAddCircle) (s : ℂ) : ℂ :=
16   HurwitzZeta.hurwitzZeta a s - (s - 1)⁻¹ * (Gammaℝ s)⁻¹
17 
18 theorem hurwitzRegularPart_entire (a : UnitAddCircle) :
19     Differentiable ℂ (hurwitzRegularPart a) := by
20   unfold hurwitzRegularPart
21   intro s
22   by_cases hs : s = 1
23   · subst s
24     simpa only [one_div, div_eq_mul_inv, one_mul] using!
25       HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div a
26   · exact (HurwitzZeta.differentiableAt_hurwitzZeta a hs).sub
27       (((show DifferentiableAt ℂ (fun z : ℂ => z - 1) s by fun_prop).inv (sub_ne_zero.mpr hs)).mul
28         (differentiable_Gammaℝ_inv s))
29 
30 theorem hurwitzZeta_meromorphicAt (a : UnitAddCircle) (s : ℂ) :
31     MeromorphicAt (HurwitzZeta.hurwitzZeta a) s := by
32   have he : HurwitzZeta.hurwitzZeta a = fun z => hurwitzRegularPart a z +
33       (z - 1)⁻¹ * (Gammaℝ z)⁻¹ := by funext z; unfold hurwitzRegularPart; ring
34   rw [he]
35   exact ((hurwitzRegularPart_entire a).analyticAt s).meromorphicAt.add
36     ((((MeromorphicAt.id s).sub (MeromorphicAt.const 1 s)).inv).mul
37       ((differentiable_Gammaℝ_inv.analyticAt s).meromorphicAt))
38 
39 /-- Positive lattice model, with argument scaled by the integer d. -/
40 def hurwitzLatticeModel (A : ℝ) (d : ℕ) (s : ℂ) : ℂ :=
41   exp (-((d : ℂ) * s) * (Real.log A : ℂ)) *
42     HurwitzZeta.hurwitzZeta (1 / 2 : ℝ) ((d : ℂ) * s)
43 
44 theorem hurwitzLatticeModel_meromorphicAt (A : ℝ) (d : ℕ) (s : ℂ) :
45     MeromorphicAt (hurwitzLatticeModel A d) s := by
46   apply MeromorphicAt.mul
47   · exact (show Differentiable ℂ (fun z : ℂ => exp (-((d : ℂ) * z) * (Real.log A : ℂ))) by
48       fun_prop).analyticAt s |>.meromorphicAt
49   · exact (hurwitzZeta_meromorphicAt _ _).comp_analyticAt (by fun_prop)
50 
51 theorem hurwitzLatticeModel_differentiableAt {A : ℝ} {d : ℕ} (hd : 0 < d)
52     {s : ℂ} (hs : s ≠ 1 / (d : ℂ)) : DifferentiableAt ℂ (hurwitzLatticeModel A d) s := by
53   have hd0 : (d : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr hd.ne'
54   have hds : (d : ℂ) * s ≠ 1 := by
55     intro h
56     apply hs
57     apply (eq_div_iff hd0).mpr
58     simpa only [mul_comm] using h
59   apply DifferentiableAt.mul
60   · fun_prop
61   · exact (HurwitzZeta.differentiableAt_hurwitzZeta _ hds).comp s (by fun_prop)
62 
63 theorem hurwitzLatticeModel_residue {A : ℝ} (hA : 0 < A) {d : ℕ} (hd : 0 < d) :
64     Tendsto (fun s : ℂ => (s - 1 / (d : ℂ)) * hurwitzLatticeModel A d s)
65       (𝓝[≠] (1 / (d : ℂ))) (𝓝 (1 / ((d : ℂ) * A))) := by
66   have hd0 : (d : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr hd.ne'
67   have ht : Tendsto (fun s : ℂ => (d : ℂ) * s) (𝓝[≠] (1 / (d : ℂ))) (𝓝[≠] 1) := by
68     rw [tendsto_nhdsWithin_iff]
69     constructor
70     · simpa only [mul_one_div_cancel hd0] using
71         ((show Continuous (fun s : ℂ => (d : ℂ) * s) by fun_prop).tendsto (1 / (d : ℂ))).mono_left nhdsWithin_le_nhds
72     · filter_upwards [self_mem_nhdsWithin] with s hs
73       change s ≠ 1 / (d : ℂ) at hs
74       change (d : ℂ) * s ≠ 1
75       intro h
76       exact hs ((eq_div_iff hd0).mpr (by simpa only [mul_comm] using h))
77   have hz := (HurwitzZeta.hurwitzZeta_residue_one (1 / 2 : ℝ)).comp ht
78   have he : Tendsto (fun s : ℂ => exp (-((d : ℂ) * s) * (Real.log A : ℂ)))
79       (𝓝[≠] (1 / (d : ℂ))) (𝓝 ((A : ℂ)⁻¹)) := by
80     have h := (show Continuous (fun s : ℂ => exp (-((d : ℂ) * s) * (Real.log A : ℂ))) by
81       fun_prop).tendsto (1 / (d : ℂ))
82     have hv : exp (-((d : ℂ) * (1 / (d : ℂ))) * (Real.log A : ℂ)) = (A : ℂ)⁻¹ := by
83       rw [mul_one_div_cancel hd0, neg_one_mul, exp_neg, ← ofReal_exp, Real.exp_log hA]
84     rw [hv] at h
85     exact h.mono_left nhdsWithin_le_nhds
86   have h := (he.mul hz).const_mul (1 / (d : ℂ))
87   convert h using 1
88   · funext s
89     simp only [Function.comp_apply, hurwitzLatticeModel]
90     field_simp
91   · congr 1
92     field_simp
93 
94 /-- A nonzero punctured residue makes the pole genuinely simple. -/
95 theorem meromorphicOrderAt_eq_neg_one_of_residue {f : ℂ → ℂ} {p r : ℂ}
96     (hf : MeromorphicAt f p) (hd : ∀ z, z ≠ p → DifferentiableAt ℂ f z)
97     (hr : r ≠ 0)
98     (ht : Tendsto (fun z => (z - p) * f z) (𝓝[≠] p) (𝓝 r)) :
99     meromorphicOrderAt f p = (-1 : ℤ) := by
100   classical
101   let g := Function.update (fun z => (z - p) * f z) p r
102   have hg : AnalyticAt ℂ g p := by
103     apply Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
104     · filter_upwards [self_mem_nhdsWithin] with z hz
105       have hz0 : z ≠ p := hz
106       have he : g =ᶠ[𝓝 z] (fun w => (w - p) * f w) := by
107         filter_upwards [eventually_ne_nhds hz0] with w hw
108         exact Function.update_of_ne hw _ _
109       exact (((differentiableAt_id.sub_const p).mul (hd z hz0))).congr_of_eventuallyEq he
110     · exact continuousAt_update_same.mpr ht
111   apply (meromorphicOrderAt_eq_int_iff hf).mpr
112   refine ⟨g, hg, ?_, ?_⟩
113   · simpa only [g, Function.update_self] using hr
114   · filter_upwards [self_mem_nhdsWithin] with z hz
115     have hz0 : z ≠ p := hz
116     simp only [g, Function.update_of_ne hz0, zpow_neg_one, smul_eq_mul]
117     field_simp
118 
119 end
120 end Komorebi.PaperIV

Back to source controls