The real number e

src/analysis.lagda.md

@@ -3,7 +3,20 @@
 ```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.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.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
+open import analysis.series-real-numbers public
 ```

src/analysis/absolute-convergence-series-real-banach-spaces.lagda.md

@@ -0,0 +1,193 @@
+# 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 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
+
+### 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 inequality-reasoning-Large-Poset ℝ-Large-Poset
+      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)
+      let
+        μ = pr1 ∘ cauchy-mod
+        is-mod-μ = pr2 ∘ cauchy-mod
+        lemma :
+          (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (μ ε) n →
+          leq-ℝ
+            ( dist-ℝ-Banach-Space V
+              ( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ k))
+              ( partial-sum-series-ℝ-Banach-Space V σ n))
+            ( real-ℚ⁺ ε)
+        lemma ε n k με≤n =
+          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-ℝ
+                  ( ε)
+                  ( _)
+                  ( _)
+                  ( is-mod-μ
+                    ( ε)
+                    ( n +ℕ k)
+                    ( n)
+                    ( transitive-leq-ℕ (μ ε) n (n +ℕ k) (leq-add-ℕ n k) με≤n)
+                    ( με≤n))
+        lemma' :
+          (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (μ ε) n → leq-ℕ n k →
+          leq-ℝ
+            ( dist-ℝ-Banach-Space V
+              ( partial-sum-series-ℝ-Banach-Space V σ k)
+              ( partial-sum-series-ℝ-Banach-Space V σ n))
+            ( real-ℚ⁺ ε)
+        lemma' ε n k με≤n n≤k =
+          let
+            (l , l+n=k) = subtraction-leq-ℕ n k n≤k
+          in
+            tr
+              ( λ p →
+                leq-ℝ
+                  ( dist-ℝ-Banach-Space V
+                    ( partial-sum-series-ℝ-Banach-Space V σ p)
+                    ( _))
+                  ( _))
+              ( commutative-add-ℕ n l ∙ l+n=k)
+              ( lemma ε n l με≤n)
+      is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space
+        ( V)
+        ( σ)
+        ( λ ε →
+          ( μ ε ,
+            λ a b με≤a με≤b →
+              rec-coproduct
+                ( λ a≤b →
+                  tr
+                    ( λ d → leq-ℝ d (real-ℚ⁺ ε))
+                    ( commutative-dist-ℝ-Banach-Space V _ _)
+                    ( lemma' ε a b με≤a a≤b))
+                ( lemma' ε b a με≤b)
+                ( linear-leq-ℕ a b)))
+```

src/analysis/absolute-convergence-series-real-numbers.lagda.md

@@ -0,0 +1,73 @@
+# 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))
+```

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

@@ -0,0 +1,63 @@
+# 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)
+```