Documentation

Mathlib.Data.Nat.Choose.Factorization

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:

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) :
pFinset.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 : ) :
pFinset.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.