The classical zero-free region of de la Vallée Poussin for the Riemann zeta function

Open

SEF.zero_free_region_classical

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

prime-number-theoremriemann-zetazero-free-region

There is an absolute positive real constant c such that the Riemann zeta function does not vanish at any complex number sigma + i t whose real part sigma satisfies sigma >= 1 - c / log(|t| + 2), for any real t. This is the classical zero-free region proved by de la Vallée Poussin in 1896 by the Hadamard-de la Vallée Poussin method; its best-known corollary is the prime number theorem. The statement is drafted for this mission as a literature anchor: there is no source file for it, and the citation is given in the item's source field. It anchors the open seven-eighths statements of the mission against the classical result of the nineteenth century.

Preamble

import Mathlib
import Definitions.Def_SEF_theta
import Definitions.Def_SEF_hecke

Formal statement

/-!
# SEF: de la Vallée Poussin's classical zero-free region for the zeta function

There is an absolute constant $c > 0$ such that $\zeta(\sigma + it) \ne 0$
whenever $\sigma \ge 1 - c / \log(|t| + 2)$. This literature milestone is
included to anchor the open goals of the mission against the classical
results: it is the theorem of de la Vallée Poussin (1896), proved by the
Hadamard-de la Vallée Poussin method, whose corollary is the prime number
theorem. The Lean statement is drafted for this mission (there is no source
file for it); the citation is given in the item's source field. Proved in
the literature; draft: the proof is a `sorry`.
-/

namespace SEF

theorem zero_free_region_classical :
    ∃ c : ℝ, 0 < c ∧
      ∀ σ t : ℝ, 1 - c / Real.log (|t| + 2) ≤ σ → riemannZeta ⟨σ, t⟩ ≠ 0 := by
  sorry

end SEF

Source

C. J. de la Vallée Poussin, Recherches analytiques sur la théorie des nombres premiers, Annales de la Société Scientifique de Bruxelles 20 (1896) 183-256, the zero-free region (the Hadamard-de la Vallée Poussin method).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: there exists a real constant c, together with a proof that c is positive, such that for all real sigma and t, if the real part sigma is at least 1 - c / log(|t| + 2), then the Riemann zeta function evaluated at the complex number with real part sigma and imaginary part t is not zero. Hypotheses: none beyond the existential constant; the bound on sigma is the hypothesis of the nonvanishing conclusion, and the argument of the logarithm is |t| + 2, which is always positive, so the region is defined for every real t.

View graph