# Zulip Chat Archive

## Stream: new members

### Topic: changing indices

#### Alex Kontorovich (Apr 15 2020 at 17:44):

Hi, I'm trying to change indices in summation:

lemma diff_sums (F:ℕ→\R) : ∀ j, ∀ i, (j≥ i) → ( ((range j).sum F) - ((range i).sum F)) = (range (j-i)).sum (λ k , F(k+i)) := sorry

I see that this kind of thing has been done already, e.g., "sum_range_def" in:

https://github.com/leanprover/lean2/blob/master/library/data/nat/bigops.lean

But I'm not able to call sum_range_def (though I am able to call "sum_range_succ" which I think is defined in the same file?)

Help please? Thanks!

#### Alex J. Best (Apr 15 2020 at 17:51):

That repo is from `lean2`

(the old version of lean) so possibly that particular lemma is not in lean 3 (with the same name).

I think the lemma `sum_Ico_eq_sub`

in algebra/big_operators.lean does half of what you want.

#### Alex J. Best (Apr 15 2020 at 17:57):

So with some minor modifications to your statement this works

lemma diff_sums (F:ℕ → ℝ) : ∀ j, ∀ i, (i ≤ j) → ( ((range j).sum F) - ((range i).sum F)) = (range (j-i)).sum (λ k , F(i+k)) := begin intros, rw ← sum_Ico_eq_sub, exact (sum_Ico_eq_sum_range _ _ _), assumption, end

I changed `j \ge i`

to be `i \le j`

as all lemmas in mathlib are stated with a less than rather than a greater than where possible (so it is best to basically never use greater than, and swap the sides in all statements). And I changed `k + i`

to `i + k`

to match the library version (not necessary but makes the proof one line shorter)

Last updated: May 13 2021 at 20:13 UTC