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 _{\begin{array}{c}{p}^k\le x\\ k>0\end{array}}\log p\vartheta (x)=\sum _{p\le x}\log p.$$

Concretely, the following inequalities are proven:

• $\psi (x)\ge 0.9x$ for $x\ge 41$
• $\vartheta (x)\ge 0.82x$ if $x\ge 97$
• $\vartheta (x)\le \psi (x)\le 1.2x$ if $x\ge 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\ge 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$).