doc-next-gen

Mathlib.Analysis.Normed.Group.InfiniteSum

Module docstring

{"# Infinite sums in (semi)normed groups

In a complete (semi)normed group,

  • summable_iff_vanishing_norm: a series ∑' i, f i is summable if and only if for any ε > 0, there exists a finite set s such that the sum ∑ i ∈ t, f i over any finite set t disjoint with s has norm less than ε;

  • Summable.of_norm_bounded, Summable.of_norm_bounded_eventually: if ‖f i‖ is bounded above by a summable series ∑' i, g i, then ∑' i, f i is summable as well; the same is true if the inequality hold only off some finite set.

  • tsum_of_norm_bounded, HasSum.norm_le_of_bounded: if ‖f i‖ ≤ g i, where ∑' i, g i is a summable series, then ‖∑' i, f i‖ ≤ ∑' i, g i.

Tags

infinite series, absolute convergence, normed group "}

cauchySeq_finset_iff_vanishing_norm theorem
{f : ι → E} : (CauchySeq fun s : Finset ι => ∑ i ∈ s, f i) ↔ ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
Full source 
theorem cauchySeq_finset_iff_vanishing_norm {f : ι → E} :
    (CauchySeq fun s : Finset ι => ∑ i ∈ s, f i) ↔
      ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i ∈ t, f i‖ < ε := by
  rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]
  · simp only [ball_zero_eq, Set.mem_setOf_eq]
  · rintro s t hst ⟨s', hs'⟩
    exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩
Cauchy Criterion for Partial Sums in Seminormed Groups: Vanishing Norm Condition
Informal description
For a function $f : \iota \to E$ from an index type $\iota$ to a seminormed additive commutative group $E$, the sequence of partial sums $\sum_{i \in s} f(i)$ indexed by finite subsets $s \subseteq \iota$ is Cauchy if and only if for every $\varepsilon > 0$, there exists a finite subset $s \subseteq \iota$ such that for any finite subset $t \subseteq \iota$ disjoint from $s$, the norm of the partial sum $\|\sum_{i \in t} f(i)\|$ is less than $\varepsilon$.
summable_iff_vanishing_norm theorem
[CompleteSpace E] {f : ι → E} : Summable f ↔ ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
Full source 
theorem summable_iff_vanishing_norm [CompleteSpace E] {f : ι → E} :
    SummableSummable f ↔ ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i ∈ t, f i‖ < ε := by
  rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing_norm]
Summability Criterion via Vanishing Norm in Complete Seminormed Groups
Informal description
Let $E$ be a complete seminormed additive commutative group and $f : \iota \to E$ be a function. The series $\sum_{i \in \iota} f(i)$ is summable if and only if for every $\varepsilon > 0$, there exists a finite subset $s \subseteq \iota$ such that for any finite subset $t \subseteq \iota$ disjoint from $s$, the norm of the partial sum $\|\sum_{i \in t} f(i)\|$ is less than $\varepsilon$.
cauchySeq_finset_of_norm_bounded_eventually theorem
{f : ι → E} {g : ι → ℝ} (hg : Summable g) (h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) : CauchySeq fun s => ∑ i ∈ s, f i
Full source 
theorem cauchySeq_finset_of_norm_bounded_eventually {f : ι → E} {g : ι → ℝ} (hg : Summable g)
    (h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) : CauchySeq fun s => ∑ i ∈ s, f i := by
  refine cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => ?_
  rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩
  classical
  refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩
  have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
    intro i hi
    simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
      Classical.not_not] at ht
    exact (ht hi).2
  calc
    ‖∑ i ∈ t, f i‖ ≤ ∑ i ∈ t, g i := norm_sum_le_of_le _ this
    _ ≤ ‖∑ i ∈ t, g i‖ := le_abs_self _
    _ < ε := hs _ (ht.mono_right le_sup_left)
