English
Let F be a real or complex inner product space and x ∈ F. For f : F → 𝕜 and f' ∈ F, f has gradient f' at x precisely when f(x+h) = f(x) + ⟪f', h⟫ + o(∥h∥) as h → 0 in F. Equivalently, the error term f(x+h) − f(x) − ⟪f', h⟫ is little-o of ∥h∥ near h = 0.
Русский
Пусть F — комплексно или вещественно-векторное пространство с внутренним продуктом, x ∈ F. Для функции f : F → 𝕜 и вектора градиента f' ∈ F равен градиенту f в точке x тогда и только тогда, когда f(x+h) = f(x) + ⟨f', h⟩ + o(∥h∥) при h → 0. Эквивалентно ошибка f(x+h) − f(x) − ⟨f', h⟩ = o(∥h∥) при h → 0.
LaTeX
$$$\text{HasGradientAt}(f,f',x) \iff f(x+h) = f(x) + \langle f',h\rangle + o(\|h\|) \quad \text{as } h \to 0$$$
Lean4
theorem hasGradientAt_iff_isLittleO_nhds_zero :
HasGradientAt f f' x ↔ (fun h => f (x + h) - f x - ⟪f', h⟫) =o[𝓝 0] fun h => h :=
hasFDerivAt_iff_isLittleO_nhds_zero
