English
If f has a Taylor series up to order n on s, and g is a continuous linear map, then f ∘ g has a Taylor series on g⁻¹(s) given by composing the coefficients with g.
Русский
Если у f есть ряд Тейлора до степени n на s, то f ∘ g имеет ряд Тейлора на g⁻¹(s), где коэффициенты получаются путём применения g к аргументам.
LaTeX
$$$\text{HasFTaylorSeriesUpToOn}_{n} f\ p\ s \quad \Rightarrow \quad \text{HasFTaylorSeriesUpToOn}_{n} (f\circ g)\ (g^{-1} s)\ (x) \text{ с коэффициентами } (p(gx))$$$
Lean4
/-- Composition by continuous linear equivs on the left respects higher differentiability at a
point in a domain. -/
theorem comp_contDiffWithinAt_iff (e : F ≃L[𝕜] G) : ContDiffWithinAt 𝕜 n (e ∘ f) s x ↔ ContDiffWithinAt 𝕜 n f s x :=
⟨fun H => by
simpa only [Function.comp_def, e.symm.coe_coe, e.symm_apply_apply] using
H.continuousLinearMap_comp (e.symm : G →L[𝕜] F),
fun H => H.continuousLinearMap_comp (e : F →L[𝕜] G)⟩
