English
If g is a continuous linear equivalence, and f is a function, then the iterated derivative within s of g ∘ f equals the derivative of f precomposed with g, etc.
Русский
Если g — непрерывное линейное эквивалентное отображение, то итеративная внутренняя производная слева преобразуется аналогично.
LaTeX
$$$\forall g:\, F \simeq F',\; \text{IteratedFDerivWithin}_{\mathbb{K}}^i(g\circ f) = g\circ \text{IteratedFDerivWithin}_{\mathbb{K}}^i f$$$
Lean4
/-- Iterated derivatives commute with left composition by continuous linear equivalences. -/
theorem iteratedFDeriv_comp_left {f : E → F} {x : E} (g : F ≃L[𝕜] G) {i : ℕ} :
iteratedFDeriv 𝕜 i (g ∘ f) x = g.toContinuousLinearMap.compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x) :=
by
simp only [← iteratedFDerivWithin_univ]
apply g.iteratedFDerivWithin_comp_left f uniqueDiffOn_univ trivial
