continuousMultilinear_apply_const

English

If c is differentiable at x with derivative c' and u is a fixed index-valued family, then the map y ↦ (c(y))u is differentiable with derivative given by the standard action of c' on u.

Русский

Если c дифференцируема в x с производной c' и u задано константно, тогда y ↦ (c(y))u дифференцируема, а производная задаётся действием c' на u.

LaTeX

$$$ HasStrictFDerivAt\left( y \mapsto (c(y))(u) \right) x = c' \text{(apply)}(u) + (c x) \circ 0$$$

Lean4

@[fun_prop]
theorem continuousMultilinear_apply_const (hc : HasStrictFDerivAt c c' x) (u : ∀ i, M i) :
    HasStrictFDerivAt (fun y ↦ (c y) u) (c'.flipMultilinear u) x :=
  (ContinuousMultilinearMap.apply 𝕜 M H u).hasStrictFDerivAt.comp x hc

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