Multinomial

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

Main declarations

• Nat.multinomial: the multinomial coefficient

Main results

• Finset.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 = (s.sum fun (i : α) => f i).factorial / s.prod fun (i : α) => (f i).factorial

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 : α → ℕ) : (s.prod fun (i : α) => (f i).factorial) * Nat.multinomial s f = (s.sum fun (i : α) => f i).factorial

@[simp]

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

theorem Nat.multinomial_cons {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) (f : α → ℕ) : Nat.multinomial (Finset.cons a s ha) f = (f a + s.sum fun (i : α) => f i).choose (f a) * Nat.multinomial s f

theorem Nat.multinomial_insert {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : a ∉ s) (f : α → ℕ) : Nat.multinomial (insert a s) f = (f a + s.sum fun (i : α) => f i).choose (f a) * Nat.multinomial s f

@[simp]

theorem Nat.multinomial_singleton {α : Type u_1} (a : α) (f : α → ℕ) : 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 = (s.sum f).succ * Nat.multinomial s f

theorem Nat.multinomial_congr {α : Type u_1} {s : Finset α} {f : α → ℕ} {g : α → ℕ} (h : ∀ 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 = (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

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

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

@[simp]

theorem Multiset.multinomial_zero {α : Type u_1} [DecidableEq α] : Multiset.multinomial 0 = 1

Multinomial theorem

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

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 : ℕ) : s.sum x ^ n = (s.sym n).sum fun (k : Sym α n) => ↑(↑k).multinomial * (Multiset.map x ↑k).prod

theorem Sym.multinomial_coe_fill_of_not_mem {n : ℕ} {α : Type u_1} [DecidableEq α] {m : Fin (n + 1)} {s : Sym α (n - ↑m)} {x : α} (hx : x ∉ s) : (↑(Sym.fill x m s)).multinomial = n.choose ↑m * (↑s).multinomial