Series in Banach spaces

docs/MIXFIX-OPERATORS.md

@@ -177,8 +177,8 @@ Below, we outline a list of general rules when assigning associativities.
 | 16               | Right homotopy whiskering `_·r_`                                                                                                                                                                   |
 | 15               | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, `_*_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` |
 | 10               | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad                                                                    |
-| 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations                                                                              |
-| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_`                                                                                               |
+| 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, `_⇔_`, and `_↔_`, elementhood relations, subtype relations                                                                             |
+| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_↪_`, `_→∗_`, `_↠_`, `_↪ᵈ_`, and `_⊆_`                                                                                             |
 | 3                | The pairing operators `_,_` and `_,ω_`                                                                                                                                                             |
 | 0-1              | Reasoning syntaxes                                                                                                                                                                                 |
 | -∞               | Function type formation `_→_`                                                                                                                                                                      |

src/analysis.lagda.md

@@ -3,8 +3,17 @@
 ```agda
 module analysis where
 
+open import analysis.complete-metric-abelian-groups public
+open import analysis.complete-metric-abelian-groups-real-banach-spaces public
+open import analysis.convergent-series-complete-metric-abelian-groups public
 open import analysis.convergent-series-metric-abelian-groups public
+open import analysis.convergent-series-real-banach-spaces public
+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.series-complete-metric-abelian-groups public
 open import analysis.series-metric-abelian-groups public
+open import analysis.series-real-banach-spaces public
+open import analysis.series-real-numbers public
 ```

src/analysis/complete-metric-abelian-groups-real-banach-spaces.lagda.md

@@ -0,0 +1,63 @@
+# The complete metric abelian groups of real Banach spaces
+
+```agda
+module analysis.complete-metric-abelian-groups-real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.complete-metric-abelian-groups
+open import analysis.metric-abelian-groups
+open import analysis.metric-abelian-groups-normed-real-vector-spaces
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+
+open import real-numbers.metric-additive-group-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+Every [real Banach space](linear-algebra.real-banach-spaces.md) forms a
+[complete metric abelian group](analysis.complete-metric-abelian-groups.md)
+under addition.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  where
+
+  metric-ab-add-ℝ-Banach-Space : Metric-Ab l2 l1
+  metric-ab-add-ℝ-Banach-Space =
+    metric-ab-Normed-ℝ-Vector-Space (normed-vector-space-ℝ-Banach-Space V)
+
+  complete-metric-ab-add-ℝ-Banach-Space : Complete-Metric-Ab l2 l1
+  complete-metric-ab-add-ℝ-Banach-Space =
+    ( metric-ab-add-ℝ-Banach-Space , is-complete-metric-space-ℝ-Banach-Space V)
+```
+
+## Properties
+
+### The complete metric abelian group from the reals as a real Banach space equals the standard complete metric abelian group of the reals under addition
+
+```agda
+abstract
+  eq-complete-metric-ab-ℝ :
+    (l : Level) →
+    complete-metric-ab-add-ℝ-Banach-Space (real-banach-space-ℝ l) ＝
+    complete-metric-ab-add-ℝ l
+  eq-complete-metric-ab-ℝ l =
+    eq-type-subtype
+      ( is-complete-prop-Metric-Ab)
+      ( eq-metric-ab-normed-real-vector-space-metric-ab-ℝ l)
+```

src/analysis/complete-metric-abelian-groups.lagda.md

