continuousMultilinear_apply_const

English

If c has derivative at x and u is fixed, the mapping y ↦ (c(y))(u) has a derivative given by the flip of c' evaluated at x acting on u.

Русский

Если c имеет производную в x и u зафиксировано, отображение y ↦ (c(y))(u) имеет производную, задаваемую fflip(c'(x)) на u.

LaTeX

$$$ HasStrictFDerivAt\left( \lambda y. (c(y))(u) \right) x = (f)\, $$$

Lean4

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

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