English
Let f, f' be as above. The Fréchet differentiability of f at x with derivative f' is equivalent to the remainder term f(x+h) − f(x) − f'(h) being little-o of h as h → 0, i.e., f(x+h) − f(x) − f'(h) = o(‖h‖) as h → 0.
Русский
Существование производной Фреше функции f в точке x с производной f' эквивалентно тому, что остаток f(x+h) − f(x) − f'(h) является малым-o по отношению к h при h → 0, то есть f(x+h) − f(x) − f'(h) = o(‖h‖) при h → 0.
LaTeX
$$$$\\text{HasFDerivAt } f\\,f'\\,x \\iff (f(x+h) - f(x) - f'(h)) = o_{\\mathcal{N}_0}(h)\\text{ as } h \\to 0,$$$$
Lean4
theorem hasFDerivAt_iff_isLittleO_nhds_zero :
HasFDerivAt f f' x ↔ (fun h : E => f (x + h) - f x - f' h) =o[𝓝 0] fun h => h :=
by
rw [HasFDerivAt, hasFDerivAtFilter_iff_isLittleO, ← map_add_left_nhds_zero x, isLittleO_map]
simp [Function.comp_def]
