Abel's limit theorem

If a real or complex power series for a function has radius of convergence 1 and the series is only known to converge conditionally at 1, Abel's limit theorem gives the value at 1 as the limit of the function at 1 from the left. "Left" for complex numbers means within a fixed cone opening to the left with angle less than π.

Main theorems

• Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone: Abel's limit theorem for complex power series.
• Real.tendsto_tsum_powerSeries_nhdsWithin_lt: Abel's limit theorem for real power series.

References

• https://planetmath.org/proofofabelslimittheorem
• https://en.wikipedia.org/wiki/Abel%27s_theorem

def Complex.stolzSet (M : ℝ) : Set ℂ

The Stolz set for a given M, roughly teardrop-shaped with the tip at 1 but tending to the open unit disc as M tends to infinity.

Equations

• Complex.stolzSet M = {z : ℂ | ‖z‖ < 1 ∧ ‖1 - z‖ < M * (1 - ‖z‖)}

def Complex.stolzCone (s : ℝ) : Set ℂ

The cone to the left of 1 with angle 2θ such that tan θ = s.

Equations

• Complex.stolzCone s = {z : ℂ | |z.im| < s * (1 - z.re)}

theorem Complex.stolzSet_empty {M : ℝ} (hM : M ≤ 1) : stolzSet M = ∅

theorem Complex.nhdsWithin_lt_le_nhdsWithin_stolzSet {M : ℝ} (hM : 1 < M) : Filter.map ofReal (nhdsWithin 1 (Set.Iio 1)) ≤ nhdsWithin 1 (stolzSet M)

theorem Complex.stolzCone_subset_stolzSet_aux {s : ℝ} (hs : 0 < s) : ∃ (M : ℝ) (ε : ℝ), 0 < M ∧ 0 < ε ∧ {z : ℂ | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M

theorem Complex.nhdsWithin_stolzCone_le_nhdsWithin_stolzSet {s : ℝ} (hs : 0 < s) : ∃ (M : ℝ), nhdsWithin 1 (stolzCone s) ≤ nhdsWithin 1 (stolzSet M)

theorem Complex.abel_aux {f : ℕ → ℂ} {l : ℂ} (h : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) {z : ℂ} (hz : ‖z‖ < 1) : Filter.Tendsto (fun (n : ℕ) => (1 - z) * ∑ i ∈ Finset.range n, (l - ∑ j ∈ Finset.range (i + 1), f j) * z ^ i) Filter.atTop (nhds (l - ∑' (n : ℕ), f n * z ^ n))

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 Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSet {f : ℕ → ℂ} {l : ℂ} (h : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) {M : ℝ} : Filter.Tendsto (fun (z : ℂ) => ∑' (n : ℕ), f n * z ^ n) (nhdsWithin 1 (stolzSet M)) (nhds l)

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 Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone {f : ℕ → ℂ} {l : ℂ} (h : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) {s : ℝ} (hs : 0 < s) : Filter.Tendsto (fun (z : ℂ) => ∑' (n : ℕ), f n * z ^ n) (nhdsWithin 1 (stolzCone s)) (nhds l)

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 Complex.tendsto_tsum_powerSeries_nhdsWithin_lt {f : ℕ → ℂ} {l : ℂ} (h : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) : Filter.Tendsto (fun (z : ℂ) => ∑' (n : ℕ), f n * z ^ n) (Filter.map ofReal (nhdsWithin 1 (Set.Iio 1))) (nhds l)

theorem Real.tendsto_tsum_powerSeries_nhdsWithin_lt {f : ℕ → ℝ} {l : ℝ} (h : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) : Filter.Tendsto (fun (x : ℝ) => ∑' (n : ℕ), f n * x ^ n) (nhdsWithin 1 (Set.Iio 1)) (nhds l)

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.