Natural number multiplicity

This file contains lemmas about the multiplicity function (the maximum prime power dividing a number) when applied to naturals, in particular calculating it for factorials and binomial coefficients.

Multiplicity calculations

• Nat.Prime.multiplicity_factorial: Legendre's Theorem. The multiplicity of p in n! is n / p + ... + n / p ^ b for any b such that n / p ^ (b + 1) = 0. See padicValNat_factorial for this result stated in the language of p-adic valuations and sub_one_mul_padicValNat_factorial for a related result.
• Nat.Prime.multiplicity_factorial_mul: The multiplicity of p in (p * n)! is n more than that of n!.
• Nat.Prime.multiplicity_choose: Kummer's Theorem. The multiplicity of p in n.choose k is the number of carries when k and n - k are added in base p. See padicValNat_choose for the same result but stated in the language of p-adic valuations and sub_one_mul_padicValNat_choose_eq_sub_sum_digits for a related result.

Other declarations

• Nat.multiplicity_eq_card_pow_dvd: The multiplicity of m in n is the number of positive natural numbers i such that m ^ i divides n.
• Nat.multiplicity_two_factorial_lt: The multiplicity of 2 in n! is strictly less than n.
• Nat.Prime.multiplicity_something: Specialization of multiplicity.something to a prime in the naturals. Avoids having to provide p ≠ 1 and other trivialities, along with translating between Prime and Nat.Prime.

Tags

Legendre, p-adic

theorem Nat.emultiplicity_eq_card_pow_dvd {m : ℕ} {n : ℕ} {b : ℕ} (hm : m ≠ 1) (hn : 0 < n) (hb : Nat.log m n < b) : emultiplicity m n = ↑(Finset.filter (fun (i : ℕ) => m ^ i ∣ n) (Finset.Ico 1 b)).card

The multiplicity of m in n is the number of positive natural numbers i such that m ^ i divides n. This set is expressed by filtering Ico 1 b where b is any bound greater than log m n.

theorem Nat.Prime.emultiplicity_one {p : ℕ} (hp : Nat.Prime p) : emultiplicity p 1 = 0

theorem Nat.Prime.emultiplicity_mul {p : ℕ} {m : ℕ} {n : ℕ} (hp : Nat.Prime p) : emultiplicity p (m * n) = emultiplicity p m + emultiplicity p n

theorem Nat.Prime.emultiplicity_pow {p : ℕ} {m : ℕ} {n : ℕ} (hp : Nat.Prime p) : emultiplicity p (m ^ n) = ↑n * emultiplicity p m

theorem Nat.Prime.emultiplicity_self {p : ℕ} (hp : Nat.Prime p) : emultiplicity p p = 1

theorem Nat.Prime.emultiplicity_pow_self {p : ℕ} {n : ℕ} (hp : Nat.Prime p) : emultiplicity p (p ^ n) = ↑n

theorem Nat.Prime.emultiplicity_factorial {p : ℕ} (hp : Nat.Prime p) {n : ℕ} {b : ℕ} : Nat.log p n < b → emultiplicity p n.factorial = ↑(∑ 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.Prime.sub_one_mul_multiplicity_factorial {n : ℕ} {p : ℕ} (hp : Nat.Prime p) : (p - 1) * multiplicity p n.factorial = n - (p.digits n).sum

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

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

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

theorem Nat.Prime.emultiplicity_factorial_mul {n : ℕ} {p : ℕ} (hp : Nat.Prime p) : emultiplicity p (p * n).factorial = emultiplicity p n.factorial + ↑n

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

theorem Nat.Prime.pow_dvd_factorial_iff {p : ℕ} {n : ℕ} {r : ℕ} {b : ℕ} (hp : Nat.Prime p) (hbn : Nat.log p n < b) : p ^ r ∣ n.factorial ↔ r ≤ ∑ i ∈ Finset.Ico 1 b, n / p ^ i

A prime power divides n! iff it is at most the sum of the quotients n / p ^ i. This sum is expressed over the set Ico 1 b where b is any bound greater than log p n

theorem Nat.Prime.emultiplicity_factorial_le_div_pred {p : ℕ} (hp : Nat.Prime p) (n : ℕ) : emultiplicity p n.factorial ≤ ↑(n / (p - 1))

theorem Nat.Prime.multiplicity_choose_aux {p : ℕ} {n : ℕ} {b : ℕ} {k : ℕ} (hp : Nat.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 + (Finset.filter (fun (i : ℕ) => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card

theorem Nat.Prime.emultiplicity_choose' {p : ℕ} {n : ℕ} {k : ℕ} {b : ℕ} (hp : Nat.Prime p) (hnb : Nat.log p (n + k) < b) : emultiplicity p ((n + k).choose k) = ↑(Finset.filter (fun (i : ℕ) => p ^ i ≤ k % p ^ i + n % p ^ i) (Finset.Ico 1 b)).card

The multiplicity 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.Prime.emultiplicity_choose {p : ℕ} {n : ℕ} {k : ℕ} {b : ℕ} (hp : Nat.Prime p) (hkn : k ≤ n) (hnb : Nat.log p n < b) : emultiplicity p (n.choose k) = ↑(Finset.filter (fun (i : ℕ) => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card

The multiplicity 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.Prime.emultiplicity_le_emultiplicity_choose_add {p : ℕ} (hp : Nat.Prime p) (n : ℕ) (k : ℕ) : emultiplicity p n ≤ emultiplicity p (n.choose k) + emultiplicity p k

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

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

theorem Nat.Prime.emultiplicity_choose_prime_pow {p : ℕ} {n : ℕ} {k : ℕ} (hp : Nat.Prime p) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) : emultiplicity p ((p ^ n).choose k) = ↑(n - multiplicity p k)

theorem Nat.Prime.dvd_choose_pow {p : ℕ} {n : ℕ} {k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) (hkp : k ≠ p ^ n) : p ∣ (p ^ n).choose k

theorem Nat.Prime.dvd_choose_pow_iff {p : ℕ} {n : ℕ} {k : ℕ} (hp : Nat.Prime p) : p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

theorem Nat.emultiplicity_two_factorial_lt {n : ℕ} : n ≠ 0 → emultiplicity 2 n.factorial < ↑n