feat(data/nat/choose/sum): alternating binomial coefficient sums (#4997)

Evaluates some sums related to binomial coefficients with alternating signs

src/data/finset/powerset.lean

@@ -92,5 +92,9 @@ by cases s; simp [powerset_len, val_le_iff.symm]; refl
   card (powerset_len n s) = nat.choose (card s) n :=
 (card_pmap _ _ _).trans (card_powerset_len n s.1)
 
+theorem powerset_len_eq_filter {n} {s : finset α} :
+  powerset_len n s = (powerset s).filter (λ x, x.card = n) :=
+by { ext, simp [mem_powerset_len] }
+
 end powerset_len
 end finset

src/data/nat/choose/sum.lean

@@ -97,3 +97,57 @@ begin
 end
 
 end nat
+
+theorem int.alternating_sum_range_choose {n : ℕ} :
+  ∑ m in range (n + 1), ((-1) ^ m * ↑(choose n m) : ℤ) = if n = 0 then 1 else 0 :=
+begin
+  cases n, { simp },
+  have h := add_pow (-1 : ℤ) 1 n.succ,
+  simp only [one_pow, mul_one, add_left_neg, int.nat_cast_eq_coe_nat] at h,
+  rw [← h, zero_pow (nat.succ_pos n), if_neg (nat.succ_ne_zero n)],
+end
+
+theorem int.alternating_sum_range_choose_of_ne {n : ℕ} (h0 : n ≠ 0) :
+  ∑ m in range (n + 1), ((-1) ^ m * ↑(choose n m) : ℤ) = 0 :=
+by rw [int.alternating_sum_range_choose, if_neg h0]
+
+namespace finset
+
+theorem sum_powerset_apply_card {α β : Type*} [add_comm_monoid α] (f : ℕ → α) {x : finset β} :
+  ∑ m in x.powerset, f m.card = ∑ m in range (x.card + 1), (x.card.choose m) •ℕ f m :=
+begin
+  transitivity ∑ m in range (x.card + 1), ∑ j in x.powerset.filter (λ z, z.card = m), f j.card,
+  rw sum_fiberwise_of_maps_to,
+  { intros y hy,
+    rw [mem_range, nat.lt_succ_iff],
+    rw mem_powerset at hy,
+    exact card_le_of_subset hy },
+  apply sum_congr rfl,
+  intros y hy,
+  rw [← card_powerset_len, ← sum_const],
+  apply sum_congr powerset_len_eq_filter.symm,
+  intros z hz,
+  rw (mem_powerset_len.1 hz).2,
+end
+
+theorem sum_powerset_neg_one_pow_card {α : Type*} [decidable_eq α] {x : finset α} :
+  ∑ m in x.powerset, (-1 : ℤ) ^ m.card = if x = ∅ then 1 else 0 :=
+begin
+  rw sum_powerset_apply_card,
+  simp only [nsmul_eq_mul', ← card_eq_zero],
+  convert int.alternating_sum_range_choose,
+  ext,
+  simp,
+end
+
+theorem sum_powerset_neg_one_pow_card_of_nonempty {α : Type*} {x : finset α}
+  (h0 : x.nonempty) :
+  ∑ m in x.powerset, (-1 : ℤ) ^ m.card = 0 :=
+begin
+  classical,
+  rw [sum_powerset_neg_one_pow_card, if_neg],
+  rw [← ne.def, ← nonempty_iff_ne_empty],
+  apply h0,
+end
+
+end finset