From 901b783268f6721b515cbf39eddfb07db4fba5ed Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Fri, 5 Jan 2024 06:57:28 +0000 Subject: [PATCH] feat: Zhu Shijie's identity (#9427) Cf. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Proof.20of.20Combinatorial.20Identities/near/411120131 --- Mathlib/Data/Nat/Choose/Sum.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Data/Nat/Choose/Sum.lean b/Mathlib/Data/Nat/Choose/Sum.lean index 4fc5443a4c328..061ac12398ff5 100644 --- a/Mathlib/Data/Nat/Choose/Sum.lean +++ b/Mathlib/Data/Nat/Choose/Sum.lean @@ -132,6 +132,14 @@ theorem four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) : _ = (2 * n + 1) * choose (2 * n) n := by simp #align nat.four_pow_le_two_mul_add_one_mul_central_binom Nat.four_pow_le_two_mul_add_one_mul_central_binom +/-- **Zhu Shijie's identity** aka hockey-stick identity. -/ +theorem sum_Icc_choose (n k : ℕ) : ∑ m in Icc k n, m.choose k = (n + 1).choose (k + 1) := by + cases' le_or_gt k n with h h + · induction' n, h using le_induction with n _ ih; · simp + rw [← Ico_insert_right (by linarith), sum_insert (by simp), + show Ico k (n + 1) = Icc k n by rfl, ih, choose_succ_succ' (n + 1)] + · rw [choose_eq_zero_of_lt (by linarith), Icc_eq_empty_of_lt h, sum_empty] + end Nat theorem Int.alternating_sum_range_choose {n : ℕ} :