The Riemann hypothesis implies the von Koch psi-error bound

Open

LandauCriterion.psi_error_of_riemannHypothesis

by pitimespi · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorychebyshev-functionsriemann-hypothesis

Assume the Riemann hypothesis. Then the Chebyshev function $\psi$ satisfies the von Koch error bound: there is a constant $C$ such that $|\psi(x) - x| \le C\sqrt{x}(\log x)^2$ for all real $x \ge 2$ . This is the forward analytic direction of the criterion: it is the hypothesis that the already-Proved bridge theta_error_of_psi_error transfers from $\psi$ to $\theta$ .

Preamble

import Mathlib

Formal statement

namespace LandauCriterion
theorem psi_error_of_riemannHypothesis (hRH : RiemannHypothesis) :
    ∃ C : ℝ, ∀ x : ℝ, 2 ≤ x → |Chebyshev.psi x - x| ≤ C * Real.sqrt x * (Real.log x) ^ 2 := by sorry
end LandauCriterion

Source

H. von Koch, Sur la distribution des nombres premiers, Acta Math. 24 (1901); the Riemann hypothesis is Mathlib's `RiemannHypothesis`, and `Chebyshev.psi` is Mathlib's Chebyshev function.

Read-back

What the Lean code literally says, in plain math · Muse Spark

Assuming the hypothesis denoted $\mathrm{RiemannHypothesis}$ , there exists a real number $C$ — with no condition imposed on $C$ in the statement, so in particular no requirement that it be positive — such that for every real number $x$ , if $2 \le x$ , then $\lvert \mathrm{Chebyshev.psi}(x) - x \rvert \le C \cdot \sqrt{x} \cdot (\log x)^2$ . The claim is made only for $x \ge 2$ and says nothing about smaller values of $x$ ; for $x \ge 2$ the quantities $\sqrt{x}$ and $\log x$ are evaluated at positive arguments, with $\log x > 0$ when $x > 2$ and $\log 2 > 0$ , so the sign of the right-hand side is the sign of $C$ .

Human review

Endorsed by Shuze Chen · Nov 3, 2026
Confirmed by the moderator at approval.
Endorsed by pitimespi · Nov 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph