Decomposing and counting Multiset.powerset

Structural decompositions of Multiset.powerset (mathlib has only the zero/cons forms), and the multiplicity of s in t.powerset as a product of binomial coefficients: a sub-multiset picks s.count x of the t.count x copies of each distinct x. (This product of binomials is not Nat.multinomial, which is the quotient (∑ᵢ kᵢ)! / ∏ᵢ kᵢ!.)

Main results

• Multiset.powerset_add: (F + G).powerset as a bind/map product of the summands' powersets — the + analogue of Multiset.powerset_cons.
• Multiset.powerset_powerset_pair_swap: the two iteration orders over nested sub-multiset pairs enumerate the same multiset of pairs.
• Multiset.count_powerset_of_le: for s ≤ t, t.powerset.count s = ∏ x ∈ t.toFinset, (t.count x).choose (s.count x).
• Multiset.count_powerset: the hypothesis-free form, indexed by (s + t).toFinset so that Nat.choose vanishing makes both sides 0 when s ≰ t.

Implementation notes

The induction runs over a fixed ambient Finset containing both supports (count_powerset_subset): the index set stays constant through the recursion and the unconditional induction hypothesis absorbs the s ≰ t boundary cases by Nat.choose vanishing. [UPSTREAM] candidate; eventual mathlib home Mathlib.Data.Multiset.Powerset.

theorem Multiset.powerset_add {α : Type u_1} (F G : Multiset α) : (F + G).powerset = F.powerset.bind fun (F₁ : Multiset α) => map (fun (G₁ : Multiset α) => F₁ + G₁) G.powerset

powerset of a sum, as a bind/map product over the summands' powersets: each sub-multiset of F + G splits (with multiplicity) into a sub-multiset of F plus a sub-multiset of G. The + analogue of powerset_cons.

theorem Multiset.powerset_powerset_pair_swap {α : Type u_1} [DecidableEq α] (F : Multiset α) : (F.powerset.bind fun (F₁ : Multiset α) => map (fun (A : Multiset α) => (A, F₁ - A)) F₁.powerset) = F.powerset.bind fun (A : Multiset α) => map (fun (B : Multiset α) => (A, B)) (F - A).powerset

Nested-powerset reparameterization: iterating F₁ ⊆ F then A ⊆ F₁ enumerates the same multiset of pairs as iterating A ⊆ F then B ⊆ F - A, via the bijection (F₁, A) ↦ (A, F₁ - A).

theorem Multiset.count_powerset_of_le {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) : count s t.powerset = ∏ x ∈ t.toFinset, (count x t).choose (count x s)

Count of a sub-multiset s ≤ t among the sub-multisets of t: for each distinct x, choose s.count x of the t.count x copies.

theorem Multiset.count_powerset {α : Type u_1} [DecidableEq α] (s t : Multiset α) : count s t.powerset = ∏ x ∈ (s + t).toFinset, (count x t).choose (count x s)

Hypothesis-free form of count_powerset_of_le: over (s + t).toFinset, some factor (t.count x).choose (s.count x) vanishes whenever s ≰ t, so both sides are 0.

theorem Multiset.count_powerset_eq_zero {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : ¬s ≤ t) : count s t.powerset = 0

A multiset that is not below t does not occur in t.powerset.

@[simp]

theorem Multiset.count_zero_powerset {α : Type u_1} [DecidableEq α] (t : Multiset α) : count 0 t.powerset = 1

@[simp]

theorem Multiset.count_powerset_self {α : Type u_1} [DecidableEq α] (t : Multiset α) : count t t.powerset = 1