lipschitz_sub — Mathlib

English

If a function approximately linear on s with a bound c, then the map x ↦ f x − f′ x is Lipschitz on s with a Lipschitz constant depending on c and ‖f′‖.

Русский

Если функция аппроксимируется линейной на s с ограничением c, то карта x ↦ f x − f′ x на s является Липшицевой с константой, зависящей от c и ‖f′‖.

LaTeX

$$hf : ApproximatesLinearOn f f' s c → LipschitzWith (‖f'‖₊ + c) (s.restrict f)$$

Lean4

theorem lipschitz_sub (hf : ApproximatesLinearOn f f' s c) : LipschitzWith c fun x : s => f x - f' x :=
  hf.lipschitzOnWith.to_restrict

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