English
Let f be a real sequence; if its partial sums converge to l, then the left-limit Abel sum converges to l as x approaches 1 from the left, i.e., along 𝓝[<] 1.
Русский
Пусть последовательность вещественных чисел имеет предел частичных сумм l. Тогда сумма Абеля слева сходится к l при приближении к 1 слева, то есть в 𝓝[<] 1.
LaTeX
$$$$\\forall f:\\mathbb{N}\\to \\mathbb{R},\\ \\forall l,\\text{ если } \\sum_{i=0}^{n-1} f(i) \\to l,\\ \\operatorname{Tendsto}_{\\mathcal{nhdsWithin}(1)}\\left(x\\mapsto \\sum_{n=0}^{\\infty} f(n) x^{n}\\right) (\\mathcal{nhds}(l)).$$$$
Lean4
/-- **Abel's limit theorem**. Given a real power series converging at 1, the corresponding function
is continuous at 1 when approaching 1 from the left. -/
theorem tendsto_tsum_powerSeries_nhdsWithin_lt (h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)) :
Tendsto (fun x ↦ ∑' n, f n * x ^ n) (𝓝[<] 1) (𝓝 l) :=
by
have m : (𝓝 l).map ofReal ≤ 𝓝 ↑l := ofRealCLM.continuous.tendsto l
replace h := (tendsto_map.comp h).mono_right m
rw [Function.comp_def] at h
push_cast at h
replace h := Complex.tendsto_tsum_powerSeries_nhdsWithin_lt h
rw [tendsto_map'_iff] at h
rw [Metric.tendsto_nhdsWithin_nhds] at h ⊢
convert h
simp_rw [Function.comp_apply, dist_eq_norm]
norm_cast
