fderiv_clm_apply — Mathlib

English

If c has derivative c' at x and u has derivative u' at x, then the map y ↦ c(y)(u(y)) is differentiable at x with derivative (c x) ∘ u' + (c' flipped)(u x).

Русский

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

LaTeX

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

Lean4

theorem fderiv_clm_apply (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :
    fderiv 𝕜 (fun y => (c y) (u y)) x = (c x).comp (fderiv 𝕜 u x) + (fderiv 𝕜 c x).flip (u x) :=
  (hc.hasFDerivAt.clm_apply hu.hasFDerivAt).fderiv

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