Stars and bars #

In this file, we prove the case n = 2 of stars and bars.

Informal statement #

If we have n objects to put in k boxes, we can do so in exactly (n + k - 1).choose n ways.

Formal statement #

We can identify the k boxes with the elements of a fintype α of card k. Then placing n elements in those boxes corresponds to choosing how many of each element of α appear in a multiset of card n. sym α n being the subtype of multiset α of multisets of card n, writing stars and bars using types gives

-- TODO: this lemma is not yet proven
lemma stars_and_bars {α : Type*} [fintype α] (n : ℕ) :
  card (sym α n) = (card α + n - 1).choose (card α) := sorry

TODO #

Prove the general case of stars and bars.

Tags #

stars and bars

source

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

(finset.image quotient.mk s.diag).card = s.card

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

source

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

2 * (finset.image quotient.mk s.off_diag).card = s.off_diag.card

source

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

(finset.image quotient.mk s.off_diag).card = s.card.choose 2

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

source

theorem sym2.card_subtype_diag {α : Type u_1} [decidable_eq α] [fintype α] :

fintype.card {a // a.is_diag} = fintype.card α

source

theorem sym2.card_subtype_not_diag {α : Type u_1} [decidable_eq α] [fintype α] :

fintype.card {a // ¬a.is_diag} = (fintype.card α).choose 2

source

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.

source

@[protected]

theorem sym2.card {α : Type u_1} [decidable_eq α] [fintype α] :

fintype.card (sym2 α) = (fintype.card α) * (fintype.card α + 1) / 2

Type stars and bars for the case n = 2.