Zulip Chat Archive

Stream: Is there code for X?

Topic: telescoping sum


view this post on Zulip Rémy Degenne (Jan 05 2021 at 08:31):

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!

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 08:33):

docs#sum_range_sub

view this post on Zulip Rémy Degenne (Jan 05 2021 at 08:34):

Great! Thank you!

view this post on Zulip Yakov Pechersky (Jan 05 2021 at 08:36):

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

view this post on Zulip Yakov Pechersky (Jan 05 2021 at 08:37):

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


Last updated: May 07 2021 at 23:11 UTC