Bertrand's Postulate

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 n 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 Nat.four_pow_lt_mul_centralBinom.

References

• [M. Aigner and G. M. Ziegler Proofs from THE BOOK][aigner1999proofs]
• [S. Tochiori, Considering the Proof of “There is a Prime between n and 2n”][tochiori_bertrand]
• [M. Carneiro, Arithmetic in Metamath, Case Study: Bertrand's Postulate][carneiro2015arithmetic]

Tags

Bertrand, prime, binomial coefficients

theorem Bertrand.real_main_inequality {x : ℝ} (x_large : 512 ≤ x) : x * (2 * x) ^ Real.sqrt (2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x

A reified version of the Bertrand.main_inequality below. This is not best possible: it actually holds for 464 ≤ x.

theorem bertrand_main_inequality {n : ℕ} (n_large : 512 ≤ n) : n * (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n

The inequality which contradicts Bertrand's postulate, for large enough n.

theorem centralBinom_factorization_small (n : ℕ) (n_large : 2 < n) (no_prime : ¬∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) : Nat.centralBinom n = Finset.prod (Finset.range (2 * n / 3 + 1)) fun (p : ℕ) => p ^ (Nat.factorization (Nat.centralBinom n)) p

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.

theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_large : 2 < n) (no_prime : ¬∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) : Nat.centralBinom n ≤ (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3)

An upper bound on the central binomial coefficient used in the proof of Bertrand's postulate. The bound splits the prime factors of centralBinom n into those

1. At most sqrt (2 * n), which contribute at most 2 * n for each such prime.
2. Between sqrt (2 * n) and 2 * n / 3, which contribute at most 4^(2 * n / 3) in total.
3. Between 2 * n / 3 and n, which do not exist.
4. Between n and 2 * n, which would not exist in the case where Bertrand's postulate is false.
5. Above 2 * n, which do not exist.

theorem Nat.exists_prime_lt_and_le_two_mul_eventually (n : ℕ) (n_large : 512 ≤ n) : ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

Proves that Bertrand's postulate holds for all sufficiently large n.

theorem Nat.exists_prime_lt_and_le_two_mul_succ {n : ℕ} (q : ℕ) {p : ℕ} (prime_p : Nat.Prime p) (covering : p ≤ 2 * q) (H : n < q → ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) (hn : n < p) : ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

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.

theorem Nat.exists_prime_lt_and_le_two_mul (n : ℕ) (hn0 : n ≠ 0) : ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

Bertrand's Postulate: For any positive natural number, there is a prime which is greater than it, but no more than twice as large.

theorem Nat.bertrand (n : ℕ) (hn0 : n ≠ 0) : ∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

Alias of Nat.exists_prime_lt_and_le_two_mul.

---

Bertrand's Postulate: For any positive natural number, there is a prime which is greater than it, but no more than twice as large.