English
The MF-derivative within s composes as the MF-derivative of the outer map after the MF-derivative of the inner map.
Русский
MF-производная внутри 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 mfderivWithin_comp_of_preimage_mem_nhdsWithin (hg : MDifferentiableWithinAt I' I'' g u (f x))
(hf : MDifferentiableWithinAt I I' f s x) (h : f ⁻¹' u ∈ 𝓝[s] x) (hxs : UniqueMDiffWithinAt I s x) :
mfderivWithin I I'' (g ∘ f) s x = (mfderivWithin I' I'' g u (f x)).comp (mfderivWithin I I' f s x) :=
by
have A : s ∩ f ⁻¹' u ∈ 𝓝[s] x := Filter.inter_mem self_mem_nhdsWithin h
have B : mfderivWithin I I'' (g ∘ f) s x = mfderivWithin I I'' (g ∘ f) (s ∩ f ⁻¹' u) x :=
by
apply MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin _ hxs A
exact hg.comp _ (hf.mono inter_subset_left) inter_subset_right
have C : mfderivWithin I I' f s x = mfderivWithin I I' f (s ∩ f ⁻¹' u) x :=
MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin (hf.mono inter_subset_left) hxs A
rw [B, C]
exact mfderivWithin_comp _ hg (hf.mono inter_subset_left) inter_subset_right (hxs.inter' h)
