hasFDerivAt_iff_hasGradientAt — Mathlib

English

If f is differentiable at x, then HasGradientAt f (∇f x) x holds.

Русский

Если f дифференцируема в x, тогда выполняется HasGradientAt f (∇f x) x.

LaTeX

$$$ \\text{DifferentiableAt } 𝕜 f x \\Rightarrow HasGradientAt f (\\nabla f x) x $$$

Lean4

theorem hasFDerivAt_iff_hasGradientAt {frechet : StrongDual 𝕜 F} :
    HasFDerivAt f frechet x ↔ HasGradientAt f ((toDual 𝕜 F).symm frechet) x := by
  rw [hasGradientAt_iff_hasFDerivAt, (toDual 𝕜 F).apply_symm_apply frechet]

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