Zeros of $L(s,\chi)$ in the critical strip are symmetric about $1/2$ for real $\chi$

Proved

Davenport.LFunction_real_zero_symm

by alya · Sep 3, 2026 · Mathlib c5ea003 (Lean v4.30.0)

Symmetry of the zeros of $L(s,\chi)$ for a real character (Davenport §9, §12). Let $\chi$ be a real (quadratic) Dirichlet character modulo $q\ge1$ , i.e. $\chi$ takes only the values $0,\pm1$ , and let $s$ be a complex number in the critical strip $0<\operatorname{Re}s<1$ . If

L(s,\chi)=0,\qquad\text{then}\qquad L(1-s,\chi)=0 .

For a primitive real character this is the functional equation $\xi(1-s,\chi)=\varepsilon(\chi)\,\xi(s,\overline{\chi})$ with $\overline\chi=\chi$ , the Gamma factor having neither zeros nor poles in the strip; an imprimitive character is induced by a primitive one and the additional Euler factors $\prod_{p\mid q}(1-\chi^*(p)p^{-s})$ do not vanish for $\operatorname{Re}s>0$ . The principal character reduces to the symmetry of the zeros of $\zeta(s)$ .

It is used to show that a real zero of $L(s,\chi)$ in the zero-free region cannot lie in $(0,\tfrac12)$ (its mirror image would be a second zero in the region), which is needed when the exceptional zero is inserted into the explicit formula for $\psi(N,\chi)$ .

Formalization Note χ.IsQuadratic is Mathlib's predicate that every value of $\chi$ is $0$ , $1$ or $-1$ ; the principal character is allowed.

Preamble

import Definitions.Def_Davenport_siegelWalfisz
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.DirichletCharacter.Basic
import Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
import Mathlib.NumberTheory.Chebyshev
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Pow.Complex
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Data.Nat.Totient

open Finset DirichletCharacter Vino

Formal statement

open Finset DirichletCharacter Vino

namespace Davenport

theorem LFunction_real_zero_symm (q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q)
    (hχ : χ.IsQuadratic) (s : ℂ) (hs0 : 0 < s.re) (hs1 : s.re < 1)
    (h : DirichletCharacter.LFunction χ s = 0) :
    DirichletCharacter.LFunction χ (1 - s) = 0 := by sorry

end Davenport

Source

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; §9 (The functional equation), pp. 65–72: ξ(1−s,χ) = (i^a q^{1/2}/τ(χ)) ξ(s,χ̄) for primitive χ, and its consequence (§9, end, and §12, p. 83) that the zeros of L(s,χ) in 0 < σ < 1 are symmetric about the line σ = 1/2 when χ is real (χ̄ = χ); imprimitive χ reduce to the inducing primitive character, the extra Euler factors having no zeros in 0 < σ < 1

View graph

Zeros of L(s,χ)L(s,\chi)L(s,χ) in the critical strip are symmetric about 1/21/21/2 for real χ\chiχ

Zeros of $L(s,\chi)$ in the critical strip are symmetric about $1/2$ for real $\chi$