hasFDerivWithinAt_iff_hasGradientWithinAt

English

Gradient exists iff the Fréchet derivative exists, with the gradient identified by the dual.

Русский

Градиент существует тогда и только тогда, когда существует Фреде- производная; градиент определяется через двойственный угол.

LaTeX

$$$ HasGradientAt f f' x \\iff HasFDerivAt f (toDual 𝕜 F f') x $$$

Lean4

theorem hasFDerivWithinAt_iff_hasGradientWithinAt {frechet : StrongDual 𝕜 F} {s : Set F} :
    HasFDerivWithinAt f frechet s x ↔ HasGradientWithinAt f ((toDual 𝕜 F).symm frechet) s x := by
  rw [hasGradientWithinAt_iff_hasFDerivWithinAt, (toDual 𝕜 F).apply_symm_apply frechet]

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