English
If f is Lipschitz with constant C on t, then composing with g on s gives eVariationOn of f ∘ g on s bounded by C times eVariationOn g on s.
Русский
Если f липшицево ограничена константой C на t, то композиция f ∘ g на s имеет вариацию, ограниченную C умножить на eVariationOn g на s.
LaTeX
$$eVariationOn (f ∘ g) s ≤ C * eVariationOn g s$$
Lean4
theorem comp_eVariationOn_le {f : E → F} {C : ℝ≥0} {t : Set E} (h : LipschitzOnWith C f t) {g : α → E} {s : Set α}
(hg : MapsTo g s t) : eVariationOn (f ∘ g) s ≤ C * eVariationOn g s :=
by
apply iSup_le _
rintro ⟨n, ⟨u, hu, us⟩⟩
calc
(∑ i ∈ Finset.range n, edist (f (g (u (i + 1)))) (f (g (u i)))) ≤
∑ i ∈ Finset.range n, C * edist (g (u (i + 1))) (g (u i)) :=
Finset.sum_le_sum fun i _ => h (hg (us _)) (hg (us _))
_ = C * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i)) := by rw [Finset.mul_sum]
_ ≤ C * eVariationOn g s := mul_le_mul_left' (eVariationOn.sum_le _ _ hu us) _
