# Bertrand's postulate

Despite it's name, Bertrand's postulate is actually a theorem rather than a postulate:

Theorem (Bertrand's Postulate): For every integer $n \geq 2$, there is a prime $p$ satisfying $n \lt p \lt 2n$.

The relevance of the postulate for the finding primes problem is that it guarantees the existence of a $k$-digit prime for any $k$. Brute force search thus yields a $k$-digit prime after about $O(10^k)$ steps; this can be considered the "trivial bound" for the problem.

This result was apparently first proved by Chebyshev. For large $n$, the claim follows as a consequence of the prime number theorem. We will give an elementary proof due to Erdos.

Our proof of Bertrand's postulate starts with a result independent interest, due to Chebyshev.

Lemma (Chebyshev bound): For integers $n \geq 2$,

$\prod_{p \leq n} p \leq 4^n,$

where the product is over all primes $p$ less than or equal to $n$.

[TBC]