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 [math]\displaystyle{ n \geq 2 }[/math], there is a prime [math]\displaystyle{ p }[/math] satisfying [math]\displaystyle{ n \lt p \lt 2n }[/math].

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

This result was apparently first proved by Chebyshev. For large [math]\displaystyle{ n }[/math], 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 [math]\displaystyle{ n \geq 2 }[/math],

[math]\displaystyle{ \prod_{p \leq n} p \leq 4^n, }[/math]

where the product is over all primes [math]\displaystyle{ p }[/math] less than or equal to [math]\displaystyle{ n }[/math].

[TBC]