theorem DirichletCharacter.riemannZeta_mul_LFunction_eq_LSeries_zetaMul {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : riemannZeta s * LFunction χ s = LSeries (⇑χ.zetaMul) s

In the half-plane of absolute convergence, the product of the Riemann zeta function and a Dirichlet L-function is the L-series of their Dirichlet convolution.

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

A nonprincipal quadratic Dirichlet L-function has nonnegative real value at 1. The proof approaches 1 along the real axis from the right and uses the nonnegative Dirichlet coefficients of ζ(s) L(s, χ).

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

A nonprincipal quadratic Dirichlet L-function is real at 1.

theorem DirichletCharacter.LFunction_apply_one_re_pos_of_sq_eq_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) : 0 < (LFunction χ 1).re

A nonprincipal quadratic Dirichlet L-function has strictly positive real part at 1.

theorem DirichletCharacter.LFunction_apply_one_positive_real_of_sq_eq_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) : (LFunction χ 1).im = 0 ∧ 0 < (LFunction χ 1).re

Positivity and realness of a nonprincipal quadratic Dirichlet L-value at 1.