eventually_hasSum — Mathlib

English

If f, p yield a power series on ball around x, then for y near 0 the partial sums converge to f(x+y), i.e. HasSum of the n-th term series equals f(x+y).

Русский

Если f, p дают степенной ряд на шаре вокруг x, то при y, приближающемся к 0, частичные суммы сходятся к f(x+y).

LaTeX

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

Lean4

theorem eventually_hasSum (hf : HasFPowerSeriesOnBall f p x r) :
    ∀ᶠ y in 𝓝 0, HasSum (fun n : ℕ => p n fun _ : Fin n => y) (f (x + y)) := by
  filter_upwards [EMetric.ball_mem_nhds (0 : E) hf.r_pos] using fun _ => hf.hasSum

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