Absolute convergence of series in the real numbers

Content created by Louis Wasserman.

Created on 2026-04-30.
Last modified on 2026-04-30.

module real-analysis.absolute-convergence-series-real-numbers where
Imports 
open import foundation.function-types
open import foundation.propositions
open import foundation.universe-levels

open import functional-analysis.absolute-convergence-series-real-banach-spaces
open import functional-analysis.convergent-series-real-banach-spaces
open import functional-analysis.real-banach-spaces
open import functional-analysis.series-real-banach-spaces

open import real-analysis.convergent-series-real-numbers
open import real-analysis.series-real-numbers

open import real-numbers.absolute-value-real-numbers

Idea

A series Σ aₙ of real numbers is said to absolutely converge if the series of absolute values Σ |aₙ| converges.

Definition

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

  is-absolutely-convergent-prop-series-ℝ : Prop (lsuc l)
  is-absolutely-convergent-prop-series-ℝ =
    is-convergent-prop-series-ℝ (map-abs-series-ℝ σ)

  is-absolutely-convergent-series-ℝ : UU (lsuc l)
  is-absolutely-convergent-series-ℝ =
    type-Prop is-absolutely-convergent-prop-series-ℝ

Properties

If a series of real numbers is absolutely convergent, it is convergent

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

  is-convergent-is-absolutely-convergent-series-ℝ :
    is-absolutely-convergent-series-ℝ σ →
    is-convergent-series-ℝ σ
  is-convergent-is-absolutely-convergent-series-ℝ H =
    is-convergent-real-is-convergent-real-banach-space-ℝ
      ( term-series-ℝ σ)
      ( is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space
        ( real-banach-space-ℝ l)
        ( series-terms-ℝ-Banach-Space
          ( real-banach-space-ℝ l)
          ( term-series-ℝ σ))
        ( H))

See also

Recent changes