English
Hockey-stick identity: the sum of binomial coefficients along an initial segment equals a shifted binomial coefficient.
Русский
Идентичность хоккейной палки: сумма биномиальных коэффициентов по начальному отрезку равна соответствующему смещённому биномиальному коэффициенту.
LaTeX
$$$\sum_{m=0}^n \binom{m+k}{k} = \binom{n+k+1}{k+1}$$$
Lean4
theorem sum_range_choose_halfway (m : ℕ) : (∑ i ∈ range (m + 1), (2 * m + 1).choose i) = 4 ^ m :=
have : (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i :=
sum_congr rfl fun i hi ↦ choose_symm <| by linarith [mem_range.1 hi]
mul_right_injective₀ two_ne_zero <|
calc
(2 * ∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
(∑ i ∈ range (m + 1), (2 * m + 1).choose i) + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) :=
by rw [two_mul, this]
_ = (∑ i ∈ range (m + 1), (2 * m + 1).choose i) + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i :=
by
rw [range_eq_Ico, sum_Ico_reflect _ _ (by cutsat)]
congr
cutsat
_ = ∑ i ∈ range (2 * m + 2), (2 * m + 1).choose i := (sum_range_add_sum_Ico _ (by cutsat))
_ = 2 ^ (2 * m + 1) := (sum_range_choose (2 * m + 1))
_ = 2 * 4 ^ m := by rw [pow_succ, pow_mul, mul_comm]; rfl
