Documentation

Mathlib.Data.Nat.Choose.Multinomial

Multinomial #

This file defines the multinomial coefficient and several small lemma's for manipulating it.

Main declarations #

Main results #

def Nat.multinomial {α : Type u_1} (s : Finset α) (f : α) :

The multinomial coefficient. Gives the number of strings consisting of symbols from s, where c ∈ s appears with multiplicity f c.

Defined as (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!.

Equations
Instances For
    theorem Nat.multinomial_pos {α : Type u_1} (s : Finset α) (f : α) :
    theorem Nat.multinomial_spec {α : Type u_1} (s : Finset α) (f : α) :
    (∏ is, (f i).factorial) * Nat.multinomial s f = (∑ is, f i).factorial
    @[simp]
    theorem Nat.multinomial_empty {α : Type u_1} (f : α) :
    @[deprecated Nat.multinomial_empty]
    theorem Nat.multinomial_nil {α : Type u_1} (f : α) :

    Alias of Nat.multinomial_empty.

    theorem Nat.multinomial_cons {α : Type u_1} {s : Finset α} {a : α} (ha : as) (f : α) :
    Nat.multinomial (Finset.cons a s ha) f = (f a + is, f i).choose (f a) * Nat.multinomial s f
    theorem Nat.multinomial_insert {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : as) (f : α) :
    Nat.multinomial (insert a s) f = (f a + is, f i).choose (f a) * Nat.multinomial s f
    @[simp]
    theorem Nat.multinomial_singleton {α : Type u_1} (a : α) (f : α) :
    @[simp]
    theorem Nat.multinomial_insert_one {α : Type u_1} {s : Finset α} {f : α} {a : α} [DecidableEq α] (h : as) (h₁ : f a = 1) :
    Nat.multinomial (insert a s) f = (s.sum f).succ * Nat.multinomial s f
    theorem Nat.multinomial_congr {α : Type u_1} {s : Finset α} {f : α} {g : α} (h : as, f a = g a) :

    Connection to binomial coefficients #

    When Nat.multinomial is applied to a Finset of two elements {a, b}, the result a binomial coefficient. We use binomial in the names of lemmas that involves Nat.multinomial {a, b}.

    theorem Nat.binomial_eq {α : Type u_1} {f : α} {a : α} {b : α} [DecidableEq α] (h : a b) :
    Nat.multinomial {a, b} f = (f a + f b).factorial / ((f a).factorial * (f b).factorial)
    theorem Nat.binomial_eq_choose {α : Type u_1} {f : α} {a : α} {b : α} [DecidableEq α] (h : a b) :
    Nat.multinomial {a, b} f = (f a + f b).choose (f a)
    theorem Nat.binomial_spec {α : Type u_1} {f : α} {a : α} {b : α} [DecidableEq α] (hab : a b) :
    (f a).factorial * (f b).factorial * Nat.multinomial {a, b} f = (f a + f b).factorial
    @[simp]
    theorem Nat.binomial_one {α : Type u_1} {f : α} {a : α} {b : α} [DecidableEq α] (h : a b) (h₁ : f a = 1) :
    Nat.multinomial {a, b} f = (f b).succ
    theorem Nat.binomial_succ_succ {α : Type u_1} {f : α} {a : α} {b : α} [DecidableEq α] (h : a b) :
    Nat.multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) = Nat.multinomial {a, b} (Function.update f a (f a).succ) + Nat.multinomial {a, b} (Function.update f b (f b).succ)
    theorem Nat.succ_mul_binomial {α : Type u_1} {f : α} {a : α} {b : α} [DecidableEq α] (h : a b) :
    (f a + f b).succ * Nat.multinomial {a, b} f = (f a).succ * Nat.multinomial {a, b} (Function.update f a (f a).succ)

    Simple cases #

    theorem Nat.multinomial_univ_two (a : ) (b : ) :
    Nat.multinomial Finset.univ ![a, b] = (a + b).factorial / (a.factorial * b.factorial)
    theorem Nat.multinomial_univ_three (a : ) (b : ) (c : ) :
    Nat.multinomial Finset.univ ![a, b, c] = (a + b + c).factorial / (a.factorial * b.factorial * c.factorial)

    Alternative definitions #

    def Finsupp.multinomial {α : Type u_1} (f : α →₀ ) :

    Alternative multinomial definition based on a finsupp, using the support for the big operations

    Equations
    • f.multinomial = (f.sum fun (x : α) => id).factorial / f.prod fun (x : α) (n : ) => n.factorial
    Instances For
      theorem Finsupp.multinomial_eq {α : Type u_1} (f : α →₀ ) :
      f.multinomial = Nat.multinomial f.support f
      theorem Finsupp.multinomial_update {α : Type u_1} (a : α) (f : α →₀ ) :
      f.multinomial = (f.sum fun (x : α) => id).choose (f a) * (f.update a 0).multinomial
      def Multiset.multinomial {α : Type u_1} [DecidableEq α] (m : Multiset α) :

      Alternative definition of multinomial based on Multiset delegating to the finsupp definition

      Equations
      • m.multinomial = (Multiset.toFinsupp m).multinomial
      Instances For
        theorem Multiset.multinomial_filter_ne {α : Type u_1} [DecidableEq α] (a : α) (m : Multiset α) :
        m.multinomial = (Multiset.card m).choose (Multiset.count a m) * (Multiset.filter (fun (x : α) => a x) m).multinomial

        Multinomial theorem #

        theorem Finset.sum_pow_eq_sum_piAntidiag_of_commute {α : Type u_1} {R : Type u_2} [DecidableEq α] [Semiring R] (s : Finset α) (f : αR) (hc : (↑s).Pairwise fun (i j : α) => Commute (f i) (f j)) (n : ) :
        (∑ is, f i) ^ n = ks.piAntidiag n, (Nat.multinomial s k) * s.noncommProd (fun (i : α) => f i ^ k i)

        The multinomial theorem.

        theorem Finset.sum_pow_of_commute {α : Type u_1} {R : Type u_2} [DecidableEq α] [Semiring R] (x : αR) (s : Finset α) (hc : (↑s).Pairwise fun (i j : α) => Commute (x i) (x j)) (n : ) :
        s.sum x ^ n = k : { x : Sym α n // x s.sym n }, (↑k).multinomial * (Multiset.map x k).noncommProd

        The multinomial theorem.

        theorem Finset.sum_pow_eq_sum_piAntidiag {α : Type u_1} {R : Type u_2} [DecidableEq α] [CommSemiring R] (s : Finset α) (f : αR) (n : ) :
        (∑ is, f i) ^ n = ks.piAntidiag n, (Nat.multinomial s k) * is, f i ^ k i
        theorem Finset.sum_pow {α : Type u_1} {R : Type u_2} [DecidableEq α] [CommSemiring R] {s : Finset α} (x : αR) (n : ) :
        s.sum x ^ n = ks.sym n, (↑k).multinomial * (Multiset.map x k).prod
        theorem Nat.multinomial_two_mul_le_mul_multinomial {ι : Type u_1} {s : Finset ι} {f : ι} :
        (Nat.multinomial s fun (i : ι) => 2 * f i) ((∑ is, f i) ^ is, f i) * Nat.multinomial s f
        theorem Sym.multinomial_coe_fill_of_not_mem {n : } {α : Type u_1} [DecidableEq α] {m : Fin (n + 1)} {s : Sym α (n - m)} {x : α} (hx : xs) :
        (↑(Sym.fill x m s)).multinomial = n.choose m * (↑s).multinomial