Stars and bars #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
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.
For any fintype α of cardinality n, card (sym α k) = multichoose (card α) k
The stars and bars lemma: the cardinality of sym α k is equal to
nat.choose (card α + k - 1) k.
The diag of s : finset α is sent on a finset of sym2 α of card s.card.
The off_diag of s : finset α is sent on a finset of sym2 α of card s.off_diag.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).
Type stars and bars for the case n = 2.