# mathlibdocumentation

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:

• 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_central_binom_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.

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

A pow form of nat.factorization_choose_le

theorem nat.factorization_choose_le_one {p n k : } (p_large : n < p ^ 2) :

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) :
theorem nat.factorization_central_binom_of_two_mul_self_lt_three_mul {p n : } (n_big : 2 < n) (p_le_n : p n) (big : 2 * n < 3 * p) :

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

theorem nat.factorization_choose_eq_zero_of_lt {p n k : } (h : n < p) :

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

Contrapositive form of nat.factorization_central_binom_eq_zero_of_two_mul_lt

theorem nat.prod_pow_factorization_choose (n k : ) (hkn : k n) :
(finset.range (n + 1)).prod (λ (p : ), p ^ ((n.choose k).factorization) p) = n.choose k

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

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