Continuity of an L-series on a closed half-plane of summability

If a Dirichlet series is summable at s, then at every point z with s.re ≤ z.re its terms have norms at most those of the terms at s, so the series converges uniformly on the closed half-plane {z | s.re ≤ z.re} and LSeries a is continuous there. On the vertical line s + ℝ * I through s the norms even agree exactly, and continuity along that line is a special case of the half-plane statement.

Mathlib's LSeries_differentiableOn gives more, but only strictly inside the half-plane of absolute convergence: it needs abscissaOfAbsConv a < s.re, whereas LSeriesSummable a s only gives abscissaOfAbsConv a ≤ s.re. The line through a point of summability may therefore be the boundary line of that half-plane, which is exactly the situation in the Wiener--Ikehara argument.

Main results

• TauCeti.LSeries.continuousOn_LSeries: LSeries a is continuous on the closed half-plane {z | s.re ≤ z.re} whenever LSeriesSummable a s.
• TauCeti.LSeries.continuous_LSeries_vertical: fun t : ℝ ↦ LSeries a (s + t * I) is continuous whenever LSeriesSummable a s.
• TauCeti.LSeries.tendsto_LSeries_nhdsGT: the real one-sided limit of LSeries a at a real point of summability is the value there.

theorem TauCeti.LSeries.continuousOn_LSeries {a : ℕ → ℂ} {s : ℂ} (hs : LSeriesSummable a s) : ContinuousOn (LSeries a) {z : ℂ | s.re ≤ z.re}

A Dirichlet series summable at s converges uniformly on the closed half-plane {z | s.re ≤ z.re}, hence is continuous there.

Mathlib's LSeries_differentiableOn gives more on the open half-plane cut out by the abscissa of absolute convergence, but says nothing on its boundary line, which is where the Wiener--Ikehara argument works.

theorem TauCeti.LSeries.continuous_LSeries_vertical {a : ℕ → ℂ} {s : ℂ} (hs : LSeriesSummable a s) : Continuous fun (t : ℝ) => LSeries a (s + ↑t * Complex.I)

A Dirichlet series summable at s is continuous along the vertical line through s.

theorem TauCeti.LSeries.tendsto_LSeries_nhdsGT {a : ℕ → ℂ} {σ : ℝ} (hs : LSeriesSummable a ↑σ) : Filter.Tendsto (fun (τ : ℝ) => LSeries a ↑τ) (nhdsWithin σ (Set.Ioi σ)) (nhds (LSeries a ↑σ))

Approaching a real point of summability from the right along the real axis, the values of a Dirichlet series converge to its value there.