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

• 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 : } :
↑() 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 ^ ↑() p n

A pow form of Nat.factorization_choose_le

theorem Nat.factorization_choose_le_one {p : } {n : } {k : } (p_large : n < p ^ 2) :
↑() 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) :
↑() 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) :
↑() 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) :
↑() p = 0
theorem Nat.factorization_choose_eq_zero_of_lt {p : } {n : } {k : } (h : n < p) :
↑() p = 0
theorem Nat.factorization_centralBinom_eq_zero_of_two_mul_lt {p : } {n : } (h : 2 * n < p) :
↑() 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 < ↑() 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) :
(Finset.prod (Finset.range (n + 1)) fun p => p ^ ↑() p) =

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

theorem Nat.prod_pow_factorization_centralBinom (n : ) :
(Finset.prod (Finset.range (2 * n + 1)) fun p => p ^ ↑() p) =

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