diff --git a/src/analysis.lagda.md b/src/analysis.lagda.md
index 8790cf7fd6..48e6e3c438 100644
--- a/src/analysis.lagda.md
+++ b/src/analysis.lagda.md
@@ -3,7 +3,10 @@
 ```agda
 module analysis where
 
+open import analysis.absolute-convergence-series-real-banach-spaces public
+open import analysis.absolute-convergence-series-real-numbers public
 open import analysis.additive-complete-metric-abelian-groups-real-banach-spaces public
+open import analysis.comparison-test-series-real-numbers public
 open import analysis.complete-metric-abelian-groups public
 open import analysis.convergent-series-complete-metric-abelian-groups public
 open import analysis.convergent-series-metric-abelian-groups public
@@ -12,6 +15,8 @@ open import analysis.convergent-series-real-numbers public
 open import analysis.derivatives-of-real-functions-on-proper-closed-intervals public
 open import analysis.metric-abelian-groups public
 open import analysis.metric-abelian-groups-normed-real-vector-spaces public
+open import analysis.ratio-test-series-real-banach-spaces public
+open import analysis.ratio-test-series-real-numbers public
 open import analysis.series-complete-metric-abelian-groups public
 open import analysis.series-metric-abelian-groups public
 open import analysis.series-real-banach-spaces public
diff --git a/src/analysis/absolute-convergence-series-real-banach-spaces.lagda.md b/src/analysis/absolute-convergence-series-real-banach-spaces.lagda.md
new file mode 100644
index 0000000000..b85da50b37
--- /dev/null
+++ b/src/analysis/absolute-convergence-series-real-banach-spaces.lagda.md
@@ -0,0 +1,203 @@
+# Absolute convergence of series in real Banach spaces
+
+```agda
+module analysis.absolute-convergence-series-real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.convergent-series-real-banach-spaces
+open import analysis.convergent-series-real-numbers
+open import analysis.series-real-banach-spaces
+open import analysis.series-real-numbers
+
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.positive-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+open import linear-algebra.sums-of-finite-sequences-of-elements-real-banach-spaces
+
+open import metric-spaces.cauchy-sequences-metric-spaces
+
+open import order-theory.large-posets
+
+open import real-numbers.cauchy-sequences-real-numbers
+open import real-numbers.difference-real-numbers
+open import real-numbers.distance-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.rational-real-numbers
+```
+
+</details>
+
+## Idea
+
+A [series](analysis.series-real-banach-spaces.md) `Σ aₙ` in a
+[real Banach space](linear-algebra.real-banach-spaces.md) is said to
+{{#concept "absolutely converge" WDID=Q332465 WD="absolute convergence" Agda=is-absolutely-convergent-prop-series-ℝ-Banach-Space Disambiguation="series in a real Banach space"}}
+if the series of norms `Σ ∥aₙ∥` is a
+[convergent series](analysis.convergent-series-real-numbers.md) of
+[real numbers](real-numbers.dedekind-real-numbers.md).
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  is-absolutely-convergent-prop-series-ℝ-Banach-Space : Prop (lsuc l1)
+  is-absolutely-convergent-prop-series-ℝ-Banach-Space =
+    is-convergent-prop-series-ℝ (map-norm-series-ℝ-Banach-Space V σ)
+
+  is-absolutely-convergent-series-ℝ-Banach-Space : UU (lsuc l1)
+  is-absolutely-convergent-series-ℝ-Banach-Space =
+    type-Prop is-absolutely-convergent-prop-series-ℝ-Banach-Space
+```
+
+## Properties
+
+### A Cauchy modulus for the sequence of partial sums of norms of terms in a series is a Cauchy modulus for the series
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  (M :
+    is-cauchy-sequence-ℝ
+      ( partial-sum-series-ℝ (map-norm-series-ℝ-Banach-Space V σ)))
+  where
+
+  abstract
+    neighborhood-add-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space :
+      (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (pr1 (M ε)) n →
+      neighborhood-ℝ-Banach-Space
+        ( V)
+        ( ε)
+        ( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ k))
+        ( partial-sum-series-ℝ-Banach-Space V σ n)
+    neighborhood-add-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space
+      ε n k με≤n =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+      in
+        chain-of-inequalities
+        dist-ℝ-Banach-Space V
+          ( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ k))
+          ( partial-sum-series-ℝ-Banach-Space V σ n)
+        ≤ map-norm-ℝ-Banach-Space V
+            ( partial-sum-series-ℝ-Banach-Space V
+              ( drop-series-ℝ-Banach-Space V n σ)
+              ( k))
+          by
+            leq-eq-ℝ
+              ( ap
+                ( map-norm-ℝ-Banach-Space V)
+                ( inv (partial-sum-drop-series-ℝ-Banach-Space V n σ k)))
+        ≤ partial-sum-series-ℝ
+            ( map-norm-series-ℝ-Banach-Space V
+              ( drop-series-ℝ-Banach-Space V n σ))
+            ( k)
+          by
+            triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space
+              ( V)
+              ( k)
+              ( _)
+        ≤ ( partial-sum-series-ℝ
+            ( map-norm-series-ℝ-Banach-Space V σ)
+            ( n +ℕ k)) -ℝ
+          ( partial-sum-series-ℝ (map-norm-series-ℝ-Banach-Space V σ) n)
+          by
+            leq-eq-ℝ
+              ( partial-sum-drop-series-ℝ
+                ( n)
+                ( map-norm-series-ℝ-Banach-Space V σ)
+                ( k))
+        ≤ dist-ℝ
+            ( partial-sum-series-ℝ
+              ( map-norm-series-ℝ-Banach-Space V σ)
+              ( n +ℕ k))
+            ( partial-sum-series-ℝ
+              ( map-norm-series-ℝ-Banach-Space V σ)
+              ( n))
+          by leq-diff-dist-ℝ _ _
+        ≤ real-ℚ⁺ ε
+          by
+            leq-dist-neighborhood-ℝ
+              ( ε)
+              ( _)
+              ( _)
+              ( pr2
+                ( M ε)
+                ( n +ℕ k)
+                ( n)
+                ( transitive-leq-ℕ (pr1 (M ε)) n (n +ℕ k) (leq-add-ℕ n k) με≤n)
+                ( με≤n))
+
+    is-cauchy-partial-sum-is-cauchy-partial-sum-norm-series-ℝ-Banach-Space :
+      is-cauchy-sequence-Metric-Space
+        ( metric-space-ℝ-Banach-Space V)
+        ( partial-sum-series-ℝ-Banach-Space V σ)
+    is-cauchy-partial-sum-is-cauchy-partial-sum-norm-series-ℝ-Banach-Space =
+      is-cauchy-sequence-modulus-neighborhood-add-sequence-Metric-Space
+        ( metric-space-ℝ-Banach-Space V)
+        ( partial-sum-series-ℝ-Banach-Space V σ)
+        ( pr1 ∘ M)
+        ( neighborhood-add-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space)
+```
+
+### If a series is absolutely convergent, it is convergent
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space :
+    is-absolutely-convergent-series-ℝ-Banach-Space V σ →
+    is-convergent-series-ℝ-Banach-Space V σ
+  is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space (lim-Σnorm , H) =
+    let
+      open
+        do-syntax-trunc-Prop
+          ( is-convergent-prop-series-ℝ-Banach-Space V σ)
+    in do
+      cauchy-mod ←
+        exists-cauchy-modulus-has-limit-sequence-ℝ
+          ( partial-sum-series-ℝ (map-norm-series-ℝ-Banach-Space V σ))
+          ( lim-Σnorm , H)
+      is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space
+        ( V)
+        ( σ)
+        ( is-cauchy-partial-sum-is-cauchy-partial-sum-norm-series-ℝ-Banach-Space
+          ( V)
+          ( σ)
+          ( cauchy-mod))
+```
+
+## See also
+
+- [Absolute convergence of series of real numbers](analysis.absolute-convergence-series-real-numbers.md)
+
+## External links
+
+- [Absolute convergence of series in Banach spaces](https://en.wikipedia.org/wiki/Absolute_convergence#Proof_that_any_absolutely_convergent_series_in_a_Banach_space_is_convergent)
+  on Wikipedia
diff --git a/src/analysis/absolute-convergence-series-real-numbers.lagda.md b/src/analysis/absolute-convergence-series-real-numbers.lagda.md
new file mode 100644
index 0000000000..309cbb81ea
--- /dev/null
+++ b/src/analysis/absolute-convergence-series-real-numbers.lagda.md
@@ -0,0 +1,80 @@
+# Absolute convergence of series in the real numbers
+
+```agda
+module analysis.absolute-convergence-series-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.absolute-convergence-series-real-banach-spaces
+open import analysis.convergent-series-real-banach-spaces
+open import analysis.convergent-series-real-numbers
+open import analysis.series-real-banach-spaces
+open import analysis.series-real-numbers
+
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+```
+
+</details>
+
+## Idea
+
+A [series](analysis.series-real-numbers.md) `Σ aₙ` of
+[real numbers](real-numbers.dedekind-real-numbers.md) is said to
+{{#concept "absolutely converge" WDID=Q332465 WD="absolute convergence" Agda=is-absolutely-convergent-prop-series-ℝ Disambiguation="series of real numbers"}}
+if the series of absolute values `Σ |aₙ|`
+[converges](analysis.convergent-series-real-numbers.md).
+
+## Definition
+
+```agda
+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
+
+```agda
+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
+
+- [Absolute convergence of series in real Banach spaces](analysis.absolute-convergence-series-real-banach-spaces.md)
+
+## External links
+
+- [Absolute convergence](https://en.wikipedia.org/wiki/Absolute_convergence) on
+  Wikipedia
diff --git a/src/analysis/comparison-test-series-real-numbers.lagda.md b/src/analysis/comparison-test-series-real-numbers.lagda.md
new file mode 100644
index 0000000000..dbc9581cb5
--- /dev/null
+++ b/src/analysis/comparison-test-series-real-numbers.lagda.md
@@ -0,0 +1,199 @@
+# Comparison test for series in the real numbers
+
+```agda
+module analysis.comparison-test-series-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.convergent-series-real-numbers
+open import analysis.series-real-numbers
+
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-transport
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import metric-spaces.cauchy-sequences-metric-spaces
+
+open import order-theory.large-posets
+
+open import real-numbers.difference-real-numbers
+open import real-numbers.distance-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.nonnegative-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.sums-of-finite-sequences-of-real-numbers
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+A [series](analysis.series-real-numbers.md) `∑ aₙ` of
+[nonnegative](real-numbers.nonnegative-real-numbers.md)
+[real numbers](real-numbers.dedekind-real-numbers.md)
+[converges](analysis.convergent-series-real-numbers.md) if there
+[exists](foundation.existential-quantification.md) a convergent series `∑ bₙ`
+such that `aₙ ≤ bₙ` for all `n`.
+
+## Definition
+
+```agda
+module _
+  {l1 : Level}
+  (l2 : Level)
+  (σ : series-ℝ l1)
+  where
+
+  comparison-test-prop-series-ℝ : Prop (l1 ⊔ lsuc l2)
+  comparison-test-prop-series-ℝ =
+    ( is-nonnegative-prop-series-ℝ σ) ∧
+    ( ∃
+      ( convergent-series-ℝ l2)
+      ( λ τ →
+        Π-Prop
+          ( ℕ)
+          ( λ n →
+            leq-prop-ℝ (term-series-ℝ σ n) (term-convergent-series-ℝ τ n))))
+
+  comparison-test-series-ℝ : UU (l1 ⊔ lsuc l2)
+  comparison-test-series-ℝ =
+    type-Prop comparison-test-prop-series-ℝ
+```
+
+## Properties
+
+### The comparison test implies convergence
+
+```agda
+module _
+  {l1 l2 : Level}
+  (σ : series-ℝ l1)
+  (τ : convergent-series-ℝ l2)
+  where
+
+  abstract
+    is-convergent-is-nonnegative-is-bounded-by-convergent-series-ℝ :
+      ((n : ℕ) → is-nonnegative-ℝ (term-series-ℝ σ n)) →
+      ((n : ℕ) → leq-ℝ (term-series-ℝ σ n) (term-convergent-series-ℝ τ n)) →
+      is-convergent-series-ℝ σ
+    is-convergent-is-nonnegative-is-bounded-by-convergent-series-ℝ 0≤σₙ σₙ≤τₙ =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+        open do-syntax-trunc-Prop (is-convergent-prop-series-ℝ σ)
+      in do
+        lim-modulus-τ ← is-sum-sum-convergent-series-ℝ τ
+        let
+          cauchy-mod-partial-sum-τ =
+            is-cauchy-has-limit-modulus-sequence-Metric-Space
+              ( metric-space-ℝ l2)
+              ( partial-sum-convergent-series-ℝ τ)
+              ( sum-convergent-series-ℝ τ)
+              ( lim-modulus-τ)
+          μ = pr1 ∘ cauchy-mod-partial-sum-τ
+          is-mod-μ = pr2 ∘ cauchy-mod-partial-sum-τ
+          is-mod'-μ ε n k με≤n =
+            neighborhood-dist-ℝ ε _ _
+              ( leq-dist-leq-diff-ℝ _ _ _
+                ( chain-of-inequalities
+                  partial-sum-series-ℝ σ (n +ℕ k) -ℝ partial-sum-series-ℝ σ n
+                  ≤ partial-sum-series-ℝ (drop-series-ℝ n σ) k
+                    by leq-eq-ℝ (inv (partial-sum-drop-series-ℝ n σ k))
+                  ≤ partial-sum-series-ℝ
+                      ( drop-series-ℝ n (series-convergent-series-ℝ τ))
+                      ( k)
+                    by
+                      leq-sum-fin-sequence-ℝ k _ _
+                        ( λ m → σₙ≤τₙ (n +ℕ nat-Fin k m))
+                  ≤ ( partial-sum-convergent-series-ℝ τ (n +ℕ k)) -ℝ
+                    ( partial-sum-convergent-series-ℝ τ n)
+                    by
+                      leq-eq-ℝ
+                        ( partial-sum-drop-series-ℝ
+                          ( n)
+                          ( series-convergent-series-ℝ τ)
+                          ( k))
+                  ≤ dist-ℝ
+                      ( partial-sum-convergent-series-ℝ τ (n +ℕ k))
+                      ( partial-sum-convergent-series-ℝ τ n)
+                    by leq-diff-dist-ℝ _ _
+                  ≤ real-ℚ⁺ ε
+                    by
+                      leq-dist-neighborhood-ℝ ε _ _
+                        ( is-mod-μ
+                          ( ε)
+                          ( n +ℕ k)
+                          ( n)
+                          ( transitive-leq-ℕ
+                            ( μ ε)
+                            ( n)
+                            ( n +ℕ k)
+                            ( leq-add-ℕ n k)
+                            ( με≤n))
+                          ( με≤n)))
+                ( transitive-leq-ℝ
+                  ( partial-sum-series-ℝ σ n -ℝ partial-sum-series-ℝ σ (n +ℕ k))
+                  ( zero-ℝ)
+                  ( real-ℚ⁺ ε)
+                  ( is-nonnegative-real-ℝ⁰⁺ (nonnegative-real-ℚ⁺ ε))
+                  ( binary-tr
+                    ( leq-ℝ)
+                    ( distributive-neg-diff-ℝ _ _)
+                    ( neg-zero-ℝ)
+                    ( neg-leq-ℝ
+                      ( is-nonnegative-diff-leq-ℝ
+                        ( is-monotonic-partial-sum-is-nonnegative-term-series-ℝ
+                          ( σ)
+                          ( 0≤σₙ)
+                          ( n)
+                          ( n +ℕ k)
+                          ( leq-add-ℕ n k)))))))
+        is-convergent-is-cauchy-sequence-partial-sum-series-ℝ
+          σ
+          ( λ ε →
+            ( μ ε ,
+              is-cauchy-modulus-is-cauchy-modulus-sequence-Metric-Space'
+                ( metric-space-ℝ l1)
+                ( partial-sum-series-ℝ σ)
+                ( ε)
+                ( μ ε)
+                ( is-mod'-μ ε)))
+
+module _
+  {l1 l2 : Level}
+  (σ : series-ℝ l1)
+  where
+
+  is-convergent-comparison-test-series-ℝ :
+    {l2 : Level} → comparison-test-series-ℝ l2 σ → is-convergent-series-ℝ σ
+  is-convergent-comparison-test-series-ℝ (0≤σₙ , ∃τ) =
+    rec-trunc-Prop
+      ( is-convergent-prop-series-ℝ σ)
+      ( λ (τ , σₙ≤τₙ) →
+        is-convergent-is-nonnegative-is-bounded-by-convergent-series-ℝ
+          ( σ)
+          ( τ)
+          ( 0≤σₙ)
+          ( σₙ≤τₙ))
+      ( ∃τ)
+```
+
+## External links
+
+- [Direct comparison test](https://en.wikipedia.org/wiki/Direct_comparison_test)
+  on Wikipedia
diff --git a/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md b/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md
index a2f53f1cf5..756e56a460 100644
--- a/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md
+++ b/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md
@@ -14,6 +14,7 @@ open import analysis.series-complete-metric-abelian-groups
 open import foundation.dependent-pair-types
 open import foundation.inhabited-types
 open import foundation.propositions
+open import foundation.subtypes
 open import foundation.universe-levels
 
 open import metric-spaces.cauchy-sequences-complete-metric-spaces
@@ -55,6 +56,11 @@ module _
 
   is-convergent-series-Complete-Metric-Ab : UU (l1 ⊔ l2)
   is-convergent-series-Complete-Metric-Ab = is-convergent-series-Metric-Ab σ
+
+convergent-series-Complete-Metric-Ab :
+  {l1 l2 : Level} (G : Complete-Metric-Ab l1 l2) → UU (l1 ⊔ l2)
+convergent-series-Complete-Metric-Ab G =
+  type-subtype (is-convergent-prop-series-Complete-Metric-Ab G)
 ```
 
 ## Properties
diff --git a/src/analysis/convergent-series-metric-abelian-groups.lagda.md b/src/analysis/convergent-series-metric-abelian-groups.lagda.md
index d78cf2b8bd..30673b9085 100644
--- a/src/analysis/convergent-series-metric-abelian-groups.lagda.md
+++ b/src/analysis/convergent-series-metric-abelian-groups.lagda.md
@@ -10,9 +10,19 @@ module analysis.convergent-series-metric-abelian-groups where
 open import analysis.metric-abelian-groups
 open import analysis.series-metric-abelian-groups
 
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
 open import foundation.dependent-pair-types
+open import foundation.functoriality-propositional-truncation
+open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.propositions
 open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import lists.sequences
@@ -79,7 +89,7 @@ module _
     partial-sum-series-Metric-Ab series-convergent-series-Metric-Ab
 ```
 
-## The partial sums of a convergent series have a limit, the sum of the series
+### The partial sums of a convergent series have a limit, the sum of the series
 
 ```agda
 module _
@@ -111,3 +121,79 @@ module _
       ( partial-sum-convergent-series-Metric-Ab G σ)
       ( has-limit-partial-sum-convergent-series-Metric-Ab)
 ```
+
+### A series converges if and only if it converges after dropping a finite number of terms
+
+```agda
+module _
+  {l1 l2 : Level}
+  {G : Metric-Ab l1 l2}
+  (σ : series-Metric-Ab G)
+  (k : ℕ)
+  where
+
+  is-convergent-is-convergent-drop-series-ℝ :
+    is-convergent-series-Metric-Ab (drop-series-Metric-Ab k σ) →
+    is-convergent-series-Metric-Ab σ
+  is-convergent-is-convergent-drop-series-ℝ (lim-drop , is-lim-drop) =
+    ( add-Metric-Ab G (partial-sum-series-Metric-Ab σ k) lim-drop ,
+      map-trunc-Prop
+        ( λ (μ , is-mod-μ) →
+          ( ( λ ε → μ ε +ℕ k) ,
+            ( λ ε n με+k≤n →
+              let
+                (l , l+k=n) =
+                  subtraction-leq-ℕ
+                    ( k)
+                    ( n)
+                    ( transitive-leq-ℕ
+                      ( k)
+                      ( μ ε +ℕ k)
+                      ( n)
+                      ( με+k≤n)
+                      ( leq-add-ℕ' k (μ ε)))
+              in
+                tr
+                  ( λ x → neighborhood-Metric-Ab G ε x _)
+                  ( equational-reasoning
+                    add-Metric-Ab G
+                      ( partial-sum-series-Metric-Ab σ k)
+                      ( partial-sum-series-Metric-Ab
+                        ( drop-series-Metric-Ab k σ)
+                        ( l))
+                    ＝
+                      add-Metric-Ab G
+                        ( partial-sum-series-Metric-Ab σ k)
+                        ( diff-Metric-Ab G
+                          ( partial-sum-series-Metric-Ab σ (k +ℕ l))
+                          ( partial-sum-series-Metric-Ab σ k))
+                      by
+                        ap-add-Metric-Ab G
+                          ( refl)
+                          ( partial-sum-drop-series-Metric-Ab k σ l)
+                    ＝ partial-sum-series-Metric-Ab σ (k +ℕ l)
+                      by is-identity-right-conjugation-Metric-Ab G _ _
+                    ＝ partial-sum-series-Metric-Ab σ n
+                      by
+                        ap
+                          ( partial-sum-series-Metric-Ab σ)
+                          ( commutative-add-ℕ k l ∙ l+k=n))
+                  ( forward-implication
+                    ( is-isometry-add-Metric-Ab
+                      ( G)
+                      ( partial-sum-series-Metric-Ab σ k)
+                      ( ε)
+                      ( partial-sum-series-Metric-Ab
+                        ( drop-series-Metric-Ab k σ)
+                        ( l))
+                      ( lim-drop))
+                      ( is-mod-μ
+                        ( ε)
+                        ( l)
+                        ( reflects-leq-left-add-ℕ
+                          ( k)
+                          ( μ ε)
+                          ( l)
+                          ( inv-tr (leq-ℕ (μ ε +ℕ k)) l+k=n με+k≤n)))))))
+        ( is-lim-drop))
+```
diff --git a/src/analysis/convergent-series-real-banach-spaces.lagda.md b/src/analysis/convergent-series-real-banach-spaces.lagda.md
index b553a4c38d..f790c49f26 100644
--- a/src/analysis/convergent-series-real-banach-spaces.lagda.md
+++ b/src/analysis/convergent-series-real-banach-spaces.lagda.md
@@ -10,16 +10,32 @@ module analysis.convergent-series-real-banach-spaces where
 open import analysis.additive-complete-metric-abelian-groups-real-banach-spaces
 open import analysis.convergent-series-complete-metric-abelian-groups
 open import analysis.convergent-series-metric-abelian-groups
+open import analysis.convergent-series-real-numbers
 open import analysis.series-real-banach-spaces
+open import analysis.series-real-numbers
 
 open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.inhabited-types
+open import foundation.logical-equivalences
 open import foundation.propositions
+open import foundation.subtypes
 open import foundation.universe-levels
 
+open import linear-algebra.normed-real-vector-spaces
 open import linear-algebra.real-banach-spaces
 
+open import lists.sequences
+
 open import metric-spaces.cauchy-sequences-metric-spaces
+open import metric-spaces.limits-of-sequences-metric-spaces
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.distance-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.sums-of-finite-sequences-of-real-numbers
+
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -56,6 +72,11 @@ module _
 
   is-convergent-series-ℝ-Banach-Space : UU (l1 ⊔ l2)
   is-convergent-series-ℝ-Banach-Space = is-convergent-series-Metric-Ab σ
+
+convergent-series-ℝ-Banach-Space :
+  {l1 l2 : Level} (V : ℝ-Banach-Space l1 l2) → UU (l1 ⊔ l2)
+convergent-series-ℝ-Banach-Space V =
+  type-subtype (is-convergent-prop-series-ℝ-Banach-Space V)
 ```
 
 ## Properties
@@ -80,6 +101,45 @@ module _
       ( σ)
 ```
 
+### A series in the real Banach space of real numbers converges if and only if its corresponding series of real numbers converges
+
+```agda
+module _
+  {l : Level}
+  (σ : sequence (ℝ l))
+  where
+
+  is-convergent-real-is-convergent-real-banach-space-ℝ :
+    is-convergent-series-ℝ-Banach-Space
+      ( real-banach-space-ℝ l)
+      ( series-terms-ℝ-Banach-Space (real-banach-space-ℝ l) σ) →
+    is-convergent-series-ℝ (series-terms-ℝ σ)
+  is-convergent-real-is-convergent-real-banach-space-ℝ (lim , is-lim) =
+    ( lim ,
+      preserves-limits-sequence-isometry-Metric-Space
+        ( metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l))
+        ( metric-space-ℝ l)
+        ( id , λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y))
+        ( λ n → sum-fin-sequence-ℝ n (σ ∘ nat-Fin n))
+        ( lim)
+        ( is-lim))
+
+  is-convergent-real-banach-space-is-convergent-ℝ :
+    is-convergent-series-ℝ (series-terms-ℝ σ) →
+    is-convergent-series-ℝ-Banach-Space
+      ( real-banach-space-ℝ l)
+      ( series-terms-ℝ-Banach-Space (real-banach-space-ℝ l) σ)
+  is-convergent-real-banach-space-is-convergent-ℝ (lim , is-lim) =
+    ( lim ,
+      preserves-limits-sequence-isometry-Metric-Space
+        ( metric-space-ℝ l)
+        ( metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l))
+        ( id , λ d x y → neighborhood-iff-leq-dist-ℝ d x y)
+        ( λ n → sum-fin-sequence-ℝ n (σ ∘ nat-Fin n))
+        ( lim)
+        ( is-lim))
+```
+
 ### If a series converges, there exists a modulus making its partial sums a Cauchy sequence
 
 ```agda
diff --git a/src/analysis/convergent-series-real-numbers.lagda.md b/src/analysis/convergent-series-real-numbers.lagda.md
index 16804c6e49..f7d5effe76 100644
--- a/src/analysis/convergent-series-real-numbers.lagda.md
+++ b/src/analysis/convergent-series-real-numbers.lagda.md
@@ -11,9 +11,13 @@ 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.dependent-pair-types
 open import foundation.propositions
+open import foundation.subtypes
 open import foundation.universe-levels
 
+open import lists.sequences
+
 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
@@ -48,6 +52,31 @@ module _
 
   is-convergent-series-ℝ : UU (lsuc l)
   is-convergent-series-ℝ = is-convergent-series-Metric-Ab σ
+
+convergent-series-ℝ : (l : Level) → UU (lsuc l)
+convergent-series-ℝ l = type-subtype (is-convergent-prop-series-ℝ {l})
+
+module _
+  {l : Level}
+  (σ : convergent-series-ℝ l)
+  where
+
+  series-convergent-series-ℝ : series-ℝ l
+  series-convergent-series-ℝ = pr1 σ
+
+  term-convergent-series-ℝ : sequence (ℝ l)
+  term-convergent-series-ℝ = term-series-ℝ series-convergent-series-ℝ
+
+  sum-convergent-series-ℝ : ℝ l
+  sum-convergent-series-ℝ = pr1 (pr2 σ)
+
+  is-sum-sum-convergent-series-ℝ :
+    is-sum-series-ℝ series-convergent-series-ℝ sum-convergent-series-ℝ
+  is-sum-sum-convergent-series-ℝ = pr2 (pr2 σ)
+
+  partial-sum-convergent-series-ℝ : sequence (ℝ l)
+  partial-sum-convergent-series-ℝ =
+    partial-sum-series-ℝ series-convergent-series-ℝ
 ```
 
 ## Properties
diff --git a/src/analysis/metric-abelian-groups.lagda.md b/src/analysis/metric-abelian-groups.lagda.md
index fffb958a61..becf60fe83 100644
--- a/src/analysis/metric-abelian-groups.lagda.md
+++ b/src/analysis/metric-abelian-groups.lagda.md
@@ -113,6 +113,11 @@ module _
   commutative-add-Metric-Ab :
     (x y : type-Metric-Ab MG) → add-Metric-Ab x y ＝ add-Metric-Ab y x
   commutative-add-Metric-Ab = commutative-add-Ab (ab-Metric-Ab MG)
+
+  is-identity-right-conjugation-Metric-Ab :
+    (x y : type-Metric-Ab MG) → add-Metric-Ab x (diff-Metric-Ab y x) ＝ y
+  is-identity-right-conjugation-Metric-Ab =
+    is-identity-right-conjugation-Ab (ab-Metric-Ab MG)
 ```
 
 ### Metric properties of metric abelian groups
diff --git a/src/analysis/ratio-test-series-real-banach-spaces.lagda.md b/src/analysis/ratio-test-series-real-banach-spaces.lagda.md
new file mode 100644
index 0000000000..53ccad85e8
--- /dev/null
+++ b/src/analysis/ratio-test-series-real-banach-spaces.lagda.md
@@ -0,0 +1,115 @@
+# The ratio test for series in real Banach spaces
+
+```agda
+module analysis.ratio-test-series-real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.absolute-convergence-series-real-banach-spaces
+open import analysis.convergent-series-real-banach-spaces
+open import analysis.ratio-test-series-real-numbers
+open import analysis.series-real-banach-spaces
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-transport
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+
+open import logic.functoriality-existential-quantification
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.nonnegative-real-numbers
+open import real-numbers.strict-inequality-nonnegative-real-numbers
+```
+
+</details>
+
+## Idea
+
+To prove that a [series](analysis.series-real-banach-spaces.md) `∑ aₙ` in a
+[real Banach space](linear-algebra.real-banach-spaces.md)
+[converges](analysis.series-real-numbers.md), it is sufficient to show that
+[there exists](foundation.existential-quantification.md) a
+[nonnegative](real-numbers.nonnegative-real-numbers.md) real number `r`
+[less than](real-numbers.strict-inequality-real-numbers.md) 1 such that for all
+`n`, `∥aₙ₊₁∥ ≤ r∥aₙ∥`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  ratio-test-prop-series-ℝ-Banach-Space : Prop (lsuc l1)
+  ratio-test-prop-series-ℝ-Banach-Space =
+    ∃ ( ℝ⁰⁺ l1)
+      ( λ r →
+        le-prop-ℝ⁰⁺ r one-ℝ⁰⁺ ∧
+        Π-Prop
+          ( ℕ)
+          ( λ n →
+            leq-prop-ℝ
+              ( map-norm-ℝ-Banach-Space V
+                ( term-series-ℝ-Banach-Space V σ (succ-ℕ n)))
+              ( ( real-ℝ⁰⁺ r) *ℝ
+                ( map-norm-ℝ-Banach-Space V
+                  ( term-series-ℝ-Banach-Space V σ n)))))
+
+  ratio-test-series-ℝ-Banach-Space : UU (lsuc l1)
+  ratio-test-series-ℝ-Banach-Space =
+    type-Prop ratio-test-prop-series-ℝ-Banach-Space
+```
+
+## Properties
+
+### The ratio test implies convergence
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  abstract
+    is-convergent-ratio-test-series-ℝ-Banach-Space :
+      ratio-test-series-ℝ-Banach-Space V σ →
+      is-convergent-series-ℝ-Banach-Space V σ
+    is-convergent-ratio-test-series-ℝ-Banach-Space H =
+      is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space
+        ( V)
+        ( σ)
+        ( is-convergent-ratio-test-series-ℝ
+          ( map-norm-series-ℝ-Banach-Space V σ)
+          ( map-tot-exists
+            ( λ r (r<1 , K) →
+              ( r<1 ,
+                λ n →
+                  binary-tr
+                    ( leq-ℝ)
+                    ( inv (abs-real-ℝ⁰⁺ (nonnegative-norm-ℝ-Banach-Space V _)))
+                    ( ap-mul-ℝ
+                      ( refl)
+                      ( inv
+                        ( abs-real-ℝ⁰⁺ (nonnegative-norm-ℝ-Banach-Space V _))))
+                    ( K n)))
+            ( H)))
+```
+
+## See also
+
+- [The ratio test for series of real numbers](analysis.ratio-test-series-real-numbers.md)
diff --git a/src/analysis/ratio-test-series-real-numbers.lagda.md b/src/analysis/ratio-test-series-real-numbers.lagda.md
new file mode 100644
index 0000000000..13d7ff672b
--- /dev/null
+++ b/src/analysis/ratio-test-series-real-numbers.lagda.md
@@ -0,0 +1,142 @@
+# The ratio test for series in the real numbers
+
+```agda
+module analysis.ratio-test-series-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.absolute-convergence-series-real-numbers
+open import analysis.comparison-test-series-real-numbers
+open import analysis.convergent-series-real-numbers
+open import analysis.series-real-numbers
+
+open import elementary-number-theory.inequality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import order-theory.large-posets
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.geometric-sequences-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.multiplication-nonnegative-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.nonnegative-real-numbers
+open import real-numbers.powers-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.strict-inequality-nonnegative-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+```
+
+</details>
+
+## Idea
+
+To prove that a [series](analysis.series-real-numbers.md) `∑ aₙ` of
+[real numbers](real-numbers.dedekind-real-numbers.md)
+[converges](analysis.convergent-series-real-numbers.md), it is sufficient to
+show that [there exists](foundation.existential-quantification.md) a
+[nonnegative](real-numbers.nonnegative-real-numbers.md) real number `r`
+[less than](real-numbers.strict-inequality-real-numbers.md) 1 such that for all
+`n`, `|aₙ₊₁| ≤ r|aₙ|`.
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (σ : series-ℝ l)
+  where
+
+  ratio-test-prop-series-ℝ : Prop (lsuc l)
+  ratio-test-prop-series-ℝ =
+    ∃ ( ℝ⁰⁺ l)
+      ( λ r →
+        le-prop-ℝ⁰⁺ r one-ℝ⁰⁺ ∧
+        Π-Prop
+          ( ℕ)
+          ( λ n →
+            ( leq-prop-ℝ
+              ( abs-ℝ (term-series-ℝ σ (succ-ℕ n)))
+              ( real-ℝ⁰⁺ r *ℝ abs-ℝ (term-series-ℝ σ n)))))
+
+  ratio-test-series-ℝ : UU (lsuc l)
+  ratio-test-series-ℝ = type-Prop ratio-test-prop-series-ℝ
+```
+
+## Properties
+
+### The ratio test implies convergence
+
+```agda
+module _
+  {l : Level}
+  (σ : series-ℝ l)
+  where
+
+  abstract
+    is-convergent-ratio-test-series-ℝ :
+      ratio-test-series-ℝ σ → is-convergent-series-ℝ σ
+    is-convergent-ratio-test-series-ℝ H =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+        open do-syntax-trunc-Prop (is-convergent-prop-series-ℝ σ)
+      in do
+        (r⁰⁺@(r , 0≤r) , r<1 , K) ← H
+        let |σ₀| = abs-ℝ (term-series-ℝ σ 0)
+        is-convergent-is-absolutely-convergent-series-ℝ
+          ( σ)
+          ( is-convergent-is-nonnegative-is-bounded-by-convergent-series-ℝ
+            ( map-abs-series-ℝ σ)
+            ( convergent-standard-geometric-series-ℝ
+              ( |σ₀|)
+              ( r)
+              ( inv-tr (λ x → le-ℝ x one-ℝ) (abs-real-ℝ⁰⁺ r⁰⁺) r<1))
+            ( λ _ → is-nonnegative-abs-ℝ _)
+            ( ind-ℕ
+              ( refl-leq-ℝ _)
+              ( λ n |σₙ|≤arⁿ →
+                chain-of-inequalities
+                  abs-ℝ (term-series-ℝ σ (succ-ℕ n))
+                  ≤ r *ℝ abs-ℝ (term-series-ℝ σ n)
+                    by K n
+                  ≤ r *ℝ seq-standard-geometric-sequence-ℝ |σ₀| r n
+                    by preserves-leq-left-mul-ℝ⁰⁺ r⁰⁺ |σₙ|≤arⁿ
+                  ≤ r *ℝ (|σ₀| *ℝ power-ℝ n r)
+                    by
+                      leq-eq-ℝ
+                        ( ap-mul-ℝ
+                          ( refl)
+                          ( compute-standard-geometric-sequence-ℝ |σ₀| r n))
+                  ≤ |σ₀| *ℝ (r *ℝ power-ℝ n r)
+                    by leq-eq-ℝ (left-swap-mul-ℝ _ _ _)
+                  ≤ |σ₀| *ℝ power-ℝ (succ-ℕ n) r
+                    by leq-eq-ℝ (ap-mul-ℝ refl (inv (power-succ-ℝ' n r)))
+                  ≤ seq-standard-geometric-sequence-ℝ |σ₀| r (succ-ℕ n)
+                    by
+                      leq-eq-ℝ
+                        ( inv
+                          ( compute-standard-geometric-sequence-ℝ
+                            ( |σ₀|)
+                            ( r)
+                            ( succ-ℕ n))))))
+```
+
+## See also
+
+- [The ratio test for series in real Banach spaces](analysis.ratio-test-series-real-banach-spaces.md)
+
+## External links
+
+- [Ratio test](https://en.wikipedia.org/wiki/Ratio_test) on Wikipedia
diff --git a/src/analysis/series-real-banach-spaces.lagda.md b/src/analysis/series-real-banach-spaces.lagda.md
index dc7d5b3651..12f7c30508 100644
--- a/src/analysis/series-real-banach-spaces.lagda.md
+++ b/src/analysis/series-real-banach-spaces.lagda.md
@@ -9,7 +9,13 @@ module analysis.series-real-banach-spaces where
 ```agda
 open import analysis.metric-abelian-groups-normed-real-vector-spaces
 open import analysis.series-metric-abelian-groups
+open import analysis.series-real-numbers
 
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.function-types
+open import foundation.identity-types
 open import foundation.universe-levels
 
 open import linear-algebra.real-banach-spaces
@@ -54,3 +60,52 @@ module _
     series-ℝ-Banach-Space → sequence (type-ℝ-Banach-Space V)
   partial-sum-series-ℝ-Banach-Space = partial-sum-series-Metric-Ab
 ```
+
+## Properties
+
+### The series of norms
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  map-norm-series-ℝ-Banach-Space : series-ℝ l1
+  map-norm-series-ℝ-Banach-Space =
+    series-terms-ℝ (map-norm-ℝ-Banach-Space V ∘ term-series-ℝ-Banach-Space V σ)
+```
+
+### Dropping terms from a series
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  where
+
+  drop-series-ℝ-Banach-Space :
+    ℕ → series-ℝ-Banach-Space V → series-ℝ-Banach-Space V
+  drop-series-ℝ-Banach-Space = drop-series-Metric-Ab
+```
+
+### The partial sums of a series after dropping terms
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  where
+
+  abstract
+    partial-sum-drop-series-ℝ-Banach-Space :
+      (n : ℕ) (σ : series-ℝ-Banach-Space V) (i : ℕ) →
+      partial-sum-series-ℝ-Banach-Space V
+        ( drop-series-ℝ-Banach-Space V n σ)
+        ( i) ＝
+      diff-ℝ-Banach-Space V
+        ( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ i))
+        ( partial-sum-series-ℝ-Banach-Space V σ n)
+    partial-sum-drop-series-ℝ-Banach-Space = partial-sum-drop-series-Metric-Ab
+```
diff --git a/src/analysis/series-real-numbers.lagda.md b/src/analysis/series-real-numbers.lagda.md
index 6b7455caa6..74b2105aae 100644
--- a/src/analysis/series-real-numbers.lagda.md
+++ b/src/analysis/series-real-numbers.lagda.md
@@ -10,12 +10,26 @@ module analysis.series-real-numbers where
 open import analysis.series-complete-metric-abelian-groups
 open import analysis.series-metric-abelian-groups
 
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
 open import foundation.universe-levels
 
 open import lists.sequences
 
+open import order-theory.increasing-sequences-posets
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.addition-nonnegative-real-numbers
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
+open import real-numbers.inequality-real-numbers
 open import real-numbers.metric-additive-group-of-real-numbers
+open import real-numbers.nonnegative-real-numbers
 ```
 
 </details>
@@ -42,3 +56,69 @@ term-series-ℝ = term-series-Metric-Ab
 partial-sum-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l)
 partial-sum-series-ℝ {l} = partial-sum-series-Metric-Ab
 ```
+
+## Properties
+
+### The proposition that the terms of a series are nonnegative
+
+```agda
+is-nonnegative-prop-series-ℝ : {l : Level} → series-ℝ l → Prop l
+is-nonnegative-prop-series-ℝ σ =
+  Π-Prop ℕ (λ n → is-nonnegative-prop-ℝ (term-series-ℝ σ n))
+
+is-nonnegative-series-ℝ : {l : Level} → series-ℝ l → UU l
+is-nonnegative-series-ℝ σ = type-Prop (is-nonnegative-prop-series-ℝ σ)
+```
+
+### If the terms of a series of real numbers are nonnegative, the partial sums are monotonic
+
+```agda
+abstract
+  is-increasing-partial-sum-is-nonnegative-term-series-ℝ :
+    {l : Level} (σ : series-ℝ l) →
+    is-nonnegative-series-ℝ σ →
+    is-increasing-sequence-Poset (ℝ-Poset l) (partial-sum-series-ℝ σ)
+  is-increasing-partial-sum-is-nonnegative-term-series-ℝ {l} σ H =
+    is-increasing-leq-succ-sequence-Poset
+      ( ℝ-Poset l)
+      ( partial-sum-series-ℝ σ)
+      ( λ n → leq-left-add-real-ℝ⁰⁺ _ (term-series-ℝ σ n , H n))
+```
+
+### The series of absolute values
+
+```agda
+module _
+  {l : Level}
+  (σ : series-ℝ l)
+  where
+
+  map-abs-series-ℝ : series-ℝ l
+  map-abs-series-ℝ = series-terms-ℝ (abs-ℝ ∘ term-series-ℝ σ)
+```
+
+### Dropping terms from a series
+
+```agda
+module _
+  {l : Level}
+  where
+
+  drop-series-ℝ : ℕ → series-ℝ l → series-ℝ l
+  drop-series-ℝ = drop-series-Metric-Ab
+```
+
+### The partial sums of a series after dropping terms
+
+```agda
+module _
+  {l : Level}
+  where
+
+  abstract
+    partial-sum-drop-series-ℝ :
+      (n : ℕ) (σ : series-ℝ l) (i : ℕ) →
+      partial-sum-series-ℝ (drop-series-ℝ n σ) i ＝
+      partial-sum-series-ℝ σ (n +ℕ i) -ℝ partial-sum-series-ℝ σ n
+    partial-sum-drop-series-ℝ = partial-sum-drop-series-Metric-Ab
+```
diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md
index 895b8bacdc..1e582c5ef5 100644
--- a/src/linear-algebra.lagda.md
+++ b/src/linear-algebra.lagda.md
@@ -51,6 +51,8 @@ open import linear-algebra.scalar-multiplication-tuples public
 open import linear-algebra.scalar-multiplication-tuples-on-rings public
 open import linear-algebra.seminormed-real-vector-spaces public
 open import linear-algebra.subsets-left-modules-rings public
+open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces public
+open import linear-algebra.sums-of-finite-sequences-of-elements-real-banach-spaces public
 open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces public
 open import linear-algebra.transposition-matrices public
 open import linear-algebra.tuples-on-commutative-monoids public
diff --git a/src/linear-algebra/normed-real-vector-spaces.lagda.md b/src/linear-algebra/normed-real-vector-spaces.lagda.md
index 42c3f8902a..9f7b406225 100644
--- a/src/linear-algebra/normed-real-vector-spaces.lagda.md
+++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md
@@ -32,8 +32,10 @@ open import metric-spaces.metrics
 open import metric-spaces.metrics-of-metric-spaces
 
 open import real-numbers.absolute-value-real-numbers
+open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.distance-real-numbers
+open import real-numbers.inequality-real-numbers
 open import real-numbers.metric-space-of-real-numbers
 open import real-numbers.nonnegative-real-numbers
 open import real-numbers.raising-universe-levels-real-numbers
@@ -207,6 +209,15 @@ module _
     nonnegative-dist-Seminormed-ℝ-Vector-Space
       ( seminormed-vector-space-Normed-ℝ-Vector-Space)
 
+  triangular-norm-Normed-ℝ-Vector-Space :
+    (v w : type-Normed-ℝ-Vector-Space) →
+    leq-ℝ
+      ( map-norm-Normed-ℝ-Vector-Space (add-Normed-ℝ-Vector-Space v w))
+      ( map-norm-Normed-ℝ-Vector-Space v +ℝ map-norm-Normed-ℝ-Vector-Space w)
+  triangular-norm-Normed-ℝ-Vector-Space =
+    triangular-seminorm-Seminormed-ℝ-Vector-Space
+      ( seminormed-vector-space-Normed-ℝ-Vector-Space)
+
   is-extensional-norm-Normed-ℝ-Vector-Space :
     (v : type-Normed-ℝ-Vector-Space) →
     map-norm-Normed-ℝ-Vector-Space v ＝ raise-ℝ l1 zero-ℝ →
@@ -384,6 +395,23 @@ module _
                   ( w)))))
 ```
 
+### The norm of the zero vector is zero
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Normed-ℝ-Vector-Space l1 l2)
+  where
+
+  abstract
+    is-zero-norm-zero-Normed-ℝ-Vector-Space :
+      map-norm-Normed-ℝ-Vector-Space V (zero-Normed-ℝ-Vector-Space V) ＝
+      raise-ℝ l1 zero-ℝ
+    is-zero-norm-zero-Normed-ℝ-Vector-Space =
+      is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space
+        ( seminormed-vector-space-Normed-ℝ-Vector-Space V)
+```
+
 ## See also
 
 - [Real Banach spaces](linear-algebra.real-banach-spaces.md), normed real vector
diff --git a/src/linear-algebra/real-banach-spaces.lagda.md b/src/linear-algebra/real-banach-spaces.lagda.md
index bdcc30ac25..3ad7b5b263 100644
--- a/src/linear-algebra/real-banach-spaces.lagda.md
+++ b/src/linear-algebra/real-banach-spaces.lagda.md
@@ -9,7 +9,10 @@ module linear-algebra.real-banach-spaces where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.positive-rational-numbers
+
 open import foundation.dependent-pair-types
+open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes
 open import foundation.transport-along-identifications
@@ -27,6 +30,7 @@ open import metric-spaces.metric-spaces
 
 open import real-numbers.cauchy-completeness-dedekind-real-numbers
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.nonnegative-real-numbers
 ```
 
 </details>
@@ -69,6 +73,15 @@ module _
   metric-space-ℝ-Banach-Space =
     metric-space-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
 
+  type-ℝ-Banach-Space : UU l2
+  type-ℝ-Banach-Space =
+    type-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
+
+  neighborhood-ℝ-Banach-Space :
+    ℚ⁺ → type-ℝ-Banach-Space → type-ℝ-Banach-Space → UU l1
+  neighborhood-ℝ-Banach-Space =
+    neighborhood-Metric-Space metric-space-ℝ-Banach-Space
+
   is-complete-metric-space-ℝ-Banach-Space :
     is-complete-Metric-Space metric-space-ℝ-Banach-Space
   is-complete-metric-space-ℝ-Banach-Space = pr2 V
@@ -77,14 +90,14 @@ module _
   complete-metric-space-ℝ-Banach-Space =
     ( metric-space-ℝ-Banach-Space , is-complete-metric-space-ℝ-Banach-Space)
 
-  type-ℝ-Banach-Space : UU l2
-  type-ℝ-Banach-Space =
-    type-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
-
   map-norm-ℝ-Banach-Space : type-ℝ-Banach-Space → ℝ l1
   map-norm-ℝ-Banach-Space =
     map-norm-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
 
+  nonnegative-norm-ℝ-Banach-Space : type-ℝ-Banach-Space → ℝ⁰⁺ l1
+  nonnegative-norm-ℝ-Banach-Space =
+    nonnegative-norm-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
+
   cauchy-sequence-ℝ-Banach-Space : UU (l1 ⊔ l2)
   cauchy-sequence-ℝ-Banach-Space =
     cauchy-sequence-Metric-Space metric-space-ℝ-Banach-Space
@@ -109,6 +122,21 @@ module _
   has-limit-cauchy-sequence-ℝ-Banach-Space =
     has-limit-cauchy-sequence-Complete-Metric-Space
       ( complete-metric-space-ℝ-Banach-Space)
+
+  dist-ℝ-Banach-Space : (u v : type-ℝ-Banach-Space) → ℝ l1
+  dist-ℝ-Banach-Space =
+    dist-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
+
+  commutative-dist-ℝ-Banach-Space :
+    (u v : type-ℝ-Banach-Space) →
+    dist-ℝ-Banach-Space u v ＝ dist-ℝ-Banach-Space v u
+  commutative-dist-ℝ-Banach-Space =
+    commutative-dist-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
+
+  diff-ℝ-Banach-Space :
+    type-ℝ-Banach-Space → type-ℝ-Banach-Space → type-ℝ-Banach-Space
+  diff-ℝ-Banach-Space =
+    diff-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space
 ```
 
 ## Properties
diff --git a/src/linear-algebra/sums-of-finite-sequences-of-elements-normed-real-vector-spaces.lagda.md b/src/linear-algebra/sums-of-finite-sequences-of-elements-normed-real-vector-spaces.lagda.md
new file mode 100644
index 0000000000..e5f32535a6
--- /dev/null
+++ b/src/linear-algebra/sums-of-finite-sequences-of-elements-normed-real-vector-spaces.lagda.md
@@ -0,0 +1,94 @@
+# Sums of finite sequences of elements in normed real vector spaces
+
+```agda
+module linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.function-types
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups
+
+open import linear-algebra.normed-real-vector-spaces
+
+open import lists.finite-sequences
+
+open import order-theory.large-posets
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.inequalities-addition-and-subtraction-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.sums-of-finite-sequences-of-real-numbers
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "sum" Disambiguation="of a finite sequence of elements of a normed vector space over ℝ" Agda=sum-fin-sequence-type-Normed-ℝ-Vector-Space}}
+of a [finite sequence](lists.finite-sequences.md) of elements of a
+[normed vector space](linear-algebra.normed-real-vector-spaces.md) over the
+[real numbers](real-numbers.dedekind-real-numbers.md) is the
+[sum of the sequence](group-theory.sums-of-finite-sequences-of-elements-abelian-groups.md)
+in the [abelian group](group-theory.abelian-groups.md) of the vector space under
+addition.
+
+## Definition
+
+```agda
+sum-fin-sequence-type-Normed-ℝ-Vector-Space :
+  {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) (n : ℕ) →
+  fin-sequence (type-Normed-ℝ-Vector-Space V) n → type-Normed-ℝ-Vector-Space V
+sum-fin-sequence-type-Normed-ℝ-Vector-Space V =
+  sum-fin-sequence-type-Ab (ab-Normed-ℝ-Vector-Space V)
+```
+
+## Properties
+
+### The norm of the sum of a finite sequence is at most the sum of the norms of the terms of the sequence
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : Normed-ℝ-Vector-Space l1 l2)
+  where
+
+  abstract
+    triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space :
+      (n : ℕ) (σ : fin-sequence (type-Normed-ℝ-Vector-Space V) n) →
+      leq-ℝ
+        ( map-norm-Normed-ℝ-Vector-Space V
+          ( sum-fin-sequence-type-Normed-ℝ-Vector-Space V n σ))
+        ( sum-fin-sequence-ℝ n (map-norm-Normed-ℝ-Vector-Space V ∘ σ))
+    triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space 0 σ =
+      leq-eq-ℝ (is-zero-norm-zero-Normed-ℝ-Vector-Space V)
+    triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space
+      (succ-ℕ n) σ =
+      let
+        open inequality-reasoning-Large-Poset ℝ-Large-Poset
+      in
+        chain-of-inequalities
+          map-norm-Normed-ℝ-Vector-Space V
+            ( sum-fin-sequence-type-Normed-ℝ-Vector-Space V (succ-ℕ n) σ)
+          ≤ ( map-norm-Normed-ℝ-Vector-Space V
+              ( sum-fin-sequence-type-Normed-ℝ-Vector-Space V
+                ( n)
+                ( σ ∘ inl-Fin n))) +ℝ
+            ( map-norm-Normed-ℝ-Vector-Space V (σ (neg-one-Fin n)))
+            by triangular-norm-Normed-ℝ-Vector-Space V _ _
+          ≤ sum-fin-sequence-ℝ (succ-ℕ n) (map-norm-Normed-ℝ-Vector-Space V ∘ σ)
+            by
+              preserves-leq-right-add-ℝ _ _ _
+                ( triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space
+                  ( n)
+                  ( σ ∘ inl-Fin n))
+```
diff --git a/src/linear-algebra/sums-of-finite-sequences-of-elements-real-banach-spaces.lagda.md b/src/linear-algebra/sums-of-finite-sequences-of-elements-real-banach-spaces.lagda.md
new file mode 100644
index 0000000000..ba3aa4cac9
--- /dev/null
+++ b/src/linear-algebra/sums-of-finite-sequences-of-elements-real-banach-spaces.lagda.md
@@ -0,0 +1,67 @@
+# Sums of finite sequences of elements in real Banach spaces
+
+```agda
+module linear-algebra.sums-of-finite-sequences-of-elements-real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.function-types
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces
+
+open import lists.finite-sequences
+
+open import real-numbers.inequality-real-numbers
+open import real-numbers.sums-of-finite-sequences-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "sum" Disambiguation="of a finite sequence of elements of a real Banach space" Agda=sum-fin-sequence-type-ℝ-Banach-Space}}
+of a [finite sequence](lists.finite-sequences.md) of elements of a
+[real Banach space](linear-algebra.real-banach-spaces.md) is the
+[sum of the sequence](group-theory.sums-of-finite-sequences-of-elements-abelian-groups.md)
+in the [abelian group](group-theory.abelian-groups.md) of the space under
+addition.
+
+## Definition
+
+```agda
+sum-fin-sequence-type-ℝ-Banach-Space :
+  {l1 l2 : Level} (V : ℝ-Banach-Space l1 l2) →
+  (n : ℕ) → fin-sequence (type-ℝ-Banach-Space V) n → type-ℝ-Banach-Space V
+sum-fin-sequence-type-ℝ-Banach-Space V =
+  sum-fin-sequence-type-Normed-ℝ-Vector-Space
+    ( normed-vector-space-ℝ-Banach-Space V)
+```
+
+## Properties
+
+### The norm of the sum of a finite sequence is at most the sum of the norms of the terms of the sequence
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  where
+
+  abstract
+    triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space :
+      (n : ℕ) (σ : fin-sequence (type-ℝ-Banach-Space V) n) →
+      leq-ℝ
+        ( map-norm-ℝ-Banach-Space V
+          ( sum-fin-sequence-type-ℝ-Banach-Space V n σ))
+        ( sum-fin-sequence-ℝ n (map-norm-ℝ-Banach-Space V ∘ σ))
+    triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space =
+      triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space
+        ( normed-vector-space-ℝ-Banach-Space V)
+```
diff --git a/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md b/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md
index 71c916ccf9..adaa01d373 100644
--- a/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md
@@ -9,6 +9,7 @@ module metric-spaces.cauchy-sequences-metric-spaces where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.addition-positive-rational-numbers
 open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.archimedean-property-positive-rational-numbers
@@ -85,6 +86,31 @@ module _
     (m k : ℕ) → leq-ℕ N m → leq-ℕ N k →
     neighborhood-Metric-Space M ε (x m) (x k)
 
+  is-cauchy-modulus-sequence-Metric-Space' : ℚ⁺ → ℕ → UU l2
+  is-cauchy-modulus-sequence-Metric-Space' ε N =
+    (m k : ℕ) → leq-ℕ N m →
+    neighborhood-Metric-Space M ε (x (m +ℕ k)) (x m)
+
+  is-cauchy-modulus-is-cauchy-modulus-sequence-Metric-Space' :
+    (ε : ℚ⁺) (N : ℕ) → is-cauchy-modulus-sequence-Metric-Space' ε N →
+    is-cauchy-modulus-sequence-Metric-Space ε N
+  is-cauchy-modulus-is-cauchy-modulus-sequence-Metric-Space' ε N H m k N≤m N≤k =
+    let
+      case a b N≤a a≤b =
+        let
+          ( c , c+a=b) = subtraction-leq-ℕ a b a≤b
+        in
+          tr
+            ( λ d → neighborhood-Metric-Space M ε (x d) (x a))
+            ( commutative-add-ℕ a c ∙ c+a=b)
+            ( H a c N≤a)
+    in
+      rec-coproduct
+        ( λ m≤k →
+          symmetric-neighborhood-Metric-Space M ε _ _ (case m k N≤m m≤k))
+        ( λ k≤m → case k m N≤k k≤m)
+        ( linear-leq-ℕ m k)
+
   is-cauchy-sequence-Metric-Space : UU l2
   is-cauchy-sequence-Metric-Space =
     (ε : ℚ⁺) → Σ ℕ (is-cauchy-modulus-sequence-Metric-Space ε)
@@ -772,6 +798,56 @@ module _
       is-cauchy-sequence-pair-cauchy-sequence-Metric-Space)
 ```
 
+### To show a sequence `aₙ` is Cauchy, it suffices to have a modulus function such that for any `ε`, `aₙ` and `aₙ₊ₖ` are in an `ε`-neighborhood for sufficiently large `n`
+
+```agda
+module
+  _
+  {l1 l2 : Level}
+  (X : Metric-Space l1 l2)
+  (a : sequence-type-Metric-Space X)
+  (μ : ℚ⁺ → ℕ)
+  where
+
+  abstract
+    is-cauchy-modulus-neighborhood-add-sequence-Metric-Space :
+      ( (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (μ ε) n →
+        neighborhood-Metric-Space X ε (a (n +ℕ k)) (a n)) →
+      (ε : ℚ⁺) →
+      is-cauchy-modulus-sequence-Metric-Space X a ε (μ ε)
+    is-cauchy-modulus-neighborhood-add-sequence-Metric-Space H ε p q με≤p με≤q =
+      let
+        lemma :
+          (m n : ℕ) → leq-ℕ (μ ε) m → leq-ℕ m n →
+          neighborhood-Metric-Space X ε (a n) (a m)
+        lemma m n με≤m m≤n =
+          let
+            ( k , k+m=n) = subtraction-leq-ℕ m n m≤n
+          in
+            tr
+              ( λ p → neighborhood-Metric-Space X ε (a p) (a m))
+              ( commutative-add-ℕ m k ∙ k+m=n)
+              ( H ε m k με≤m)
+      in
+        rec-coproduct
+          ( λ p≤q →
+            symmetric-neighborhood-Metric-Space
+              ( X)
+              ( ε)
+              ( a q)
+              ( a p)
+              ( lemma p q με≤p p≤q))
+          ( lemma q p με≤q)
+          ( linear-leq-ℕ p q)
+
+  is-cauchy-sequence-modulus-neighborhood-add-sequence-Metric-Space :
+    ( (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (μ ε) n →
+      neighborhood-Metric-Space X ε (a (n +ℕ k)) (a n)) →
+    is-cauchy-sequence-Metric-Space X a
+  is-cauchy-sequence-modulus-neighborhood-add-sequence-Metric-Space H ε =
+    ( μ ε , is-cauchy-modulus-neighborhood-add-sequence-Metric-Space H ε)
+```
+
 ## See also
 
 - [Cauchy sequences in complete metric spaces](metric-spaces.cauchy-sequences-complete-metric-spaces.md)
diff --git a/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md b/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md
index 2cfda0f25e..984330b2f5 100644
--- a/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md
+++ b/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md
@@ -31,6 +31,7 @@ open import foundation.universe-levels
 open import lists.sequences
 
 open import metric-spaces.cartesian-products-metric-spaces
+open import metric-spaces.isometries-metric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.modulated-uniformly-continuous-functions-metric-spaces
 open import metric-spaces.sequences-metric-spaces
@@ -383,6 +384,46 @@ module _
     map-is-inhabited short-map-limit-modulus-sequence-Metric-Space
 ```
 
+### Isometries between metric spaces preserve limits
+
+```agda
+module _
+  {la la' lb lb' : Level}
+  (A : Metric-Space la la')
+  (B : Metric-Space lb lb')
+  (f : isometry-Metric-Space A B)
+  (u : sequence-type-Metric-Space A)
+  (lim : type-Metric-Space A)
+  where
+
+  isometry-map-limit-modulus-sequence-Metric-Space :
+    limit-modulus-sequence-Metric-Space A u lim →
+    limit-modulus-sequence-Metric-Space
+      ( B)
+      ( map-sequence
+        ( map-isometry-Metric-Space A B f)
+        ( u))
+      ( map-isometry-Metric-Space A B f lim)
+  isometry-map-limit-modulus-sequence-Metric-Space =
+    short-map-limit-modulus-sequence-Metric-Space
+      ( A)
+      ( B)
+      ( short-isometry-Metric-Space A B f)
+      ( u)
+      ( lim)
+
+  preserves-limits-sequence-isometry-Metric-Space :
+    is-limit-sequence-Metric-Space A u lim →
+    is-limit-sequence-Metric-Space
+      ( B)
+      ( map-sequence
+        ( map-isometry-Metric-Space A B f)
+        ( u))
+      ( map-isometry-Metric-Space A B f lim)
+  preserves-limits-sequence-isometry-Metric-Space =
+    map-is-inhabited isometry-map-limit-modulus-sequence-Metric-Space
+```
+
 ### If two sequences have limits in metric spaces, their pairing has a limit in the product space
 
 The converse has yet to be proved.
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index 8210a60b2e..06ea8bb3f3 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -107,6 +107,7 @@ open import real-numbers.strict-inequality-nonnegative-real-numbers public
 open import real-numbers.strict-inequality-positive-real-numbers public
 open import real-numbers.strict-inequality-real-numbers public
 open import real-numbers.subsets-real-numbers public
+open import real-numbers.sums-of-finite-sequences-of-real-numbers public
 open import real-numbers.suprema-families-real-numbers public
 open import real-numbers.totally-bounded-subsets-real-numbers public
 open import real-numbers.transposition-addition-subtraction-cuts-dedekind-real-numbers public
diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md
index 29a635cae2..fc56fd9d72 100644
--- a/src/real-numbers/absolute-value-real-numbers.lagda.md
+++ b/src/real-numbers/absolute-value-real-numbers.lagda.md
@@ -302,6 +302,20 @@ module _
     leq-abs-leq-leq-neg-ℝ = leq-max-leq-leq-ℝ x (neg-ℝ x) y
 ```
 
+### If `x < y` and `-x < y`, `|x| < y`
+
+```agda
+module _
+  {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2}
+  where
+
+  abstract opaque
+    unfolding abs-ℝ
+
+    le-abs-le-le-neg-ℝ : le-ℝ x y → le-ℝ (neg-ℝ x) y → le-ℝ (abs-ℝ x) y
+    le-abs-le-le-neg-ℝ = le-max-le-le-ℝ
+```
+
 ### Triangle inequality
 
 ```agda
diff --git a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md
index a7d81021a9..8a716b033f 100644
--- a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md
+++ b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md
@@ -9,6 +9,8 @@ module real-numbers.cauchy-sequences-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
+open import foundation.inhabited-types
 open import foundation.universe-levels
 
 open import lists.sequences
@@ -20,6 +22,7 @@ open import metric-spaces.cauchy-sequences-metric-spaces
 open import real-numbers.cauchy-completeness-dedekind-real-numbers
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.isometry-addition-real-numbers
+open import real-numbers.limits-sequences-real-numbers
 open import real-numbers.metric-space-of-real-numbers
 ```
 
@@ -75,3 +78,20 @@ add-cauchy-sequence-ℝ {l1} {l2} u v =
       ( u)
       ( v))
 ```
+
+### If a sequence has a limit, there exists a modulus making it a Cauchy sequence
+
+```agda
+abstract
+  exists-cauchy-modulus-has-limit-sequence-ℝ :
+    {l : Level} (σ : sequence (ℝ l)) →
+    has-limit-sequence-ℝ σ →
+    is-inhabited (is-cauchy-sequence-ℝ σ)
+  exists-cauchy-modulus-has-limit-sequence-ℝ {l} σ (lim , is-lim) =
+    map-is-inhabited
+      ( is-cauchy-has-limit-modulus-sequence-Metric-Space
+        ( metric-space-ℝ l)
+        ( σ)
+        ( lim))
+      ( is-lim)
+```
diff --git a/src/real-numbers/distance-real-numbers.lagda.md b/src/real-numbers/distance-real-numbers.lagda.md
index 9ca6388089..e21335fbd5 100644
--- a/src/real-numbers/distance-real-numbers.lagda.md
+++ b/src/real-numbers/distance-real-numbers.lagda.md
@@ -257,6 +257,16 @@ abstract
       ( leq-transpose-right-add-ℝ _ _ _ y≤z+x)
 ```
 
+### The difference of two real numbers is at most their distance
+
+```agda
+abstract
+  leq-diff-dist-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) →
+    leq-ℝ (x -ℝ y) (dist-ℝ x y)
+  leq-diff-dist-ℝ _ _ = leq-abs-ℝ _
+```
+
 ### Addition preserves distance between real numbers
 
 ```agda
diff --git a/src/real-numbers/geometric-sequences-real-numbers.lagda.md b/src/real-numbers/geometric-sequences-real-numbers.lagda.md
index f5625e7f4e..dfc8de55e8 100644
--- a/src/real-numbers/geometric-sequences-real-numbers.lagda.md
+++ b/src/real-numbers/geometric-sequences-real-numbers.lagda.md
@@ -18,6 +18,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.binary-transport
+open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types
 open import foundation.transport-along-identifications
@@ -242,6 +243,13 @@ module _
             ( λ n → power-ℝ n r)
             ( raise-ℝ l zero-ℝ)
             ( is-zero-lim-power-le-one-abs-ℝ r |r|<1))
+
+  convergent-standard-geometric-series-ℝ :
+    le-ℝ (abs-ℝ r) one-ℝ → convergent-series-ℝ l
+  convergent-standard-geometric-series-ℝ |r|<1 =
+    ( standard-geometric-series-ℝ ,
+      a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1) ,
+      compute-sum-standard-geometric-series-ℝ |r|<1)
 ```
 
 ## References
diff --git a/src/real-numbers/limits-sequences-real-numbers.lagda.md b/src/real-numbers/limits-sequences-real-numbers.lagda.md
index 2aaf9e43a0..8b183862a6 100644
--- a/src/real-numbers/limits-sequences-real-numbers.lagda.md
+++ b/src/real-numbers/limits-sequences-real-numbers.lagda.md
@@ -44,6 +44,9 @@ is-limit-prop-sequence-ℝ {l} =
 
 is-limit-sequence-ℝ : {l : Level} → sequence (ℝ l) → ℝ l → UU l
 is-limit-sequence-ℝ {l} = is-limit-sequence-Metric-Space (metric-space-ℝ l)
+
+has-limit-sequence-ℝ : {l : Level} → sequence (ℝ l) → UU (lsuc l)
+has-limit-sequence-ℝ {l} = has-limit-sequence-Metric-Space (metric-space-ℝ l)
 ```
 
 ## Properties
diff --git a/src/real-numbers/sums-of-finite-sequences-of-real-numbers.lagda.md b/src/real-numbers/sums-of-finite-sequences-of-real-numbers.lagda.md
new file mode 100644
index 0000000000..8da6c6955b
--- /dev/null
+++ b/src/real-numbers/sums-of-finite-sequences-of-real-numbers.lagda.md
@@ -0,0 +1,69 @@
+# Sums of finite sequences of real numbers
+
+```agda
+module real-numbers.sums-of-finite-sequences-of-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.function-types
+open import foundation.universe-levels
+
+open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups
+
+open import lists.finite-sequences
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.inequalities-addition-and-subtraction-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.large-additive-group-of-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "sum operation" Disambiguation="of a finite sequence in ℝ" WD="sum" WDID=Q218005 Agda=sum-fin-sequence-ℝ}}
+extends the operation of [addition](real-numbers.addition-real-numbers.md) on
+the [real numbers](real-numbers.dedekind-real-numbers.md) to any
+[finite sequence](lists.finite-sequences.md) of real numbers.
+
+## Definition
+
+```agda
+sum-fin-sequence-ℝ : {l : Level} (n : ℕ) → fin-sequence (ℝ l) n → ℝ l
+sum-fin-sequence-ℝ {l} = sum-fin-sequence-type-Ab (ab-add-ℝ l)
+```
+
+## Properties
+
+### If `aₙ ≤ bₙ` for all `n`, then `∑ aₙ ≤ ∑ bₙ`
+
+```agda
+abstract
+  leq-sum-fin-sequence-ℝ :
+    {l1 l2 : Level} (n : ℕ) →
+    (a : fin-sequence (ℝ l1) n) (b : fin-sequence (ℝ l2) n) →
+    ((k : Fin n) → leq-ℝ (a k) (b k)) →
+    leq-ℝ (sum-fin-sequence-ℝ n a) (sum-fin-sequence-ℝ n b)
+  leq-sum-fin-sequence-ℝ {l1} {l2} 0 _ _ _ =
+    leq-sim-ℝ
+      ( transitive-sim-ℝ _ _ _ (sim-raise-ℝ l2 zero-ℝ) (sim-raise-ℝ' l1 zero-ℝ))
+  leq-sum-fin-sequence-ℝ (succ-ℕ n) a b H =
+    preserves-leq-add-ℝ
+      ( leq-sum-fin-sequence-ℝ
+        ( n)
+        ( a ∘ inl-Fin n)
+        ( b ∘ inl-Fin n)
+        ( H ∘ inl-Fin n))
+      ( H (neg-one-Fin n))
+```