Sub of Finset.sum

Stream: new members

[Junjie Bai]

Is there any function can prove that

variable {a : ℤ} (f : ℚ → ℚ)

example : (∑ x in Icc 0 (a + 1), f x) - (∑ x in Icc 0 a, f x) = f (a + 1) := by sorry

[Kevin Buzzard]

I don't think that's true. What if a=-37?

[Junjie Bai]

You're right. I think this is what I mean:

variable {a : ℤ} (f : ℚ → ℚ)

example (ha : a ≥ 0) : (∑ x in Icc 0 (a + 1), f x) - (∑ x in Icc 0 a, f x) = f (a + 1) := by sorry

[Eric Wieser]

We won't have this lemma, but it follows in not too many steps. Can you see how to break the problem down? Try doing so with have statements, and using exact? for each

[Johan Commelin]

Can you prove Icc 0 (a + 1) = Icc 0 a \cup {a+1}?

[Eric Wieser]

(or possibly, Icc 0 (a + 1) = (Icc 0 a).cons a sorry, which is a slightly stronger result)

[Junjie Bai]

I think I can solve this now, thanks a lot!