Finset.sum_add_adjacent_intervals

Stream: Is there code for X?

[Alex Kontorovich]

Do we not have something like this (mimicking intervalIntegral.integral_add_adjacent_intervals)?

import Mathlib

open BigOperators

lemma Finset.sum_add_adjacent_intervals {a b c : ℤ} (f : ℤ → ℝ) (h : a ≤ b) (h' : b ≤ c) :
  (∑ n in Finset.Ioc a b, f n) + (∑ n in Finset.Ioc b c, f n) = ∑ n in Finset.Ioc a c, f n := by
  sorry

Thanks!

[Notification Bot]

Alex Kontorovich has marked this topic as resolved.

[Notification Bot]

Alex Kontorovich has marked this topic as unresolved.

[Notification Bot]

Alex Kontorovich has marked this topic as resolved.

[Notification Bot]

Alex Kontorovich has marked this topic as unresolved.

[Notification Bot]

Alex Kontorovich has marked this topic as resolved.

[Notification Bot]

Alex Kontorovich has marked this topic as unresolved.

[Yaël Dillies]

It's part of an API I've been working on, but it's ot on mathlib

[Alex Kontorovich]

Ok thanks! Did I guess the name right? (Tried editing the title, and the "edit" button kept sliding away, putting my cursor on the "resolved" button! Haha...)

[Yaël Dillies]

Finset.sum_Ioc_add_sum_Ioc it would be, rather!