Theorems · Theorem · complex analysis

Complex.abel_aux

∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l) →
    ∀ {z : ℂ},
      ‖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.

Defined in

Mathlib.Analysis.Complex.AbelLimit

Cited by

1 results in Mathlib

Foundations

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