Binomial coefficients

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

Main definition and results

• Nat.choose: binomial coefficients, defined inductively
• Nat.choose_eq_factorial_div_factorial: a proof that choose n k = n! / (k! * (n - k)!)
• Nat.choose_symm: symmetry of binomial coefficients
• Nat.choose_le_succ_of_lt_half_left: choose n k is increasing for small values of k
• Nat.choose_le_middle: choose n r is maximised when r is n/2
• Nat.descFactorial_eq_factorial_mul_choose: Relates binomial coefficients to the descending factorial. This is used to prove Nat.choose_le_pow and variants. We provide similar statements for the ascending factorial.
• Nat.multichoose: whereas choose counts combinations, multichoose counts multicombinations. The fact that this is indeed the correct counting function for multisets is proved in Sym.card_sym_eq_multichoose in Data.Sym.Card.
• Nat.multichoose_eq : a proof that multichoose n k = (n + k - 1).choose k. This is central to the "stars and bars" technique in informal mathematics, where we switch between counting multisets of size k over an alphabet of size n to counting strings of k elements ("stars") separated by n-1 dividers ("bars"). See Data.Sym.Card for more detail.

Tags

binomial coefficient, combination, multicombination, stars and bars

def Nat.choose : ℕ → ℕ → ℕ

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

Equations

• Nat.choose x 0 = 1
• Nat.choose 0 (Nat.succ n) = 0
• Nat.choose (Nat.succ n) (Nat.succ k) = Nat.choose n k + Nat.choose n (k + 1)

@[simp]

theorem Nat.choose_zero_right (n : ℕ) : Nat.choose n 0 = 1

@[simp]

theorem Nat.choose_zero_succ (k : ℕ) : Nat.choose 0 (Nat.succ k) = 0

theorem Nat.choose_succ_succ (n : ℕ) (k : ℕ) : Nat.choose (Nat.succ n) (Nat.succ k) = Nat.choose n k + Nat.choose n (Nat.succ k)

theorem Nat.choose_succ_succ' (n : ℕ) (k : ℕ) : Nat.choose (n + 1) (k + 1) = Nat.choose n k + Nat.choose n (k + 1)

theorem Nat.choose_eq_zero_of_lt {n : ℕ} {k : ℕ} : n < k → Nat.choose n k = 0

@[simp]

theorem Nat.choose_self (n : ℕ) : Nat.choose n n = 1

@[simp]

theorem Nat.choose_succ_self (n : ℕ) : Nat.choose n (Nat.succ n) = 0

@[simp]

theorem Nat.choose_one_right (n : ℕ) : Nat.choose n 1 = n

