lipschitzOnWith_of_nnnorm_fderivWithin_le

English

On convex s, if f is differentiable with derivative bounded by C, then the norm of f(y)-f(x) is ≤ C times norm(y-x).

Русский

На выпуклом s, если производная ограничена C, то нормa разности значений не больше C умножить на норму разности аргументов.

LaTeX

$$$\forall x,y\in s, \|f(y)-f(x)\| ≤ C \|y-x\|$$$

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 `fderivWithin` and
`LipschitzOnWith`. -/
theorem lipschitzOnWith_of_nnnorm_fderivWithin_le {C : ℝ≥0} (hf : DifferentiableOn 𝕜 f s)
    (bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖₊ ≤ C) (hs : Convex ℝ s) : LipschitzOnWith C f s :=
  hs.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivWithinAt) bound

Похожие утверждения