$\zeta(\sigma)$ is real and negative for $0 < \sigma < 1$

Proved

Davenport.riemannZeta_neg_of_lt_one

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

analytic-number-theorydirichlet-l-functionnumber-theorysiegel-theoremsiegel-walfiszthree-primes

Negativity of $\zeta$ on the real segment $(0,1)$ . For every real $\sigma$ with $0 < \sigma < 1$ , the value $\zeta(\sigma)$ of the analytically continued Riemann zeta function is a real number and

\zeta(\sigma) < 0 .

This follows from the Euler–Maclaurin (Abel summation) representation, valid for $\operatorname{Re} s > 0$ , $s \ne 1$ ,

\zeta(s) = \frac{1}{2} + \frac{1}{s-1} + s\int_1^\infty \Bigl(\lfloor x\rfloor + \tfrac12 - x\Bigr)x^{-s-1}\,dx ,

in which, for real $s = \sigma \in (0,1)$ , the integral term has modulus at most $\tfrac12$ while $1/(\sigma - 1) < -1$ . It is the sign fact used in the proof of Estermann's lemma (Montgomery–Vaughan, proof of Lemma 11.13: " $\zeta(\sigma) < 0$ for $1/2 < \sigma < 1$ "), and it is what allows a zero, or a nonnegative value, of $L(\sigma,\chi_1)L(\sigma,\chi_2)L(\sigma,\chi_1\chi_2)$ to force $F(\sigma) = \zeta(\sigma)L(\sigma,\chi_1)L(\sigma,\chi_2)L(\sigma,\chi_1\chi_2) \le 0$ .

Formalization Note. The statement is expressed as: the imaginary part of $\zeta(\sigma)$ vanishes and its real part is negative.

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 riemannZeta_neg_of_lt_one (σ : ℝ) (hσ₀ : 0 < σ) (hσ₁ : σ < 1) :
    (riemannZeta σ).im = 0 ∧ (riemannZeta σ).re < 0 := by sorry

end Davenport

Source

H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge Studies in Advanced Mathematics 97, CUP 2007, proof of Lemma 11.13 (p. 371): ζ(σ) < 0 for 1/2 < σ < 1; E. C. Titchmarsh, The Theory of the Riemann Zeta-Function, 2nd ed., OUP 1986, §2.1 (Euler–Maclaurin/Abel-summation representation of ζ(s) for σ > 0)

View graph

ζ(σ)\zeta(\sigma)ζ(σ) is real and negative for 0<σ<10 < \sigma < 10<σ<1

$\zeta(\sigma)$ is real and negative for $0 < \sigma < 1$