exists_lipschitzOnWith_of_nnnorm_lt

English

If f is C^1 at x and ‖fderiv x‖ < K, then f is K-Lipschitz in a neighborhood of x.

Русский

Если функция C^1 в точке x и ‖fderiv x‖ < K, то функция локально Lipschitz с константой K около x.

LaTeX

$$$ContDiffAt\\ 𝕂\\ 1 f x \\Rightarrow ∃ t ∈ 𝓝 x, LipschitzOnWith K f t$ where $‖fderiv f x‖₊ < K$$$

Lean4

/-- If `f` is `C^1` at `x` and `K > ‖fderiv 𝕂 f x‖`, then `f` is `K`-Lipschitz in a neighborhood of
`x`. -/
theorem exists_lipschitzOnWith_of_nnnorm_lt {f : E' → F'} {x : E'} (hf : ContDiffAt 𝕂 1 f x) (K : ℝ≥0)
    (hK : ‖fderiv 𝕂 f x‖₊ < K) : ∃ t ∈ 𝓝 x, LipschitzOnWith K f t :=
  (hf.hasStrictFDerivAt le_rfl).exists_lipschitzOnWith_of_nnnorm_lt K hK

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