hasGradientAt_iff_tendsto — Mathlib

English

hasGradientWithinAt_iff_tendsto: HasGradientWithinAt f f' s x iff a certain Tendsto condition to 0 holds.

Русский

Градиент внутри эквивалентен тому, что нормируемая ошибка стремится к нулю.

LaTeX

$$$\\text{HasGradientWithinAt } f f' s x \\iff \\ Tendsto (\\lambda x' . \\|x'-x\\|^{-1} \\|f(x')-f(x)-⟪f',x'-x⟫\\|) (\\nhdsWithin x s) (\\nhds 0)$$$

Lean4

theorem hasGradientAt_iff_tendsto :
    HasGradientAt f f' x ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - ⟪f', x' - x⟫‖) (𝓝 x) (𝓝 0) :=
  hasFDerivAtFilter_iff_tendsto

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