Convergent series in the real numbers

Content created by Louis Wasserman.

Created on 2025-12-03.
Last modified on 2025-12-03.

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

open import foundation.propositions
open import foundation.universe-levels

open import real-numbers.cauchy-sequences-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.metric-additive-group-of-real-numbers

Idea

A series of real numbers is convergent if its sequence of partial sums converges in the metric space of real numbers.

Definition

module _
  {l : Level}
  (σ : series-ℝ l)
  where

  is-sum-prop-series-ℝ : ℝ l → Prop l
  is-sum-prop-series-ℝ = is-sum-prop-series-Metric-Ab σ

  is-sum-series-ℝ : ℝ l → UU l
  is-sum-series-ℝ = is-sum-series-Metric-Ab σ

  is-convergent-prop-series-ℝ : Prop (lsuc l)
  is-convergent-prop-series-ℝ =
    is-convergent-prop-series-Metric-Ab σ

  is-convergent-series-ℝ : UU (lsuc l)
  is-convergent-series-ℝ = is-convergent-series-Metric-Ab σ

Properties

If the partial sums of a series form a Cauchy sequence, the series converges

module _
  {l : Level}
  (σ : series-ℝ l)
  where

  is-convergent-is-cauchy-sequence-partial-sum-series-ℝ :
    is-cauchy-sequence-ℝ (partial-sum-series-ℝ σ) →
    is-convergent-series-ℝ σ
  is-convergent-is-cauchy-sequence-partial-sum-series-ℝ =
    is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab
      ( complete-metric-ab-add-ℝ l)
      ( σ)

Recent changes