English
If c has derivative c' at x and u has derivative u' at x, then the map y ↦ c(y)(u(y)) has derivative at x equal to (c(x) ∘ u') + (c' flipped at u(x)).
Русский
Если c имеет производную в точке x и u имеет производную в точке x, тогда y ↦ c(y)(u(y)) имеет производную в x равную (c(x) ∘ u') + (c' flipped (u(x))).
LaTeX
$$$ HasFDerivAt\left( y \mapsto (c(y))(u(y)) \right)\ x = (c(x) \circ u') + (c'\ flip)(u(x))$$$
Lean4
@[fun_prop]
theorem clm_apply (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :
HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x := by
-- `by exact` to solve unification issues.
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp x (hc.prodMk hu)
