Series and convergence

src/analysis.lagda.md

@@ -0,0 +1,8 @@
+# Analysis
+
+```agda
+module analysis where
+
+open import analysis.commutative-rings-in-complete-metric-spaces public
+open import analysis.series public
+```

src/analysis/commutative-rings-in-complete-metric-spaces.lagda.md

@@ -0,0 +1,100 @@
+# Commutative rings in complete metric spaces
+
+```agda
+module analysis.commutative-rings-in-complete-metric-spaces where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.commutative-rings
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+
+open import metric-spaces.complete-metric-spaces
+open import metric-spaces.metric-spaces
+open import metric-spaces.metric-structures
+open import metric-spaces.premetric-spaces
+open import metric-spaces.premetric-structures
+```
+
+</details>
+
+## Idea
+
+A commutative ring in a complete metric space is a setting in which power series
+and their convergence can be considered.
+
+## Definition
+
+```agda
+Commutative-Ring-In-Complete-Metric-Space :
+  (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Commutative-Ring-In-Complete-Metric-Space l1 l2 =
+  Σ ( Commutative-Ring l1)
+    ( λ R →
+      Σ ( Premetric l2 (type-Commutative-Ring R))
+        ( λ μ →
+          Σ ( is-metric-Premetric μ)
+            ( λ is-metric-μ →
+              is-complete-Metric-Space
+                ( (type-Commutative-Ring R , μ) , is-metric-μ))))
+
+module _
+  {l1 l2 : Level} (RM : Commutative-Ring-In-Complete-Metric-Space l1 l2)
+  where
+
+  commutative-ring-Commutative-Ring-In-Complete-Metric-Space :
+    Commutative-Ring l1
+  commutative-ring-Commutative-Ring-In-Complete-Metric-Space = pr1 RM
+
+  type-Commutative-Ring-In-Complete-Metric-Space : UU l1
+  type-Commutative-Ring-In-Complete-Metric-Space =
+    type-Commutative-Ring
+      ( commutative-ring-Commutative-Ring-In-Complete-Metric-Space)
+
+  structure-Commutative-Ring-In-Complete-Metric-Space :
+    Premetric l2 type-Commutative-Ring-In-Complete-Metric-Space
+  structure-Commutative-Ring-In-Complete-Metric-Space = pr1 (pr2 RM)
+
+  is-metric-structure-Commutative-Ring-In-Complete-Metric-Space :
+    is-metric-Premetric structure-Commutative-Ring-In-Complete-Metric-Space
+  is-metric-structure-Commutative-Ring-In-Complete-Metric-Space =
+    pr1 (pr2 (pr2 RM))
+
+  metric-space-Commutative-Ring-In-Complete-Metric-Space : Metric-Space l1 l2
+  metric-space-Commutative-Ring-In-Complete-Metric-Space =
+    ( ( type-Commutative-Ring-In-Complete-Metric-Space ,
+        structure-Commutative-Ring-In-Complete-Metric-Space) ,
+      is-metric-structure-Commutative-Ring-In-Complete-Metric-Space)
+
+  is-complete-metric-space-Commutative-Ring-In-Complete-Metric-Space :
+    is-complete-Metric-Space
+      metric-space-Commutative-Ring-In-Complete-Metric-Space
+  is-complete-metric-space-Commutative-Ring-In-Complete-Metric-Space =
+    pr2 (pr2 (pr2 RM))
+
+  complete-metric-space-Commutative-Ring-In-Complete-Metric-Space :
+    Complete-Metric-Space l1 l2
+  complete-metric-space-Commutative-Ring-In-Complete-Metric-Space =
+    ( metric-space-Commutative-Ring-In-Complete-Metric-Space ,
+      is-complete-metric-space-Commutative-Ring-In-Complete-Metric-Space)
+```
+
+### Construction
+
+```agda
+commutative-ring-in-complete-metric-space-Commutative-Ring-Complete-Metric-Space :
+  {l1 l2 : Level} →
+  (R : Commutative-Ring l1) (M : Complete-Metric-Space l1 l2) →
+  (type-Commutative-Ring R ＝ type-Complete-Metric-Space M) →
+  Commutative-Ring-In-Complete-Metric-Space l1 l2
+commutative-ring-in-complete-metric-space-Commutative-Ring-Complete-Metric-Space
+  R M refl =
+    ( R ,
+      structure-Complete-Metric-Space M ,
+      is-metric-structure-Complete-Metric-Space M ,
+      is-complete-metric-space-Complete-Metric-Space M)
+```

