Theorems · Theorem · combinatorics

Nat.sum_range_add_choose

∀ (n k : ℕ), ∑ i ∈ Finset.range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)

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.

Defined in

Mathlib.Data.Nat.Choose.Sum

Cited by

1 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound