English
The MF-derivative within s equals the composition of the outer and inner MF-derivatives within u and s, respectively, under appropriate unique differentiability conditions.
Русский
MF-производная внутри s равна композиции производных внутри u и s при подходящих условиях уникальной дифференциации.
LaTeX
$$$mfderivWithin I I'' (g \\circ f) s x = (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f s x)$$$
Lean4
theorem mfderiv_comp (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableAt I I' f x) :
mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x) :=
by
apply HasMFDerivAt.mfderiv
exact HasMFDerivAt.comp x hg.hasMFDerivAt hf.hasMFDerivAt
