Chu-Vandermonde Identity

Statement

The Chu–Vandermonde identity generalizes Vandermonde's convolution to arbitrary upper parameters in a binomial ring. For $r, s$ in a binomial ring and $n \in \mathbb{N}$, where $\binom{r}{k}$ is defined via the falling factorial $r^{\underline{k}} / k!$:

This extends the classical combinatorial identity to polynomial rings and formal power series. The key symmetric-function viewpoint: in $\mathbb{Z}<a class="concept-link" data-concept="X">X</a>$, multiplying the generating series $(1+X)^r \cdot (1+X)^s = (1+X)^{r+s}$ and extracting the coefficient of $X^n$ yields the identity directly.

For natural numbers $r = m$, $s = n$ the identity reduces to Vandermonde's convolution: choosing $r$ items from two disjoint pools of sizes $m$ and $n$ decomposes as $\sum_k \binom{m}{k}\binom{n}{r-k}$.

Visualization

Small case $m = 4$, $n = 2$, $r = 3$. Check $\binom{6}{3} = 20$:

$k$	$\binom{4}{k}$	$\binom{2}{3-k}$	product
1	4	1	4
2	6	0	0
3	4	0	0

Wait — that gives 4, not 20. Include $k=0$ and $k=1$ with $\binom{2}{3}=0$, and note $\binom{2}{2}=1$ at $k=1$:

$k$	$\binom{4}{k}$	$\binom{2}{3-k}$	product
0	1	$\binom{2}{3}=0$	0
1	4	$\binom{2}{2}=1$	4
2	6	$\binom{2}{1}=2$	12
3	4	$\binom{2}{0}=1$	4
sum			20

Confirmed: $0 + 4 + 12 + 4 = 20 = \binom{6}{3}$.

Proof Sketch

1. Polynomial identity. In the polynomial ring $\mathbb{Z}[X]$, the generalized binomial series satisfies $(1+X)^r = \sum_k \binom{r}{k} X^k$ as formal power series (or polynomials when $r \in \mathbb{N}$).
2. Multiply series. $(1+X)^r \cdot (1+X)^s = (1+X)^{r+s}$.
3. Extract coefficient. The coefficient of $X^n$ on the left is $\sum_k \binom{r}{k}\binom{s}{n-k}$; on the right it is $\binom{r+s}{n}$.
4. Chu's extension. For $r, s$ in a binomial ring the same algebraic steps go through because the ring axioms and the definition of the generalized $\binom{\cdot}{\cdot}$ are enough.

Connections

This is a direct generalization of Vandermonde's IdentityVandermonde's Identity$$\binom{m+n}{r} = \sum_{k=0}^{r} \binom{m}{k}\binom{n}{r-k}$$The convolution identity for binomial coefficients: C(m+n,r) = sum over k of C(m,k)*C(n,r-k).Read more → and specializes to Pascal's IdentityPascal's Identity$$\binom{n}{k} = \binom{n-1}{k-1} + \binom{n-1}{k}$$The binomial coefficient recurrence: C(n,k) = C(n-1,k-1) + C(n-1,k), the engine of Pascal's triangle.Read more → when $r = n-1$, $s = 1$. It also connects to the Binomial TheoremBinomial Theorem$$(x+y)^n = \sum_{k=0}^{n} \binom{n}{k} x^k y^{n-k}$$Expanding powers of a sum via binomial coefficientsRead more → (the $n=1$ case).

import Mathlib.Data.Nat.Choose.Vandermonde

/-- Vandermonde's identity in Mathlib:
    ∑ k in Finset.range (r+1), C(m,k) * C(n, r-k) = C(m+n, r).
    `Nat.add_choose_eq` packages this as `Nat.choose (m+n) r`. -/
theorem vandermonde_identity (m n r : ℕ) :
    ∑ k ∈ Finset.range (r + 1), Nat.choose m k * Nat.choose n (r - k) =
    Nat.choose (m + n) r :=
  Nat.add_choose_eq m n r

/-- Chu–Vandermonde concrete instance (m=4, n=2, r=3):
    C(4,1)*C(2,2) + C(4,2)*C(2,1) + C(4,3)*C(2,0) = 4 + 12 + 4 = 20 = C(6,3).
    Proved by reducing to Vandermonde then `decide`. -/
theorem chu_vandermonde_4_2_3 :
    ∑ k ∈ Finset.range 4, Nat.choose 4 k * Nat.choose 2 (3 - k) = 20 := by
  have := vandermonde_identity 4 2 3
  simp [Finset.sum_range_succ] at this ⊢
  omega