English
Another form of the composition invariance for monotone φ on t, relating V(f∘φ) and V(f).
Русский
Еще одно представление инвариантности композиции для монотонного φ на t, связывающее вариацию V(f∘φ) и V(f).
LaTeX
$$variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)$$
Lean4
protected theorem sub_self_monotoneOn {f : α → ℝ} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α}
(as : a ∈ s) : MonotoneOn (variationOnFromTo f s a - f) s :=
by
rintro b bs c cs bc
rw [Pi.sub_apply, Pi.sub_apply, le_sub_iff_add_le, add_comm_sub, ← le_sub_iff_add_le']
calc
f c - f b ≤ |f c - f b| := le_abs_self _
_ = dist (f b) (f c) := by rw [dist_comm, Real.dist_eq]
_ ≤ variationOnFromTo f s b c :=
by
rw [variationOnFromTo.eq_of_le f s bc, dist_edist]
apply ENNReal.toReal_mono (hf b c bs cs)
apply eVariationOn.edist_le f
exacts [⟨bs, le_rfl, bc⟩, ⟨cs, bc, le_rfl⟩]
_ = variationOnFromTo f s a c - variationOnFromTo f s a b := by
rw [← variationOnFromTo.add hf as bs cs, add_sub_cancel_left]
