tendsto_partialSum — Mathlib

English

If f has a formal power series within a ball around x with p, then partial sums p.partialSum n y converge to f(x+y) as n → ∞ for y in the ball.

Русский

Если вокруг x функция имеет степенной ряд в-ball с коэффициентами p, то частичные суммы сходятся к f(x+y) при n→∞ и y внутри окружности.

LaTeX

$$$\text{HasFPowerSeriesWithinOnBall}_{\mathcal{K}}(f,p,s,x,r) \Rightarrow \forall y\in E\!\text{Metric ball}(0,r)\!:\, \lim_{n\to\infty} p.partialSum(n,y) = f(x+y)$$$

Lean4

theorem tendsto_partialSum (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E} (hy : y ∈ EMetric.ball (0 : E) r)
    (h'y : x + y ∈ insert x s) : Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y))) :=
  (hf.hasSum h'y hy).tendsto_sum_nat

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