English
If a function f is differentiable everywhere and its derivative is uniformly bounded by C, then f is globally C-Lipschitz.
Русский
Если функция f дифференцируема на всей области и её производная по всей области ограничена сверху константой C, то f глобально C-липшицева.
LaTeX
$$$\text{If } f: E \to G \text{ is differentiable on all of } E\text{ and } \forall x:\|f'(x)\| \le C,\ then\\ \forall x,y:\ \|f(x)-f(y)\| \le C\|x-y\|.$$$
Lean4
/-- The mean value theorem: if the derivative of a function is bounded by `C`, then the function is
`C`-Lipschitz. Version with `fderiv` and `LipschitzWith`. -/
theorem _root_.lipschitzWith_of_nnnorm_fderiv_le {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → G}
{C : ℝ≥0} (hf : Differentiable 𝕜 f) (bound : ∀ x, ‖fderiv 𝕜 f x‖₊ ≤ C) : LipschitzWith C f :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
let A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
rw [← lipschitzOnWith_univ]
exact lipschitzOnWith_of_nnnorm_fderiv_le (fun x _ ↦ hf x) (fun x _ ↦ bound x) convex_univ
