tendsto_partialSum — Mathlib

English

If a full HasFPowerSeriesWithinOnBall holds for f and p, then the two-argument partial sums converge to f(x+y) along the product filter in (n,y).

Русский

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

LaTeX

$$$\text{HasFPowerSeriesWithinOnBall}(f,p,s,x,r) \Rightarrow \text{Tendsto}( (z\mapsto p.partialSum(z.fst,z.snd)) )(atTop \times \mathcal{N}(y)) \to f(x+y)$$$

Lean4

theorem tendsto_partialSum (hf : HasFPowerSeriesAt f p x) :
    ∀ᶠ y in 𝓝 0, Tendsto (fun n => p.partialSum n y) atTop (𝓝 (f (x + y))) :=
  by
  rcases hf with ⟨r, hr⟩
  filter_upwards [EMetric.ball_mem_nhds (0 : E) hr.r_pos] with y hy
  exact hr.tendsto_partialSum hy

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