mathlib3 documentation

data.nat.choose.factorization

Factorization of Binomial Coefficients #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

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.