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 : 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 := }
Instances For
    def Sym.e2 {n : } {k : } :
    { s : Sym (Fin n.succ.succ) k // 0s } 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.
    Instances For
      @[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_3} [Fintype α] :
      Fintype.card (Sym2 α) = (Fintype.card α + 1).choose 2

      Type stars and bars for the case n = 2.