Non-vanishing of L(χ, 1) for nontrivial quadratic characters χ

The main result of this file is the statement DirichletCharacter.LFunction_at_one_ne_zero_of_quadratic, which says that if χ is a nontrivial (χ ≠ 1) quadratic (χ^2 = 1) Dirichlet character, then the value of its L-function at s = 1 is nonzero.

This is an important step in the proof of Dirichlet's Theorem on Primes in Arithmetic Progression.

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.

The main result

theorem DirichletCharacter.LFunction_at_one_ne_zero_of_quadratic {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) (χ_ne : χ ≠ 1) : DirichletCharacter.LFunction χ 1 ≠ 0

If χ is a nontrivial quadratic Dirichlet character, then L(χ, 1) ≠ 0.