English
If c and d have strict derivatives at x, then the derivative of y ↦ (c(y) ∘ d(y)) is the sum of two compositions as above, in the strictly differentiable sense.
Русский
Если c и d имеют строгие производные в x, то производная функции y ↦ c(y) ∘ d(y) равна сумме двух композиционных производных в строгом смысле.
LaTeX
$$$$ \text{HasStrictFDerivAt } c c' x \to \text{HasStrictFDerivAt } d d' x \to \\ \text{HasStrictFDerivAt } (\lambda y \mapsto (c y).comp (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 : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
HasFDerivWithinAt (fun y => (c y).comp (d y)) ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c')
s x :=
by
-- `by exact` to solve unification issues.
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x)).comp_hasFDerivWithinAt x (hc.prodMk hd)
