English
A generalization: on convex sets, a derivative bound implies Lipschitz continuity with the corresponding constant.
Русский
Обобщение: на выпуклых множествах ограничение по производной влечет за собой липшицевость с соответствующей константой.
LaTeX
$$$\text{Convex Real } s \Rightarrow\; (\text{DifferentiableOn } f\ s) \Rightarrow \text{LipschitzOnWith } C f s$$$
Lean4
/-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C`,
then the function is `C`-Lipschitz. Version with `fderiv`. -/
theorem norm_image_sub_le_of_norm_fderiv_le (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x) (bound : ∀ x ∈ s, ‖fderiv 𝕜 f x‖ ≤ C)
(hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) : ‖f y - f x‖ ≤ C * ‖y - x‖ :=
hs.norm_image_sub_le_of_norm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivAt.hasFDerivWithinAt) bound xs ys
