Multinomial

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

Main declarations

• Nat.multinomial: the multinomial coefficient

Main results

• Finest.sum_pow: The expansion of (s.sum x) ^ n using multinomial coefficients

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 in s, f i)! / ∏ i in s, (f i)!.

Equations

• Nat.multinomial s f = Nat.factorial (Finset.sum s fun i => f i) / Finset.prod s fun i => Nat.factorial (f i)

theorem Nat.multinomial_pos {α : Type u_1} (s : Finset α) (f : α → ℕ) : 0 < Nat.multinomial s f

theorem Nat.multinomial_spec {α : Type u_1} (s : Finset α) (f : α → ℕ) : (Finset.prod s fun i => Nat.factorial (f i)) * Nat.multinomial s f = Nat.factorial (Finset.sum s fun i => f i)

@[simp]

theorem Nat.multinomial_nil {α : Type u_1} (f : α → ℕ) : Nat.multinomial ∅ f = 1

@[simp]

theorem Nat.multinomial_singleton {α : Type u_1} (f : α → ℕ) {a : α} : Nat.multinomial {a} f = 1

@[simp]

theorem Nat.multinomial_insert_one {α : Type u_1} (s : Finset α) (f : α → ℕ) {a : α} [DecidableEq α] (h : ¬a ∈ s) (h₁ : f a = 1) : Nat.multinomial (insert a s) f = Nat.succ (Finset.sum s f) * Nat.multinomial s f

theorem Nat.multinomial_insert {α : Type u_1} (s : Finset α) (f : α → ℕ) {a : α} [DecidableEq α] (h : ¬a ∈ s) : Nat.multinomial (insert a s) f = Nat.choose (f a + Finset.sum s f) (f a) * Nat.multinomial s f

theorem Nat.multinomial_congr {α : Type u_1} (s : Finset α) {f : α → ℕ} {g : α → ℕ} (h : ∀ (a : α), a ∈ s → f a = g a) : Nat.multinomial s f = Nat.multinomial s g

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 = Nat.factorial (f a + f b) / (Nat.factorial (f a) * Nat.factorial (f b))

theorem Nat.binomial_eq_choose {α : Type u_1} (f : α → ℕ) {a : α} {b : α} [DecidableEq α] (h : a ≠ b) : Nat.multinomial {a, b} f = Nat.choose (f a + f b) (f a)

theorem Nat.binomial_spec {α : Type u_1} (f : α → ℕ) {a : α} {b : α} [DecidableEq α] (hab : a ≠ b) : Nat.factorial (f a) * Nat.factorial (f b) * Nat.multinomial {a, b} f = Nat.factorial (f a + f b)

@[simp]

theorem Nat.binomial_one {α : Type u_1} (f : α → ℕ) {a : α} {b : α} [DecidableEq α] (h : a ≠ b) (h₁ : f a = 1) : Nat.multinomial {a, b} f = Nat.succ (f b)

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 (Nat.succ (f a))) b (Nat.succ (f b))) = Nat.multinomial {a, b} (Function.update f a (Nat.succ (f a))) + Nat.multinomial {a, b} (Function.update f b (Nat.succ (f b)))

theorem Nat.succ_mul_binomial {α : Type u_1} (f : α → ℕ) {a : α} {b : α} [DecidableEq α] (h : a ≠ b) : Nat.succ (f a + f b) * Nat.multinomial {a, b} f = Nat.succ (f a) * Nat.multinomial {a, b} (Function.update f a (Nat.succ (f a)))

Simple cases

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

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

Alternative definitions

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

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

Equations

• Finsupp.multinomial f = Nat.factorial (Finsupp.sum f fun x => id) / Finsupp.prod f fun x n => Nat.factorial n

theorem Finsupp.multinomial_eq {α : Type u_1} (f : α →₀ ℕ) : Finsupp.multinomial f = Nat.multinomial f.support ↑f

theorem Finsupp.multinomial_update {α : Type u_1} (a : α) (f : α →₀ ℕ) : Finsupp.multinomial f = Nat.choose (Finsupp.sum f fun x => id) (↑f a) * Finsupp.multinomial (Finsupp.update f a 0)

def Multiset.multinomial {α : Type u_1} [DecidableEq α] (m : Multiset α) : ℕ

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

Equations

• Multiset.multinomial m = Finsupp.multinomial (↑Multiset.toFinsupp m)

theorem Multiset.multinomial_filter_ne {α : Type u_1} [DecidableEq α] (a : α) (m : Multiset α) : Multiset.multinomial m = Nat.choose (↑Multiset.card m) (Multiset.count a m) * Multiset.multinomial (Multiset.filter ((fun x x_1 => x ≠ x_1) a) m)

Multinomial theorem

theorem Finset.sum_pow_of_commute {α : Type u_1} [DecidableEq α] (s : Finset α) {R : Type u_2} [Semiring R] (x : α → R) (hc : Set.Pairwise ↑s fun i j => Commute (x i) (x j)) (n : ℕ) : Finset.sum s x ^ n = Finset.sum Finset.univ fun k => ↑(Multiset.multinomial ↑↑k) * Multiset.noncommProd (Multiset.map x ↑↑k) (_ : Set.Pairwise {b | b ∈ Multiset.map x ↑↑k} Commute)

The multinomial theorem

Proof is by induction on the number of summands.

theorem Finset.sum_pow {α : Type u_1} [DecidableEq α] (s : Finset α) {R : Type u_2} [CommSemiring R] (x : α → R) (n : ℕ) : Finset.sum s x ^ n = Finset.sum (Finset.sym s n) fun k => ↑(Multiset.multinomial ↑k) * Multiset.prod (Multiset.map x ↑k)