Bertrand's Postulate #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains a proof of Bertrand's postulate: That between any positive number and its double there is a prime.
The proof follows the outline of the Erdős proof presented in "Proofs from THE BOOK": One considers
the prime factorization of
(2 * n).choose n, and splits the constituent primes up into various
groups, then upper bounds the contribution of each group. This upper bounds the central binomial
coefficient, and if the postulate does not hold, this upper bound conflicts with a simple lower
bound for large enough
n. This proves the result holds for large enough
n, and for smaller
an explicit list of primes is provided which covers the remaining cases.
As in the Metamath implementation, we rely on some optimizations from
Shigenori Tochiori. In particular we use the cleaner bound on the central
binomial coefficient given in
- M. Aigner and G. M. Ziegler Proofs from THE BOOK
- S. Tochiori, Considering the Proof of “There is a Prime between n and 2n”
- M. Carneiro, Arithmetic in Metamath, Case Study: Bertrand's Postulate
Bertrand, prime, binomial coefficients
A lemma that tells us that, in the case where Bertrand's postulate does not hold, the prime
factorization of the central binomial coefficent only has factors at most
2 * n / 3 + 1.
An upper bound on the central binomial coefficient used in the proof of Bertrand's postulate.
The bound splits the prime factors of
central_binom n into those
- At most
sqrt (2 * n), which contribute at most
2 * nfor each such prime.
sqrt (2 * n)and
2 * n / 3, which contribute at most
4^(2 * n / 3)in total.
2 * n / 3and
n, which do not exist.
2 * n, which would not exist in the case where Bertrand's postulate is false.
2 * n, which do not exist.
Proves that Bertrand's postulate holds over all positive naturals less than n by identifying a descending list of primes, each no more than twice the next, such that the list contains a witness for each number ≤ n.