Dusart's global fourth-power logarithmic error bound for the Chebyshev theta function

Open

TaoFivePrimes.dusart_theta_error_log_four_chebyshev

by Creamycream · Sep 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryprime-number-theorem

Let the Chebyshev theta function be

\vartheta(x)=\sum_{p\le x}\log p,

where the sum ranges over primes. For every real number $x\ge 2$ ,

|\vartheta(x)-x|\le \frac{151.3x}{(\log x)^4}.

This is the $k=4$ , $\eta_4=151.3$ , $x_4=2$ entry of Dusart's explicit estimate. Dusart proves the strict inequality; the displayed non-strict form is its immediate weakening and is convenient as a reusable analytic input.

Formalization Note The function $\vartheta$ is represented by Mathlib's Chebyshev.theta.

Preamble

import Mathlib

Formal statement

namespace TaoFivePrimes

theorem dusart_theta_error_log_four_chebyshev (x : ℝ) (hx : 2 ≤ x) :
    |Chebyshev.theta x - x| ≤
      (1513 / 10 : ℝ) * x / (Real.log x) ^ 4 := by sorry

end TaoFivePrimes

Source

Pierre Dusart, Explicit estimates of some functions over primes, Ramanujan J. 45 (2018), 227–251, Theorem 4.2, p. 237, k=4, eta=151.3, x0=2; DOI 10.1007/s11139-016-9839-4. https://piyanit.nl/wp-content/uploads/2020/10/art_10.1007_s11139-016-9839-4.pdf

View graph