Prove2Me

The classical zero-free region for ζ\zeta: ζ(s)≠0\zeta(s)\ne0 for σ≥1−c/log⁡(∣t∣+2)\sigma\ge1-c/\log(|t|+2) (Davenport §13)

Proved
Davenport.zeta_zero_free_region

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

analytic-number-theorydirichlet-l-functionnumber-theorysiegel-walfiszzero-free-region

The de la Vallée Poussin zero-free region for the Riemann zeta function (Davenport §13). There is an absolute constant c>0c>0 such that

ζ(s)≠0whenevers≠1  and  Re⁡s  ≥  1−clog⁡(∣Im⁡s∣+2).\zeta(s)\neq0\qquad\text{whenever}\qquad s\neq1\ \text{ and }\ \operatorname{Re}s\;\ge\;1-\frac{c}{\log(|\operatorname{Im}s|+2)} .

Here ζ\zeta is Mathlib's analytically continued Riemann zeta function (its value at the pole s=1s=1 is excluded). Davenport proves it from the 33–44–11 inequality for −ζ′/ζ-\zeta'/\zeta and the partial-fraction bound −Re⁡ζ′/ζ(s)<clog⁡∣t∣−Re⁡1s−ρ-\operatorname{Re}\zeta'/\zeta(s)<c\log|t|-\operatorname{Re}\frac1{s-\rho} for 1≤σ≤21\le\sigma\le2, ∣t∣≥2|t|\ge2; near the real axis the region is zero-free because ζ(s)≠0\zeta(s)\neq0 on Re⁡s≥1\operatorname{Re}s\ge1 (Mathlib) and ζ\zeta has no zeros in a neighbourhood of the compact set {σ≥1−ε,∣t∣≤2}\{\sigma\ge1-\varepsilon, |t|\le2\} apart from the pole. It is the q=1q=1 (principal character) case of the zero-free region for L(s,χ)L(s,\chi) and the input for the prime number theorem with error term O(xexp⁡(−clog⁡x))O(x\exp(-c\sqrt{\log x})) (§18).

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
import Mathlib.NumberTheory.LSeries.RiemannZeta

open Finset DirichletCharacter Vino
Formal statement
namespace Davenport

theorem zeta_zero_free_region :
    ∃ c : ℝ, 0 < c ∧
      ∀ s : ℂ, s ≠ 1 → 1 - c / Real.log (|s.im| + 2) ≤ s.re → riemannZeta 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; §13 (A zero-free region for ζ(s)), pp. 84–87: ζ(σ+it) ≠ 0 for σ ≥ 1 − c/log(|t|+2) (stated there for |t| ≥ 2 with the small-|t| case by nonvanishing on σ ≥ 1)
Human review

  • Endorsed by Shuze Chen · Sep 3, 2026

  • Endorsed by alya · Sep 3, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph