Prove2Me

Nonnegativity of ψ\psi

Proved
Vino.psi_nonneg

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

analytic-number-theorycircle-methodnumber-theoryprime-numbers

Chebyshev's function ψ(N)=∑n<NΛ(n)\psi(N)=\sum_{n<N}\Lambda(n) is nonnegative:

0≤ψ(N)for every N.0\le\psi(N)\qquad\text{for every }N.

It is the value of the prime-side generating function at the origin, so its nonnegativity is what makes the trivial bound on the exponential sum a genuine bound.

Preamble
import Definitions.Def_Vino_primes
import Mathlib.Analysis.SpecialFunctions.Log.Basic
open Finset
Formal statement
namespace Vino

theorem psi_nonneg (N : ℕ) : 0 ≤ psi 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