English
A variant of the partition sum: the sum of eVariationOn f over Icc blocks equals eVariationOn f over the whole interval defined by the end points.
Русский
Вариант суммирования по разбиениям: сумма по Icc-блокам равна вариации по всему отрезку.
LaTeX
$$$\forall f:α\to E,\; I: \mathbb{N}\to α,\; (Monotone I)\Rightarrow \sum_{i=0}^{n-1} eVariationOn f (Icc(I_i, I_{i+1})) = eVariationOn f (Icc(I_0, I_n))$$
Lean4
theorem sum (f : α → E) {s : Set α} {E : ℕ → α} (hE : Monotone E) {n : ℕ} (hn : ∀ i, 0 < i → i < n → E i ∈ s) :
∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n)) := by
induction n with
| zero => simp [eVariationOn.subsingleton f Subsingleton.inter_singleton]
| succ n ih =>
by_cases hn₀ : n = 0
· simp [hn₀]
rw [← Icc_add_Icc (b := E n)]
· rw [← ih (by intros; apply hn <;> omega)]
apply Finset.sum_range_succ
· apply hE; omega
· apply hE; omega
· apply hn <;> omega
