norm_fderiv_le_of_lipschitz — Mathlib

English

If f is Lipschitz with constant C then the norm of its derivative at x0 is at most C.

Русский

Если f липшицево ограничено константой C, то норма производной в x0 не превосходит C.

LaTeX

$$$\|fderiv\,\, 𝕜\, f\, x_0\| \le C$ for LipschitzWith C f$$

Lean4

/-- Converse to the mean value inequality: if `f` is `C`-lipschitz then
its derivative at `x₀` has norm bounded by `C`.
Version using `fderiv`. -/
theorem norm_fderiv_le_of_lipschitz {f : E → F} {x₀ : E} {C : ℝ≥0} (hlip : LipschitzWith C f) : ‖fderiv 𝕜 f x₀‖ ≤ C :=
  norm_fderiv_le_of_lipschitzOn 𝕜 univ_mem (lipschitzOnWith_univ.2 hlip)

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