isBigO_sub — Mathlib

English

If f has a Frechet derivative f' within s at x₀, then the difference f(x)−f(x₀) is little-o of x−x₀ within s.

Русский

Если для функции f внутри множества s в точке x₀ существует производная Фреше f', тогда разность f(x)−f(x₀) является little-o по отношению к x−x₀ внутри s.

LaTeX

$$HasFDerivWithinAt f f' s x₀ → Asymptotics.IsBigO (nhdsWithin x₀ s) (fun x => f x - f x₀) (fun x => x - x₀)$$

Lean4

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

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