English
If f has a Taylor series UpToOn n with p, and g is a linear map, then g ∘ f has a Taylor series with coefficients g ∘ p_k.
Русский
Если f имеет ряд Тейлора вплоть до порядка n с p, и g линейно, то g ∘ f имеет ряд Тейлора с коэффициентами g ∘ p_k.
LaTeX
$$$ g \text{ is linear and } HasFTaylorSeriesUpToOn\ n\ f\ p\ s \Rightarrow HasFTaylorSeriesUpToOn n (g \circ f) (\lambda x k. g \circ p x k) s $$$
Lean4
/-- If `f` admits a Taylor series `p` in a set `s`, and `g` is linear, then `g ∘ f` admits a Taylor
series whose `k`-th term is given by `g ∘ (p k)`. -/
theorem continuousLinearMap_comp {n : WithTop ℕ∞} (g : F →L[𝕜] G) (hf : HasFTaylorSeriesUpToOn n f p s) :
HasFTaylorSeriesUpToOn n (g ∘ f) (fun x k => g.compContinuousMultilinearMap (p x k)) s
where
zero_eq x hx := congr_arg g (hf.zero_eq x hx)
fderivWithin m hm x
hx :=
(ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun _ : Fin m => E) F G g).hasFDerivAt.comp_hasFDerivWithinAt
x (hf.fderivWithin m hm x hx)
cont m
hm :=
(ContinuousLinearMap.compContinuousMultilinearMapL 𝕜 (fun _ : Fin m => E) F G g).continuous.comp_continuousOn
(hf.cont m hm)
