The L-function of a Dirichlet character does not vanish on Re(s) ≥ 1

The main result in this file is DirichletCharacter.Lfunction_ne_zero_of_one_le_re: if χ is a Dirichlet character, s ∈ ℂ with 1 ≤ s.re, and either χ is nontrivial or s ≠ 1, then the L-function of χ does not vanish at s.

As a consequence, we have the corresponding statement for the Riemann ζ function: riemannZeta_ne_zero_of_one_le_re (which does not require s ≠ 1, since the junk value at s = 1 happens to be non-zero).

These results are prerequisites for the Prime Number Theorem and Dirichlet's Theorem on primes in arithmetic progressions.

Outline of proofs

We split into two cases: first, the special case of (non-trivial) quadratic characters at s = 1; then the remaining case when either s ≠ 1 or χ ^ 2 ≠ 1.

The first case is handled using a positivity argument applied to the series L χ s * ζ s: we show that this function has non-negative Dirichlet coefficients, is strictly positive for s ≫ 0, but vanishes at s = -2, so it must have a pole somewhere in between.

The second case is dealt with using the product L(χ^0, 1 + x)^3 L(χ, 1 + x + I * y)^4 L(χ^2, 1 + x + 2 * I * y), which we show has absolute value ≥ 1 for all positive x and real y; if L(χ, 1 + I * y) = 0 then this product would have to tend to 0 as x → 0, which is a contradiction.

Convolution of a Dirichlet character with ζ

We define DirichletCharacter.zetaMul χ to be the arithmetic function obtained by taking the product (as arithmetic functions = Dirichlet convolution) of the arithmetic function ζ with χ.

We then show that for a quadratic character χ, this arithmetic function is multiplicative and takes nonnegative real values.

def DirichletCharacter.zetaMul {N : ℕ} (χ : DirichletCharacter ℂ N) : ArithmeticFunction ℂ

The complex-valued arithmetic function that is the convolution of the constant function 1 with χ.

Equations

• χ.zetaMul = ↑ArithmeticFunction.zeta * toArithmeticFunction fun (x : ℕ) => χ ↑x

theorem DirichletCharacter.isMultiplicative_zetaMul {N : ℕ} (χ : DirichletCharacter ℂ N) : χ.zetaMul.IsMultiplicative

The arithmetic function zetaMul χ is multiplicative.

theorem DirichletCharacter.LSeriesSummable_zetaMul {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (⇑χ.zetaMul) s

theorem DirichletCharacter.zetaMul_prime_pow_nonneg {N : ℕ} {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) {p : ℕ} (hp : Nat.Prime p) (k : ℕ) : 0 ≤ χ.zetaMul (p ^ k)

theorem DirichletCharacter.zetaMul_nonneg {N : ℕ} {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) (n : ℕ) : 0 ≤ χ.zetaMul n

zetaMul χ takes nonnegative real values when χ is a quadratic character.

theorem DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : Summable fun (p : Nat.Primes) => -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))

The logarithms of the Euler factors of a Dirichlet L-series form a summable sequence.

theorem DirichletCharacter.norm_LSeries_product_ge_one {N : ℕ} (χ : DirichletCharacter ℂ N) {x : ℝ} (hx : 0 < x) (y : ℝ) : ‖LSeries (fun (n : ℕ) => 1 ↑n) (1 + ↑x) ^ 3 * LSeries (fun (n : ℕ) => χ ↑n) (1 + ↑x + Complex.I * ↑y) ^ 4 * LSeries (fun (n : ℕ) => (χ ^ 2) ↑n) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥ 1

For positive x and nonzero y and a Dirichlet character χ we have that `|L(χ^0, 1 + x)^3 L(χ, 1 + x + I * y)^4 L(χ^2, 1 + x + 2 * I * y)| ≥ 1.

theorem DirichletCharacter.norm_LFunction_product_ge_one {N : ℕ} (χ : DirichletCharacter ℂ N) [NeZero N] {x : ℝ} (hx : 0 < x) (y : ℝ) : ‖DirichletCharacter.LFunctionTrivChar N (1 + ↑x) ^ 3 * DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y) ^ 4 * DirichletCharacter.LFunction (χ ^ 2) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥ 1

A variant of DirichletCharacter.norm_LSeries_product_ge_one in terms of the L-functions.

theorem DirichletCharacter.LFunctionTrivChar_isBigO_near_one_horizontal {N : ℕ} [NeZero N] : (fun (x : ℝ) => DirichletCharacter.LFunctionTrivChar N (1 + ↑x)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1 / ↑x

theorem DirichletCharacter.LFunction_isBigO_horizontal {N : ℕ} (χ : DirichletCharacter ℂ N) [NeZero N] {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1) : (fun (x : ℝ) => DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1

theorem DirichletCharacter.LFunction_ne_zero_of_re_eq_one {N : ℕ} (χ : DirichletCharacter ℂ N) [NeZero N] {s : ℂ} (hs : s.re = 1) (hχs : χ ≠ 1 ∨ s ≠ 1) : DirichletCharacter.LFunction χ s ≠ 0

If χ is a Dirichlet character, then L(χ, s) does not vanish when s.re = 1 except when χ is trivial and s = 1 (then L(χ, s) has a simple pole at s = 1).

theorem DirichletCharacter.LFunction_ne_zero_of_one_le_re {N : ℕ} (χ : DirichletCharacter ℂ N) [NeZero N] ⦃s : ℂ⦄ (hχs : χ ≠ 1 ∨ s ≠ 1) (hs : 1 ≤ s.re) : DirichletCharacter.LFunction χ s ≠ 0

If χ is a Dirichlet character, then L(χ, s) does not vanish for s.re ≥ 1 except when χ is trivial and s = 1 (then L(χ, s) has a simple pole at s = 1).

theorem DirichletCharacter.LFunction_apply_one_ne_zero {N : ℕ} {χ : DirichletCharacter ℂ N} [NeZero N] (hχ : χ ≠ 1) : DirichletCharacter.LFunction χ 1 ≠ 0

The L-function of a nontrivial Dirichlet character does not vanish at s = 1.

theorem riemannZeta_ne_zero_of_one_le_re ⦃s : ℂ⦄ (hs : 1 ≤ s.re) : riemannZeta s ≠ 0

The Riemann Zeta Function does not vanish on the closed half-plane re s ≥ 1. (Note that the value at s = 1 is a junk value, which happens to be nonzero.)