fderiv_continuousMultilinear_apply_const

English

If c is strictly differentiable at x with derivative c', and u is a fixed finite-index family, then the map y ↦ (c(y)) u is strictly differentiable at x with derivative c'.flipMultilinear u.

Русский

Если c строго дифференцируема в x с производной c', а фиксировано задано множество индексов u, то f(y)=(c(y))u имеет строгую дифференцируемость в x с производной c'.flipMultilinear u.

LaTeX

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

Lean4

theorem fderiv_continuousMultilinear_apply_const (hc : DifferentiableAt 𝕜 c x) (u : ∀ i, M i) :
    (fderiv 𝕜 (fun y ↦ (c y) u) x) = (fderiv 𝕜 c x).flipMultilinear u :=
  (hc.hasFDerivAt.continuousMultilinear_apply_const u).fderiv

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