def Real_Analysis.Series.AbsolutelyConvergent (x : ℕ → ℝ) : Prop

A real series ∑ x n is absolutely convergent if the series of absolute values ∑ |x n| is summable.

theorem Real_Analysis.Series.abs_convergent_rearrangement {s : ℝ} (x : ℕ → ℝ) (σ : ℕ ≃ ℕ) (habs : Summable fun (n : ℕ) => |x n|) (hsum : HasSum x s) : (Summable fun (n : ℕ) => |x (σ n)|) ∧ HasSum (x ∘ ⇑σ) s

Rearrangement theorem for absolutely convergent series: if ∑ |x n| is summable and ∑ x n has sum s, then for any permutation σ : ℕ ≃ ℕ the rearranged series ∑ x (σ n) is also absolutely convergent and has the same sum s.

def Real_Analysis.Series.SeriesConverges (x : ℕ → ℝ) : Prop

The series ∑ x n converges if the sequence of partial sums s m = ∑ n ∈ range m, x n converges to some real number s.