English
Let E and F be normed spaces over a nontrivial normed field, and f : E → F. For a point x ∈ E and a subset s ⊆ E, f has a Fréchet derivative f' at x within s if and only if the limit of the remainder divided by the distance to x tends to 0 when approaching x through s, i.e. the expression ‖x′ − x‖⁻¹‖f(x′) − f(x) − f′(x′ − x)‖ tends to 0 as x′ → x with x′ ∈ s.
Русский
Пусть E, F — нормированные пространства над поля 𝕜, не равного нулю; пусть f : E → F. Пусть x ∈ E и s ⊆ E. Тогда f имеет производную Фреше внутри s в точке x, если и только если предел остатка при делении на расстояние к x стремится к нулю при подходе к x по s, т.е. выражение ‖x′ − x‖⁻¹‖f(x′) − f(x) − f′(x′ − x)‖ стремится к 0 при x′ → x и x′ ∈ s.
LaTeX
$$$HasFDerivWithinAt\ f\ f'\ s\ x \;\Longleftrightarrow\; \ \lim_{x'\to x,\ x'\in s} \frac{\|f(x') - f(x) - f'(x' - x)\|}{\|x' - x\|} = 0$$$
Lean4
theorem hasFDerivWithinAt_iff_tendsto :
HasFDerivWithinAt f f' s x ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) (𝓝[s] x) (𝓝 0) :=
hasFDerivAtFilter_iff_tendsto
