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:

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.

theorem nat.factorization_choose_le_log {p n k : ℕ} :

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_factorial_eq_zero_of_lt {p n : ℕ} (h : n < p) :

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

p ≤ 2 * n

theorem nat.prod_pow_factorization_choose (n k : ℕ) (hkn : k ≤ n) :

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.