Ordinary convergence of a Dirichlet series, and its abscissa

Mathlib measures a Dirichlet series only through LSeriesSummable, which in ℂ is absolute convergence, and through the resulting LSeries.abscissaOfAbsConv. A Dirichlet series can converge without converging absolutely, so the classical theory carries a second abscissa, lying to the left of the first.

TauCeti.LSeriesConverges f s says that the partial sums ∑_{n < N} f n / n ^ s tend to a limit as N → ∞, the index being summed in its natural order, and TauCeti.LSeries.abscissaOfConv f is the infimum of the real points at which they do. Abel summation bounds that abscissa by any exponent controlling the partial sums of the coefficients, and in particular turns ordinary convergence at one point into ordinary convergence at every point further to the right; so this infimum is again the edge of a half-plane of convergence, and the two abscissae satisfy σ_c ≤ σ_a ≤ σ_c + 1.

The alternating coefficients (-1) ^ n show that the first inequality can be strict: their partial sums are bounded, so σ_c ≤ 0, while σ_a = 1. For nonnegative coefficients, on the other hand, the two abscissae agree, because at a real point the terms are then nonnegative reals, for which bounded partial sums and summability are the same condition. This is the case a Landau-type singularity argument works in, so for such a series it does not matter which of the two abscissae is named.

Main results

• TauCeti.LSeriesConverges_of_sum_isBigO: partial sums of the coefficients that are O(n ^ r) give ordinary convergence on Re s > r.
• TauCeti.LSeriesConverges.of_re_lt_re: ordinary convergence at s gives ordinary convergence at every s' with s.re < s'.re, and TauCeti.LSeriesConverges_of_abscissaOfConv_lt_re: the series converges on the open half-plane to the right of TauCeti.LSeries.abscissaOfConv.
• TauCeti.LSeries.abscissaOfConv_le_of_sum_isBigO: the same bound read off as an inequality between the exponent and the abscissa.
• TauCeti.LSeries.abscissaOfConv_le_abscissaOfAbsConv and TauCeti.LSeries.abscissaOfAbsConv_le_abscissaOfConv_add_one: the classical comparisons σ_c ≤ σ_a ≤ σ_c + 1.
• TauCeti.LSeries.abscissaOfConv_lt_abscissaOfAbsConv_neg_one_pow: the two abscissae are different for the alternating coefficients.
• TauCeti.LSeries.abscissaOfConv_eq_abscissaOfAbsConv_of_nonneg: for nonnegative coefficients they are equal, ordinary convergence at a real point being absolute there (TauCeti.lSeriesConverges_iff_lSeriesSummable_of_nonneg).

References

• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter II.1.
• J.-P. Serre, A Course in Arithmetic, Chapter VI, §2.

The statements and their proofs are modelled on Mathlib's treatment of the abscissa of absolute convergence in Mathlib/NumberTheory/LSeries/Convergence.lean; the reduction of a coefficient sequence to one vanishing at 0 is the device used by LSeriesSummable_of_sum_norm_bigO in Mathlib/NumberTheory/LSeries/SumCoeff.lean.

def TauCeti.LSeriesConverges (f : ℕ → ℂ) (s : ℂ) : Prop

Ordinary convergence of a Dirichlet series. The partial sums ∑_{n < N} f n / n ^ s, taken in the natural order of the index, tend to a limit.

This is weaker than LSeriesSummable f s, which in ℂ amounts to absolute convergence.

Equations

• TauCeti.LSeriesConverges f s = ∃ (L : ℂ), Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.range N, LSeries.term f s n) Filter.atTop (nhds L)

theorem TauCeti.LSeriesConverges.congr {f : ℕ → ℂ} {s : ℂ} {g : ℕ → ℂ} (h : ∀ (n : ℕ), LSeries.term f s n = LSeries.term g s n) : LSeriesConverges f s ↔ LSeriesConverges g s

Ordinary convergence is unchanged when the terms of two Dirichlet series agree pointwise.

