continuousMultilinear_apply_const

English

If c has derivative within s at x and u has derivative within s at x, then the map y ↦ (c(y))(u(y)) has a derivative within s at x with value (c x) ∘ u' + c'.flip(u x).

Русский

Если c имеет производную внутри s в x и u имеет производную внутри s в x, тогда f(y)=c(y)(u(y)) имеет производную внутри s в x, равную (c x) ∘ u' + c'.flip(u x).

LaTeX

$$$ HasFDerivWithinAt\left( y \mapsto (c(y))(u(y)) \right) s x = ( (c x) \circ u' ) + ( c' \flip )(u x)$$$

Lean4

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

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