English
In the setting of 1D mean value theorem on a convex set, if the derivative is bounded by C in norm, then the function is C-Lipschitz on the set.
Русский
В одномерном смысле теоремы о средних на выпуклом множество, если производная ограничена нормой ≤ C, то функция Lipshitz с константой C на этом множестве.
LaTeX
$$$$ \|f(y) - f(x)\| ≤ C \|y - x\|, \quad x,y ∈ s, $$$$
Lean4
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function within
this set is bounded by `C`, then the function is `C`-Lipschitz. Version with `derivWithin` -/
theorem norm_image_sub_le_of_norm_derivWithin_le {C : ℝ} (hf : DifferentiableOn 𝕜 f s)
(bound : ∀ x ∈ s, ‖derivWithin f s 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_hasDerivWithin_le (fun x hx => (hf x hx).hasDerivWithinAt) bound xs ys