theorem TauCeti.lSeriesConverges_of_lSeriesSummable {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : LSeriesConverges f s

An absolutely convergent Dirichlet series converges.

theorem TauCeti.LSeriesConverges_of_sum_isBigO {f : ℕ → ℂ} {s : ℂ} {r : ℝ} (hO : (fun (n : ℕ) => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r) (hs : r < s.re) : LSeriesConverges f s

Ordinary convergence from a bound on the partial sums of the coefficients. If ∑_{1 ≤ k ≤ n} f k is O(n ^ r), then the Dirichlet series of f converges at every s with Re s > r.

This is the criterion that produces a half-plane of ordinary convergence. Abel summation against the multiplier t ↦ t ^ (-s) turns the partial sums into a boundary term, which tends to 0 because Re s > r, plus an integral whose integrand is dominated by the integrable majorant t ^ (r - Re s - 1).

@[simp]

theorem TauCeti.LSeries.term_term_sub (f : ℕ → ℂ) (s s' : ℂ) (n : ℕ) : LSeries.term (LSeries.term f s) (s' - s) n = LSeries.term f s' n

Iterating the Dirichlet term: dividing the terms at s by n ^ (s' - s) gives the terms at s'.

theorem TauCeti.LSeriesConverges.of_re_lt_re {f : ℕ → ℂ} {s s' : ℂ} (h : LSeriesConverges f s) (hs : s.re < s'.re) : LSeriesConverges f s'

A Dirichlet series converges on a half-plane. Ordinary convergence at s forces ordinary convergence at every point strictly to the right of s: the partial sums of the terms at s are bounded, which is TauCeti.LSeriesConverges_of_sum_isBigO with exponent 0.

noncomputable def TauCeti.LSeries.abscissaOfConv (f : ℕ → ℂ) : EReal

The abscissa of ordinary convergence of the L-series of f: the infimum of the real points at which the partial sums of the series converge. The series converges at every s with Re s above it (TauCeti.LSeriesConverges_of_abscissaOfConv_lt_re), and it lies below the abscissa of absolute convergence.

Equations

• TauCeti.LSeries.abscissaOfConv f = sInf (Real.toEReal '' {x : ℝ | TauCeti.LSeriesConverges f ↑x})

theorem TauCeti.LSeries.abscissaOfConv_congr {f g : ℕ → ℂ} (h : ∀ {n : ℕ}, n ≠ 0 → f n = g n) : abscissaOfConv f = abscissaOfConv g

The abscissa of ordinary convergence depends only on the coefficients away from zero.

theorem TauCeti.LSeries.abscissaOfConv_le_of_forall_lt_LSeriesConverges {f : ℕ → ℂ} {x : ℝ} (h : ∀ (y : ℝ), x < y → LSeriesConverges f ↑y) : abscissaOfConv f ≤ ↑x

If the series converges at every real point above x, its abscissa of ordinary convergence is at most x.

theorem TauCeti.LSeries.abscissaOfConv_le_abscissaOfAbsConv (f : ℕ → ℂ) : abscissaOfConv f ≤ LSeries.abscissaOfAbsConv f

The ordinary abscissa lies to the left of the absolute one.

theorem TauCeti.LSeries.abscissaOfConv_le_of_sum_isBigO {f : ℕ → ℂ} {r : ℝ} (hO : (fun (n : ℕ) => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r) : abscissaOfConv f ≤ ↑r

Partial sums of the coefficients that are O(n ^ r) bound the abscissa of ordinary convergence by r.

theorem TauCeti.LSeriesConverges_of_abscissaOfConv_lt_re {f : ℕ → ℂ} {s : ℂ} (hs : LSeries.abscissaOfConv f < ↑s.re) : LSeriesConverges f s

A Dirichlet series converges at every point strictly to the right of its abscissa of ordinary convergence.

theorem TauCeti.LSeriesConverges.abscissaOfConv_le {f : ℕ → ℂ} {s : ℂ} (h : LSeriesConverges f s) : LSeries.abscissaOfConv f ≤ ↑s.re

Ordinary convergence at s bounds the abscissa of ordinary convergence by Re s.

theorem TauCeti.LSeries.abscissaOfAbsConv_le_abscissaOfConv_add_one (f : ℕ → ℂ) : LSeries.abscissaOfAbsConv f ≤ abscissaOfConv f + 1

The two abscissae differ by at most one. Where the series converges its terms are bounded, so ‖f n‖ = O(n ^ x) for every real x above the ordinary abscissa.

Alternating coefficients: the two abscissae can differ

theorem TauCeti.LSeries.abscissaOfConv_neg_one_pow_le_zero : (abscissaOfConv fun (n : ℕ) => (-1) ^ n) ≤ 0

The alternating coefficients have bounded partial sums, so their Dirichlet series converges for Re s > 0.

theorem TauCeti.LSeries.abscissaOfAbsConv_neg_one_pow : (LSeries.abscissaOfAbsConv fun (n : ℕ) => (-1) ^ n) = 1

The alternating coefficients have modulus one, so their Dirichlet series converges absolutely exactly where the Riemann zeta series does.

theorem TauCeti.LSeries.abscissaOfConv_lt_abscissaOfAbsConv_neg_one_pow : (abscissaOfConv fun (n : ℕ) => (-1) ^ n) < LSeries.abscissaOfAbsConv fun (n : ℕ) => (-1) ^ n

The two abscissae can be different. For the alternating coefficients the ordinary abscissa is at most 0 while the absolute one is 1.

Nonnegative coefficients

theorem TauCeti.lSeriesConverges_iff_lSeriesSummable_of_nonneg {f : ℕ → ℂ} (ha : ∀ (n : ℕ), n ≠ 0 → 0 ≤ f n) (x : ℝ) : LSeriesConverges f ↑x ↔ LSeriesSummable f ↑x

For coefficients nonnegative away from the ignored index zero, convergence at a real point is absolute. The terms are then nonnegative reals, so their partial sums converge exactly when they are bounded.

theorem TauCeti.LSeries.abscissaOfConv_eq_abscissaOfAbsConv_of_nonneg {f : ℕ → ℂ} (ha : ∀ (n : ℕ), n ≠ 0 → 0 ≤ f n) : abscissaOfConv f = LSeries.abscissaOfAbsConv f

For coefficients nonnegative away from the ignored index zero the two abscissae agree. A Dirichlet series with nonnegative coefficients therefore has a single half-plane of convergence, and the abscissa appearing in Landau's theorem is the ordinary one as well as the absolute one.