Multinomial

This file defines the multinomial coefficients and several small lemmas for manipulating them.

• Nat.multinomial: the multinomial coefficient, Given a function f : α → ℕ and s : Finset α, this is the number of strings consisting of symbols from s, where c ∈ s appears with multiplicity f c.

  It is defined as (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!.

• Multiset.countPerms: multinomial coefficient associated with the Multiset.count function of a multiset. This is the number of lists that induce the given multiset.

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

• Multiset.multinomial. Given a multiset m of natural numbers, m.multinomial is the multinomial coefficient defined by (m.sum) ! / ∏ i ∈ m, m i !.

This should not be confused with m.countPerms which is defined as m.toFinsupp.multinomial.

As an example, one has Multiset.multinomial {1, 2, 2} = 30, while Multiset.countPerms {1, 2, 2} = 3.

• Multiset.multinomial_cons proves that (x ::ₘ m).multinomial = Nat.choose (x + m.sum) x * m.multinomial
• Multiset.multinomial_add proves that (m + m').multinomial = Nat.choose (m + m').sum m.sum * m.multinomial * m'.multinomial

Implementation note for Multiset.multinomial.

To avoid the definition of Multiset.multinomial as a quotient given above, we define it in terms of Finsupp.multinomial, via lists: If m : Multiset ℕ is the multiset associated with a list l : List ℕ, then m.multinomial = l.toFinsupp.multinomial. Then we prove its invariance under permutation.

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

• Nat.multinomial s f = (∑ i ∈ s, f i).factorial / ∏ i ∈ s, (f i).factorial

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

theorem Nat.multinomial_spec {α : Type u_1} (s : Finset α) (f : α → ℕ) : (∏ i ∈ s, (f i).factorial) * multinomial s f = (∑ i ∈ s, f i).factorial

@[simp]

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

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

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

@[simp]

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

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

theorem Nat.multinomial_congr_of_eq_on_inter {α : Type u_1} [DecidableEq α] {f g : α → ℕ} {s t : Finset α} (hf : ∀ a ∈ s \ t, f a = 0) (hg : ∀ a ∈ t \ s, g a = 0) (hfg : ∀ a ∈ s ∩ t, f a = g a) : multinomial s f = multinomial t g

theorem Nat.multinomial_congr_of_sdiff {α : Type u_1} [DecidableEq α] {f g : α → ℕ} {s t : Finset α} (hst : s ⊆ t) (hg : ∀ a ∈ t \ s, g a = 0) (hfg : ∀ a ∈ s, f a = g a) : multinomial s f = multinomial t g

theorem Nat.multinomial_single {α : Type u_1} (s : Finset α) (a : α) (n : ℕ) [DecidableEq α] : multinomial s (Pi.single a n) = 1

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) : 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) : 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 * multinomial {a, b} f = (f a + f b).factorial

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

theorem Nat.binomial_succ_succ {α : Type u_1} {f : α → ℕ} {a b : α} [DecidableEq α] (h : a ≠ b) : multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) = multinomial {a, b} (Function.update f a (f a).succ) + 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 * multinomial {a, b} f = (f a).succ * multinomial {a, b} (Function.update f a (f a).succ)

Simple cases

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

theorem Nat.multinomial_univ_three (a b c : ℕ) : 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_eq_of_support_subset {α : Type u_1} {f : α →₀ ℕ} {s : Finset α} (h : f.support ⊆ s) : f.multinomial = Nat.multinomial s ⇑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

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

The number of permutations of a given multiset.

Equations

• m.countPerms = (Multiset.toFinsupp m).multinomial

theorem Multiset.countPerms_filter_ne {α : Type u_1} [DecidableEq α] (a : α) (m : Multiset α) : m.countPerms = m.card.choose (count a m) * (filter (fun (x : α) => a ≠ x) m).countPerms

@[simp]

theorem Multiset.countPerms_zero {α : Type u_1} [DecidableEq α] : countPerms 0 = 1

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 (Function.onFun Commute f)) (n : ℕ) : (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.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 (Function.onFun Commute x)) (n : ℕ) : s.sum x ^ n = ∑ k : ↥(s.sym n), ↑(↑↑k).countPerms * (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 : ℕ) : (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(Nat.multinomial s k) * ∏ i ∈ s, 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 = ∑ k ∈ s.sym n, ↑(↑k).countPerms * (Multiset.map x ↑k).prod

theorem Nat.multinomial_two_mul_le_mul_multinomial {ι : Type u_1} {s : Finset ι} {f : ι → ℕ} : (multinomial s fun (i : ι) => 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f

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

theorem Finsupp.multinomial_of_support_subset {σ : Type u_1} {d : σ →₀ ℕ} {s : Finset σ} (h : d.support ⊆ s) : Nat.multinomial s ⇑d = d.multinomial

theorem List.toFinsupp_sum {α : Type u_1} [AddCommMonoid α] [DecidableEq α] (l : List α) : (l.toFinsupp.sum fun (x : ℕ) (a : α) => a) = l.sum

@[reducible, inline]

abbrev List.multinomial (l : List ℕ) : ℕ

The multinomial coefficients given by a list of natural numbers.

See also Multiset.multinomial

Equations

• l.multinomial = l.toFinsupp.multinomial

theorem List.multinomial_cons (x : ℕ) (l : List ℕ) : (x :: l).multinomial = (x + l.sum).choose x * l.multinomial

def Multiset.multinomial (m : Multiset ℕ) : ℕ

The multinomial coefficients on Multiset ℕ.

Equations

• m.multinomial = Quot.liftOn m List.multinomial ⋯

theorem Multiset.multinomial_cons (x : ℕ) (m : Multiset ℕ) : (x ::ₘ m).multinomial = (x + m.sum).choose x * m.multinomial

@[simp]

theorem Multiset.multinomial_zero : multinomial 0 = 1

@[simp]

theorem Multiset.multinomial_singleton (n : ℕ) : {n}.multinomial = 1

theorem Multiset.multinomial_add (m m' : Multiset ℕ) : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial

theorem Multiset.multinomial_nsmul (k : ℕ) (m : Multiset ℕ) : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun (x : ℕ) => m.sum) * m.multinomial ^ k

theorem Multiset.multinomial_nsmul_singleton (k n : ℕ) : (k • {n}).multinomial = Nat.multinomial (Finset.range k) fun (x : ℕ) => n