mathlib documentation

data.nat.choose.basic

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.desc_factorial_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.

def nat.choose :

ℕ → ℕ → ℕ

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

Equations

(n + 1).choose (k + 1) = n.choose k + n.choose (k + 1)
n.succ.choose 0 = 1
0.choose (k + 1) = 0
0.choose 0 = 1

@[simp]

theorem nat.choose_zero_right (n : ℕ) :

n.choose 0 = 1

@[simp]

theorem nat.choose_zero_succ (k : ℕ) :

0.choose k.succ = 0

theorem nat.choose_succ_succ (n k : ℕ) :

n.succ.choose k.succ = n.choose k + n.choose k.succ

theorem nat.choose_eq_zero_of_lt {n k : ℕ} :

n < k → n.choose k = 0

@[simp]

theorem nat.choose_self (n : ℕ) :

n.choose n = 1

@[simp]

theorem nat.choose_succ_self (n : ℕ) :

n.choose n.succ = 0

@[simp]

theorem nat.choose_one_right (n : ℕ) :

n.choose 1 = n

theorem nat.triangle_succ (n : ℕ) :

(n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

theorem nat.choose_two_right (n : ℕ) :

n.choose 2 = n * (n - 1) / 2

choose n 2 is the n-th triangle number.

theorem nat.choose_pos {n k : ℕ} :

k ≤ n → 0 < n.choose k

theorem nat.choose_eq_zero_iff {n k : ℕ} :

n.choose k = 0 ↔ n < k

theorem nat.succ_mul_choose_eq (n k : ℕ) :

(n.succ) * n.choose k = (n.succ.choose k.succ) * k.succ

theorem nat.choose_mul_factorial_mul_factorial {n k : ℕ} :

k ≤ n → ((n.choose k) * k!) * (n - k)! = n!

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)

theorem nat.choose_eq_factorial_div_factorial {n k : ℕ} (hk : k ≤ n) :

n.choose k = n! / k! * (n - k)!

theorem nat.add_choose (i j : ℕ) :

(i + j).choose j = (i + j)! / i! * j!

theorem nat.add_choose_mul_factorial_mul_factorial (i j : ℕ) :

(((i + j).choose j) * i!) * j! = (i + j)!

theorem nat.factorial_mul_factorial_dvd_factorial {n k : ℕ} (hk : k ≤ n) :

k! * (n - k)! ∣ n!

theorem nat.factorial_mul_factorial_dvd_factorial_add (i j : ℕ) :

i! * j! ∣ (i + j)!

@[simp]

theorem nat.choose_symm {n k : ℕ} (hk : k ≤ n) :

n.choose (n - k) = n.choose k

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

n.choose a = n.choose b

theorem nat.choose_symm_add {a b : ℕ} :

(a + b).choose a = (a + b).choose b

theorem nat.choose_symm_half (m : ℕ) :

(2 * m + 1).choose (m + 1) = (2 * m + 1).choose m

theorem nat.choose_succ_right_eq (n k : ℕ) :

(n.choose (k + 1)) * (k + 1) = (n.choose k) * (n - k)

@[simp]

theorem nat.choose_succ_self_right (n : ℕ) :

(n + 1).choose n = n + 1

theorem nat.choose_mul_succ_eq (n k : ℕ) :

(n.choose k) * (n + 1) = ((n + 1).choose k) * (n + 1 - k)

theorem nat.asc_factorial_eq_factorial_mul_choose (n k : ℕ) :

n.asc_factorial k = k! * (n + k).choose k

theorem nat.factorial_dvd_asc_factorial (n k : ℕ) :

k! ∣ n.asc_factorial k

theorem nat.choose_eq_asc_factorial_div_factorial (n k : ℕ) :

(n + k).choose k = n.asc_factorial k / k!

theorem nat.desc_factorial_eq_factorial_mul_choose (n k : ℕ) :

n.desc_factorial k = k! * n.choose k

theorem nat.factorial_dvd_desc_factorial (n k : ℕ) :

k! ∣ n.desc_factorial k

theorem nat.choose_eq_desc_factorial_div_factorial (n k : ℕ) :

n.choose k = n.desc_factorial k / k!

Inequalities #

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.

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 #

theorem nat.choose_le_succ (a c : ℕ) :

a.choose c ≤ a.succ.choose c

theorem nat.choose_le_add (a b c : ℕ) :

a.choose c ≤ (a + b).choose c

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

a.choose c ≤ b.choose c

theorem nat.choose_mono (b : ℕ) :

monotone (λ (a : ℕ), a.choose b)