tendsto_partialSum — Mathlib

English

If f has a power series p around x with radius r, then the bivariate partial sums p.partialSum z1 z2 converge to f(x+y) as (n,y) → (∞, y).

Русский

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

LaTeX

$$$\text{HasFPowerSeriesWithinOnBall}(f,p,s,x,r) \Rightarrow \forall y\in E,\; (x+y)\in insert x s \Rightarrow \text{Tendsto}(\lambda z, p.partialSum(z_1,z_2))(\text{atTop} \times \mathcal{N}(y)) \to f(x+y)$$$

Lean4

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

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