English
Let E and F be normed spaces over a nontrivially normed field 𝕜. The map f : E → F is differentiable at x with derivative f' (a continuous linear map) if and only if f(x′) − f(x) − f′(x′ − x) is little-o of the norm of x′ − x as x′ → x; equivalently, lim_{h→0} ||f(x+h) − f(x) − f′h|| / ||h|| = 0.
Русский
Пусть E и F — нормированные пространства над нормированным полем 𝕜. Отображение f : E → F дифференцируемо в точке x с производной-f′ (переходящий линейный оператор) тогда и только тогда, когда f(x+h) − f(x) − f′h = o(||h||) при h → 0; эквивалентно lim_{h→0} ||f(x+h) − f(x) − f′h|| / ||h|| = 0.
LaTeX
$$$$\\text{There is a Fréchet derivative } f' \\text{ at } x \\iff \\lim_{h \\to 0} \\frac{\\|f(x+h) - f(x) - f'(h)\\|}{\\|h\\|} = 0.$$$$
Lean4
theorem hasFDerivAt_iff_tendsto :
HasFDerivAt f f' x ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝 x) (𝓝 0) :=
hasFDerivAtFilter_iff_tendsto
