hasDerivAtFilter_iff_tendsto — Mathlib

English

HasDerivAtFilter f f' x L is equivalent to the Tendsto condition of a normalized error term to 0 as x'→ along L.

Русский

HasDerivAtFilter эквивалентно условию, что нормированная ошибка стремится к 0 по L.

LaTeX

$$$\\mathrm{HasDerivAtFilter}(f,f',x,L) \\iff \\mathrm{Tendsto}\\left( \\lambda x' . \\|x' - x\\|^{-1} \\cdot \\|f x' - f x - (x' - x) \\cdot f'\\| \\right)\\; L \\; (\\mathsf{nhds} 0).$$$

Lean4

theorem hasDerivAtFilter_iff_tendsto :
    HasDerivAtFilter f f' x L ↔ Tendsto (fun x' : 𝕜 => ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) L (𝓝 0) :=
  hasFDerivAtFilter_iff_tendsto

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