comp_locallyBoundedVariationOn — Mathlib

English

If f is C-Lipschitz on t, g maps s into t, and g has locally bounded variation on s, then f∘g has locally bounded variation on s.

Русский

Если f является C-липшицевой на t, g отображает s в t и g имеет локально ограниченную вариацию на s, тогда f ∘ g имеет локально ограниченную вариацию на s.

LaTeX

$$$ (LipschitzOnWith\ C\ f\ t) \land (MapsTo\ g\ s\ t) \land (LocallyBoundedVariationOn\ g\ s) \Rightarrow LocallyBoundedVariationOn\ (f \circ g)\ s $$$

Lean4

theorem comp_locallyBoundedVariationOn {f : E → F} {C : ℝ≥0} {t : Set E} (hf : LipschitzOnWith C f t) {g : α → E}
    {s : Set α} (hg : MapsTo g s t) (h : LocallyBoundedVariationOn g s) : LocallyBoundedVariationOn (f ∘ g) s :=
  fun x y xs ys => hf.comp_boundedVariationOn (hg.mono_left inter_subset_left) (h x y xs ys)

Похожие утверждения