English
A variant of the monotone-on composition identity holds for an extended index set β, relating the variation of f∘φ on t to that of f on φ(t).
Русский
Расширенная версия тождества композиции для монотонной на t отображения сохраняет равенство вариаций.
LaTeX
$$variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)$$
Lean4
protected theorem add {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s)
(hc : c ∈ s) : variationOnFromTo f s a b + variationOnFromTo f s b c = variationOnFromTo f s a c :=
by
symm
refine additive_of_isTotal (· ≤ · : α → α → Prop) (variationOnFromTo f s) (· ∈ s) ?_ ?_ ha hb hc
· rintro x y _xs _ys
simp only [variationOnFromTo.eq_neg_swap f s y x, add_neg_cancel]
· rintro x y z xy yz xs ys zs
rw [variationOnFromTo.eq_of_le f s xy, variationOnFromTo.eq_of_le f s yz,
variationOnFromTo.eq_of_le f s (xy.trans yz), ← ENNReal.toReal_add (hf x y xs ys) (hf y z ys zs),
eVariationOn.Icc_add_Icc f xy yz ys]