Cauchy Criterion for Partial Sums with Eventual Norm Bounds in Seminormed Groups
Informal description
Let $E$ be a seminormed additive commutative group and let $f \colon \iota \to E$ and $g \colon \iota \to \mathbb{R}$ be functions. If the series $\sum_{i \in \iota} g(i)$ is summable and there exists a finite subset $s \subseteq \iota$ such that $\|f(i)\| \leq g(i)$ for all $i \notin s$, then the sequence of partial sums $\sum_{i \in t} f(i)$ indexed by finite subsets $t \subseteq \iota$ is a Cauchy sequence.
cauchySeq_finset_of_norm_bounded theorem
{f : ι → E} (g : ι → ℝ) (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : CauchySeq fun s : Finset ι => ∑ i ∈ s, f i
Full source 
theorem cauchySeq_finset_of_norm_bounded {f : ι → E} (g : ι → ℝ) (hg : Summable g)
    (h : ∀ i, ‖f i‖ ≤ g i) : CauchySeq fun s : Finset ι => ∑ i ∈ s, f i :=
  cauchySeq_finset_of_norm_bounded_eventually hg <| Eventually.of_forall h
Cauchy Criterion for Partial Sums with Norm Bounds in Seminormed Groups
Informal description
Let $E$ be a seminormed additive commutative group and let $f \colon \iota \to E$ and $g \colon \iota \to \mathbb{R}$ be functions. If the series $\sum_{i \in \iota} g(i)$ is summable and $\|f(i)\| \leq g(i)$ for all $i \in \iota$, then the sequence of partial sums $\sum_{i \in s} f(i)$, indexed by finite subsets $s \subseteq \iota$, is a Cauchy sequence.
cauchySeq_range_of_norm_bounded theorem
{f : ℕ → E} (g : ℕ → ℝ) (hg : CauchySeq fun n => ∑ i ∈ range n, g i) (hf : ∀ i, ‖f i‖ ≤ g i) : CauchySeq fun n => ∑ i ∈ range n, f i
Full source 
/-- A version of the **direct comparison test** for conditionally convergent series.
See `cauchySeq_finset_of_norm_bounded` for the same statement about absolutely convergent ones. -/
theorem cauchySeq_range_of_norm_bounded {f : ℕ → E} (g : ℕ → ℝ)
    (hg : CauchySeq fun n => ∑ i ∈ range n, g i) (hf : ∀ i, ‖f i‖ ≤ g i) :
    CauchySeq fun n => ∑ i ∈ range n, f i := by
  refine Metric.cauchySeq_iff'.2 fun ε hε => ?_
  refine (Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => ?_
  specialize hg n hn
  rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg ⊢
  calc
    ‖∑ k ∈ Ico N n, f k‖ ≤ ∑ k ∈ _, ‖f k‖ := norm_sum_le _ _
    _ ≤ ∑ k ∈ _, g k := sum_le_sum fun x _ => hf x
    _ ≤ ‖∑ k ∈ _, g k‖ := le_abs_self _
    _ < ε := hg
Cauchy Criterion for Partial Sums with Norm Bounds
Informal description
Let $E$ be a seminormed additive commutative group and let $f \colon \mathbb{N} \to E$ and $g \colon \mathbb{N} \to \mathbb{R}$ be sequences. If the sequence of partial sums $\left(\sum_{i=0}^{n-1} g(i)\right)_{n \in \mathbb{N}}$ is a Cauchy sequence and $\|f(i)\| \leq g(i)$ for all $i \in \mathbb{N}$, then the sequence of partial sums $\left(\sum_{i=0}^{n-1} f(i)\right)_{n \in \mathbb{N}}$ is also a Cauchy sequence.
cauchySeq_finset_of_summable_norm theorem
{f : ι → E} (hf : Summable fun a => ‖f a‖) : CauchySeq fun s : Finset ι => ∑ a ∈ s, f a
Full source 
theorem cauchySeq_finset_of_summable_norm {f : ι → E} (hf : Summable fun a => ‖f a‖) :
    CauchySeq fun s : Finset ι => ∑ a ∈ s, f a :=
  cauchySeq_finset_of_norm_bounded _ hf fun _i => le_rfl
Cauchy Criterion for Partial Sums with Summable Norm in Seminormed Groups
Informal description
Let $E$ be a seminormed additive commutative group and $f \colon \iota \to E$ be a function. If the series $\sum_{a \in \iota} \|f(a)\|$ is summable, then the sequence of partial sums $\sum_{a \in s} f(a)$, indexed by finite subsets $s \subseteq \iota$, is a Cauchy sequence in $E$.
hasSum_of_subseq_of_summable theorem
{f : ι → E} (hf : Summable fun a => ‖f a‖) {s : α → Finset ι} {p : Filter α} [NeBot p] (hs : Tendsto s p atTop) {a : E} (ha : Tendsto (fun b => ∑ i ∈ s b, f i) p (𝓝 a)) : HasSum f a
Full source 
/-- If a function `f` is summable in norm, and along some sequence of finsets exhausting the space
its sum is converging to a limit `a`, then this holds along all finsets, i.e., `f` is summable
with sum `a`. -/
theorem hasSum_of_subseq_of_summable {f : ι → E} (hf : Summable fun a => ‖f a‖) {s : α → Finset ι}
    {p : Filter α} [NeBot p] (hs : Tendsto s p atTop) {a : E}
    (ha : Tendsto (fun b => ∑ i ∈ s b, f i) p (𝓝 a)) : HasSum f a :=
  tendsto_nhds_of_cauchySeq_of_subseq (cauchySeq_finset_of_summable_norm hf) hs ha
Summability via convergence along an exhausting sequence of finite subsets
Informal description
Let $E$ be a seminormed additive commutative group and $f \colon \iota \to E$ a function such that the series $\sum_{a \in \iota} \|f(a)\|$ is summable. Suppose there exists a sequence of finite subsets $s_b \subseteq \iota$ indexed by $\alpha$, tending to $\iota$ along a nontrivial filter $p$, and an element $a \in E$ such that the partial sums $\sum_{i \in s_b} f(i)$ converge to $a$ along $p$. Then $f$ is summable with sum $a$.
hasSum_iff_tendsto_nat_of_summable_norm theorem
{f : ℕ → E} {a : E} (hf : Summable fun i => ‖f i‖) : HasSum f a ↔ Tendsto (fun n : ℕ => ∑ i ∈ range n, f i) atTop (𝓝 a)
Full source 
theorem hasSum_iff_tendsto_nat_of_summable_norm {f : ℕ → E} {a : E} (hf : Summable fun i => ‖f i‖) :
    HasSumHasSum f a ↔ Tendsto (fun n : ℕ => ∑ i ∈ range n, f i) atTop (𝓝 a) :=
  ⟨fun h => h.tendsto_sum_nat, fun h => hasSum_of_subseq_of_summable hf tendsto_finset_range h⟩
Summability Criterion via Partial Sums in Seminormed Groups: $\sum f_i = a \iff \lim_{n\to\infty} \sum_{i=0}^{n-1} f_i = a$ when $\sum \|f_i\|$ converges
Informal description
Let $E$ be a seminormed additive commutative group and $f \colon \mathbb{N} \to E$ a function such that the series $\sum_{i \in \mathbb{N}} \|f(i)\|$ is summable. Then $f$ has sum $a \in E$ if and only if the sequence of partial sums $\sum_{i=0}^{n-1} f(i)$ converges to $a$ as $n \to \infty$.
Summable.of_norm_bounded theorem
[CompleteSpace E] {f : ι → E} (g : ι → ℝ) (hg : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : Summable f
Full source 
/-- The direct comparison test for series:  if the norm of `f` is bounded by a real function `g`
which is summable, then `f` is summable. -/
theorem Summable.of_norm_bounded [CompleteSpace E] {f : ι → E} (g : ι → ℝ) (hg : Summable g)
    (h : ∀ i, ‖f i‖ ≤ g i) : Summable f := by
  rw [summable_iff_cauchySeq_finset]
  exact cauchySeq_finset_of_norm_bounded g hg h
Comparison Test for Summability: $\sum f_i$ is summable when $\|f_i\| \leq g_i$ and $\sum g_i$ is summable
Informal description
Let $E$ be a complete seminormed additive commutative group. Given functions $f \colon \iota \to E$ and $g \colon \iota \to \mathbb{R}$ such that: 1. The series $\sum_{i \in \iota} g(i)$ is summable, 2. $\|f(i)\| \leq g(i)$ for all $i \in \iota$. Then the series $\sum_{i \in \iota} f(i)$ is summable in $E$.
HasSum.norm_le_of_bounded theorem
{f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ} (hf : HasSum f a) (hg : HasSum g b) (h : ∀ i, ‖f i‖ ≤ g i) : ‖a‖ ≤ b
Full source 
theorem HasSum.norm_le_of_bounded {f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ} (hf : HasSum f a)
    (hg : HasSum g b) (h : ∀ i, ‖f i‖ ≤ g i) : ‖a‖ ≤ b := by
  classical exact le_of_tendsto_of_tendsto' hf.norm hg fun _s ↦ norm_sum_le_of_le _ fun i _hi ↦ h i
Norm of Sum Bounded by Sum of Norms in Seminormed Groups
Informal description
Let $E$ be a complete seminormed additive commutative group. Given functions $f \colon \iota \to E$ and $g \colon \iota \to \mathbb{R}$ such that: 1. $f$ has sum $a \in E$ (i.e., $\sum_{i} f_i = a$), 2. $g$ has sum $b \in \mathbb{R}$ (i.e., $\sum_{i} g_i = b$), 3. $\|f_i\| \leq g_i$ for all $i \in \iota$. Then the norm of the sum satisfies $\|a\| \leq b$.
tsum_of_norm_bounded theorem
{f : ι → E} {g : ι → ℝ} {a : ℝ} (hg : HasSum g a) (h : ∀ i, ‖f i‖ ≤ g i) : ‖∑' i : ι, f i‖ ≤ a
Full source 
/-- Quantitative result associated to the direct comparison test for series:  If `∑' i, g i` is
summable, and for all `i`, `‖f i‖ ≤ g i`, then `‖∑' i, f i‖ ≤ ∑' i, g i`. Note that we do not
assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
theorem tsum_of_norm_bounded {f : ι → E} {g : ι → ℝ} {a : ℝ} (hg : HasSum g a)
    (h : ∀ i, ‖f i‖ ≤ g i) : ‖∑' i : ι, f i‖ ≤ a := by
  by_cases hf : Summable f
  · exact hf.hasSum.norm_le_of_bounded hg h
  · rw [tsum_eq_zero_of_not_summable hf, norm_zero]
    classical exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)
Norm of Sum Bounded by Sum of Norms: $\|\sum_{i} f_i\| \leq \sum_{i} g_i$
Informal description
Let $E$ be a seminormed additive commutative group, and let $\{f_i\}_{i \in \iota}$ be a family of elements in $E$ indexed by $\iota$. Suppose $\{g_i\}_{i \in \iota}$ is a family of real numbers such that: 1. The series $\sum_{i \in \iota} g_i$ converges to $a \in \mathbb{R}$, 2. $\|f_i\| \leq g_i$ for all $i \in \iota$. Then the norm of the sum $\sum_{i \in \iota} f_i$ satisfies $\|\sum_{i \in \iota} f_i\| \leq a$.
norm_tsum_le_tsum_norm theorem
{f : ι → E} (hf : Summable fun i => ‖f i‖) : ‖∑' i, f i‖ ≤ ∑' i, ‖f i‖
Full source 
/-- If `∑' i, ‖f i‖` is summable, then `‖∑' i, f i‖ ≤ (∑' i, ‖f i‖)`. Note that we do not assume
that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete space. -/
theorem norm_tsum_le_tsum_norm {f : ι → E} (hf : Summable fun i => ‖f i‖) :
    ‖∑' i, f i‖ ≤ ∑' i, ‖f i‖ :=
  tsum_of_norm_bounded hf.hasSum fun _i => le_rfl
Norm of Sum Bounded by Sum of Norms: $\|\sum_i f_i\| \leq \sum_i \|f_i\|$
Informal description
Let $E$ be a seminormed additive commutative group and $\{f_i\}_{i \in \iota}$ be a family of elements in $E$ such that $\sum_{i \in \iota} \|f_i\|$ is summable. Then the norm of the sum satisfies $\|\sum_{i \in \iota} f_i\| \leq \sum_{i \in \iota} \|f_i\|$.
tsum_of_nnnorm_bounded theorem
{f : ι → E} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : HasSum g a) (h : ∀ i, ‖f i‖₊ ≤ g i) : ‖∑' i : ι, f i‖₊ ≤ a
Full source 
/-- Quantitative result associated to the direct comparison test for series: If `∑' i, g i` is
summable, and for all `i`, `‖f i‖₊ ≤ g i`, then `‖∑' i, f i‖₊ ≤ ∑' i, g i`. Note that we
do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
space. -/
theorem tsum_of_nnnorm_bounded {f : ι → E} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : HasSum g a)
    (h : ∀ i, ‖f i‖₊ ≤ g i) : ‖∑' i : ι, f i‖₊ ≤ a := by
  simp only [← NNReal.coe_le_coe, ← NNReal.hasSum_coe, coe_nnnorm] at *
  exact tsum_of_norm_bounded hg h
