hasDerivAt_iff_isLittleO — Mathlib

English

HasDerivWithinAt f f' s x is equivalent to a Tendsto condition of the normalized error to 0 along nhdsWithin x s.

Русский

HasDerivWithinAt эквивалентно условию, что нормированная ошибка стремится к нулю вдоль nhdsWithin x s.

LaTeX

$$$\\mathrm{HasDerivWithinAt}(f,f',s,x) \\iff \\mathrm{Tendsto}\\left( \\lambda x' \\;\\rightarrow\\; \\|x' - x\\|^{-1} \\cdot \\|f x' - f x - (x' - x) \\cdot f'\\| \\right) (\\mathcal{N}[s] x) (\\mathcal{N} 0\\,).$$$

Lean4

theorem hasDerivAt_iff_isLittleO :
    HasDerivAt f f' x ↔ (fun x' : 𝕜 => f x' - f x - (x' - x) • f') =o[𝓝 x] fun x' => x' - x :=
  hasFDerivAtFilter_iff_isLittleO ..

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