English
An analytic function has a formal power series expansion given by iterated derivatives at x.
Русский
Аналитическая функция имеет разложение по степенным словам в точке x через итеративные производные.
LaTeX
$$$\\forall {f:\\mathbb{K}\\to \\mathbb{K}}\\; (\\text{AnalyticAt } 𝕜 f x) \\Rightarrow HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 (\\lambda n. \\operatorname{iteratedDeriv} n f x / n!.cast)) x$$$
Lean4
theorem hasFPowerSeriesAt {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜}
(h : AnalyticAt 𝕜 f x) :
HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / n.factorial)) x :=
by
obtain ⟨p, hp⟩ := h
convert hp
obtain ⟨r, hpr⟩ := hp
ext n
have h_fact_smul := hpr.factorial_smul 1
simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff, Finset.prod_const, Finset.card_univ, Fintype.card_fin,
smul_eq_mul, nsmul_eq_mul, one_pow, one_mul] at h_fact_smul
simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff, FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul,
mul_eq_mul_left_iff]
left
rw [div_eq_iff, mul_comm, h_fact_smul, ← iteratedDeriv_eq_iteratedFDeriv]
norm_cast
positivity
