Documentation

Mathlib.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 #

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
  • x.choose 0 = 1
  • Nat.choose 0 n.succ = 0
  • n.succ.choose k.succ = n.choose k + n.choose (k + 1)
Instances For
    @[simp]
    theorem Nat.choose_zero_right (n : ) :
    n.choose 0 = 1
    @[simp]
    theorem Nat.choose_zero_succ (k : ) :
    Nat.choose 0 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_succ_succ' (n : ) (k : ) :
    (n + 1).choose (k + 1) = n.choose k + n.choose (k + 1)
    theorem Nat.choose_succ_left (n : ) (k : ) (hk : 0 < k) :
    (n + 1).choose k = n.choose (k - 1) + n.choose k
    theorem Nat.choose_succ_right (n : ) (k : ) (hn : 0 < n) :
    n.choose (k + 1) = (n - 1).choose k + (n - 1).choose (k + 1)
    theorem Nat.choose_eq_choose_pred_add {n : } {k : } (hn : 0 < n) (hk : 0 < k) :
    n.choose k = (n - 1).choose (k - 1) + (n - 1).choose k
    theorem Nat.choose_eq_zero_of_lt {n : } {k : } :
    n < kn.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 n0 < 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 nn.choose k * k.factorial * (n - k).factorial = n.factorial
    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.factorial / (k.factorial * (n - k).factorial)
    theorem Nat.add_choose (i : ) (j : ) :
    (i + j).choose j = (i + j).factorial / (i.factorial * j.factorial)
    theorem Nat.add_choose_mul_factorial_mul_factorial (i : ) (j : ) :
    (i + j).choose j * i.factorial * j.factorial = (i + j).factorial
    theorem Nat.factorial_mul_factorial_dvd_factorial {n : } {k : } (hk : k n) :
    k.factorial * (n - k).factorial n.factorial
    theorem Nat.factorial_mul_factorial_dvd_factorial_add (i : ) (j : ) :
    i.factorial * j.factorial (i + j).factorial
    @[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.ascFactorial_eq_factorial_mul_choose (n : ) (k : ) :
    (n + 1).ascFactorial k = k.factorial * (n + k).choose k
    theorem Nat.ascFactorial_eq_factorial_mul_choose' (n : ) (k : ) :
    n.ascFactorial k = k.factorial * (n + k - 1).choose k
    theorem Nat.factorial_dvd_ascFactorial (n : ) (k : ) :
    k.factorial n.ascFactorial k
    theorem Nat.choose_eq_asc_factorial_div_factorial (n : ) (k : ) :
    (n + k).choose k = (n + 1).ascFactorial k / k.factorial
    theorem Nat.choose_eq_asc_factorial_div_factorial' (n : ) (k : ) :
    (n + k - 1).choose k = n.ascFactorial k / k.factorial
    theorem Nat.descFactorial_eq_factorial_mul_choose (n : ) (k : ) :
    n.descFactorial k = k.factorial * n.choose k
    theorem Nat.factorial_dvd_descFactorial (n : ) (k : ) :
    k.factorial n.descFactorial k
    theorem Nat.choose_eq_descFactorial_div_factorial (n : ) (k : ) :
    n.choose k = n.descFactorial k / k.factorial
    def Nat.fast_choose (n : ) (k : ) :

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

    Equations
    • n.fast_choose k = n.descFactorial k / k.factorial
    Instances For

      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 fun (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

      @[irreducible]
      def Nat.multichoose :

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

      Equations
      • x.multichoose 0 = 1
      • Nat.multichoose 0 n.succ = 0
      • n.succ.multichoose k.succ = n.multichoose (k + 1) + (n + 1).multichoose k
      Instances For
        @[simp]
        theorem Nat.multichoose_zero_right (n : ) :
        n.multichoose 0 = 1
        @[simp]
        theorem Nat.multichoose_succ_succ (n : ) (k : ) :
        (n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k
        @[simp]
        @[simp]
        theorem Nat.multichoose_two (k : ) :
        @[simp]
        theorem Nat.multichoose_one_right (n : ) :
        n.multichoose 1 = n
        @[irreducible]
        theorem Nat.multichoose_eq (n : ) (k : ) :
        n.multichoose k = (n + k - 1).choose k