hasFDerivAtFilter_iff_isLittleO — Mathlib

English

A strict Fréchet derivative at x is equivalent to a little-o condition for the difference quotient with respect to the product space.

Русский

Строгий производный Фреше в точке x эквивалентен условию малого o для разности разностей на произведении пространств.

LaTeX

$$$\text{HasStrictFDerivAt } f f' x \iff \text{IsLittleO } (nhds \{(x, x)\}) (f(x')-f(x)-f'(x'-x)) (x'-x)$$$

Lean4

theorem hasFDerivAtFilter_iff_isLittleO {L : Filter E} :
    HasFDerivAtFilter f f' x L ↔ (fun x' => f x' - f x - f' (x' - x)) =o[L] fun x' => x' - x :=
  (hasFDerivAtFilter_iff_isLittleOTVS ..).trans isLittleOTVS_iff_isLittleO

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