## 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?)

#### 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 ito 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