Axler explicit fourth-power logarithmic theta error

Open

TaoFivePrimes.axler_theta_error_log_four

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryprime-number-theorem

For every real $x\ge70111$ , the Chebyshev theta function satisfies

|\vartheta(x)-x|<\frac{100x}{\log^4 x},\qquad \vartheta(x)=\sum_{p\le x}\log p.

This quantitative prime number theorem estimate is Proposition 1 of Axler (2018). It provides a reusable input for partial-summation estimates of reciprocal primes and Euler products. The statement includes the whole certified threshold range; the numerical verification and analytic estimates in the source remain to be formalized.

Preamble

import Mathlib

Formal statement

theorem TaoFivePrimes.axler_theta_error_log_four (x : ℝ) (hx : 70111 ≤ x) :
  |(∑ p ∈ Nat.primesLE ⌊x⌋₊, Real.log (p : ℝ)) - x| <
    100 * x / (Real.log x) ^ 4 := by sorry

Source

Christian Axler, New Estimates for Some Functions Defined over Primes, Integers 18 (2018), A52, p. 6, Proposition 1, equation (2.4). https://math.colgate.edu/~integers/s52/s52.pdf

View graph