src/analysis/series.lagda.md

@@ -0,0 +1,75 @@
+# Series
+
+```agda
+module analysis.series where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.commutative-rings-in-complete-metric-spaces
+
+open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings
+
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.sequences
+open import foundation.universe-levels
+
+open import metric-spaces.limits-of-sequences-metric-spaces
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+A series is an infinite sum taken over the natural numbers. If it has a limit,
+it is said to converge, otherwise it is said to diverge.
+
+## Definition
+
+```agda
+record
+  series
+    {l1 l2 : Level} (RM : Commutative-Ring-In-Complete-Metric-Space l1 l2) :
+    UU l1
+  where
+
+  constructor series-terms
+
+  field
+    terms-series : sequence (type-Commutative-Ring-In-Complete-Metric-Space RM)
+
+open series public
+
+module _
+  {l1 l2 : Level}
+  (RM : Commutative-Ring-In-Complete-Metric-Space l1 l2) (σ : series RM)
+  where
+
+  partial-sums-series :
+    sequence (type-Commutative-Ring-In-Complete-Metric-Space RM)
+  partial-sums-series n =
+    sum-fin-sequence-type-Commutative-Ring
+      ( commutative-ring-Commutative-Ring-In-Complete-Metric-Space RM)
+      ( n)
+      ( λ k → terms-series σ (nat-Fin n k))
+
+  converges-series : UU (l1 ⊔ l2)
+  converges-series =
+    has-limit-sequence-Metric-Space
+      ( metric-space-Commutative-Ring-In-Complete-Metric-Space RM)
+      ( partial-sums-series)
+
+  is-prop-converges-series : is-prop converges-series
+  is-prop-converges-series =
+    is-prop-has-limit-sequence-Metric-Space
+      ( metric-space-Commutative-Ring-In-Complete-Metric-Space RM)
+      ( partial-sums-series)
+
+  converges-prop-series : Prop (l1 ⊔ l2)
+  pr1 converges-prop-series = converges-series
+  pr2 converges-prop-series = is-prop-converges-series
+```

src/metric-spaces/complete-metric-spaces.lagda.md

@@ -21,6 +21,8 @@ open import foundation.universe-levels
 open import metric-spaces.cauchy-approximations-metric-spaces
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces
 open import metric-spaces.metric-spaces
+open import metric-spaces.metric-structures
+open import metric-spaces.premetric-structures
 ```
 
 </details>
@@ -85,6 +87,15 @@ module _
   is-complete-metric-space-Complete-Metric-Space :
     is-complete-Metric-Space metric-space-Complete-Metric-Space
   is-complete-metric-space-Complete-Metric-Space = pr2 A
+
+  structure-Complete-Metric-Space : Premetric l2 type-Complete-Metric-Space
+  structure-Complete-Metric-Space =
+    structure-Metric-Space metric-space-Complete-Metric-Space
+
+  is-metric-structure-Complete-Metric-Space :
+    is-metric-Premetric structure-Complete-Metric-Space
+  is-metric-structure-Complete-Metric-Space =
+    is-metric-structure-Metric-Space metric-space-Complete-Metric-Space
 ```
 
 ### The equivalence between Cauchy approximations and convergent Cauchy approximations in a complete metric space