lipschitzOnWith_of_nnnorm_deriv_le

English

If on a convex set s, the derivative (within) has bounded norm in NNReal by C, then LipschitzOnWith C f s.

Русский

Если на выпуклом s производная внутри имеет ограничение в NNReal на C, то LipschitzOnWith C f s.

LaTeX

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

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