Norm of Sum Bounded by Sum of Nonnegative Norms: $\|\sum_{i} f_i\| \leq \sum_{i} g_i$
Informal description
Let $E$ be a seminormed additive commutative group, and let $\{f_i\}_{i \in \iota}$ be a family of elements in $E$ indexed by $\iota$. Suppose $\{g_i\}_{i \in \iota}$ is a family of nonnegative real numbers such that: 1. The series $\sum_{i \in \iota} g_i$ converges to $a \in \mathbb{R}_{\geq 0}$, 2. $\|f_i\| \leq g_i$ for all $i \in \iota$. Then the norm of the sum $\sum_{i \in \iota} f_i$ satisfies $\|\sum_{i \in \iota} f_i\| \leq a$.
nnnorm_tsum_le theorem
{f : ι → E} (hf : Summable fun i => ‖f i‖₊) : ‖∑' i, f i‖₊ ≤ ∑' i, ‖f i‖₊
Full source 
/-- If `∑' i, ‖f i‖₊` is summable, then `‖∑' i, f i‖₊ ≤ ∑' i, ‖f i‖₊`. Note that
we do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
space. -/
theorem nnnorm_tsum_le {f : ι → E} (hf : Summable fun i => ‖f i‖₊) : ‖∑' i, f i‖₊ ≤ ∑' i, ‖f i‖₊ :=
  tsum_of_nnnorm_bounded hf.hasSum fun _i => le_rfl
