HasGradientAtFilter — Mathlib

English

The HasGradientWithinAt condition is equivalent to HasFDerivWithinAt, via the dual identification.

Русский

Условие HasGradientWithinAt эквивалентно HasFDerivWithinAt через двойственный тождественный образ.

LaTeX

$$$ HasGradientWithinAt f f' s x \\iff HasFDerivWithinAt f (toDual 𝕜 F f') s x $$$

Lean4

/-- A function `f` has the gradient `f'` as derivative along the filter `L` if
  `f x' = f x + ⟨f', x' - x⟩ + o (x' - x)` when `x'` converges along the filter `L`. -/
def HasGradientAtFilter (f : F → 𝕜) (f' x : F) (L : Filter F) :=
  HasFDerivAtFilter f (toDual 𝕜 F f') x L

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