mathlib3 documentation

data.nat.choose.basic

Binomial coefficients #

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

This file defines binomial coefficients and proves simple lemmas (i.e. those not requiring more imports).

Main definition and results #

Tags #

binomial coefficient, combination, multicombination, stars and bars

source
def nat.choose  :
ℕ → ℕ → ℕ

choose n k is the number of k-element subsets in an n-element set. Also known as binomial coefficients.

Equations
source
@[simp]
theorem nat.choose_zero_right (n : ℕ) :
n.choose 0 = 1
source
@[simp]
theorem nat.choose_zero_succ (k : ℕ) :
0.choose k.succ = 0
source
theorem nat.choose_succ_succ (n k : ℕ) :
n.succ.choose k.succ = n.choose k + n.choose k.succ
source
theorem nat.choose_eq_zero_of_lt {n k : ℕ} :
n < k → n.choose k = 0
source
@[simp]
theorem nat.choose_self (n : ℕ) :
n.choose n = 1
source
@[simp]
theorem nat.choose_succ_self (n : ℕ) :
n.choose n.succ = 0
source
@[simp]
theorem nat.choose_one_right (n : ℕ) :
n.choose 1 = n
source
theorem nat.triangle_succ (n : ℕ) :
(n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n
source
theorem nat.choose_two_right (n : ℕ) :
n.choose 2 = n * (n - 1) / 2

choose n 2 is the n-th triangle number.

source
theorem nat.choose_pos {n k : ℕ} :
k ≤ n → 0 < n.choose k
source
theorem nat.choose_eq_zero_iff {n k : ℕ} :
n.choose k = 0 ↔ n < k
source
theorem nat.succ_mul_choose_eq (n k : ℕ) :
n.succ * n.choose k = n.succ.choose k.succ * k.succ
source
theorem nat.choose_mul_factorial_mul_factorial {n k : ℕ} :
k ≤ n → n.choose k * k.factorial * (n - k).factorial = n.factorial
source
theorem nat.choose_mul {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) :
n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
source
theorem nat.choose_eq_factorial_div_factorial {n k : ℕ} (hk : k ≤ n) :
n.choose k = n.factorial / (k.factorial * (n - k).factorial)
source
theorem nat.add_choose (i j : ℕ) :
(i + j).choose j = (i + j).factorial / (i.factorial * j.factorial)
source
theorem nat.add_choose_mul_factorial_mul_factorial (i j : ℕ) :
(i + j).choose j * i.factorial * j.factorial = (i + j).factorial
source
theorem nat.factorial_mul_factorial_dvd_factorial {n k : ℕ} (hk : k ≤ n) :
k.factorial * (n - k).factorial ∣ n.factorial
source
theorem nat.factorial_mul_factorial_dvd_factorial_add (i j : ℕ) :
i.factorial * j.factorial ∣ (i + j).factorial
source
@[simp]
theorem nat.choose_symm {n k : ℕ} (hk : k ≤ n) :
n.choose (n - k) = n.choose k
source
theorem nat.choose_symm_of_eq_add {n a b : ℕ} (h : n = a + b) :
n.choose a = n.choose b
source
theorem nat.choose_symm_add {a b : ℕ} :
(a + b).choose a = (a + b).choose b
source
theorem nat.choose_symm_half (m : ℕ) :
(2 * m + 1).choose (m + 1) = (2 * m + 1).choose m
source
theorem nat.choose_succ_right_eq (n k : ℕ) :
n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
source
@[simp]
theorem nat.choose_succ_self_right (n : ℕ) :
(n + 1).choose n = n + 1
source
theorem nat.choose_mul_succ_eq (n k : ℕ) :
n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)
source
theorem nat.asc_factorial_eq_factorial_mul_choose (n k : ℕ) :
n.asc_factorial k = k.factorial * (n + k).choose k
source
theorem nat.factorial_dvd_asc_factorial (n k : ℕ) :
k.factorial ∣ n.asc_factorial k
source
theorem nat.choose_eq_asc_factorial_div_factorial (n k : ℕ) :
(n + k).choose k = n.asc_factorial k / k.factorial
source
theorem nat.desc_factorial_eq_factorial_mul_choose (n k : ℕ) :
n.desc_factorial k = k.factorial * n.choose k
source
theorem nat.factorial_dvd_desc_factorial (n k : ℕ) :
k.factorial ∣ n.desc_factorial k
source
theorem nat.choose_eq_desc_factorial_div_factorial (n k : ℕ) :
n.choose k = n.desc_factorial k / k.factorial

Inequalities #

source
theorem nat.choose_le_succ_of_lt_half_left {r n : ℕ} (h : r < n / 2) :
n.choose r ≤ n.choose (r + 1)

Show that nat.choose is increasing for small values of the right argument.

source
theorem nat.choose_le_middle (r n : ℕ) :
n.choose r ≤ n.choose (n / 2)

choose n r is maximised when r is n/2.

Inequalities about increasing the first argument #

source
theorem nat.choose_le_succ (a c : ℕ) :
a.choose c ≤ a.succ.choose c
source
theorem nat.choose_le_add (a b c : ℕ) :
a.choose c ≤ (a + b).choose c
source
theorem nat.choose_le_choose {a b : ℕ} (c : ℕ) (h : a ≤ b) :
a.choose c ≤ b.choose c
source
theorem nat.choose_mono (b : ℕ) :
monotone (λ (a : ℕ), a.choose b)

Multichoose #

Whereas choose n k is the number of subsets of cardinality k from a type of cardinality n, multichoose n k is the number of multisets of cardinality k from a type of cardinality n.

Alternatively, whereas choose n k counts the number of combinations, i.e. ways to select k items (up to permutation) from n items without replacement, multichoose n k counts the number of multicombinations, i.e. ways to select k items (up to permutation) from n items with replacement.

Note that multichoose is not the multinomial coefficient, although it can be computed in terms of multinomial coefficients. For details see https://mathworld.wolfram.com/Multichoose.html

TODO: Prove that choose (-n) k = (-1)^k * multichoose n k, where choose is the generalized binomial coefficient. https://github.com/leanprover-community/mathlib/pull/15072#issuecomment-1171415738

source
def nat.multichoose  :
ℕ → ℕ → ℕ

multichoose n k is the number of multisets of cardinality k from a type of cardinality n.

Equations
source
@[simp]
theorem nat.multichoose_zero_right (n : ℕ) :
n.multichoose 0 = 1
source
@[simp]
theorem nat.multichoose_zero_succ (k : ℕ) :
0.multichoose (k + 1) = 0
source
theorem nat.multichoose_succ_succ (n k : ℕ) :
(n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k
source
@[simp]
theorem nat.multichoose_one (k : ℕ) :
1.multichoose k = 1
source
@[simp]
theorem nat.multichoose_two (k : ℕ) :
2.multichoose k = k + 1
source
@[simp]
theorem nat.multichoose_one_right (n : ℕ) :
n.multichoose 1 = n
source
theorem nat.multichoose_eq (n k : ℕ) :
n.multichoose k = (n + k - 1).choose k