Tail_of_Convergent_Series_tends_to_Zero
Provedproofwikiseries
If sum a_n converges, then the tail sum from n to infinity converges to 0 as n goes to infinity.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Tail_of_Convergent_Series_tends_to_Zero (a : ℕ → ℝ) (ha : Summable a) : Filter.Tendsto (fun n => ∑' k, a (n + k)) Filter.atTop (nhds 0) := by sorry
Source