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
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]
@[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 #
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)
Alternative definition of multinomial based on Multiset
delegating to the
finsupp definition
Instances For
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)