isBigO_sub — Mathlib

English

If f has Frechet derivative f' at x₀, then f(x)−f(x₀) is big-O of x−x₀ near x₀.

Русский

Если у f в точке x₀ существует Фреше-производная f', то f(x)−f(x₀) = O(x−x₀) около x₀.

LaTeX

$$HasFDerivAt f f' x₀ → Asymptotics.IsBigO (nhds x₀) (fun x => f x - f x₀) (fun x => x - x₀)$$

Lean4

nonrec theorem isBigO_sub {f : E → F} {x₀ : E} {f' : E →L[𝕜] F} (h : HasFDerivAt f f' x₀) :
    (f · - f x₀) =O[𝓝 x₀] (· - x₀) :=
  h.isBigO_sub

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