English
If HasFTaylorSeriesUpToOn n f p s holds and g is linear, then HasFTaylorSeriesUpToOn n (g ∘ f) (g ∘ p) s holds with the k-th term adjusted by g.
Русский
Если есть ряд Тейлора для f и линейный g, то имеется ряд Тейлора для g ∘ f с коэффициентами, получаемымиApplying g к p_k.
LaTeX
$$$ g \text{ linear }, hf : HasFTaylorSeriesUpToOn\ n\ f\ p\ s \Rightarrow HasFTaylorSeriesUpToOn n (g \circ f) (\lambda x k. g \circ p x k) s $$$
Lean4
/-- Composition by continuous linear maps on the left preserves `C^n` functions in a domain
at a point. -/
theorem continuousLinearMap_comp (g : F →L[𝕜] G) (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (g ∘ f) s x :=
by
match n with
| ω =>
obtain ⟨u, hu, p, hp, h'p⟩ := hf
refine ⟨u, hu, _, hp.continuousLinearMap_comp g, fun i ↦ ?_⟩
change
AnalyticOn 𝕜 (fun x ↦ (ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun _ : Fin i ↦ E) F G g) (p x i)) u
apply AnalyticOnNhd.comp_analyticOn _ (h'p i) (Set.mapsTo_univ _ _)
exact ContinuousLinearMap.analyticOnNhd _ _
| (n : ℕ∞) =>
intro m hm
rcases hf m hm with ⟨u, hu, p, hp⟩
exact ⟨u, hu, _, hp.continuousLinearMap_comp g⟩
