English
If f has a Taylor series up to order n on s, composing with a linear map g produces a Taylor series for f ∘ g on g⁻¹(s) with coefficients appropriately transformed by g.
Русский
Если f имеет ряд Тейлора до n на s, композиция с линейным отображением g имеет ряд Тейлора для f ∘ g на g⁻¹(s) с коэффициентами, преобразованными g.
LaTeX
$$$\text{HasFTaylorSeriesUpToOn}_{n} f p s \Rightarrow \text{HasFTaylorSeriesUpToOn}_{n} (f\circ g) (g^{-1}'s) $$$
Lean4
/-- The iterated derivative within a set of the composition with a linear map on the right is
obtained by composing the iterated derivative with the linear map. -/
theorem iteratedFDerivWithin_comp_right {f : E → F} (g : G →L[𝕜] E) (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s)
(h's : UniqueDiffOn 𝕜 (g ⁻¹' s)) {x : G} (hx : g x ∈ s) {i : ℕ} (hi : i ≤ n) :
iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
(iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g :=
((((hf.of_le hi).ftaylorSeriesWithin hs).compContinuousLinearMap g).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl h's
hx).symm
