English
If c has strictly differentiable at x with derivative c' and u has strictly differentiable at x with derivative u', then the derivative of y ↦ c(y)(u(y)) at x is (c(x) ∘ u') + (c' flipped at u(x)).
Русский
Если c имеет строго дифференцируемость в точке x с производной c' и u имеет строго дифференцируемость в x с u', тогда производная функции 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'\text{ flip})\,(u(x))$$$
Lean4
@[fun_prop]
theorem clm_apply (hc : HasStrictFDerivAt c c' x) (hu : HasStrictFDerivAt u u' x) :
HasStrictFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x :=
(isBoundedBilinearMap_apply.hasStrictFDerivAt (c x, u x)).comp x (hc.prodMk hu)
