Theorems · Theorem · complex analysis

Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSet

∀ {f : ℕ → ℂ} {l : ℂ},
  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 (Complex.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.

Defined in

Mathlib.Analysis.Complex.AbelLimit

Cited by

2 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound