The pointwise convolution form of product coefficients

MvPolynomial.coeff of a product, reindexed from the Finsupp antidiagonal to guarded pointwise splits over a bounded pi-set — the shape produced by the colour-character convolution.

theorem RS.coeff_mul_split {k : ℕ} (P Q : MvPolynomial (Fin k) ℂ) (α : Fin k → ℕ) (n : ℕ) (hn : ∀ (a : Fin k), α a ≤ n) : (P * Q).coeff (∑ a : Fin k, Finsupp.single a (α a)) = ∑ w ∈ Fintype.piFinset fun (x : Fin k) => Finset.range (n + 1), if ∀ (a : Fin k), w a ≤ α a then P.coeff (∑ a : Fin k, Finsupp.single a (α a - w a)) * Q.coeff (∑ a : Fin k, Finsupp.single a (w a)) else 0

The guarded pointwise convolution.