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 : Sym (Fin (n + 1)) (k + 1) // 0 ∈ s } ≃ Sym (Fin n.succ) 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.

Equations

• Sym.e1 = { toFun := fun (s : { s : Sym (Fin (n + 1)) (k + 1) // 0 ∈ s }) => (↑s).erase 0 ⋯, invFun := fun (s : Sym (Fin n.succ) k) => ⟨0 ::ₛ s, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def Sym.e2 {n : ℕ} {k : ℕ} : { s : Sym (Fin n.succ.succ) k // 0 ∉ s } ≃ Sym (Fin n.succ) 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.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

theorem Sym.card_sym_fin_eq_multichoose (n : ℕ) (k : ℕ) : Fintype.card (Sym (Fin n) k) = n.multichoose k

theorem Sym.card_sym_eq_multichoose (α : Type u_3) (k : ℕ) [Fintype α] [Fintype (Sym α k)] : Fintype.card (Sym α k) = (Fintype.card α).multichoose k

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

theorem Sym.card_sym_eq_choose {α : Type u_3} [Fintype α] (k : ℕ) [Fintype (Sym α k)] : Fintype.card (Sym α k) = (Fintype.card α + k - 1).choose 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} [DecidableEq α] (s : Finset α) : (Finset.image Sym2.mk s.diag).card = s.card

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} [DecidableEq α] (s : Finset α) : 2 * (Finset.image Sym2.mk s.offDiag).card = s.offDiag.card

theorem Sym2.card_image_offDiag {α : Type u_1} [DecidableEq α] (s : Finset α) : (Finset.image Sym2.mk s.offDiag).card = s.card.choose 2

The offDiag of s : Finset α is sent on a finset of Sym2 α of card s.offDiag.card / 2. This is because every element s(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} [DecidableEq α] [Fintype α] : Fintype.card { a : Sym2 α // a.IsDiag } = Fintype.card α

theorem Sym2.card_subtype_not_diag {α : Type u_1} [DecidableEq α] [Fintype α] : Fintype.card { a : Sym2 α // ¬a.IsDiag } = (Fintype.card α).choose 2

theorem Sym2.card {α : Type u_1} [Fintype α] : Fintype.card (Sym2 α) = (Fintype.card α + 1).choose 2

Type stars and bars for the case n = 2.