English
If on a convex set s, a function has derivative whose nn-norm is bounded by C (C ∈ ℝ≥0), then the function is Lipschitz with constant C on s, in the nn-norm sense.
Русский
На выпуклом множестве s производная имеет норму nnnorm ≤ C, следовательно функция сант Lipschitz с константой C на s.
LaTeX
$$$$ \\|f(y) - f(x)\\|_{+} \\le C \\|y - x\\|, \\quad x,y \\in s, \\ C \\in ℝ_{≥0}, $$$$
Lean4
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
bounded by `C` on `s`, then the function is `C`-Lipschitz on `s`.
Version with `HasDerivWithinAt` and `LipschitzOnWith`. -/
theorem lipschitzOnWith_of_nnnorm_hasDerivWithin_le {C : ℝ≥0} (hs : Convex ℝ s)
(hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C) : LipschitzOnWith C f s :=
Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivWithinAt)
(fun x hx => le_trans (by simp) (bound x hx)) hs