Nonnegative Norm of Sum Bounded by Sum of Nonnegative Norms: $\|\sum_i f_i\|_{\mathbb{R}_{\geq 0}} \leq \sum_i \|f_i\|_{\mathbb{R}_{\geq 0}}$
Informal description
Let $E$ be a seminormed additive commutative group and $\{f_i\}_{i \in \iota}$ be a family of elements in $E$ such that $\sum_{i \in \iota} \|f_i\|_{\mathbb{R}_{\geq 0}}$ is summable. Then the nonnegative norm of the sum satisfies $\|\sum_{i \in \iota} f_i\|_{\mathbb{R}_{\geq 0}} \leq \sum_{i \in \iota} \|f_i\|_{\mathbb{R}_{\geq 0}}$.
Summable.of_norm_bounded_eventually theorem
{f : ι → E} (g : ι → ℝ) (hg : Summable g) (h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) : Summable f
Full source 
/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
real function `g` which is summable, then `f` is summable. -/
theorem Summable.of_norm_bounded_eventually {f : ι → E} (g : ι → ℝ) (hg : Summable g)
    (h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) : Summable f :=
  summable_iff_cauchySeq_finset.2 <| cauchySeq_finset_of_norm_bounded_eventually hg h
Summability from Eventual Norm Boundedness by a Summable Series
Informal description
Let $E$ be a seminormed additive commutative group, and let $f \colon \iota \to E$ and $g \colon \iota \to \mathbb{R}$ be functions. If the series $\sum_{i \in \iota} g(i)$ is summable and there exists a finite subset $s \subseteq \iota$ such that $\|f(i)\| \leq g(i)$ for all $i \notin s$, then the series $\sum_{i \in \iota} f(i)$ is summable.
Summable.of_norm_bounded_eventually_nat theorem
{f : ℕ → E} (g : ℕ → ℝ) (hg : Summable g) (h : ∀ᶠ i in atTop, ‖f i‖ ≤ g i) : Summable f
Full source 
/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
real function `g` which is summable, then `f` is summable. -/
theorem Summable.of_norm_bounded_eventually_nat {f : ℕ → E} (g : ℕ → ℝ) (hg : Summable g)
    (h : ∀ᶠ i in atTop, ‖f i‖ ≤ g i) : Summable f :=
  .of_norm_bounded_eventually g hg <| Nat.cofinite_eq_atTop ▸ h
