Tauberian theorems for power series

TheoremTauber's theorem#✓fully proved

Tauber's theorem (1897). If the power series ∑ aₙ rⁿ converges (in the Abel sense) to A as r → 1⁻ and n * aₙ → 0, then the partial sums of a converge to A.

theorem tauber_tendsto_partial_sums {a : ℕ → ℝ} {A : ℝ}
    (hAbel : Tendsto (fun r => ∑' n, a n * r ^ n) (𝓝[<] 1) (𝓝 A))
    (hTaub : Tendsto (fun n : ℕ => (n : ℝ) * a n) atTop (𝓝 0)) :
    Tendsto (fun N => ∑ n ∈ Finset.range N, a n) atTop (𝓝 A)

TheoremHardy–Littlewood Tauberian theorem#✓fully proved

Hardy–Littlewood Tauberian theorem (1914). If aₙ ≥ 0 and the power series ∑ aₙ rⁿ converges for every r ∈ (0, 1) with Abel limit A as r → 1⁻, then the partial sums of a converge to A.

theorem hardy_littlewood_tendsto_partial_sums {a : ℕ → ℝ} {A : ℝ}
    (hnonneg : ∀ n, 0 ≤ a n)
    (hsum : ∀ r ∈ Set.Ioo (0 : ℝ) 1, Summable (fun n => a n * r ^ n))
    (hAbel : Tendsto (fun r => ∑' n, a n * r ^ n) (𝓝[<] 1) (𝓝 A)) :
    Tendsto (fun N => ∑ n ∈ Finset.range N, a n) atTop (𝓝 A)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.