eventually_hasSum_sub — Mathlib

English

If f has a formal power series at x, then for y near x the sum with p_n evaluated at y−x equals f(y).

Русский

Если у f имеется степенной ряд в точке x, то для y, близкого к 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 : HasFPowerSeriesOnBall f p x r) :
    ∀ᶠ y in 𝓝 x, HasSum (fun n : ℕ => p n fun _ : Fin n => y - x) (f y) := by
  filter_upwards [EMetric.ball_mem_nhds x hf.r_pos] with y using hf.hasSum_sub

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