fderiv_continuousMultilinear_apply_const_apply

English

Application of a fixed multilinear map to a fixed vector commutes with taking strict Fréchet derivatives.

Русский

Применение фиксированного мультиляйнерного отображения к фиксированному вектору коммутирует с вычислением строгой Фрéш-дифференцирования.

LaTeX

$$$ HasStrictFDerivAt\left( y \mapsto (c(y)) u \right) x = c'.flipMultilinear(u)$$$

Lean4

/-- Application of a `ContinuousMultilinearMap` to a constant commutes with `fderiv`. -/
theorem fderiv_continuousMultilinear_apply_const_apply (hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) (m : E) :
    (fderiv 𝕜 (fun y ↦ (c y) u) x) m = (fderiv 𝕜 c x) m u := by simp [fderiv_continuousMultilinear_apply_const hc]

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