Series in real Banach spaces

Content created by Louis Wasserman.

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

module analysis.series-real-banach-spaces where
Imports 
open import analysis.metric-abelian-groups-normed-real-vector-spaces
open import analysis.series-metric-abelian-groups

open import foundation.universe-levels

open import linear-algebra.real-banach-spaces

open import lists.sequences

Idea

A series is a series in the metric abelian group associated with the underlying normed real vector space.

Definition

module _
  {l1 l2 : Level}
  (V : ℝ-Banach-Space l1 l2)
  where

  series-ℝ-Banach-Space : UU l2
  series-ℝ-Banach-Space =
    series-Metric-Ab
      ( metric-ab-Normed-ℝ-Vector-Space (normed-vector-space-ℝ-Banach-Space V))

  series-terms-ℝ-Banach-Space :
    sequence (type-ℝ-Banach-Space V) → series-ℝ-Banach-Space
  series-terms-ℝ-Banach-Space = series-terms-Metric-Ab

  term-series-ℝ-Banach-Space :
    series-ℝ-Banach-Space → sequence (type-ℝ-Banach-Space V)
  term-series-ℝ-Banach-Space = term-series-Metric-Ab

  partial-sum-series-ℝ-Banach-Space :
    series-ℝ-Banach-Space → sequence (type-ℝ-Banach-Space V)
  partial-sum-series-ℝ-Banach-Space = partial-sum-series-Metric-Ab

Recent changes