hasGradientAtFilter — Mathlib

English

From HasGradientAt g g' u we obtain HasDerivAt g (starRingEnd 𝕜 g') u.

Русский

Из градиента функции g выводится производная в точке u через соответствующий эндоморфизм.

LaTeX

$$$\\text{HasGradientAt } g g' u \\Rightarrow \\text{HasDerivAt } g (\\starRingEnd 𝕜\\ g')\\ u$$$

Lean4

theorem hasGradientAtFilter (h : HasDerivAtFilter g g' u L') : HasGradientAtFilter g (starRingEnd 𝕜 g') u L' :=
  by
  have : ContinuousLinearMap.smulRight (1 : 𝕜 →L[𝕜] 𝕜) g' = (toDual 𝕜 𝕜) (starRingEnd 𝕜 g') := by ext; simp
  rwa [HasGradientAtFilter, ← this]

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