Convergent series in metric abelian groups

Content created by Fredrik Bakke and Louis Wasserman.

Created on 2025-09-03.
Last modified on 2025-09-24.

module analysis.convergent-series-metric-abelian-groups where
Imports 
open import analysis.metric-abelian-groups
open import analysis.series-metric-abelian-groups

open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import lists.sequences

open import metric-spaces.convergent-sequences-metric-spaces
open import metric-spaces.limits-of-sequences-metric-spaces

Idea

A series in a metric abelian group is convergent if its sequence of partial sums converges in the associated metric space.

Definition

module _
  {l1 l2 : Level} (G : Metric-Ab l1 l2) (σ : series-Metric-Ab G)
  where

  is-convergent-prop-series-Metric-Ab : Prop (l1 ⊔ l2)
  is-convergent-prop-series-Metric-Ab =
    subtype-convergent-sequence-Metric-Space
      ( metric-space-Metric-Ab G)
      ( partial-sum-series-Metric-Ab G σ)

  is-convergent-series-Metric-Ab : UU (l1 ⊔ l2)
  is-convergent-series-Metric-Ab =
    type-Prop is-convergent-prop-series-Metric-Ab

convergent-series-Metric-Ab :
  {l1 l2 : Level} (G : Metric-Ab l1 l2) → UU (l1 ⊔ l2)
convergent-series-Metric-Ab G =
  type-subtype (is-convergent-prop-series-Metric-Ab G)

Properties

module _
  {l1 l2 : Level} (G : Metric-Ab l1 l2) (σ : convergent-series-Metric-Ab G)
  where

  series-convergent-series-Metric-Ab : series-Metric-Ab G
  series-convergent-series-Metric-Ab = pr1 σ

  partial-sum-convergent-series-Metric-Ab : sequence (type-Metric-Ab G)
  partial-sum-convergent-series-Metric-Ab =
    partial-sum-series-Metric-Ab G series-convergent-series-Metric-Ab

The partial sums of a convergent series have a limit, the sum of the series

module _
  {l1 l2 : Level} (G : Metric-Ab l1 l2) (σ : convergent-series-Metric-Ab G)
  where

  has-limit-partial-sum-convergent-series-Metric-Ab :
    has-limit-sequence-Metric-Space
      ( metric-space-Metric-Ab G)
      ( partial-sum-convergent-series-Metric-Ab G σ)
  has-limit-partial-sum-convergent-series-Metric-Ab =
    pr2 σ

  sum-convergent-series-Metric-Ab : type-Metric-Ab G
  sum-convergent-series-Metric-Ab =
    limit-has-limit-sequence-Metric-Space
      ( metric-space-Metric-Ab G)
      ( partial-sum-convergent-series-Metric-Ab G σ)
      ( has-limit-partial-sum-convergent-series-Metric-Ab)

  is-limit-partial-sum-convergent-series-Metric-Ab :
    is-limit-sequence-Metric-Space
      ( metric-space-Metric-Ab G)
      ( partial-sum-convergent-series-Metric-Ab G σ)
      ( sum-convergent-series-Metric-Ab)
  is-limit-partial-sum-convergent-series-Metric-Ab =
    is-limit-limit-has-limit-sequence-Metric-Space
      ( metric-space-Metric-Ab G)
      ( partial-sum-convergent-series-Metric-Ab G σ)
      ( has-limit-partial-sum-convergent-series-Metric-Ab)

Recent changes