English
Let h describe a limit of partial sums of a sequence f, and fix a complex number z with |z| < 1. Then the transformed sequence (1 − z) times a tail-sum series converges to l minus the generating series evaluated at z.
Русский
Пусть h задаёт предел частичных сумм последовательности f, фиксируем комплексное число z с |z| < 1. Тогда последовательность, являющаяся произведением (1 − z) на хвостовую сумму и умноженная на z^i, сходится к l − ∑′ n f(n) z^n.
LaTeX
$$$$\\text{If } h : \\operatorname{Tendsto}\\left(n \\mapsto \\sum_{i=0}^{n-1} f(i)\\right)_{\\mathrm{atTop}} (\\mathcal{N} l) \\text{ and } |z| < 1, \\\\ \\text{then } \\operatorname{Tendsto}\\left(n \\mapsto (1 - z) \\sum_{i=0}^{n-1} \\Bigl(l - \\sum_{j=0}^{i} f(j)\\Bigr) z^i\\right)_{\\mathrm{atTop}} (\\mathcal{N} l - \\sum_{n=0}^{\\infty} f(n) z^n).$$$$
Lean4
/-- Auxiliary lemma for Abel's limit theorem. The difference between the sum `l` at 1 and the
power series's value at a point `z` away from 1 can be rewritten as `1 - z` times a power series
whose coefficients are tail sums of `l`. -/
theorem abel_aux (h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)) {z : ℂ} (hz : ‖z‖ < 1) :
Tendsto (fun n ↦ (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i) atTop
(𝓝 (l - ∑' n, f n * z ^ n)) :=
by
let s := fun n ↦ ∑ i ∈ range n, f i
have k := h.sub (summable_powerSeries_of_norm_lt_one h.cauchySeq hz).hasSum.tendsto_sum_nat
simp_rw [← sum_sub_distrib, ← mul_one_sub, ← geom_sum_mul_neg, ← mul_assoc, ← sum_mul, mul_comm, mul_sum _ _ (f _),
range_eq_Ico, ← sum_Ico_Ico_comm', ← range_eq_Ico, ← sum_mul] at k
conv at k =>
enter [1, n]
rw [sum_congr (g := fun j ↦ (∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k) * z ^ j) rfl
(fun j hj ↦ by congr 1; exact sum_Ico_eq_sub _ (mem_range.mp hj))]
suffices Tendsto (fun n ↦ (l - s n) * ∑ i ∈ range n, z ^ i) atTop (𝓝 0)
by
simp_rw [mul_sum] at this
replace this := (this.const_mul (1 - z)).add k
conv at this =>
enter [1, n]
rw [← mul_add, ← sum_add_distrib]
enter [2, 2, i]
rw [← add_mul, sub_add_sub_cancel]
rwa [mul_zero, zero_add] at this
rw [← zero_mul (-1 / (z - 1))]
apply Tendsto.mul
· simpa only [neg_zero, neg_sub] using (tendsto_sub_nhds_zero_iff.mpr h).neg
· conv =>
enter [1, n]
rw [geom_sum_eq (by contrapose! hz; simp [hz]), sub_div, sub_eq_add_neg, ← neg_div]
rw [← zero_add (-1 / (z - 1)), ← zero_div (z - 1)]
apply Tendsto.add (Tendsto.div_const (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hz) (z - 1))
simp only [zero_div, zero_add, tendsto_const_nhds_iff]