theorem Nat.triangle_succ (n : ℕ) : (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

theorem Nat.choose_two_right (n : ℕ) : Nat.choose n 2 = n * (n - 1) / 2

choose n 2 is the n-th triangle number.

theorem Nat.choose_pos {n : ℕ} {k : ℕ} : k ≤ n → 0 < Nat.choose n k

theorem Nat.choose_eq_zero_iff {n : ℕ} {k : ℕ} : Nat.choose n k = 0 ↔ n < k

theorem Nat.succ_mul_choose_eq (n : ℕ) (k : ℕ) : Nat.succ n * Nat.choose n k = Nat.choose (Nat.succ n) (Nat.succ k) * Nat.succ k

theorem Nat.choose_mul_factorial_mul_factorial {n : ℕ} {k : ℕ} : k ≤ n → Nat.choose n k * Nat.factorial k * Nat.factorial (n - k) = Nat.factorial n

theorem Nat.choose_mul {n : ℕ} {k : ℕ} {s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) : Nat.choose n k * Nat.choose k s = Nat.choose n s * Nat.choose (n - s) (k - s)

theorem Nat.choose_eq_factorial_div_factorial {n : ℕ} {k : ℕ} (hk : k ≤ n) : Nat.choose n k = Nat.factorial n / (Nat.factorial k * Nat.factorial (n - k))

theorem Nat.add_choose (i : ℕ) (j : ℕ) : Nat.choose (i + j) j = Nat.factorial (i + j) / (Nat.factorial i * Nat.factorial j)

theorem Nat.add_choose_mul_factorial_mul_factorial (i : ℕ) (j : ℕ) : Nat.choose (i + j) j * Nat.factorial i * Nat.factorial j = Nat.factorial (i + j)

theorem Nat.factorial_mul_factorial_dvd_factorial {n : ℕ} {k : ℕ} (hk : k ≤ n) : Nat.factorial k * Nat.factorial (n - k) ∣ Nat.factorial n

theorem Nat.factorial_mul_factorial_dvd_factorial_add (i : ℕ) (j : ℕ) : Nat.factorial i * Nat.factorial j ∣ Nat.factorial (i + j)

@[simp]

theorem Nat.choose_symm {n : ℕ} {k : ℕ} (hk : k ≤ n) : Nat.choose n (n - k) = Nat.choose n k

theorem Nat.choose_symm_of_eq_add {n : ℕ} {a : ℕ} {b : ℕ} (h : n = a + b) : Nat.choose n a = Nat.choose n b

theorem Nat.choose_symm_add {a : ℕ} {b : ℕ} : Nat.choose (a + b) a = Nat.choose (a + b) b

theorem Nat.choose_symm_half (m : ℕ) : Nat.choose (2 * m + 1) (m + 1) = Nat.choose (2 * m + 1) m

theorem Nat.choose_succ_right_eq (n : ℕ) (k : ℕ) : Nat.choose n (k + 1) * (k + 1) = Nat.choose n k * (n - k)

@[simp]

theorem Nat.choose_succ_self_right (n : ℕ) : Nat.choose (n + 1) n = n + 1

theorem Nat.choose_mul_succ_eq (n : ℕ) (k : ℕ) : Nat.choose n k * (n + 1) = Nat.choose (n + 1) k * (n + 1 - k)

theorem Nat.ascFactorial_eq_factorial_mul_choose (n : ℕ) (k : ℕ) : Nat.ascFactorial n k = Nat.factorial k * Nat.choose (n + k) k

theorem Nat.factorial_dvd_ascFactorial (n : ℕ) (k : ℕ) : Nat.factorial k ∣ Nat.ascFactorial n k

theorem Nat.choose_eq_asc_factorial_div_factorial (n : ℕ) (k : ℕ) : Nat.choose (n + k) k = Nat.ascFactorial n k / Nat.factorial k

theorem Nat.descFactorial_eq_factorial_mul_choose (n : ℕ) (k : ℕ) : Nat.descFactorial n k = Nat.factorial k * Nat.choose n k

theorem Nat.factorial_dvd_descFactorial (n : ℕ) (k : ℕ) : Nat.factorial k ∣ Nat.descFactorial n k

theorem Nat.choose_eq_descFactorial_div_factorial (n : ℕ) (k : ℕ) : Nat.choose n k = Nat.descFactorial n k / Nat.factorial k

def Nat.fast_choose (n : ℕ) (k : ℕ) : ℕ

A faster implementation of choose, to be used during bytecode evaluation and in compiled code.

Equations

• Nat.fast_choose n k = Nat.descFactorial n k / Nat.factorial k

@[csimp]

theorem Nat.choose_eq_fast_choose : Nat.choose = Nat.fast_choose

Inequalities

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

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

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

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

Inequalities about increasing the first argument

theorem Nat.choose_le_succ (a : ℕ) (c : ℕ) : Nat.choose a c ≤ Nat.choose (Nat.succ a) c

theorem Nat.choose_le_add (a : ℕ) (b : ℕ) (c : ℕ) : Nat.choose a c ≤ Nat.choose (a + b) c

theorem Nat.choose_le_choose {a : ℕ} {b : ℕ} (c : ℕ) (h : a ≤ b) : Nat.choose a c ≤ Nat.choose b c

theorem Nat.choose_mono (b : ℕ) : Monotone fun a => Nat.choose a 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

def Nat.multichoose : ℕ → ℕ → ℕ

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

Equations

• Nat.multichoose x 0 = 1
• Nat.multichoose 0 (Nat.succ n) = 0
• Nat.multichoose (Nat.succ n) (Nat.succ k) = Nat.multichoose n (k + 1) + Nat.multichoose (n + 1) k

@[simp]

theorem Nat.multichoose_zero_right (n : ℕ) : Nat.multichoose n 0 = 1

@[simp]

theorem Nat.multichoose_zero_succ (k : ℕ) : Nat.multichoose 0 (k + 1) = 0

theorem Nat.multichoose_succ_succ (n : ℕ) (k : ℕ) : Nat.multichoose (n + 1) (k + 1) = Nat.multichoose n (k + 1) + Nat.multichoose (n + 1) k

@[simp]

theorem Nat.multichoose_one (k : ℕ) : Nat.multichoose 1 k = 1

@[simp]

theorem Nat.multichoose_two (k : ℕ) : Nat.multichoose 2 k = k + 1

@[simp]

theorem Nat.multichoose_one_right (n : ℕ) : Nat.multichoose n 1 = n

theorem Nat.multichoose_eq (n : ℕ) (k : ℕ) : Nat.multichoose n k = Nat.choose (n + k - 1) k