Elementary identities for binomial coefficients

This file records arithmetic identities involving natural-number binomial coefficients.

Besides two identities for the second binomial coefficient, it develops Vandermonde's convolution ∑ i, C(A, i) * C(B, r - i) = C(A + B, r) in the shape taken by factorial moments of a law supported on such a convolution: each summand is weighted by the falling factorial (i)ₘ of the summation index. The weighted sum is again a single binomial coefficient, (A)ₘ * C(A + B - m, r - m), because (i)ₘ lowers both indices of C(A, i) at once.

Main results

• Nat.choose_two_add_mul_succ_div_two: the sum of the second binomial coefficient and the triangular number is the corresponding square.
• Nat.add_choose_two: the second binomial coefficient of a sum, with its cross term.
• Nat.descFactorial_mul_choose: a falling factorial of the lower index lowers both indices, (i)ₘ * C(A, i) = (A)ₘ * C(A - m, i - m).
• Nat.sum_range_descFactorial_mul_choose_mul_choose: Vandermonde's convolution weighted by a falling factorial of the summation index.

References

• R. L. Graham, D. E. Knuth, O. Patashnik, Concrete Mathematics, 2nd ed., Addison-Wesley, 1994, Section 5.1 (the absorption identity and Vandermonde's convolution, equation (5.27)).

theorem Nat.choose_two_add_mul_succ_div_two (N : ℕ) : N.choose 2 + N * (N + 1) / 2 = N * N

The sum of N.choose 2 and the Nth triangular number is N ^ 2.

theorem Nat.add_choose_two (m n : ℕ) : (m + n).choose 2 = m.choose 2 + n.choose 2 + m * n

The second binomial coefficient of a sum: C(m + n, 2) = C(m, 2) + C(n, 2) + mn.

theorem Nat.descFactorial_mul_choose {m i : ℕ} (hmi : m ≤ i) (A : ℕ) : i.descFactorial m * A.choose i = A.descFactorial m * (A - m).choose (i - m)

A falling factorial of the lower index lowers both indices of a binomial coefficient: (i)ₘ * C(A, i) = (A)ₘ * C(A - m, i - m) for m ≤ i.

Both sides count the pairs consisting of an i-element subset of an A-element set and an ordered m-tuple of distinct elements of that subset. The hypothesis m ≤ i is needed: for i < m the left-hand side vanishes while the right-hand side need not.

theorem Nat.sum_range_descFactorial_mul_choose_mul_choose {m r : ℕ} (hmr : m ≤ r) (A B : ℕ) : ∑ i ∈ Finset.range (r + 1), i.descFactorial m * (A.choose i * B.choose (r - i)) = A.descFactorial m * (A + B - m).choose (r - m)

Vandermonde's convolution weighted by a falling factorial of the summation index.

Weighting the ith summand of ∑ i, C(A, i) * C(B, r - i) = C(A + B, r) by (i)ₘ multiplies the value by (A)ₘ and lowers both indices by m. After division by C(A + B, r), the cases m = 1 and m = 2 give the first two factorial moments of a hypergeometric law.