English
If c and d are pointwise differentiable linear maps, then the function y ↦ c(y) ∘ d(y) has a derivative given by the sum of two composed derivatives: (compL(c x)) ∘ d' + (flip(d x)) ∘ c'.
Русский
Если c и d — дифференцируемые линейные отображения, то y ↦ c(y) ∘ d(y) имеет производную, равную сумме двух композиции производных: (compL(c x) ∘ d') + ((compL ...).flip (d x)) ∘ c'.
LaTeX
$$$$ \text{HasStrictFDerivAt } c c' x \to \text{HasStrictFDerivAt } d d' x \to \\ HasStrictFDerivAt \ (\lambda y \mapsto (c(y) \circ d(y)))\ x \;\text{with derivative }\ ((compL\ 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c'). $$$$
Lean4
@[fun_prop]
theorem clm_comp (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
HasStrictFDerivAt (fun y => (c y).comp (d y)) ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c')
x :=
(isBoundedBilinearMap_comp.hasStrictFDerivAt (c x, d x)).comp x (hc.prodMk hd)
