Theorems · Definition · global analysis

HasGradientAtFilter

{𝕜 : Type u_1} →
  {F : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup F] → [InnerProductSpace 𝕜 F] → [CompleteSpace F] → (F → 𝕜) → F → F → Filter F → Prop

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.

Defined in

Mathlib.Analysis.Calculus.Gradient.Basic

Cited by

10 results in Mathlib

Foundations

Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace