English
For differentiable c and d in the setting, the derivative within s at x of y ↦ (c(y) ∘ d(y)) is the sum of two terms: left- and right-derivative contributions through c and d, respectively.
Русский
Для дифференцируемых c и d в рамках s: производная внутри s в точке x функции y ↦ c(y) ∘ d(y) равна сумме двух членов, отражающих вклад c и d.
LaTeX
$$$ f\,'_{s,x}(y) = (\mathrm{compL}_{\mathbb{K}}(F,G,H)(c x)) \circ f\,'_{s,x}(d) \, + \, ( (\mathrm{compL}_{\mathbb{K}}(F,G,H))^{\!} \mathrm{flip} (d x) ) \circ f\,'_{s,x}(c) $$$
Lean4
theorem fderivWithin_clm_comp (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x)
(hd : DifferentiableWithinAt 𝕜 d s x) :
fderivWithin 𝕜 (fun y => (c y).comp (d y)) s x =
(compL 𝕜 F G H (c x)).comp (fderivWithin 𝕜 d s x) + ((compL 𝕜 F G H).flip (d x)).comp (fderivWithin 𝕜 c s x) :=
(hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).fderivWithin hxs
