English
Let f: N × N → R be a function into a semiring R. Then the sum over the antidiagonal of size n of binomial weights times f equals the sum of two partial sums over the antidiagonal of size n−1 with shifted arguments.
Русский
Пусть f: ℕ × ℕ → R. Тогда сумма по антидиагонали размера n диапазона (n+1).choose i с учётом умножения на f(i,j) разложится на две части сдвинутых аргументов.
LaTeX
$$$$\sum_{(i,j) \in \operatorname{antidiagonal}(n+1)} \binom{n+1}{i} f(i,j) = \sum_{(i,j) \in \operatorname{antidiagonal}(n)} \binom{n}{i} f(i,j+1) + \sum_{(i,j) \in \operatorname{antidiagonal}(n)} \binom{n}{j} f(i+1,j).$$$$
Lean4
/-- The sum of `(n+1).choose i * f i (n+1-i)` can be split into two sums at rank `n`,
respectively of `n.choose i * f i (n+1-i)` and `n.choose i * f (i+1) (n-i)`. -/
theorem sum_choose_succ_mul (f : ℕ → ℕ → R) (n : ℕ) :
(∑ i ∈ range (n + 2), ((n + 1).choose i : R) * f i (n + 1 - i)) =
(∑ i ∈ range (n + 1), (n.choose i : R) * f i (n + 1 - i)) +
∑ i ∈ range (n + 1), (n.choose i : R) * f (i + 1) (n - i) :=
by simpa only [nsmul_eq_mul] using sum_choose_succ_nsmul f n
