hasGradientAtFilter_iff_isLittleO

English

hasGradientAtFilter_iff_isLittleO: HasGradientAtFilter f f' x L iff the Little-O condition relative to the linear approximation holds.

Русский

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

LaTeX

$$$\\text{HasGradientAtFilter } f f' x L \\iff \\IsLittleO_L\\big( f(x')-f(x)-⟪f',x'-x⟫ \\big)\\;\\text{ w.r.t. } x'$$$

Lean4

theorem hasGradientAtFilter_iff_isLittleO :
    HasGradientAtFilter f f' x L ↔ (fun x' : F => f x' - f x - ⟪f', x' - x⟫) =o[L] fun x' => x' - x :=
  hasFDerivAtFilter_iff_isLittleO ..

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