Pull out a lemma

Author: lowasser

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

@@ -150,57 +150,16 @@ module _
                 ( transitive-leq-ℕ (pr1 (M ε)) n (n +ℕ k) (leq-add-ℕ n k) με≤n)
                 ( με≤n))
 
-    neighborhood-leq-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space :
-      (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (pr1 (M ε)) n → leq-ℕ n k →
-      neighborhood-ℝ-Banach-Space
-        ( V)
-        ( ε)
-        ( partial-sum-series-ℝ-Banach-Space V σ k)
-        ( partial-sum-series-ℝ-Banach-Space V σ n)
-    neighborhood-leq-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space
-      ε 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)
-          ( neighborhood-add-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space
-            ( ε)
-            ( n)
-            ( l)
-            ( με≤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
-      ε =
-      ( pr1 (M ε) ,
-        λ a b με≤a με≤b →
-          rec-coproduct
-            ( λ a≤b →
-              tr
-                ( λ d → leq-ℝ d (real-ℚ⁺ ε))
-                ( commutative-dist-ℝ-Banach-Space V _ _)
-                ( neighborhood-leq-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space
-                  ( ε)
-                  ( a)
-                  ( b)
-                  ( με≤a)
-                  ( a≤b)))
-            ( neighborhood-leq-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space
-              ( ε)
-              ( b)
-              ( a)
-              ( με≤b))
-            ( linear-leq-ℕ a b))
+    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

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
@@ -772,6 +773,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)