hasGradientWithinAt_iff_isLittleO

English

hasGradientAt_iff_isLittleO: HasGradientAt f f' x iff the Little-O condition with the linearization holds at x.

Русский

Условие Малого О для линейной аппроксимации в точке эквивалентно существованию градиента.

LaTeX

$$$\\text{HasGradientAt } f f' x \\iff (f(x')-f(x)-⟪f',x'-x⟫) =o[𝓝 x]\\; (x'\\to x)$$$

Lean4

theorem hasGradientWithinAt_iff_isLittleO :
    HasGradientWithinAt f f' s x ↔ (fun x' : F => f x' - f x - ⟪f', x' - x⟫) =o[𝓝[s] x] fun x' => x' - x :=
  hasGradientAtFilter_iff_isLittleO

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