Summing finitely many jumps on an ordered interval

A function into an additive commutative group, constant between finitely many events, has total change equal to the sum of its local changes. This is the finite telescoping step in the signed Sturm theorem; it uses no topology or completeness.

theorem Finset.exists_right_gap {R : Type u_1} [LinearOrder R] [DenselyOrdered R] (S : Finset R) {r b : R} (hrb : r < b) : ∃ (c : R), r < c ∧ c < b ∧ ∀ x ∈ S, r < x → c < x

Choose a point to the right of an event, before all later events and a given bound.

theorem Finset.exists_left_gap {R : Type u_1} [LinearOrder R] [DenselyOrdered R] (S : Finset R) {a r : R} (har : a < r) : ∃ (c : R), a < c ∧ c < r ∧ ∀ x ∈ S, x < r → x < c

Choose a point to the left of an event, after all earlier events and a given bound.

theorem Finset.sum_jumps {R : Type u_1} [LinearOrder R] [DenselyOrdered R] {G : Type u_2} [AddCommGroup G] (S : Finset R) (V w : R → G) {a₀ b₀ : R} (hconst : ∀ (a b : R), a₀ ≤ a → b ≤ b₀ → a < b → (∀ x ∈ S, x ∉ Set.Icc a b) → V a = V b) (hjump : ∀ (a r b : R), a₀ ≤ a → b ≤ b₀ → a < r → r < b → r ∈ S → (∀ x ∈ S, x ∈ Set.Icc a b → x = r) → V a - V b = w r) (hab : a₀ < b₀) (ha : a₀ ∉ S) (hb : b₀ ∉ S) : V a₀ - V b₀ = ∑ x ∈ S with a₀ < x ∧ x < b₀, w x

Local changes at isolated events sum to the total change between two points outside the event set.