Counting pairs in Multiset.antidiagonal

Multiset.antidiagonal w enumerates the ordered splits w = p.1 + p.2 with multiplicities; this file computes those multiplicities: (u, v) occurs ∏ x, (w.count x).choose (v.count x) times when u + v = w, and 0 times otherwise.

Main results

• Multiset.antidiagonal_add: (F + G).antidiagonal as a bind/map product of the summands' antidiagonals — the + analogue of Multiset.antidiagonal_cons.
• Multiset.powerset_partition_swap: a partition sum over C.powerset is invariant under the involution C₁ ↦ C - C₁.
• Multiset.count_antidiagonal: the closed form for (antidiagonal w).count (u, v).
• Multiset.count_antidiagonal_eq_count_powerset: the guard-free bridge to Multiset.count_powerset_of_le.
• Multiset.count_antidiagonal_swap: the multiplicity is symmetric in the two slots.

[UPSTREAM] candidate; eventual mathlib home Mathlib.Data.Multiset.Antidiagonal, where the closed form also evaluates Finsupp.antidiagonal'.

theorem Multiset.antidiagonal_swap {α : Type u_1} (s : Multiset α) : map Prod.swap s.antidiagonal = s.antidiagonal

antidiagonal is invariant under Prod.swap: commutativity of + permutes the ordered splits.

theorem Multiset.antidiagonal_add {α : Type u_1} [DecidableEq α] (F G : Multiset α) : (F + G).antidiagonal = F.antidiagonal.bind fun (p : Multiset α × Multiset α) => map (fun (q : Multiset α × Multiset α) => (p.1 + q.1, p.2 + q.2)) G.antidiagonal

The antidiagonal of a sum decomposes as the bind/map product of the summands' antidiagonals: transport of powerset_add through antidiagonal_eq_map_powerset, closed by (F + G) - (F₁ + G₁) = (F - F₁) + (G - G₁) for F₁ ≤ F, G₁ ≤ G. The + analogue of antidiagonal_cons.

theorem Multiset.powerset_partition_swap {α : Type u_1} [DecidableEq α] {β : Type u_2} [AddCommMonoid β] (C : Multiset α) (f : Multiset α → Multiset α → β) : (map (fun (C₁ : Multiset α) => f C₁ (C - C₁)) C.powerset).sum = (map (fun (C₁ : Multiset α) => f (C - C₁) C₁) C.powerset).sum

Reindex a partition-sum over C.powerset by the involution C₁ ↦ C - C₁: summing f C₁ (C - C₁) equals summing f (C - C₁) C₁. Specialisation of antidiagonal_swap to the (C₁, C - C₁) parametrisation.

theorem Multiset.count_antidiagonal_eq_count_powerset {α : Type u_1} [DecidableEq α] (s t : Multiset α) : count (s, t) (s + t).antidiagonal = count t (s + t).powerset

The multiplicity of (s, t) in antidiagonal (s + t) is the number of ways to select the sub-multiset t from s + t.

theorem Multiset.count_antidiagonal {α : Type u_1} [DecidableEq α] (u v w : Multiset α) : count (u, v) w.antidiagonal = if u + v = w then ∏ x ∈ w.toFinset, (count x w).choose (count x v) else 0

Closed form for the multiplicities of Multiset.antidiagonal: an ordered split (u, v) of w occurs ∏ x, (w.count x).choose (v.count x) times.

theorem Multiset.count_antidiagonal_swap {α : Type u_1} [DecidableEq α] (u v w : Multiset α) : count (u, v) w.antidiagonal = count (v, u) w.antidiagonal

The antidiagonal multiplicity is symmetric in the two slots.