English
For any i ≤ n, the i-th iterated derivative within s of g ∘ f equals g applied to the i-th iterated derivative within s of f.
Русский
Для любого i ≤ n i-я итерационная производная внутри s от g ∘ f равна применению g к i-й итерационной производной внутри s от f.
LaTeX
$$$\forall i\le n:\; \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^i(g\circ f)\,s\,x = g\circ\operatorname{iteratedFDerivWithin}_{\mathbb{K}}^i f\,s\,x$$$
Lean4
/-- The iterated derivative of the composition with a linear map on the left is
obtained by applying the linear map to the iterated derivative. -/
theorem iteratedFDeriv_comp_left {f : E → F} (g : F →L[𝕜] G) (hf : ContDiffAt 𝕜 n f x) {i : ℕ} (hi : i ≤ n) :
iteratedFDeriv 𝕜 i (g ∘ f) x = g.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x) :=
by
simp only [← iteratedFDerivWithin_univ]
exact g.iteratedFDerivWithin_comp_left hf.contDiffWithinAt uniqueDiffOn_univ (mem_univ x) hi
