English
Let f be analytic on a set s and assume s has the unique-differentiability property. Then there exists a function p assigning to every point x in E a formal multilinear series such that f has a Taylor expansion of infinite order up to on s, and each coordinate function x ↦ p(x)i is analytic on s for every i.
Русский
Пусть f аналитична на множестве s и на s выполняется условие уникальной точки дифференцируемости. Тогда существует отображение p, где для каждой точки x ∈ E задан ряд формальных многочлены̆, такой что f имеет бесконечное разложение в ряд Тейлора на s, и для каждого i функция x ↦ p(x)i аналитична на s.
LaTeX
$$$\exists p: E \to \text{FormalMultilinearSeries}_{\mathbb{k}}(E,F),\ HasFTaylorSeriesUpToOn \top f p s \land \forall i, AnalyticOn 𝕜 (\lambda x. p x i) s$$$
Lean4
theorem exists_hasFTaylorSeriesUpToOn (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
∃ p : E → FormalMultilinearSeries 𝕜 E F, HasFTaylorSeriesUpToOn ⊤ f p s ∧ ∀ i, AnalyticOn 𝕜 (fun x ↦ p x i) s :=
⟨ftaylorSeriesWithin 𝕜 f s, h.hasFTaylorSeriesUpToOn hu, h.iteratedFDerivWithin hu⟩
