The ratio test for convergence in real Banach spaces

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

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

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