data.sym.card

# 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

@[protected]
def sym.E1 {n k : } :
{s // 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
@[protected]
def sym.E2 {n k : } :
{s // 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
theorem sym.card_sym_eq_multichoose (α : Type u_1) (k : ) [fintype α] [fintype (sym α k)] :
fintype.card (sym α k) = k

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

theorem sym.card_sym_eq_choose {α : Type u_1} [fintype α] (k : ) [fintype (sym α k)] :
fintype.card (sym α k) = + 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} [decidable_eq α] (s : finset α) :
= s.card

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

theorem sym2.card_image_off_diag {α : Type u_1} [decidable_eq α] (s : finset α) :

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).

theorem sym2.card_subtype_diag {α : Type u_1} [decidable_eq α] [fintype α] :
theorem finset.card_sym2 {α : Type u_1} [decidable_eq α] (s : finset α) :
s.sym2.card = s.card * (s.card + 1) / 2

Finset stars and bars for the case n = 2.

@[protected]
theorem sym2.card {α : Type u_1} [decidable_eq α] [fintype α] :
fintype.card (sym2 α) = * + 1) / 2

Type stars and bars for the case n = 2.