Concrete bounds for Chebyshev’s prime counting functions

This entry derives explicit lower and upper bounds for Chebyshev's prime counting functions \[\psi(x) = \sum_{\substack{p^k \leq x \\ k > 0}} \log p\hskip4em \vartheta(x) = \sum_{p\leq x} \log p\ .\]

Concretely, the following inequalities are proven:

• $\psi(x)\geq 0.9x$ for $x\geq 41$
• $\vartheta(x) \geq 0.82x$ if $x\geq 97$
• $\vartheta(x) \leq \psi(x) \leq 1.2x$ if $x\geq 0$

The proofs work by careful estimation of $\psi(x)$, with Stirling's formula as a starting point, to prove the bound for all $x\geq x_0$ with a concrete $x_0$, followed by brute-force approximation for all $x$ below $x_0$.

An easy corollary of this is Bertrand's postulate, i.e. the fact that for any $x > 1$ the interval $(x,2x)$ contains at least one prime (a fact that has already been shown in the AFP using weaker bounds for $\psi$ and $\vartheta$).