norm_deriv_le_of_lipschitzOn — Mathlib

English

If f is Lipschitz with constant C, then ||deriv f x0|| ≤ C.

Русский

Если f липшицева с константой C, то ||deriv f x0|| ≤ C.

LaTeX

$$$\\|\\operatorname{deriv}f(x_0)\\| \\le C$ for LipschitzWith C f$$

Lean4

/-- Converse to the mean value inequality: if `f` is `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`.
Version using `deriv`. -/
theorem norm_deriv_le_of_lipschitzOn {f : 𝕜 → F} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0}
    (hlip : LipschitzOnWith C f s) : ‖deriv f x₀‖ ≤ C := by
  simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitzOn 𝕜 hs hlip

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