Theorems · Definition · global analysis

gradient

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

Gradient of f at the point x, if it exists. Zero otherwise. Denoted as ∇ within the Gradient namespace. If the derivative exists (i.e., ∃ f', HasGradientAt f f' x), then f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x.

Defined in

Mathlib.Analysis.Calculus.Gradient.Basic

Cited by

19 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace