data.sym.card

# 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

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.two_mul_card_image_off_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
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 sym2.card_subtype_not_diag {α : Type u_1} [decidable_eq α] [fintype α] :
theorem sym2.card {α : Type u_1} [decidable_eq α] [fintype α] :