lipschitzOnWith_of_nnnorm_derivWithin_le

English

If on a convex set s, a function is differentiable and its derivative is bounded by C in norm, then the function is C-Lipschitz on s.

Русский

Если на выпуклом множестве s функция дифференцируема и её производная ограничена по норме C, то функция Lipschitz с константой C на s.

LaTeX

$$$$ \|f(y) - f(x)\| ≤ C \|y - x\|, \quad x,y ∈ s, \ C ≥ 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 `derivWithin` and `LipschitzOnWith`. -/
theorem lipschitzOnWith_of_nnnorm_derivWithin_le {C : ℝ≥0} (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s)
    (bound : ∀ x ∈ s, ‖derivWithin f s x‖₊ ≤ C) : LipschitzOnWith C f s :=
  hs.lipschitzOnWith_of_nnnorm_hasDerivWithin_le (fun x hx => (hf x hx).hasDerivWithinAt) bound

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