Theorems · Theorem · global analysis

hasGradientAtFilter_iff_isLittleO

∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F},
  HasGradientAtFilter f f' x L ↔ (fun x' => f x' - f x - inner 𝕜 f' (x' - x)) =o[L] fun x' => x' - x

Defined in

Mathlib.Analysis.Calculus.Gradient.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace