English
If f is differentiable on a convex set s and the derivative is uniformly bounded by C on s, then f is C-Lipschitz on s.
Русский
Если функция f дифференцируема на выпуклом множестве s и производная ограничена сверху константой C на s, то f является C-липшицевой на s.
LaTeX
$$$\text{If } f: E \to G,\ s \subset E \text{ convex},\ for\ x\in s: \ f \text{ differentiable at } x,\\ \forall x\in s: \|f'(x)\| \le C,\ Then\\ \forall x,y\in s:\ \|f(x)-f(y)\| \le C\|x-y\|.$$$
Lean4
/-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C` on
`s`, then the function is `C`-Lipschitz on `s`. Version with `fderiv` and `LipschitzOnWith`. -/
theorem lipschitzOnWith_of_nnnorm_fderiv_le {C : ℝ≥0} (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x)
(bound : ∀ x ∈ s, ‖fderiv 𝕜 f x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith C f s :=
hs.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivAt.hasFDerivWithinAt) bound
