English
If a function has a Taylor series up to order n in a scalar field 𝕜′, then after restricting scalars to 𝕜, the Taylor series exists with the appropriately restricted coefficients.
Русский
Если функция имеет ряд Тейлора до порядка n над полем 𝕜′, то после ограничения скаляров к 𝕜 существует ряд Тейлора с соответствующими ограниченными коэффициентами.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn } n\, f\, p'\, s \;\Longrightarrow\; \text{HasFTaylorSeriesUpToOn } n\, f\, (\lambda x. (p'(x)).\text{restrictScalars } 𝕜)\, s.$$$$
Lean4
theorem restrictScalars {n : WithTop ℕ∞} (h : HasFTaylorSeriesUpToOn n f p' s) :
HasFTaylorSeriesUpToOn n f (fun x => (p' x).restrictScalars 𝕜) s
where
zero_eq x hx := h.zero_eq x hx
fderivWithin m hm x
hx :=
((ContinuousMultilinearMap.restrictScalarsLinear 𝕜).hasFDerivAt.comp_hasFDerivWithinAt x <|
(h.fderivWithin m hm x hx).restrictScalars 𝕜 :)
cont m hm := ContinuousMultilinearMap.continuous_restrictScalars.comp_continuousOn (h.cont m hm)
