Source indexedlemma · leanprover/lean4:v4.32.0

Complex.hasSum_sub_succ_of_tendsto_zero

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/DigammaSeries.lean:138 to 148

Source documentation

A summable telescoping series whose terms tend to zero sums to its first term.

Exact Lean statement

lemma hasSum_sub_succ_of_tendsto_zero {E : Type*} [AddCommGroup E] [TopologicalSpace E]
    [IsTopologicalAddGroup E] [T2Space E] {a : ℕ → E} (h0 : Tendsto a atTop (𝓝 0))
    (hs : Summable fun n => a n - a (n + 1)) :
    HasSum (fun n => a n - a (n + 1)) (a 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasSum_sub_succ_of_tendsto_zero {E : Type*} [AddCommGroup E] [TopologicalSpace E]    [IsTopologicalAddGroup E] [T2Space E] {a : ℕ → E} (h0 : Tendsto a atTop (𝓝 0))    (hs : Summable fun n => a n - a (n + 1)) :    HasSum (fun n => a n - a (n + 1)) (a 0) := by  have h1 : Tendsto (fun n => ∑ i ∈ Finset.range n, (a i - a (i + 1))) atTop (𝓝 (a 0)) := by    have he : ∀ n, ∑ i ∈ Finset.range n, (a i - a (i + 1)) = a 0 - a n :=      fun n => Finset.sum_range_sub' a n    simp only [he]    simpa using tendsto_const_nhds.sub h0  have h2 := hs.hasSum  rwa [tendsto_nhds_unique h2.tendsto_sum_nat h1] at h2