English
In dimension 1, on a convex set, if the derivative is bounded by C, then the function is C-Lipschitz on that set. More precisely, if HasDerivWithinAt f (f′(x)) s x holds for all x ∈ s and ‖f′(x)‖ ≤ C for all x ∈ s, then ‖f(y) − f(x)‖ ≤ C‖y − x‖ for all x,y ∈ s.
Русский
В одномерном случае на выпуклом множество если производная ограничена сверху коэффициентом C, то функция C-липшицова на этом множестве: для любых x,y ∈ s выполняется неравенство ‖f(y) − f(x)‖ ≤ C‖y − x‖.
LaTeX
$$$$ \|f(y) - f(x)\| \le C \|y - x\|, \quad x,y \in s, $$$$
Lean4
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
bounded by `C`, then the function is `C`-Lipschitz. Version with `HasDerivWithinAt`. -/
theorem norm_image_sub_le_of_norm_hasDerivWithin_le {C : ℝ} (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x)
(bound : ∀ x ∈ s, ‖f' x‖ ≤ C) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) : ‖f y - f x‖ ≤ C * ‖y - x‖ :=
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivWithinAt)
(fun x hx => le_trans (by simp) (bound x hx)) hs xs ys
