hasDerivAt_iff_isLittleO_nhds_zero

English

For a function f: 𝕜 → F, the derivative at x with value f' exists if and only if the error term f(x+h) − f(x) − h f' is little-o of h as h tends to 0.

Русский

Для функции f: 𝕜 → F предел дифференцируемости в точке x равен нулю, если и только если ошибка f(x+h) − f(x) − h f' является малым по отношению к h при h → 0.

LaTeX

$$$\text{HasDerivAt } f\; f'\; x \iff (f(x+h) - f(x) - h\cdot f') = o(h) \text{ as } h \to 0$$$

Lean4

theorem hasDerivAt_iff_isLittleO_nhds_zero :
    HasDerivAt f f' x ↔ (fun h => f (x + h) - f x - h • f') =o[𝓝 0] fun h => h :=
  hasFDerivAt_iff_isLittleO_nhds_zero

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