English
The iterated derivative within a set of a composition f ∘ g is obtained by composing the derivative within by g.
Русский
Итеративная производная внутри множества композиции f ∘ g получается путем композиции внутри производной f по g.
LaTeX
$$$\text{iteratedFDerivWithin}_{\mathbb{K}}^i (f\circ g) (g^{-1}'s) x = (\text{iteratedFDerivWithin}_{\mathbb{K}}^i f s (g x)).comp\text{ContinuousLinearMap} g$$$
Lean4
/-- The iterated derivative of the composition with a linear map on the right is
obtained by composing the iterated derivative with the linear map. -/
theorem iteratedFDeriv_comp_right (g : G →L[𝕜] E) {f : E → F} (hf : ContDiff 𝕜 n f) (x : G) {i : ℕ} (hi : i ≤ n) :
iteratedFDeriv 𝕜 i (f ∘ g) x = (iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap fun _ => g :=
by
simp only [← iteratedFDerivWithin_univ]
exact g.iteratedFDerivWithin_comp_right hf.contDiffOn uniqueDiffOn_univ uniqueDiffOn_univ (mem_univ _) hi
