mathlib documentation

data.nat.choose.sum

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 {α : Type u_1} [semiring α] {x y : α} (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.

theorem add_pow {α : Type u_1} [comm_semiring α] (x y : α) (n : ) :
(x + y) ^ n = ∑ (m : ) in finset.range (n + 1), ((x ^ m) * y ^ (n - m)) * (n.choose m)

The binomial theorem

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

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

theorem nat.choose_middle_le_pow (n : ) :
(2 * n + 1).choose n 4 ^ n

theorem int.alternating_sum_range_choose {n : } :
∑ (m : ) in finset.range (n + 1), ((-1) ^ m) * (n.choose m) = ite (n = 0) 1 0

theorem int.alternating_sum_range_choose_of_ne {n : } (h0 : n 0) :
∑ (m : ) in finset.range (n + 1), ((-1) ^ m) * (n.choose m) = 0

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

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

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