English
Let f: Nat → C be a complex sequence with its partial sums converging to l. Then for any α-type, the Abel-sum ∑ f(n) z^n converges along Stolz-sets to l, uniformly with respect to the appropriate variable.
Русский
Пусть f: Nat → ℂ имеет предел частичных сумм l. Тогда сумма Абеля ∑ f(n) z^n сходится вдоль множеств Стольца, к пределу l, единичная сумма в общем случае.
LaTeX
$$$$\\forall f:\\mathbb{N}\\to \\mathbb{C},\\ \\forall l\\in \\mathbb{C},\\ \\operatorname{Tendsto}_{\\mathrm{nhdsWithin}}\\left(z\\mapsto \\sum_{n=0}^{\\infty} f(n) z^{n}\\right)_{(\\mathrm{nhdsWithin\\}(1))} (\\mathcal{N} l).$$$$
Lean4
theorem tendsto_tsum_powerSeries_nhdsWithin_lt (h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)) :
Tendsto (fun z ↦ ∑' n, f n * z ^ n) ((𝓝[<] 1).map ofReal) (𝓝 l) :=
(tendsto_tsum_powerSeries_nhdsWithin_stolzSet (M := 2) h).mono_left (nhdsWithin_lt_le_nhdsWithin_stolzSet one_lt_two)
