Documentation

Mathlib.Analysis.Complex.AbelLimit

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 #

References #

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
Instances For

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

    Equations
    Instances For
      theorem Complex.stolzCone_subset_stolzSet_aux {s : } (hs : 0 < s) :
      ∃ (M : ) (ε : ), 0 < M 0 < ε {z : | 1 - ε < z.re} Complex.stolzCone s Complex.stolzSet M
      theorem Complex.abel_aux {f : } {l : } (h : Filter.Tendsto (fun (n : ) => iFinset.range n, f i) Filter.atTop (nhds l)) {z : } (hz : z < 1) :
      Filter.Tendsto (fun (n : ) => (1 - z) * iFinset.range n, (l - jFinset.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 : ) => iFinset.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.

      theorem Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone {f : } {l : } (h : Filter.Tendsto (fun (n : ) => iFinset.range n, f i) Filter.atTop (nhds l)) {s : } (hs : 0 < s) :
      Filter.Tendsto (fun (z : ) => ∑' (n : ), f n * z ^ n) (nhdsWithin 1 (Complex.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 : ) => iFinset.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)
      theorem Real.tendsto_tsum_powerSeries_nhdsWithin_lt {f : } {l : } (h : Filter.Tendsto (fun (n : ) => iFinset.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.