eventually_hasSum — Mathlib

English

Near the base point x, the HasSum with coefficients p_n applied to y−x converges to f(y) when y is close to x.

Русский

Вблизи точки x сумма степенного ряда с коэффициентами p_n, применёнными к y−x, сходится к f(y).

LaTeX

$$$HasFPowerSeriesOnBall f p x r \\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 (hf : HasFPowerSeriesAt f p x) :
    ∀ᶠ y in 𝓝 0, HasSum (fun n : ℕ => p n fun _ : Fin n => y) (f (x + y)) :=
  let ⟨_, hr⟩ := hf
  hr.eventually_hasSum

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