Landau's theorem on Dirichlet series with nonnegative coefficients

A Dirichlet series whose coefficients are nonnegative real numbers is singular at the real point of its abscissa of absolute convergence. Writing σ for that abscissa, no function analytic on a disc around σ can agree with LSeries a immediately to the right of σ: the series would then already converge to the left of σ.

The obstruction is recorded by TauCeti.LSeries.HasAnalyticExtensionAt a σ, the existence of such a disc and such a function; TauCeti.LSeries.hasAnalyticExtensionAt_of_abscissaOfAbsConv_lt shows the predicate is not vacuous, since strictly inside the half-plane of convergence the L-series is its own analytic continuation.

Main results

• TauCeti.LSeries.landau: Landau's theorem. If 0 ≤ a and LSeries.abscissaOfAbsConv a = (σ : EReal), then ¬ HasAnalyticExtensionAt a σ. The equality hypothesis is what makes σ the actual boundary and records its finiteness; convergence throughout Re s > σ alone would not suffice.
• TauCeti.LSeries.landau_of_abscissaOfConv: the same conclusion from the equality LSeries.abscissaOfConv a = (σ : EReal), which for nonnegative coefficients is the same hypothesis.
• TauCeti.LSeries.meromorphicOrderAt_lt_zero_of_eq_LSeries: a meromorphic continuation at the actual abscissa has negative order there, so the singularity is a pole rather than removable.
• TauCeti.LSeries.abscissaOfAbsConv_le_of_differentiableOn: the half-plane form. A nonnegative Dirichlet series with finite abscissa converges as far to the left as it continues analytically.
• TauCeti.LSeries.abscissaOfAbsConv_eq_bot_of_hasEntireExtension: the same conclusion phrased through the repository's LSeries.HasEntireExtension predicate, which is what a nonvanishing argument applies once a positive combination of L-series has been shown entire.

Implementation notes

Mathlib formalizes only the abscissa of absolute convergence: LSeriesSummable is equivalent to absolute summability of the Dirichlet terms because summable_norm_iff holds in ℂ. The classical abscissa of ordinary convergence is TauCeti.LSeries.abscissaOfConv, and for the nonnegative coefficients considered here the two are equal (TauCeti.LSeries.abscissaOfConv_eq_abscissaOfAbsConv_of_nonneg), so it does not matter which of them the hypothesis names.

The proof follows the classical argument. Suppose F is analytic on a disc around σ and agrees with LSeries a to its right. Patching F with LSeries a produces a function G analytic on a disc of radius slightly larger than 1 around σ + 1, and the Taylor coefficients of G at σ + 1 are, up to sign, the numbers ∑ a n (log n) ^ k / n ^ (σ + 1) ≥ 0 (LSeries.iteratedDeriv_alternating). Evaluating the Taylor series at a real point x < σ of that disc and exchanging the two nonnegative summations exhibits ∑ a n / n ^ x as a convergent series, contradicting abscissaOfAbsConv a = σ.

References

• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter II.1, Theorem 10.

theorem TauCeti.LSeries.term_logPowMul (f : ℕ → ℂ) (s : ℂ) (k n : ℕ) : LSeries.term (LSeries.logMul^[k] f) s n = ↑(Real.log ↑n) ^ k * LSeries.term f s n

Applying Mathlib's logPowMul operation multiplies the Dirichlet term by a power of Real.log n.

theorem TauCeti.LSeries.re_term_of_ne_zero (a : ℕ → ℂ) (x : ℝ) {n : ℕ} (hn : n ≠ 0) : (LSeries.term a (↑x) n).re = (a n).re / ↑n ^ x

The real part of a Dirichlet term at a real point.

theorem TauCeti.LSeries.hasSum_logPowMul_re_term {a : ℕ → ℂ} {x : ℝ} (hx : LSeries.abscissaOfAbsConv a < ↑x) (k : ℕ) : HasSum (fun (n : ℕ) => Real.log ↑n ^ k * (LSeries.term a (↑x) n).re) (LSeries (LSeries.logMul^[k] a) ↑x).re

At a real point x in the half-plane of absolute convergence, the real series obtained by taking real parts of the terms of logPowMul converges to the real part of its L-series.

def TauCeti.LSeries.HasAnalyticExtensionAt (a : ℕ → ℂ) (σ : ℝ) : Prop

