Dusart theta error beyond the tabulated range

Open

TaoFivePrimes.dusart_theta_error_log_four_tail

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

explicit-boundsnumber-theoryprime-number-theorem

For every real $x\ge e^{13900}$ , the Chebyshev theta function satisfies

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

This is the large-value part of Dusart's Theorem 4.2, obtained in the paper from the explicit zero-free-region estimate cited as [10, Theorem 1.1], combined with the bound for $|\psi(x)-\vartheta(x)|$ .

Preamble

import Mathlib.NumberTheory.Chebyshev

Formal statement

namespace TaoFivePrimes

theorem dusart_theta_error_log_four_tail (x : ℝ)
    (hx : Real.exp 13900 ≤ 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 and its proof, pp. 234-237; Table 1 through b = 13900 and the large-value argument citing [10, Theorem 1.1]. 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