Series in the real numbers

Content created by Louis Wasserman.

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

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

open import foundation.universe-levels

open import lists.sequences

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

Idea

A series in the real numbers is a series in the metric additive group of real numbers.

Definition

series-ℝ : (l : Level) → UU (lsuc l)
series-ℝ l = series-Complete-Metric-Ab (complete-metric-ab-add-ℝ l)

series-terms-ℝ : {l : Level} → sequence (ℝ l) → series-ℝ l
series-terms-ℝ = series-terms-Metric-Ab

term-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l)
term-series-ℝ = term-series-Metric-Ab

partial-sum-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l)
partial-sum-series-ℝ {l} = partial-sum-series-Metric-Ab

Recent changes