HasAnalyticExtensionAt a σ says that the L-series of a continues analytically across the real point σ: some function differentiable on a disc around σ agrees with LSeries a on the part of that disc lying in the half-plane Re s > σ.

Equations

• TauCeti.LSeries.HasAnalyticExtensionAt a σ = ∃ (r : ℝ), 0 < r ∧ ∃ (F : ℂ → ℂ), DifferentiableOn ℂ F (Metric.ball (↑σ) r) ∧ ∀ s ∈ Metric.ball (↑σ) r, σ < s.re → F s = LSeries a s

theorem TauCeti.LSeries.hasAnalyticExtensionAt_of_abscissaOfAbsConv_lt {a : ℕ → ℂ} {σ : ℝ} (h : LSeries.abscissaOfAbsConv a < ↑σ) : HasAnalyticExtensionAt a σ

Above the abscissa of absolute convergence the L-series continues across every real point: it is already analytic there.

theorem TauCeti.LSeries.landau {a : ℕ → ℂ} (ha : 0 ≤ a) {σ : ℝ} (habs : LSeries.abscissaOfAbsConv a = ↑σ) : ¬HasAnalyticExtensionAt a σ

Landau's theorem. If a has nonnegative values and its abscissa of absolute convergence is the real number σ, then LSeries a has no analytic continuation across σ.

theorem TauCeti.LSeries.landau_of_abscissaOfConv {a : ℕ → ℂ} (ha : ∀ (n : ℕ), n ≠ 0 → 0 ≤ a n) {σ : ℝ} (hconv : abscissaOfConv a = ↑σ) : ¬HasAnalyticExtensionAt a σ

Landau's theorem at the abscissa of ordinary convergence. A Dirichlet series whose coefficients away from the ignored index zero are nonnegative has a single abscissa of convergence, so the singularity may equally be located by the ordinary one.

theorem TauCeti.LSeries.meromorphicOrderAt_lt_zero_of_eq_LSeries {a : ℕ → ℂ} (ha : 0 ≤ a) {σ r : ℝ} (habs : LSeries.abscissaOfAbsConv a = ↑σ) (hr : 0 < r) {F : ℂ → ℂ} (hF : MeromorphicAt F ↑σ) (hFeq : ∀ s ∈ Metric.ball (↑σ) r, σ < s.re → F s = LSeries a s) : meromorphicOrderAt F ↑σ < 0

Meromorphic form of Landau's theorem. Let F be a meromorphic continuation of a Dirichlet series with nonnegative coefficients to a neighborhood of its finite, actual abscissa of absolute convergence. Then the meromorphic order of F at that abscissa is negative. In particular, the singularity forced by landau is a pole, not a removable singularity.

Meromorphicity and meromorphic order depend only on the punctured germ, so no convention is imposed on the value of F at the centre.

theorem TauCeti.LSeries.abscissaOfAbsConv_le_of_differentiableOn {a : ℕ → ℂ} (ha : 0 ≤ a) (hfin : LSeries.abscissaOfAbsConv a ≠ ⊤) {σ₁ : ℝ} {F : ℂ → ℂ} (hF : DifferentiableOn ℂ F {s : ℂ | σ₁ < s.re}) (hFeq : ∀ (s : ℂ), σ₁ < s.re → LSeries.abscissaOfAbsConv a < ↑s.re → F s = LSeries a s) : LSeries.abscissaOfAbsConv a ≤ ↑σ₁

Landau's theorem, half-plane form. A Dirichlet series with nonnegative coefficients and finite abscissa of absolute convergence converges as far to the left as it continues analytically: if some function differentiable on Re s > σ₁ agrees with LSeries a on the part of the absolute-convergence half-plane where it is differentiable, then that abscissa is at most σ₁.

This is the form consumed by nonvanishing arguments, where F is a quotient of L-functions known to be analytic on a half-plane, or on the complement of a pole that a positive combination has already cancelled.

theorem TauCeti.LSeries.abscissaOfAbsConv_eq_bot_of_hasEntireExtension {a : ℕ → ℂ} (ha : 0 ≤ a) (h : LSeries.HasEntireExtension a) : LSeries.abscissaOfAbsConv a = ⊥

A Dirichlet series with nonnegative coefficients that has an entire extension in the sense of LSeries.HasEntireExtension converges absolutely at every point of the plane.