eventually_hasSum_sub — Mathlib

English

If f has a formal power series at x, then near x the HasSum with terms p_n(y−x) converges to f(y).

Русский

Если у f есть степенной ряд в точке x, то около x сумма с членами p_n(y−x) сходится к f(y).

LaTeX

$$$HasFPowerSeriesAt\\; f\\; p\\; x \\Rightarrow \\forall^\\infty y \\in 𝓝 x,\n HasSum\\left(\\lambda n. p_n(\\lambda _ : Fin n => y - x)\\right)(f(y)).$$$

Lean4

theorem eventually_hasSum_sub (hf : HasFPowerSeriesAt f p x) :
    ∀ᶠ y in 𝓝 x, HasSum (fun n : ℕ => p n fun _ : Fin n => y - x) (f y) :=
  let ⟨_, hr⟩ := hf
  hr.eventually_hasSum_sub

Похожие утверждения