is real for real when is a real character
ProvedDavenport.LFunction_ofReal_im_eq_zeroanalytic-number-theorydirichlet-l-functionnumber-theorysiegel-theoremsiegel-walfiszthree-primes
Reality of on the real axis for real characters. Let be a real (quadratic: all values in ) non-principal Dirichlet character modulo . Then for every real , the value of the entire function is a real number:
For this is clear from the Dirichlet series , whose terms are real; for the remaining it follows by analytic continuation (for instance from the Taylor expansion of the entire function about , all of whose coefficients are real). It is the fact that lets one speak of real zeros of and of the sign of on in Siegel's theorem.
Formalization Note. The non-principality hypothesis is included so that is entire; for the principal character the value assigned at the pole is not covered by this statement.
Preamble
import Mathlib.NumberTheory.LSeries.DirichletContinuation import Mathlib.NumberTheory.LSeries.Nonvanishing import Mathlib.NumberTheory.LSeries.Positivity import Mathlib.NumberTheory.LSeries.Convolution import Mathlib.NumberTheory.DirichletCharacter.Basic import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Analysis.SpecialFunctions.Pow.Complex import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.SpecialFunctions.Exp open Finset DirichletCharacter
Formal statement
namespace Davenport
theorem LFunction_ofReal_im_eq_zero (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q)
(hχ : χ.IsQuadratic) (hχ₁ : χ ≠ 1) (σ : ℝ) :
(DirichletCharacter.LFunction χ σ).im = 0 := by sorry
end DavenportSource
H. Davenport, Multiplicative Number Theory, 3rd ed. (revised by H. L. Montgomery), GTM 74, Springer 2000, https://doi.org/10.1007/978-1-4757-5927-3, §21, pp. 126–131 (real zeros β₁ of L(s,χ) for real χ presuppose that L(σ,χ) is real on the real axis); H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge Studies in Advanced Mathematics 97, CUP 2007, §11.3, proof of Theorem 11.14 (pp. 372–373)