English
Let f be a sequence such that its partial sums converge to l. Then the Abel sum ∑ f(n) z^n converges to l as z approaches 1 from within a Stolz cone of parameter s > 0.
Русский
Пусть частичные суммы последовательности сходятся к l. Тогда сумма Абеля ∑ f(n) z^n сходится к l, когда z стремится к 1 внутри конуса Стольца с параметром s > 0.
LaTeX
$$$$\\forall {f:\\nrightarrow \\mathbb{N} \\to \\mathbb{C}}, \\forall l, \\text{ if } \\operatorname{Tendsto}\\left(n \\mapsto \\sum_{i=0}^{n-1} f(i)\\right)_{\\mathrm{atTop}} (\\mathcal{N} l), \\forall s>0, \\operatorname{Tendsto}\\left(z \\mapsto \\sum_{n=0}^{\\infty} f(n) z^n\\right) (\\mathcal{N}_{\\operatorname{stolzCone}(s)}(1)) (\\mathcal{N} l).$$$$
Lean4
/-- **Abel's limit theorem**. Given a power series converging at 1, the corresponding function
is continuous at 1 when approaching 1 within any fixed Stolz cone. -/
theorem tendsto_tsum_powerSeries_nhdsWithin_stolzCone (h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)) {s : ℝ}
(hs : 0 < s) : Tendsto (fun z ↦ ∑' n, f n * z ^ n) (𝓝[stolzCone s] 1) (𝓝 l) :=
(tendsto_tsum_powerSeries_nhdsWithin_stolzSet h).mono_left
(nhdsWithin_stolzCone_le_nhdsWithin_stolzSet hs).choose_spec
