Documentation

Mathlib.Data.Sym.Card

Stars and bars #

In this file, we prove (in Sym.card_sym_eq_multichoose) that the function multichoose n k defined in Data/Nat/Choose/Basic counts the number of multisets of cardinality k over an alphabet of cardinality n. In conjunction with Nat.multichoose_eq proved in Data/Nat/Choose/Basic, which shows that multichoose n k = choose (n + k - 1) k, this is central to the "stars and bars" technique in combinatorics, where we switch between counting multisets of size k over an alphabet of size n to counting strings of k elements ("stars") separated by n-1 dividers ("bars").

Informal statement #

Many problems in mathematics are of the form of (or can be reduced to) putting k indistinguishable objects into n distinguishable boxes; for example, the problem of finding natural numbers x1, ..., xn whose sum is k. This is equivalent to forming a multiset of cardinality k from an alphabet of cardinality n -- for each box i ∈ [1, n] the multiset contains as many copies of i as there are items in the ith box.

The "stars and bars" technique arises from another way of presenting the same problem. Instead of putting k items into n boxes, we take a row of k items (the "stars") and separate them by inserting n-1 dividers (the "bars"). For example, the pattern *|||**|*| exhibits 4 items distributed into 6 boxes -- note that any box, including the first and last, may be empty. Such arrangements of k stars and n-1 bars are in 1-1 correspondence with multisets of size k over an alphabet of size n, and are counted by choose (n + k - 1) k.

Note that this problem is one component of Gian-Carlo Rota's "Twelvefold Way" https://en.wikipedia.org/wiki/Twelvefold_way

Formal statement #

Here we generalise the alphabet to an arbitrary fintype α, and we use Sym α k as the type of multisets of size k over α. Thus the statement that these are counted by multichoose is: Sym.card_sym_eq_multichoose : card (Sym α k) = multichoose (card α) k while the "stars and bars" technique gives Sym.card_sym_eq_choose : card (Sym α k) = choose (card α + k - 1) k

Tags #

stars and bars, multichoose

def Sym.e1 {n : } {k : } :
{ s // 0 s } Sym (Fin ()) k

Over Fin (n + 1), the multisets of size k + 1 containing 0 are equivalent to those of size k, as demonstrated by respectively erasing or appending 0.

Instances For
def Sym.e2 {n : } {k : } :
{ s // ¬0 s } Sym (Fin ()) k

The multisets of size k over Fin n+2 not containing 0 are equivalent to those of size k over Fin n+1, as demonstrated by respectively decrementing or incrementing every element of the multiset.

Instances For
theorem Sym.card_sym_eq_multichoose (α : Type u_3) (k : ) [] [Fintype (Sym α k)] :

For any fintype α of cardinality n, card (Sym α k) = multichoose (card α) k.

theorem Sym.card_sym_eq_choose {α : Type u_3} [] (k : ) [Fintype (Sym α k)] :
Fintype.card (Sym α k) = Nat.choose ( - 1) k

The stars and bars lemma: the cardinality of Sym α k is equal to Nat.choose (card α + k - 1) k.

theorem Sym2.card_image_diag {α : Type u_1} [] (s : ) :
Finset.card (Finset.image Quotient.mk' ()) =

The diag of s : Finset α is sent on a finset of Sym2 α of card s.card.

theorem Sym2.two_mul_card_image_offDiag {α : Type u_1} [] (s : ) :
2 * Finset.card (Finset.image Quotient.mk' ()) =
theorem Sym2.card_image_offDiag {α : Type u_1} [] (s : ) :
Finset.card (Finset.image Quotient.mk' ()) =

The offDiag of s : Finset α is sent on a finset of Sym2 α of card s.offDiag.card / 2. This is because every element ⟦(x, y)⟧ of Sym2 α not on the diagonal comes from exactly two pairs: (x, y) and (y, x).

theorem Sym2.card_subtype_diag {α : Type u_1} [] [] :
Fintype.card { a // } =
theorem Sym2.card_subtype_not_diag {α : Type u_1} [] [] :
Fintype.card { a // } =
theorem Finset.card_sym2 {α : Type u_1} [] (s : ) :
= * ( + 1) / 2

Finset stars and bars for the case n = 2.

theorem Sym2.card {α : Type u_1} [] [] :
Fintype.card (Sym2 α) = * () / 2

Type stars and bars for the case n = 2.