Theorems · Definition · global analysis

gradientWithin

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

Gradient of f at the point x within the set s, if it exists. Zero otherwise. If the derivative exists (i.e., ∃ f', HasGradientWithinAt f f' s x), then f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x inside s.

Defined in

Mathlib.Analysis.Calculus.Gradient.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace