English
Let f: ℕ → M be monotone in the sense of an ordered substructure, with M a partially ordered additive structure. Then
Русский
Пусть f: ℕ → M монотонна в смысле упорядоченной подструктуры; тогда сумма разностей подряд удовлетворяет туб(период).
LaTeX
$$$\sum_{i=0}^{n-1} (f(i+1) - f(i)) = f(n) - f(0)$$$
Lean4
/-- A telescoping sum along `{0, ..., n-1}` of an `ℕ`-valued function reduces to the difference of
the last and first terms when the function we are summing is monotone. -/
theorem sum_range_tsub {f : ℕ → M} (h : Monotone f) (n : ℕ) : ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0 :=
by
apply sum_range_induction
case base => apply tsub_eq_of_eq_add; rw [zero_add]
case step =>
intro n _
have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]
