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_factorial {p : ℕ} (hp : Prime p) {n b : ℕ} : log p n < b → n.factorial.factorization p = ∑ i ∈ Finset.Ico 1 b, n / p ^ i

Legendre's Theorem

The multiplicity of a prime in n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

theorem Nat.sub_one_mul_factorization_factorial {n p : ℕ} (hp : Prime p) : (p - 1) * n.factorial.factorization p = n - (p.digits n).sum

For a prime number p, taking (p - 1) times the factorization of p in n! equals n minus the sum of base p digits of n.

theorem Nat.factorization_factorial_mul_succ {n p : ℕ} (hp : Prime p) : (p * (n + 1)).factorial.factorization p = (p * n).factorial.factorization p + (n + 1).factorization p + 1

The factorization of p in (p * (n + 1))! is one more than the sum of the factorizations of p in (p * n)! and n + 1.

theorem Nat.factorization_factorial_mul {n p : ℕ} (hp : Prime p) : (p * n).factorial.factorization p = n.factorial.factorization p + n

The factorization of p in (p * n)! is n more than that of n!.

theorem Nat.factorization_factorial_le_div_pred {p : ℕ} (hp : Prime p) (n : ℕ) : n.factorial.factorization p ≤ n / (p - 1)

theorem Nat.multiplicity_choose_aux {p n b k : ℕ} (hp : Prime p) (hkn : k ≤ n) : ∑ i ∈ Finset.Ico 1 b, n / p ^ i = ∑ i ∈ Finset.Ico 1 b, k / p ^ i + ∑ i ∈ Finset.Ico 1 b, (n - k) / p ^ i + {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card

theorem Nat.factorization_choose' {p n k b : ℕ} (hp : Prime p) (hnb : log p (n + k) < b) : ((n + k).choose k).factorization p = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card

The factorization of p in choose (n + k) k is the number of carries when k and n are added in base p. The set is expressed by filtering Ico 1 b where b is any bound greater than log p (n + k).

theorem Nat.factorization_choose {p n k b : ℕ} (hp : Prime p) (hkn : k ≤ n) (hnb : log p n < b) : (n.choose k).factorization p = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}.card

The factorization of p in choose n k is the number of carries when k and n - k are added in base p. The set is expressed by filtering Ico 1 b where b is any bound greater than log p n.

theorem Nat.factorization_le_factorization_of_dvd_right {a b c : ℕ} (h : b ∣ c) (hb : b ≠ 0) (hc : c ≠ 0) : b.factorization a ≤ c.factorization a

Modified version of emultiplicity_le_emultiplicity_of_dvd_right but for factorization.

theorem Nat.factorization_le_factorization_choose_add {p n k : ℕ} : k ≤ n → k ≠ 0 → n.factorization p ≤ (n.choose k).factorization p + k.factorization p

A lower bound on the factorization of p in choose n k.

theorem Nat.factorization_choose_prime_pow_add_factorization {p n k : ℕ} (hp : Prime p) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : ((p ^ n).choose k).factorization p + k.factorization p = n

theorem Nat.factorization_choose_prime_pow {p n k : ℕ} (hp : Prime p) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : ((p ^ n).choose k).factorization p = n - k.factorization p

theorem Nat.factorization_choose_le_log {p n k : ℕ} : (n.choose k).factorization p ≤ 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) : ∏ p ∈ Finset.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 : ℕ) : ∏ p ∈ Finset.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.