Vandermonde's identity for finitely many groups

Choosing n objects from a disjoint union of groups of sizes K i, for i ∈ s, amounts to choosing k i objects from each group, for some function k whose values sum to n. Counting both ways gives the multivariate Vandermonde identity

  ∑ k ∈ s.piAntidiag n, ∏ i ∈ s, choose (K i) (k i) = choose (∑ i ∈ s, K i) n.

Restricting to the choices with a prescribed number m of objects from one group i leaves choose (K i) m choices there, times the Vandermonde count for the remaining groups. These identities normalize the multivariate hypergeometric distribution and compute its coordinate marginals. Grouping the categories along a map f and prescribing the number of objects drawn from each group gives a product of Vandermonde counts, one for each group; this is the aggregation property of the multivariate hypergeometric distribution.

Main results

• Finset.sum_piAntidiag_prod_choose: the multivariate Vandermonde identity, generalizing Mathlib's Nat.add_choose_eq.
• Finset.sum_filter_piAntidiag_prod_choose: the same count with one coordinate prescribed.
• Finset.sum_filter_piAntidiag_prod_choose_fiberwise: the same count with the totals over the fibres of a map prescribed.

theorem Finset.sum_piAntidiag_prod_choose {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (K : ι → ℕ) (n : ℕ) : ∑ k ∈ s.piAntidiag n, ∏ i ∈ s, (K i).choose (k i) = (∑ i ∈ s, K i).choose n

Vandermonde's identity for finitely many groups: the ways of choosing n objects from groups of sizes K i, i ∈ s, sorted by how many come from each group.

theorem Finset.sum_filter_piAntidiag_prod_choose {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {i : ι} (hi : i ∈ s) (K : ι → ℕ) (n m : ℕ) : ∑ k ∈ s.piAntidiag n with k i = m, ∏ j ∈ s, (K j).choose (k j) = if m ≤ n then (K i).choose m * (∑ j ∈ s.erase i, K j).choose (n - m) else 0

The ways of choosing n objects from groups of sizes K j, j ∈ s, with exactly m objects from the group i ∈ s: there are choose (K i) m choices in that group, times the Vandermonde count for the other groups.

theorem Finset.sum_filter_piAntidiag_prod_choose_fiberwise {ι : Type u_1} [DecidableEq ι] {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq κ] (f : ι → κ) (K : ι → ℕ) (m : κ → ℕ) : ∑ k ∈ univ.piAntidiag (∑ j : κ, m j) with ∀ (j : κ), ∑ i : ι with f i = j, k i = m j, ∏ i : ι, (K i).choose (k i) = ∏ j : κ, (∑ i : ι with f i = j, K i).choose (m j)

Vandermonde's identity grouped along a map f : ι → κ: the ways of choosing objects from groups of sizes K i so that, for every j, exactly m j objects come from the groups in the fibre of f over j. Merging the groups of each fibre into one group of size ∑ i with f i = j, K i counts these choices as a product of binomial coefficients.