@@ -0,0 +1,65 @@
+# Complete metric abelian groups
+
+```agda
+module analysis.complete-metric-abelian-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.metric-abelian-groups
+
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import metric-spaces.complete-metric-spaces
+open import metric-spaces.metric-spaces
+```
+
+</details>
+
+## Idea
+
+A {{#concept "complete metric abelian group" Agda=Complete-Metric-Ab}} is a
+[metric abelian group](analysis.metric-abelian-groups.md) whose associated
+[metric space](metric-spaces.metric-spaces.md) is
+[complete](metric-spaces.complete-metric-spaces.md).
+
+## Definition
+
+```agda
+is-complete-prop-Metric-Ab : {l1 l2 : Level} → Metric-Ab l1 l2 → Prop (l1 ⊔ l2)
+is-complete-prop-Metric-Ab G =
+  is-complete-prop-Metric-Space (metric-space-Metric-Ab G)
+
+is-complete-Metric-Ab : {l1 l2 : Level} → Metric-Ab l1 l2 → UU (l1 ⊔ l2)
+is-complete-Metric-Ab G = is-complete-Metric-Space (metric-space-Metric-Ab G)
+
+Complete-Metric-Ab : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Complete-Metric-Ab l1 l2 = type-subtype (is-complete-prop-Metric-Ab {l1} {l2})
+```
+
+## Properties
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Complete-Metric-Ab l1 l2)
+  where
+
+  metric-ab-Complete-Metric-Ab : Metric-Ab l1 l2
+  metric-ab-Complete-Metric-Ab = pr1 G
+
+  metric-space-Complete-Metric-Ab : Metric-Space l1 l2
+  metric-space-Complete-Metric-Ab =
+    metric-space-Metric-Ab metric-ab-Complete-Metric-Ab
+
+  complete-metric-space-Complete-Metric-Ab : Complete-Metric-Space l1 l2
+  complete-metric-space-Complete-Metric-Ab =
+    ( metric-space-Complete-Metric-Ab , pr2 G)
+
+  type-Complete-Metric-Ab : UU l1
+  type-Complete-Metric-Ab = type-Metric-Ab metric-ab-Complete-Metric-Ab
+```

src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md

@@ -0,0 +1,105 @@
+# Convergent series in complete metric abelian groups
+
+```agda
+module analysis.convergent-series-complete-metric-abelian-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.complete-metric-abelian-groups
+open import analysis.convergent-series-metric-abelian-groups
+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.universe-levels
+
+open import metric-spaces.cauchy-sequences-complete-metric-spaces
+open import metric-spaces.cauchy-sequences-metric-spaces
+```
+
+</details>
+
+## Idea
+
+A [series](analysis.series-metric-abelian-groups.md)
+[converges](analysis.convergent-series-metric-abelian-groups.md) in a
+[complete metric abelian group](analysis.complete-metric-abelian-groups.md) if
+its partial sums form a
+[Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md).
+
+A slightly modified converse is also true: if a series converges, there
+[exists](foundation.existential-quantification.md) a modulus making it a Cauchy
+sequence.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Complete-Metric-Ab l1 l2)
+  (σ : series-Complete-Metric-Ab G)
+  where
+
+  is-sum-prop-series-Complete-Metric-Ab : type-Complete-Metric-Ab G → Prop l2
+  is-sum-prop-series-Complete-Metric-Ab = is-sum-prop-series-Metric-Ab σ
+
+  is-sum-series-Complete-Metric-Ab : type-Complete-Metric-Ab G → UU l2
+  is-sum-series-Complete-Metric-Ab = is-sum-series-Metric-Ab σ
+
+  is-convergent-prop-series-Complete-Metric-Ab : Prop (l1 ⊔ l2)
+  is-convergent-prop-series-Complete-Metric-Ab =
+    is-convergent-prop-series-Metric-Ab σ
+
+  is-convergent-series-Complete-Metric-Ab : UU (l1 ⊔ l2)
+  is-convergent-series-Complete-Metric-Ab = is-convergent-series-Metric-Ab σ
+```
+
+## Properties
+
+### If the partial sums of a series form a Cauchy sequence, the series converges
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Complete-Metric-Ab l1 l2)
+  (σ : series-Complete-Metric-Ab G)
+  where
+
+  is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab :
+    is-cauchy-sequence-Metric-Space
+      ( metric-space-Complete-Metric-Ab G)
+      ( partial-sum-series-Complete-Metric-Ab G σ) →
+    is-convergent-series-Complete-Metric-Ab G σ
+  is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab H =
+    has-limit-cauchy-sequence-Complete-Metric-Space
+      ( complete-metric-space-Complete-Metric-Ab G)
+      ( partial-sum-series-Complete-Metric-Ab G σ , H)
+```
+
+### If a series converges, there exists a modulus making its partial sums a Cauchy sequence
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Complete-Metric-Ab l1 l2)
+  (σ : series-Complete-Metric-Ab G)
+  where
+
+  is-cauchy-sequence-partial-sum-is-convergent-series-Complete-Metric-Ab :
+    is-convergent-series-Complete-Metric-Ab G σ →
+    is-inhabited
+      ( is-cauchy-sequence-Metric-Space
+        ( metric-space-Complete-Metric-Ab G)
+        ( partial-sum-series-Complete-Metric-Ab G σ))
+  is-cauchy-sequence-partial-sum-is-convergent-series-Complete-Metric-Ab
+    (lim , is-lim) =
+    map-is-inhabited
+      ( is-cauchy-has-limit-modulus-sequence-Metric-Space
+        ( metric-space-Complete-Metric-Ab G)
+        ( partial-sum-series-Complete-Metric-Ab G σ)
+        ( lim))
+      ( is-lim)
+```

