telescoping sum

Stream: Is there code for X?

[Rémy Degenne]

Is there code for the following lemma:

lemma telescoping_sum {α} [add_comm_group α] (f : ℕ → α) (n : ℕ) :
  f (n+1) = f 0 + ∑ i in finset.range (n+1), (f (i+1) - f i) :=
sorry

Thanks!

[Bryan Gin-ge Chen]

docs#sum_range_sub

[Rémy Degenne]

Great! Thank you!

[Yakov Pechersky]

Brute force:

import algebra.big_operators
import tactic.ring

open_locale big_operators

lemma telescoping_sum {α} [add_comm_group α] (f : ℕ → α) (n : ℕ) :
  f (n+1) = f 0 + ∑ i in finset.range (n+1), (f (i+1) - f i) :=
begin
  induction n with n hn,
  { simp },
  { rw [finset.sum_range_succ, hn],
    abel,
    simp },
end

[Yakov Pechersky]

Ah, there are nice induction principles for it. Oh well!