Rosser–Schoenfeld: $\psi(x) \lt 1.03883\,x$

Proved

TaoFivePrimes.rosser_schoenfeld_psi_bound

by shivm · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorychebyshevexplicit-boundsnumber-theorytao-five-primes

For every positive integer $x$ , the second Chebyshev function satisfies

\psi(x) \;=\; \sum_{n \le x} \Lambda(n) \;\lt\; 1.03883\,x .

This is the explicit prime-mass estimate of Rosser and Schoenfeld, and the constant is sharp in the sense that it cannot be replaced by anything much smaller: the ratio $\psi(x)/x$ comes within a fraction of a percent of $1.03883$ near $x = 113$ , so the bound must be verified against the small- $x$ regime and not only asymptotically. That is what distinguishes it from softer Chebyshev bounds such as $\psi(x) \le x\log 4$ , which are far weaker.

It enters Tao's argument as the crude upper bound on total prime mass used to control error terms.

Provenance note. This statement was previously bundled, in a single platform node, with an unrelated Montgomery large-sieve estimate. The two come from different papers and neither depends on the other, so they are separated here.

Formalization note. The sum is written over Finset.range (x + 1), i.e. over $n \le x$ , and $\Lambda$ is Mathlib's ArithmeticFunction.vonMangoldt. Note that the mission also carries the weaker psi_le_112_large, with constant $1.12$ and only for large $x$ ; that result does not imply this one.

Preamble

import Definitions.Def_TaoFivePrimes_ArcSplit
import Mathlib.MeasureTheory.Integral.Bochner.Set

open scoped BigOperators ArithmeticFunction.vonMangoldt
open MeasureTheory

Formal statement

namespace TaoFivePrimes

theorem rosser_schoenfeld_psi_bound :
    ∀ x : ℕ, 0 < x →
      (∑ n ∈ Finset.range (x + 1), (Λ n : ℝ)) <
        1.03883 * (x : ℝ) := by
  sorry

end TaoFivePrimes

Source

J. Barkley Rosser and Lowell Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois J. Math. 6 (1962), 64-94, Theorem 12 (psi(x) < 1.03883 x). Used in Terence Tao, arXiv:1201.6656v4, Section 4.

View graph

Rosser–Schoenfeld: ψ(x)<1.03883 x\psi(x) \lt 1.03883\,xψ(x)<1.03883x

Rosser–Schoenfeld: $\psi(x) \lt 1.03883\,x$