English
On a convex set, if the derivative is bounded by C, then the function is C-Lipschitz on that set.
Русский
На выпуклом множестве, если производная ограничена сверху C, то функция C-Липшицева на этом множестве.
LaTeX
$$$\text{If } s\subset E \text{ convex and } \|f'(x)\| ≤ C \text{ for all } x∈s,\; f \text{ is LipschitzOnWith } C \text{ on } s.$$$
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 `HasFDerivWithinAt` and
`LipschitzOnWith`. -/
theorem lipschitzOnWith_of_nnnorm_hasFDerivWithin_le {C : ℝ≥0} (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
(bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith C f s :=
by
rw [lipschitzOnWith_iff_norm_sub_le]
intro x x_in y y_in
exact hs.norm_image_sub_le_of_norm_hasFDerivWithin_le hf bound y_in x_in