src/analysis/convergent-series-real-banach-spaces.lagda.md

@@ -0,0 +1,106 @@
+# Convergent series in real Banach spaces
+
+```agda
+module analysis.convergent-series-real-banach-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.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.series-real-banach-spaces
+
+open import foundation.dependent-pair-types
+open import foundation.inhabited-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import linear-algebra.real-banach-spaces
+
+open import metric-spaces.cauchy-sequences-metric-spaces
+```
+
+</details>
+
+## Idea
+
+A [series](analysis.series-real-banach-spaces.md)
+[converges](analysis.convergent-series-metric-abelian-groups.md) in a
+[real Banach space](linear-algebra.real-banach-spaces.md) if its partial sums
+form a [Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md).
+
+A slightly modified converse is also true: if a series converges, there
+[exists](foundation.existential-quantification.md) a modulus making its partial
+sums a Cauchy sequence.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  is-sum-prop-series-ℝ-Banach-Space : type-ℝ-Banach-Space V → Prop l1
+  is-sum-prop-series-ℝ-Banach-Space = is-sum-prop-series-Metric-Ab σ
+
+  is-sum-series-ℝ-Banach-Space : type-ℝ-Banach-Space V → UU l1
+  is-sum-series-ℝ-Banach-Space = is-sum-series-Metric-Ab σ
+
+  is-convergent-prop-series-ℝ-Banach-Space : Prop (l1 ⊔ l2)
+  is-convergent-prop-series-ℝ-Banach-Space =
+    is-convergent-prop-series-Metric-Ab σ
+
+  is-convergent-series-ℝ-Banach-Space : UU (l1 ⊔ l2)
+  is-convergent-series-ℝ-Banach-Space = is-convergent-series-Metric-Ab σ
+```
+
+## Properties
+
+### If the partial sums of a series form a Cauchy sequence, the series converges
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space :
+    is-cauchy-sequence-Metric-Space
+      ( metric-space-ℝ-Banach-Space V)
+      ( partial-sum-series-ℝ-Banach-Space V σ) →
+    is-convergent-series-ℝ-Banach-Space V σ
+  is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space =
+    is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab
+      ( complete-metric-ab-add-ℝ-Banach-Space V)
+      ( σ)
+```
+
+### If a series converges, there exists a modulus making its partial sums a Cauchy sequence
+
+```agda
+module _
+  {l1 l2 : Level}
+  (V : ℝ-Banach-Space l1 l2)
+  (σ : series-ℝ-Banach-Space V)
+  where
+
+  is-cauchy-sequence-partial-sum-is-convergent-series-ℝ-Banach-Space :
+    is-convergent-series-ℝ-Banach-Space V σ →
+    is-inhabited
+      ( is-cauchy-sequence-Metric-Space
+        ( metric-space-ℝ-Banach-Space V)
+        ( partial-sum-series-ℝ-Banach-Space V σ))
+  is-cauchy-sequence-partial-sum-is-convergent-series-ℝ-Banach-Space
+    (lim , is-lim) =
+    map-is-inhabited
+      ( is-cauchy-has-limit-modulus-sequence-Metric-Space
+        ( metric-space-ℝ-Banach-Space V)
+        ( partial-sum-series-ℝ-Banach-Space V σ)
+        ( lim))
+      ( is-lim)
+```