Factorization of Binomial Coefficients

This file contains a few results on the multiplicity of prime factors within certain size bounds in binomial coefficients. These include:

• Nat.factorization_choose_le_log: a logarithmic upper bound on the multiplicity of a prime in a binomial coefficient.
• Nat.factorization_choose_le_one: Primes above sqrt n appear at most once in the factorization of n choose k.
• Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul: Primes from 2 * n / 3 to n do not appear in the factorization of the nth central binomial coefficient.
• Nat.factorization_choose_eq_zero_of_lt: Primes greater than n do not appear in the factorization of n choose k.

These results appear in the Erdős proof of Bertrand's postulate.

theorem Nat.factorization_choose_le_log {p : ℕ} {n : ℕ} {k : ℕ} : (n.choose k).factorization p ≤ Nat.log p n

A logarithmic upper bound on the multiplicity of a prime in a binomial coefficient.

theorem Nat.pow_factorization_choose_le {p : ℕ} {n : ℕ} {k : ℕ} (hn : 0 < n) : p ^ (n.choose k).factorization p ≤ n

A pow form of Nat.factorization_choose_le

theorem Nat.factorization_choose_le_one {p : ℕ} {n : ℕ} {k : ℕ} (p_large : n < p ^ 2) : (n.choose k).factorization p ≤ 1

Primes greater than about sqrt n appear only to multiplicity 0 or 1 in the binomial coefficient.

theorem Nat.factorization_choose_of_lt_three_mul {p : ℕ} {n : ℕ} {k : ℕ} (hp' : p ≠ 2) (hk : p ≤ k) (hk' : p ≤ n - k) (hn : n < 3 * p) : (n.choose k).factorization p = 0

theorem Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul {p : ℕ} {n : ℕ} (n_big : 2 < n) (p_le_n : p ≤ n) (big : 2 * n < 3 * p) : n.centralBinom.factorization p = 0

Primes greater than about 2 * n / 3 and less than n do not appear in the factorization of centralBinom n.

theorem Nat.factorization_factorial_eq_zero_of_lt {p : ℕ} {n : ℕ} (h : n < p) : n.factorial.factorization p = 0

theorem Nat.factorization_choose_eq_zero_of_lt {p : ℕ} {n : ℕ} {k : ℕ} (h : n < p) : (n.choose k).factorization p = 0

theorem Nat.factorization_centralBinom_eq_zero_of_two_mul_lt {p : ℕ} {n : ℕ} (h : 2 * n < p) : n.centralBinom.factorization p = 0

If a prime p has positive multiplicity in the nth central binomial coefficient, p is no more than 2 * n

theorem Nat.le_two_mul_of_factorization_centralBinom_pos {p : ℕ} {n : ℕ} (h_pos : 0 < n.centralBinom.factorization p) : p ≤ 2 * n

Contrapositive form of Nat.factorization_centralBinom_eq_zero_of_two_mul_lt

theorem Nat.prod_pow_factorization_choose (n : ℕ) (k : ℕ) (hkn : k ≤ n) : ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k

A binomial coefficient is the product of its prime factors, which are at most n.

theorem Nat.prod_pow_factorization_centralBinom (n : ℕ) : ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p = n.centralBinom

The nth central binomial coefficient is the product of its prime factors, which are at most 2n.