English
If a function is analytic within a set at a point, there exists a Taylor series data around a neighborhood and the corresponding analyticity on that neighborhood for all coefficients.
Русский
Если функция аналитична внутри множества в точке, существует выбор ряда Тейлора и аналитичность для всех коэффициентов на окрестности.
LaTeX
$$$\\exists u \\in \\mathcal{N}, \\exists p : E \\to FormalMultilinearSeries 𝕜 E F, HasFTaylorSeriesUpToOn n f p u \\land \\forall i, AnalyticOn 𝕜 (fun x \\mapsto p x i) u$$$
Lean4
theorem exists_hasFTaylorSeriesUpToOn [CompleteSpace F] (n : WithTop ℕ∞) (h : AnalyticWithinAt 𝕜 f s x) :
∃ u ∈ 𝓝[insert x s] x,
∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn n f p u ∧ ∀ i, AnalyticOn 𝕜 (fun x ↦ p x i) u :=
by
rcases h.exists_analyticAt with ⟨g, -, fg, hg⟩
rcases hg.exists_mem_nhds_analyticOnNhd with ⟨v, vx, hv⟩
refine ⟨insert x s ∩ v, inter_mem_nhdsWithin _ vx, ftaylorSeries 𝕜 g, ?_, fun i ↦ ?_⟩
· suffices HasFTaylorSeriesUpToOn n g (ftaylorSeries 𝕜 g) (insert x s ∩ v) from this.congr (fun y hy ↦ fg hy.1)
exact AnalyticOnNhd.hasFTaylorSeriesUpToOn _ (hv.mono Set.inter_subset_right)
· exact (hv.iteratedFDeriv i).analyticOn.mono Set.inter_subset_right
