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.

source

theorem commute.add_pow {R : Type u_1} [semiring R] {x y : R} (h : commute x y) (n : ℕ) :

(x + y) ^ n = ∑ (m : ℕ) in finset.range (n + 1), ((x ^ m) * y ^ (n - m)) * ↑(n.choose m)

A version of the binomial theorem for noncommutative semirings.

source

theorem commute.add_pow' {R : Type u_1} [semiring R] {x y : R} (h : commute x y) (n : ℕ) :

(x + y) ^ n = ∑ (m : ℕ × ℕ) in finset.nat.antidiagonal n, n.choose m.fst • (x ^ m.fst) * y ^ m.snd

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 ℕ.

source

theorem add_pow {R : Type u_1} [comm_semiring R] (x y : R) (n : ℕ) :

(x + y) ^ n = ∑ (m : ℕ) in finset.range (n + 1), ((x ^ m) * y ^ (n - m)) * ↑(n.choose m)

The binomial theorem

source

theorem nat.sum_range_choose (n : ℕ) :

∑ (m : ℕ) in finset.range (n + 1), n.choose m = 2 ^ n

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

source

theorem nat.sum_range_choose_halfway (m : ℕ) :

∑ (i : ℕ) in finset.range (m + 1), (2 * m + 1).choose i = 4 ^ m

source

theorem nat.choose_middle_le_pow (n : ℕ) :

(2 * n + 1).choose n ≤ 4 ^ n

source

theorem nat.four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) :

4 ^ n ≤ (2 * n + 1) * (2 * n).choose n

source

theorem int.alternating_sum_range_choose {n : ℕ} :

∑ (m : ℕ) in finset.range (n + 1), ((-1) ^ m) * ↑(n.choose m) = ite (n = 0) 1 0

source

theorem int.alternating_sum_range_choose_of_ne {n : ℕ} (h0 : n ≠ 0) :

∑ (m : ℕ) in finset.range (n + 1), ((-1) ^ m) * ↑(n.choose m) = 0

source

theorem finset.sum_powerset_apply_card {α : Type u_1} {β : Type u_2} [add_comm_monoid α] (f : ℕ → α) {x : finset β} :

∑ (m : finset β) in x.powerset, f m.card = ∑ (m : ℕ) in finset.range (x.card + 1), x.card.choose m • f m

source

theorem finset.sum_powerset_neg_one_pow_card {α : Type u_1} [decidable_eq α] {x : finset α} :

∑ (m : finset α) in x.powerset, (-1) ^ m.card = ite (x = ∅) 1 0

source

theorem finset.sum_powerset_neg_one_pow_card_of_nonempty {α : Type u_1} {x : finset α} (h0 : x.nonempty) :

∑ (m : finset α) in x.powerset, (-1) ^ m.card = 0