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:
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
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