Summability of Natural-Indexed Series via Eventual Norm Boundedness
Informal description
Let $E$ be a seminormed additive commutative group, and let $f \colon \mathbb{N} \to E$ and $g \colon \mathbb{N} \to \mathbb{R}$ be sequences. If the series $\sum_{i=0}^\infty g(i)$ is summable and there exists $N \in \mathbb{N}$ such that $\|f(i)\| \leq g(i)$ for all $i \geq N$, then the series $\sum_{i=0}^\infty f(i)$ is summable.
Summable.of_nnnorm_bounded theorem
{f : ι → E} (g : ι → ℝ≥0) (hg : Summable g) (h : ∀ i, ‖f i‖₊ ≤ g i) : Summable f
Full source 
theorem Summable.of_nnnorm_bounded {f : ι → E} (g : ι → ℝ≥0) (hg : Summable g)
    (h : ∀ i, ‖f i‖₊ ≤ g i) : Summable f :=
  .of_norm_bounded (fun i => (g i : ℝ)) (NNReal.summable_coe.2 hg) h
Summability via Nonnegative Norm Boundedness
Informal description
Let $E$ be a complete seminormed additive commutative group. Given functions $f \colon \iota \to E$ and $g \colon \iota \to \mathbb{R}_{\geq 0}$ such that: 1. The series $\sum_{i \in \iota} g(i)$ is summable, 2. $\|f(i)\| \leq g(i)$ for all $i \in \iota$. Then the series $\sum_{i \in \iota} f(i)$ is summable in $E$.
Summable.of_norm theorem
{f : ι → E} (hf : Summable fun a => ‖f a‖) : Summable f
Full source 
theorem Summable.of_norm {f : ι → E} (hf : Summable fun a => ‖f a‖) : Summable f :=
  .of_norm_bounded _ hf fun _i => le_rfl
Summability via Absolute Summability in Seminormed Groups
Informal description
Let $E$ be a complete seminormed additive commutative group and $f \colon \iota \to E$ a function. If the series $\sum_{a \in \iota} \|f(a)\|$ is summable, then the series $\sum_{a \in \iota} f(a)$ is summable in $E$.
Summable.of_nnnorm theorem
{f : ι → E} (hf : Summable fun a => ‖f a‖₊) : Summable f
Full source 
theorem Summable.of_nnnorm {f : ι → E} (hf : Summable fun a => ‖f a‖₊) : Summable f :=
  .of_nnnorm_bounded _ hf fun _i => le_rfl
Summability via Nonnegative Norm Summability in Seminormed Groups
Informal description
Let $E$ be a complete seminormed additive commutative group and $f \colon \iota \to E$ a function. If the series $\sum_{a \in \iota} \|f(a)\|$ is summable (where $\|\cdot\|$ denotes the seminorm on $E$), then the series $\sum_{a \in \iota} f(a)$ is summable in $E$.