English
Zhu Shijie's hockey-stick identity in the Icc form: the total of binomial coefficients from k to n equals a shifted binomial coefficient.
Русский
Идентичность хоккейной палки Жу Шицзе в форме Icc: сумма биномиальных коэффициентов от k до n равна смещённому биномиальному коэффициенту.
LaTeX
$$$\sum_{m=k}^n {m\choose k} = {n+1 \choose k+1}$$$
Lean4
/-- **Zhu Shijie's identity** aka hockey-stick identity, version with `range`.
Summing `(i + k).choose k` for `i ∈ [0, n]` gives `(n + k + 1).choose (k + 1)`.
Combinatorial interpretation: `(i + k).choose k` is the number of decompositions of `[0, i)` in
`k + 1` (possibly empty) intervals (this follows from a stars and bars description). In particular,
`(n + k + 1).choose (k + 1)` corresponds to decomposing `[0, n)` into `k + 2` intervals.
By putting away the last interval (of some length `n - i`),
we have to decompose the remaining interval `[0, i)` into `k + 1` intervals, hence the sum. -/
theorem sum_range_add_choose (n k : ℕ) : ∑ i ∈ Finset.range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1) :=
by
rw [← sum_Icc_choose, range_eq_Ico]
convert (sum_map _ (addRightEmbedding k) (·.choose k)).symm using 2
rw [map_add_right_Ico, zero_add, add_right_comm, Ico_add_one_right_eq_Icc]
