Sums of binomial coefficients

This file includes variants of the binomial theorem and other results on sums of binomial coefficients. Theorems whose proofs depend on such sums may also go in this file for import reasons.

theorem Commute.add_pow {R : Type u_1} [Semiring R] {x : R} {y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ n = (Finset.range (n + 1)).sum fun (m : ℕ) => x ^ m * y ^ (n - m) * ↑(n.choose m)

A version of the binomial theorem for commuting elements in noncommutative semirings.

theorem Commute.add_pow' {R : Type u_1} [Semiring R] {x : R} {y : R} (h : Commute x y) (n : ℕ) : (x + y) ^ n = (Finset.antidiagonal n).sum fun (m : ℕ × ℕ) => n.choose m.1 • (x ^ m.1 * y ^ m.2)

A version of Commute.add_pow that avoids ℕ-subtraction by summing over the antidiagonal and also with the binomial coefficient applied via scalar action of ℕ.

theorem add_pow {R : Type u_1} [CommSemiring R] (x : R) (y : R) (n : ℕ) : (x + y) ^ n = (Finset.range (n + 1)).sum fun (m : ℕ) => x ^ m * y ^ (n - m) * ↑(n.choose m)

The binomial theorem

theorem Nat.sum_range_choose (n : ℕ) : ((Finset.range (n + 1)).sum fun (m : ℕ) => n.choose m) = 2 ^ n

The sum of entries in a row of Pascal's triangle

theorem Nat.sum_range_choose_halfway (m : ℕ) : ((Finset.range (m + 1)).sum fun (i : ℕ) => (2 * m + 1).choose i) = 4 ^ m

theorem Nat.choose_middle_le_pow (n : ℕ) : (2 * n + 1).choose n ≤ 4 ^ n

theorem Nat.four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) : 4 ^ n ≤ (2 * n + 1) * (2 * n).choose n

theorem Nat.sum_Icc_choose (n : ℕ) (k : ℕ) : ((Finset.Icc k n).sum fun (m : ℕ) => m.choose k) = (n + 1).choose (k + 1)

Zhu Shijie's identity aka hockey-stick identity.

theorem Int.alternating_sum_range_choose {n : ℕ} : ((Finset.range (n + 1)).sum fun (m : ℕ) => (-1) ^ m * ↑(n.choose m)) = if n = 0 then 1 else 0

theorem Int.alternating_sum_range_choose_of_ne {n : ℕ} (h0 : n ≠ 0) : ((Finset.range (n + 1)).sum fun (m : ℕ) => (-1) ^ m * ↑(n.choose m)) = 0

theorem Finset.sum_powerset_apply_card {α : Type u_2} {β : Type u_3} [AddCommMonoid α] (f : ℕ → α) {x : Finset β} : (x.powerset.sum fun (m : Finset β) => f m.card) = (Finset.range (x.card + 1)).sum fun (m : ℕ) => x.card.choose m • f m

theorem Finset.sum_powerset_neg_one_pow_card {α : Type u_2} [DecidableEq α] {x : Finset α} : (x.powerset.sum fun (m : Finset α) => (-1) ^ m.card) = if x = ∅ then 1 else 0

theorem Finset.sum_powerset_neg_one_pow_card_of_nonempty {α : Type u_2} {x : Finset α} (h0 : x.Nonempty) : (x.powerset.sum fun (m : Finset α) => (-1) ^ m.card) = 0

theorem Finset.sum_choose_succ_nsmul {M : Type u_4} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ((Finset.range (n + 2)).sum fun (i : ℕ) => (n + 1).choose i • f i (n + 1 - i)) = ((Finset.range (n + 1)).sum fun (i : ℕ) => n.choose i • f i (n + 1 - i)) + (Finset.range (n + 1)).sum fun (i : ℕ) => n.choose i • f (i + 1) (n - i)

theorem Finset.prod_pow_choose_succ {M : Type u_4} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ((Finset.range (n + 2)).prod fun (i : ℕ) => f i (n + 1 - i) ^ (n + 1).choose i) = ((Finset.range (n + 1)).prod fun (i : ℕ) => f i (n + 1 - i) ^ n.choose i) * (Finset.range (n + 1)).prod fun (i : ℕ) => f (i + 1) (n - i) ^ n.choose i

theorem Finset.sum_antidiagonal_choose_succ_nsmul {M : Type u_4} [AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ((Finset.antidiagonal (n + 1)).sum fun (ij : ℕ × ℕ) => (n + 1).choose ij.1 • f ij.1 ij.2) = ((Finset.antidiagonal n).sum fun (ij : ℕ × ℕ) => n.choose ij.1 • f ij.1 (ij.2 + 1)) + (Finset.antidiagonal n).sum fun (ij : ℕ × ℕ) => n.choose ij.2 • f (ij.1 + 1) ij.2

theorem Finset.prod_antidiagonal_pow_choose_succ {M : Type u_4} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) : ((Finset.antidiagonal (n + 1)).prod fun (ij : ℕ × ℕ) => f ij.1 ij.2 ^ (n + 1).choose ij.1) = ((Finset.antidiagonal n).prod fun (ij : ℕ × ℕ) => f ij.1 (ij.2 + 1) ^ n.choose ij.1) * (Finset.antidiagonal n).prod fun (ij : ℕ × ℕ) => f (ij.1 + 1) ij.2 ^ n.choose ij.2

theorem Finset.sum_choose_succ_mul {R : Type u_3} [NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ) : ((Finset.range (n + 2)).sum fun (i : ℕ) => ↑((n + 1).choose i) * f i (n + 1 - i)) = ((Finset.range (n + 1)).sum fun (i : ℕ) => ↑(n.choose i) * f i (n + 1 - i)) + (Finset.range (n + 1)).sum fun (i : ℕ) => ↑(n.choose i) * f (i + 1) (n - i)

The sum of (n+1).choose i * f i (n+1-i) can be split into two sums at rank n, respectively of n.choose i * f i (n+1-i) and n.choose i * f (i+1) (n-i).

theorem Finset.sum_antidiagonal_choose_succ_mul {R : Type u_3} [NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ) : ((Finset.antidiagonal (n + 1)).sum fun (ij : ℕ × ℕ) => ↑((n + 1).choose ij.1) * f ij.1 ij.2) = ((Finset.antidiagonal n).sum fun (ij : ℕ × ℕ) => ↑(n.choose ij.1) * f ij.1 (ij.2 + 1)) + (Finset.antidiagonal n).sum fun (ij : ℕ × ℕ) => ↑(n.choose ij.2) * f (ij.1 + 1) ij.2

The sum along the antidiagonal of (n+1).choose i * f i j can be split into two sums along the antidiagonal at rank n, respectively of n.choose i * f i (j+1) and n.choose j * f (i+1) j.

theorem Finset.sum_antidiagonal_choose_add (d : ℕ) (n : ℕ) : ((Finset.antidiagonal n).sum fun (ij : ℕ × ℕ) => (d + ij.2).choose d) = (d + n).choose d + (d + n).choose d.succ