Chebyshev bound $\psi(N)\le N\log N$

Proved

Vino.psi_le

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methodnumber-theoryprime-numbers

For every $N\ge1$ ,

\psi(N)=\sum_{n<N}\Lambda(n)\;\le\;N\log N.

This crude form of Chebyshev's estimate is all that is needed to make the trivial bound on the prime-side generating function explicit; no prime number theorem is involved.

Preamble

import Definitions.Def_Vino_primes
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Finset

Formal statement

namespace Vino

theorem psi_le (N : ℕ) (hN : 1 ≤ N) : psi N ≤ (N : ℝ) * Real.log N := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Chapter 3 (the three primes theorem).

View graph

Chebyshev bound ψ(N)≤Nlog⁡N\psi(N)\le N\log Nψ(N)≤NlogN

Chebyshev bound $\psi(N)\le N\log N$