English
Derivation within a composition with scalar restriction obeys a simple chain rule form.
Русский
Производная внутри композиции с ограничением скаляров следует правилу подобного касательного отношения.
LaTeX
$$$$ fderivWithin_𝕜 (\text{restrictScalars } 𝕜 \circ φ) s x = (\text{restrictScalars } 𝕜) (fderivWithin_{𝕜'} φ s x) \text{ restrictScalars } 𝕜.$$$$
Lean4
/-- Derivation rule for compositions of scalar restriction with continuous multilinear maps. -/
theorem fderivWithin_restrictScalars_comp {φ : E → (ContinuousMultilinearMap 𝕜' (fun _ : Fin n ↦ E) F)}
(h : DifferentiableWithinAt 𝕜' φ s x) (hs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 ((restrictScalars 𝕜) ∘ φ) s x = (restrictScalars 𝕜) ∘ ((fderivWithin 𝕜' φ s x).restrictScalars 𝕜) :=
by
simp only [← restrictScalarsLinear_apply]
rw [fderiv_comp_fderivWithin _ (by fun_prop) (h.restrictScalars 𝕜) hs, ContinuousLinearMap.fderiv]
ext a b
simp [h.restrictScalars_fderivWithin 𝕜 hs]
