Alternating multi-index binomial convolution cancellation

Proved

MultiIndex.alternating_binomial_convolution

by Mazecto · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebracombinatorics

Let the coordinate type be finite, R a commutative ring, α a natural-valued multi-index, and S a finite set containing every coordinatewise sub-index of α. For an arbitrary R-valued two-index array F, summing the nested binomial expression in the formal statement leaves only (−1)^|α| F(0,α). All subtractions are coordinatewise truncated natural subtraction. Extra indices in S contribute zero: nonzero coefficients require γ≤β≤α. On that down-set the first argument of F becomes α−γ, and the identity follows by the binomial coefficient product formula and coordinatewise alternating binomial cancellation. This theorem is purely algebraic and does not assume any calculus structure.

Preamble

import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Data.Fintype.Basic

Formal statement

theorem MultiIndex.alternating_binomial_convolution
    {ι R : Type*} [Fintype ι] [CommRing R]
    (α : ι → ℕ) (s : Finset (ι → ℕ))
    (hs : ∀ β : ι → ℕ, (∀ i, β i ≤ α i) → β ∈ s)
    (F : (ι → ℕ) → (ι → ℕ) → R) :
    (∑ β ∈ s, (∏ i, (Nat.choose (α i) (β i) : R)) *
      (-1 : R) ^ (∑ i, β i) *
      (∑ γ ∈ s, (∏ i, (Nat.choose (β i) (γ i) : R)) *
        F (fun i => α i - β i + (β i - γ i)) γ)) =
      (-1 : R) ^ (∑ i, α i) * F (fun _ => 0) α := by sorry

Source

Derived multi-index binomial inversion identity. Elementary ingredients in the pinned Mathlib are Nat.choose_mul (Mathlib/Data/Nat/Choose/Basic.lean) and Int.alternating_sum_range_choose (Mathlib/Data/Nat/Choose/Sum.lean), https://github.com/leanprover-community/mathlib4/tree/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Data/Nat/Choose. The multi-index convolution statement is a derived algebraic lemma, not quoted as a theorem from Hunter.

View graph