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 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_central_binom.

References #

Tags #

Bertrand, prime, binomial coefficients

source

theorem bertrand.real_main_inequality {x : ℝ} (n_large : 512 ≤ x) :

x * (2 * x) ^ √ (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.

source

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.

source

theorem central_binom_factorization_small (n : ℕ) (n_large : 2 < n) (no_prime : ¬∃ (p : ℕ), nat.prime p ∧ n < p ∧ p ≤ 2 * n) :

n.central_binom = (finset.range (2 * n / 3 + 1)).prod (λ (p : ℕ), p ^ ⇑(n.central_binom.factorization) 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.

source

theorem central_binom_le_of_no_bertrand_prime (n : ℕ) (n_big : 2 < n) (no_prime : ¬∃ (p : ℕ), nat.prime p ∧ n < p ∧ p ≤ 2 * n) :

n.central_binom ≤ (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 central_binom n into those

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

source

theorem nat.exists_prime_lt_and_le_two_mul_eventually (n : ℕ) (n_big : 512 ≤ n) :

∃ (p : ℕ), nat.prime p ∧ n < p ∧ p ≤ 2 * n

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

source

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.

source

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.

source

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.