Terms of a Dirichlet series with nonnegative coefficients at a real point

At a real point sigma, the terms of a Dirichlet series with nonnegative coefficients are themselves nonnegative reals. Each term therefore equals its own norm, plain summability at sigma is already absolute summability, and the value of the series is the sum of the norms of its terms. These are the facts that turn a bound on the value LSeries a sigma into a bound on ∑' n, ‖LSeries.term a sigma n‖, which is the shape a comparison or truncation argument needs.

Mathlib's Mathlib/NumberTheory/LSeries/Positivity.lean records the positivity of the values of such a series; the statements here are about its individual terms.

Main declarations

• TauCeti.LSeries.term_eq_ofReal_norm_of_nonneg: a nonnegative coefficient makes the term at a real point equal to its own norm.
• TauCeti.LSeries.summable_norm_term_of_nonneg: for nonnegative coefficients, summability at a real point is absolute summability.
• TauCeti.LSeries.LSeries_eq_ofReal_tsum_norm_of_nonneg: for nonnegative coefficients, the value at a real point is the sum of the norms of the terms.

theorem TauCeti.LSeries.term_eq_ofReal_norm_of_nonneg {a : ℕ → ℂ} {n : ℕ} (ha : 0 ≤ a n) (sigma : ℝ) : LSeries.term a (↑sigma) n = ↑‖LSeries.term a (↑sigma) n‖

At a real point, a nonnegative Dirichlet coefficient gives a term equal to its own norm.

theorem TauCeti.LSeries.summable_norm_term_of_nonneg {a : ℕ → ℂ} (ha : 0 ≤ a) {sigma : ℝ} (h : LSeriesSummable a ↑sigma) : Summable fun (n : ℕ) => ‖LSeries.term a (↑sigma) n‖

For nonnegative coefficients, summability at a real point is absolute summability.

theorem TauCeti.LSeries.LSeries_eq_ofReal_tsum_norm_of_nonneg {a : ℕ → ℂ} (ha : 0 ≤ a) (sigma : ℝ) : LSeries a ↑sigma = ↑(∑' (n : ℕ), ‖LSeries.term a (↑sigma) n‖)

For nonnegative coefficients, the value of the Dirichlet series at a real point is the sum of the norms of its terms.