Vandermonde collapse of multi-index binomial sums

The multi-index Leibniz rule for ∂^α (g h) produces the weights C(α₀, a) C(α₁, b) C(α₂, c); summed over a + b + c = m they give C(|α|, m). This is the combinatorial input of the product estimates in the proof of thm:analytic:interior.

theorem CIV.sum_choose_mul_choose_collapse (A B : ℕ) (F : ℕ → ℝ) : ∑ a ∈ Finset.range (A + 1), ∑ b ∈ Finset.range (B + 1), ↑(A.choose a * B.choose b) * F (a + b) = ∑ m ∈ Finset.range (A + B + 1), ↑((A + B).choose m) * F m

Vandermonde collapse of a double binomial sum.

theorem CIV.sum_choose_mul_choose_mul_choose_collapse (A B D : ℕ) (F : ℕ → ℝ) : ∑ a ∈ Finset.range (A + 1), ∑ b ∈ Finset.range (B + 1), ∑ c ∈ Finset.range (D + 1), ↑(A.choose a * B.choose b * D.choose c) * F (a + b + c) = ∑ m ∈ Finset.range (A + B + D + 1), ↑((A + B + D).choose m) * F m

Vandermonde collapse of a triple binomial sum: the multi-index binomial weights of order m sum to (A + B + D).choose m.