English
Let f be a sequence of complex numbers with a convergent partial sums to l. Then the power series ∑ f(n) z^n converges to l at the boundary z=1 for Stolz-sets; more precisely, for every M there is a Stolz set neighborhood that yields convergence to l.
Русский
Пусть последовательность f имеет частичные суммы сходящейся к l; тогда сило Abel, для каждой концентации, при наборе Stolz существует окрестность, где ∑ f(n) z^n сходится к l.
LaTeX
$$$$\\forall {f:\\nrightarrow \\mathbb{N} \\to \\mathbb{C}}, \\forall l, \\text{ if } \\sum_{i=0}^{n-1} f(i) \\to l, \\text{ then } \\sum_{n=0}^{\\infty} f(n) z^n \\to l \\text{ as } z \\to 1 \\text{ within } \\operatorname{stolzSet}(M).$$$$
Lean4
/-- **Abel's limit theorem**. Given a power series converging at 1, the corresponding function
is continuous at 1 when approaching 1 within a fixed Stolz set. -/
theorem tendsto_tsum_powerSeries_nhdsWithin_stolzSet (h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)) {M : ℝ} :
Tendsto (fun z ↦ ∑' n, f n * z ^ n) (𝓝[stolzSet M] 1) (𝓝 l) := by
-- If `M ≤ 1` the Stolz set is empty and the statement is trivial
rcases le_or_gt M 1 with hM | hM
·
simp_rw [stolzSet_empty hM, nhdsWithin_empty, tendsto_bot]
-- Abbreviations
let s := fun n ↦ ∑ i ∈ range n, f i
let g := fun z ↦ ∑' n, f n * z ^ n
have hm := Metric.tendsto_atTop.mp h
rw [Metric.tendsto_nhdsWithin_nhds]
simp only [dist_eq_norm] at hm
⊢
-- Introduce the "challenge" `ε`
intro ε εpos
obtain ⟨B₁, hB₁⟩ :=
hm (ε / 4 / M)
(by positivity)
-- Second bound, handles the head
let F := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
use ε / 4 / (F + 1), by positivity
intro z ⟨zn, zm⟩ zd
have p := abel_aux h zn
simp_rw [Metric.tendsto_atTop, dist_eq_norm, norm_sub_rev] at p
obtain ⟨B₂, hB₂⟩ := p (ε / 2) (by positivity)
clear hm p
replace hB₂ := hB₂ (max B₁ B₂) (by simp)
suffices ‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ < ε / 2 by
calc
_ = ‖l - g z‖ := by rw [norm_sub_rev]
_ =
‖l - g z - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i +
(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ :=
by rw [sub_add_cancel _]
_ ≤
‖l - g z - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ +
‖(1 - z) * ∑ i ∈ range (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ :=
(norm_add_le _ _)
_ < ε / 2 + ε / 2 := (add_lt_add hB₂ this)
_ = _ := add_halves ε
calc
_ =
‖(1 - z) * ∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i +
(1 - z) * ∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ :=
by rw [← mul_add, sum_range_add_sum_Ico _ (le_max_left B₁ B₂)]
_ ≤
‖(1 - z) * ∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i‖ +
‖(1 - z) * ∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ :=
(norm_add_le _ _)
_ =
‖1 - z‖ * ‖∑ i ∈ range B₁, (l - s (i + 1)) * z ^ i‖ +
‖1 - z‖ * ‖∑ i ∈ Ico B₁ (max B₁ B₂), (l - s (i + 1)) * z ^ i‖ :=
by rw [norm_mul, norm_mul]
_ ≤
‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i +
‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i :=
by
gcongr <;>
simp_rw [← norm_pow, ← norm_mul, norm_sum_le]
-- then prove that the two pieces are each less than `ε / 4`
have S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4 :=
calc
_ ≤ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ := by
gcongr; nth_rw 3 [← mul_one ‖_‖]
gcongr; exact pow_le_one₀ (norm_nonneg _) zn.le
_ ≤ ‖1 - z‖ * (F + 1) := by gcongr; linarith only
_ < _ := by rwa [norm_sub_rev, lt_div_iff₀ (by positivity)] at zd
have S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4 :=
calc
_ ≤ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ε / 4 / M * ‖z‖ ^ i :=
by
gcongr with i hi
have := hB₁ (i + 1) (by linarith only [(mem_Ico.mp hi).1])
rw [norm_sub_rev] at this
exact this.le
_ = ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i := by rw [← mul_sum, ← mul_assoc]
_ ≤ ‖1 - z‖ * (ε / 4 / M) * ∑' i, ‖z‖ ^ i := by
gcongr
exact Summable.sum_le_tsum _ (fun _ _ ↦ by positivity) (summable_geometric_of_lt_one (by positivity) zn)
_ = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) := by rw [tsum_geometric_of_lt_one (by positivity) zn, ← div_eq_mul_inv]
_ < M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖) := by gcongr; linarith only [zn]
_ = _ := by
rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]), div_mul_cancel₀ _ (by linarith only [hM])]
convert add_lt_add S₁ S₂ using 1
linarith only
