English
For a differentiable-on-s function with bound on the derivative’s norm, the inequality ‖f(y) − f(x)‖ ≤ ‖f′‖∞‖y − x‖ holds for x,y ∈ s.
Русский
Для дифференцируемой на s функции с ограниченной нормой производной выполняется неравенство ‖f(y) − f(x)‖ ≤ ‖f′‖∞‖y − x‖ для x,y∈s.
LaTeX
$$$$ \|f(y) - f(x)\| ≤ \|\mathrm{deriv}\ f\|_{∞,s} \cdot \|y - x\|, \quad x,y ∈ s, $$$$
Lean4
/-- The mean value theorem set in dimension 1: if the derivative of a function is bounded by `C`,
then the function is `C`-Lipschitz. Version with `deriv` and `LipschitzWith`. -/
theorem _root_.lipschitzWith_of_nnnorm_deriv_le {C : ℝ≥0} (hf : Differentiable 𝕜 f) (bound : ∀ x, ‖deriv f x‖₊ ≤ C) :
LipschitzWith C f :=
lipschitzOnWith_univ.1 <| convex_univ.lipschitzOnWith_of_nnnorm_deriv_le (fun x _ => hf x) fun x _ => bound x
