Theorems · Theorem · complex analysis

Complex.tendsto_tsum_powerSeries_nhdsWithin_lt

∀ {f : ℕ → ℂ} {l : ℂ},
  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 Complex.ofReal (nhdsWithin 1 (Set.Iio 1))) (nhds l)

Defined in: Mathlib.Analysis.Complex.AbelLimit
Cited by: 1 results in Mathlib
Foundations: Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
Complexstatement and proof · cited by 5,565
nhdsstatement and proof · cited by 5,554
Finset.sumstatement and proof · cited by 5,195
Filter.Tendstostatement and proof · cited by 3,814
Filter.atTopstatement and proof · cited by 2,405
SummationFilter.unconditionalstatement · cited by 2,068
nhdsWithinstatement · cited by 1,912
Complex.ofRealstatement · cited by 1,654
Finset.rangestatement and proof · cited by 1,341
Set.Iiostatement · cited by 1,166
tsumstatement · cited by 1,148

Cited by1

Results whose statement or proof uses this declaration.

Real.tendsto_tsum_powerSeries_nhdsWithin_ltproof · cited by 1