Error term in the prime number theorem
TheoremPrime number theorem with error term for Chebyshev's \(\theta\)#●ready to prove
Let \(\theta(x) = \sum_{p \le x} \log p\) be the sum of \(\log p\) over the primes \(p \le x\). For every real \(\varepsilon > 0\), \(\theta(x) - x = O(x \exp(-(\log x)^{3/5 - \varepsilon}))\) as \(x \to \infty\).
public theorem_wanted prime_number_theorem_chebyshev_theta_error :
∀ epsilon : ℝ, 0 < epsilon →
(fun x : ℝ => Chebyshev.theta x - x) =O[Filter.atTop]
(fun x : ℝ => x * Real.exp (-(Real.rpow (Real.log x) ((3 / 5 : ℝ) - epsilon))))Sources
- Julian Ransford, "A Sum of Gcd's over Friable Numbers", Journal of Integer Sequences 19 (2016), Prime Number Theorem at lines 288–292; URL: https://cs.uwaterloo.ca/journals/JIS/VOL19/Ransford/ransford2.tex
TheoremDusart's bound for \(\vartheta\) and \(\psi\) from a zero-free region#●ready to prove
Let \(R = 5.69693\), let \(\log\) be the natural logarithm, and let \(\vartheta(x) = \sum_{p \le x} \log p\) (over primes \(p\)) and \(\psi(x) = \sum_{n \le x} \Lambda(n)\), with \(\Lambda\) the von Mangoldt function, be Chebyshev's functions. Suppose the Riemann zeta function has no zero \(s\) with \(|\operatorname{Im} s| \ge 2\pi\) and \(\operatorname{Re} s \ge 1 - \frac{1}{R \log |\operatorname{Im} s|}\). Then for every real number \(x \ge \exp\bigl(R \max(8.36, 8/R)^2\bigr)\), writing \(X = \sqrt{(\log x)/R}\),
public theorem_wanted dusart2016_tail_theorem
(hzfr : ∀ s : ℂ, 2 * Real.pi ≤ |s.im| →
1 - 1 / (5.69693 * Real.log |s.im|) ≤ s.re → riemannZeta s ≠ 0)
(x : ℝ) (hx : Real.exp (5.69693 * (max 8.36 (8 / 5.69693)) ^ 2) ≤ x) :
max |Chebyshev.theta x - x| |Chebyshev.psi x - x|
< x * Real.sqrt (8 / Real.pi)
* Real.sqrt (Real.sqrt (Real.log x / 5.69693))
* Real.exp (-(Real.sqrt (Real.log x / 5.69693)))Sources
- Pierre Dusart, Estimates of ψ, θ for large values of x without the Riemann hypothesis, Math. Comp. 85 (2016), 875–888, Theorem 1.1.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.