Positivity of the L-function of a quadratic character on [1, ∞)

A quadratic Dirichlet character χ takes only the values 0, 1 and -1. At a real point s > 1 every Euler factor (1 - χ(p) p⁻ˢ)⁻¹ is then a positive real number, and the logarithmic form of the Euler product writes L(s, χ) as the exponential of a real number. Hence L(s, χ) is real and positive there. For nontrivial χ the continued L-function is continuous at s = 1, so L(1, χ) is a nonnegative real number; Mathlib's nonvanishing theorem DirichletCharacter.LFunction_apply_one_ne_zero then makes it positive.

Positivity is stated with ComplexOrder, where 0 < z means that z is a positive real number. The value L(1, χ) is the one that enters the analytic class number formula of a quadratic field, where it is compared with real quantities.

To the left of 1 the continued L-function is still real on the real axis, so by the intermediate value theorem it stays positive until its first real zero. This is the sign information about possible exceptional zeros used in Siegel's theorem.

Main results

• DirichletCharacter.LFunction_pos_of_one_lt: for a quadratic character χ and real s > 1, 0 < L(s, χ).
• DirichletCharacter.LFunction_apply_one_pos: for a nontrivial quadratic character χ, 0 < L(1, χ).
• DirichletCharacter.LFunction_pos_of_one_le: for a nontrivial quadratic character χ and real s ≥ 1, 0 < L(s, χ).
• DirichletCharacter.LFunction_pos_of_forall_ne_zero, DirichletCharacter.LFunction_nonneg_of_forall_ne_zero: positivity persists to the left of 1 up to the first real zero. If L(σ, χ) ≠ 0 for β ≤ σ < 1, then 0 < L(β, χ); if only L(σ, χ) ≠ 0 for β < σ < 1, then 0 ≤ L(β, χ).

References

• H. Davenport, Multiplicative Number Theory, Chapter 4 (the nonvanishing of L(1, χ) for real characters).

theorem DirichletCharacter.LFunction_pos_of_one_lt {N : ℕ} {χ : DirichletCharacter ℂ N} [NeZero N] (hχ : MulChar.IsQuadratic χ) {s : ℝ} (hs : 1 < s) : 0 < LFunction χ ↑s

The L-function of a quadratic Dirichlet character is a positive real number at every real point s > 1.

theorem DirichletCharacter.LFunction_apply_one_pos {N : ℕ} {χ : DirichletCharacter ℂ N} [NeZero N] (hχ : MulChar.IsQuadratic χ) (hχ₁ : χ ≠ 1) : 0 < LFunction χ 1

The value at s = 1 of the L-function of a nontrivial quadratic Dirichlet character is a positive real number.

theorem DirichletCharacter.LFunction_pos_of_one_le {N : ℕ} {χ : DirichletCharacter ℂ N} [NeZero N] (hχ : MulChar.IsQuadratic χ) (hχ₁ : χ ≠ 1) {s : ℝ} (hs : 1 ≤ s) : 0 < LFunction χ ↑s

The continued L-function of a nontrivial quadratic Dirichlet character is a positive real number at every real point s ≥ 1.

theorem DirichletCharacter.LFunction_pos_of_forall_ne_zero {N : ℕ} {χ : DirichletCharacter ℂ N} [NeZero N] (hχ : MulChar.IsQuadratic χ) (hχ₁ : χ ≠ 1) {β : ℝ} (h : ∀ σ ∈ Set.Ico β 1, LFunction χ ↑σ ≠ 0) : 0 < LFunction χ ↑β

The continued L-function of a nontrivial quadratic Dirichlet character is a positive real number at every real point β such that it has no zero in [β, 1).

theorem DirichletCharacter.LFunction_nonneg_of_forall_ne_zero {N : ℕ} {χ : DirichletCharacter ℂ N} [NeZero N] (hχ : MulChar.IsQuadratic χ) (hχ₁ : χ ≠ 1) {β : ℝ} (h : ∀ σ ∈ Set.Ioo β 1, LFunction χ ↑σ ≠ 0) : 0 ≤ LFunction χ ↑β

The continued L-function of a nontrivial quadratic Dirichlet character is a nonnegative real number at every real point β such that it has no zero in (β, 1).