mathlib3 documentation

data.nat.choose.multinomial

Multinomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

Main results #

source
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
source
theorem nat.multinomial_pos {α : Type u_1} (s : finset α) (f : α → ℕ) :
0 < nat.multinomial s f
source
theorem nat.multinomial_spec {α : Type u_1} (s : finset α) (f : α → ℕ) :
s.prod (λ (i : α), (f i).factorial) * nat.multinomial s f = (s.sum (λ (i : α), f i)).factorial
source
@[simp]
theorem nat.multinomial_nil {α : Type u_1} (f : α → ℕ) :
nat.multinomial ∅ f = 1
source
@[simp]
theorem nat.multinomial_singleton {α : Type u_1} (f : α → ℕ) {a : α} :
nat.multinomial {a} f = 1
source
@[simp]
theorem nat.multinomial_insert_one {α : Type u_1} (s : finset α) (f : α → ℕ) {a : α} [decidable_eq α] (h : a ∉ s) (h₁ : f a = 1) :
nat.multinomial (has_insert.insert a s) f = (s.sum f).succ * nat.multinomial s f
source
theorem nat.multinomial_insert {α : Type u_1} (s : finset α) (f : α → ℕ) {a : α} [decidable_eq α] (h : a ∉ s) :
nat.multinomial (has_insert.insert a s) f = (f a + s.sum f).choose (f a) * nat.multinomial s f
source
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}.

source
theorem nat.binomial_eq {α : Type u_1} (f : α → ℕ) {a b : α} [decidable_eq α] (h : a ≠ b) :
nat.multinomial {a, b} f = (f a + f b).factorial / ((f a).factorial * (f b).factorial)
source
theorem nat.binomial_eq_choose {α : Type u_1} (f : α → ℕ) {a b : α} [decidable_eq α] (h : a ≠ b) :
nat.multinomial {a, b} f = (f a + f b).choose (f a)
source
theorem nat.binomial_spec {α : Type u_1} (f : α → ℕ) {a b : α} [decidable_eq α] (hab : a ≠ b) :
(f a).factorial * (f b).factorial * nat.multinomial {a, b} f = (f a + f b).factorial
source
@[simp]
theorem nat.binomial_one {α : Type u_1} (f : α → ℕ) {a b : α} [decidable_eq α] (h : a ≠ b) (h₁ : f a = 1) :
nat.multinomial {a, b} f = (f b).succ
source
theorem nat.binomial_succ_succ {α : Type u_1} (f : α → ℕ) {a b : α} [decidable_eq α] (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)
source
theorem nat.succ_mul_binomial {α : Type u_1} (f : α → ℕ) {a b : α} [decidable_eq α] (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 #

source
theorem nat.multinomial_univ_two (a b : ℕ) :
nat.multinomial finset.univ ![a, b] = (a + b).factorial / (a.factorial * b.factorial)
source
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 #

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

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

Equations
source
theorem finsupp.multinomial_eq {α : Type u_1} (f : α →₀ ℕ) :
f.multinomial = nat.multinomial f.support ⇑f
source
theorem finsupp.multinomial_update {α : Type u_1} (a : α) (f : α →₀ ℕ) :
f.multinomial = (f.sum (λ (_x : α), id)).choose (⇑f a) * (f.update a 0).multinomial
source
noncomputable def multiset.multinomial {α : Type u_1} (m : multiset α) :
ℕ

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

Equations
source
theorem multiset.multinomial_filter_ne {α : Type u_1} [decidable_eq α] (a : α) (m : multiset α) :
m.multinomial = (⇑multiset.card m).choose (multiset.count a m) * (multiset.filter (ne a) m).multinomial

Multinomial theorem #

source
theorem finset.sum_pow_of_commute {α : Type u_1} [decidable_eq α] (s : finset α) {R : Type u_2} [semiring R] (x : α → R) (hc : ↑s.pairwise (λ (i j : α), commute (x i) (x j))) (n : ℕ) :
s.sum x ^ n = finset.univ.sum (λ (k : ↥(s.sym n)), ↑(k.val.val.multinomial) * (multiset.map x k.val.val).noncomm_prod _)

The multinomial theorem

Proof is by induction on the number of summands.

source
theorem finset.sum_pow {α : Type u_1} [decidable_eq α] (s : finset α) {R : Type u_2} [comm_semiring R] (x : α → R) (n : ℕ) :
s.sum x ^ n = (s.sym n).sum (λ (k : sym α n), ↑(k.val.multinomial) * (multiset.map x k.val).prod)