# 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 `i`

th 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

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

.

Finset **stars and bars** for the case `n = 2`

.

Type **stars and bars** for the case `n = 2`

.