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
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)!
.
Instances For
theorem
Nat.multinomial_insert
{α : Type u_1}
{s : Finset α}
{a : α}
[DecidableEq α]
(ha : a ∉ s)
(f : α → ℕ)
:
@[simp]
@[simp]
theorem
Nat.multinomial_insert_one
{α : Type u_1}
{s : Finset α}
{f : α → ℕ}
{a : α}
[DecidableEq α]
(h : a ∉ s)
(h₁ : f a = 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}
.
@[simp]
theorem
Nat.binomial_one
{α : Type u_1}
{f : α → ℕ}
{a b : α}
[DecidableEq α]
(h : a ≠ b)
(h₁ : f a = 1)
:
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 #
Alternative definitions #
Alternative multinomial definition based on a finsupp, using the support for the big operations
Equations
Instances For
Alternative definition of multinomial based on Multiset
delegating to the
finsupp definition
Instances For
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 : { x : Sym α n // x ∈ s.sym n }, ↑(↑↑k).multinomial * (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 : ℕ)
:
theorem
Finset.sum_pow
{α : Type u_1}
{R : Type u_2}
[DecidableEq α]
[CommSemiring R]
{s : Finset α}
(x : α → R)
(n : ℕ)
:
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)
: