Bertrand's postulate

Since mathlib already pretty closely follows Proofs From The BOOK here, we on adapt a little here the proof formalized by Patrick Stevens and Bolton Bailey.

TODO

• rewrite the proof to follow even more closely what is done int The BOOK.
• Appendix: Some estimates
  • Estimating via integrals
  • Estimating factorials - Stirling's formula
  • Estimating binomial coefficients

theorem chapter2.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.

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

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

theorem chapter2.centralBinom_factorization_small (n : ℕ) (n_large : 2 < n) (no_prime : ¬∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) : n.centralBinom = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.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.

theorem chapter2.centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_big : 2 < n) (no_prime : ¬∃ (p : ℕ), Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 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 chapter2.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.

theorem chapter2.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 chapter2.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 chapter2.harmonic_number_bounds {n : ℕ} : Real.log ↑n + 1 / ↑n < ↑(harmonic n) ∧ ↑(harmonic n) < Real.log ↑n + 1

noncomputable def chapter2.e : ℝ

Equations

• chapter2.e = Real.exp 1

theorem chapter2.bound_factorial {n : ℕ} : ↑n.factorial < chapter2.e * (↑n / chapter2.e) ^ n

theorem chapter2.bound_binomial_coeff {k : ℕ} {n : ℕ} : n.choose k ≤ n ^ k / n.factorial ∧ n ^ k / n.factorial ≤ n ^ k / 2 ^ (k - 1)