The sum of geometric series in the real numbers (#1676)

Builds on #1675, #1673, and #1672.  Completes #1605.

Author: lowasser

src/commutative-algebra/commutative-rings.lagda.md

@@ -200,6 +200,13 @@ module _
   right-subtraction-Commutative-Ring =
     right-subtraction-Ring ring-Commutative-Ring
 
+  ap-right-subtraction-Commutative-Ring :
+    {x x' y y' : type-Commutative-Ring} → x ＝ x' → y ＝ y' →
+    right-subtraction-Commutative-Ring x y ＝
+    right-subtraction-Commutative-Ring x' y'
+  ap-right-subtraction-Commutative-Ring =
+    ap-right-subtraction-Ring ring-Commutative-Ring
+
   is-section-right-subtraction-Commutative-Ring :
     (x : type-Commutative-Ring) →
     ( add-Commutative-Ring' x ∘
@@ -659,3 +666,20 @@ module _
   preserves-concat-add-list-Commutative-Ring =
     preserves-concat-add-list-Ring ring-Commutative-Ring
 ```
+
+### The sum of `x - y` and `y - z` is `x - z`
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l)
+  where
+
+  add-right-subtraction-Commutative-Ring :
+    (x y z : type-Commutative-Ring R) →
+    add-Commutative-Ring R
+      ( right-subtraction-Commutative-Ring R x y)
+      ( right-subtraction-Commutative-Ring R y z) ＝
+    right-subtraction-Commutative-Ring R x z
+  add-right-subtraction-Commutative-Ring =
+    add-right-subtraction-Ab (ab-Commutative-Ring R)
+```

src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md

@@ -10,7 +10,10 @@ module commutative-algebra.geometric-sequences-commutative-rings where
 open import commutative-algebra.commutative-rings
 open import commutative-algebra.commutative-semirings
 open import commutative-algebra.geometric-sequences-commutative-semirings
+open import commutative-algebra.groups-of-units-commutative-rings
+open import commutative-algebra.invertible-elements-commutative-rings
 open import commutative-algebra.powers-of-elements-commutative-rings
+open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings
 
 open import elementary-number-theory.natural-numbers
 
@@ -288,6 +291,11 @@ module _
 ```agda
 module _
   {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
+  (let _*R_ = mul-Commutative-Ring R)
+  (let _+R_ = add-Commutative-Ring R)
+  (let _-R_ = right-subtraction-Commutative-Ring R)
+  (let zero-R = zero-Commutative-Ring R)
+  (let one-R = one-Commutative-Ring R)
   where
 
   abstract
@@ -307,4 +315,141 @@ module _
         ( commutative-semiring-Commutative-Ring R)
         ( a)
         ( r)
+
+  abstract
+    compute-sum-standard-geometric-fin-sequence-Commutative-Ring :
+      (H :
+        is-invertible-element-Commutative-Ring R
+          ( right-subtraction-Commutative-Ring R (one-Commutative-Ring R) r)) →
+      (n : ℕ) →
+      sum-standard-geometric-fin-sequence-Commutative-Ring R a r n ＝
+      mul-Commutative-Ring R
+        ( mul-Commutative-Ring R
+          ( a)
+          ( inv-is-invertible-element-Commutative-Ring R H))
+        ( right-subtraction-Commutative-Ring R
+          ( one-Commutative-Ring R)
+          ( power-Commutative-Ring R n r))
+    compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+      (1/⟨1-r⟩ , H) 0 =
+      inv
+        ( equational-reasoning
+          (a *R 1/⟨1-r⟩) *R (one-R -R one-R)
+          ＝ (a *R 1/⟨1-r⟩) *R zero-R
+            by
+              ap-mul-Commutative-Ring R
+                ( refl)
+                ( right-inverse-law-add-Commutative-Ring R one-R)
+          ＝ zero-R
+            by right-zero-law-mul-Commutative-Ring R _)
+    compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+      (1/⟨1-r⟩ , H) (succ-ℕ n) =
+      equational-reasoning
+        sum-standard-geometric-fin-sequence-Commutative-Ring R a r (succ-ℕ n)
+        ＝
+          sum-standard-geometric-fin-sequence-Commutative-Ring R a r n +R
+          seq-standard-geometric-sequence-Commutative-Ring R a r n
+          by
+            cons-sum-fin-sequence-type-Commutative-Ring R
+              ( n)
+              ( standard-geometric-fin-sequence-Commutative-Ring R
+                ( a)
+                ( r)
+                ( succ-ℕ n))
+              ( refl)
+        ＝
+          ( (a *R 1/⟨1-r⟩) *R (one-R -R power-Commutative-Ring R n r)) +R
+          ( a *R power-Commutative-Ring R n r)
+          by
+            ap-add-Commutative-Ring R
+              ( compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+                ( 1/⟨1-r⟩ , H)
+                ( n))
+              ( inv
+                ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring R
+                  ( a)
+                  ( r)
+                  ( n)))
+        ＝
+          ( a *R (1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r))) +R
+          ( a *R (one-R *R power-Commutative-Ring R n r))
+          by
+            ap-add-Commutative-Ring R
+              ( associative-mul-Commutative-Ring R _ _ _)
+              ( ap-mul-Commutative-Ring R
+                ( refl)
+                ( inv (left-unit-law-mul-Commutative-Ring R _)))
+        ＝
+          a *R
+          ( (1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
+            (one-R *R power-Commutative-Ring R n r))
+          by inv (left-distributive-mul-add-Commutative-Ring R a _ _)
+        ＝
+          a *R
+          ( ( 1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
+            ( (1/⟨1-r⟩ *R (one-R -R r)) *R power-Commutative-Ring R n r))
+            by
+              ap-mul-Commutative-Ring R
+                ( refl)
+                ( ap-add-Commutative-Ring R
+                  ( refl)
+                  ( ap-mul-Commutative-Ring R (inv (pr2 H)) refl))
+        ＝
+          a *R
+          ( ( 1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
+            ( 1/⟨1-r⟩ *R ((one-R -R r) *R power-Commutative-Ring R n r)))
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( ap-add-Commutative-Ring R
+                ( refl)
+                ( associative-mul-Commutative-Ring R _ _ _))
+        ＝
+          a *R
+          ( 1/⟨1-r⟩ *R
+            ( ( one-R -R power-Commutative-Ring R n r) +R
+              ( (one-R -R r) *R power-Commutative-Ring R n r)))
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( inv (left-distributive-mul-add-Commutative-Ring R _ _ _))
+        ＝
+          ( a *R 1/⟨1-r⟩) *R
+          ( ( one-R -R power-Commutative-Ring R n r) +R
+            ( (one-R -R r) *R power-Commutative-Ring R n r))
+          by inv (associative-mul-Commutative-Ring R _ _ _)
+        ＝
+          ( a *R 1/⟨1-r⟩) *R
+          ( ( one-R -R power-Commutative-Ring R n r) +R
+            ( (one-R *R power-Commutative-Ring R n r) -R
+              (r *R power-Commutative-Ring R n r)))
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( ap-add-Commutative-Ring R
+                ( refl)
+                ( right-distributive-mul-right-subtraction-Commutative-Ring R
+                  ( _)
+                  ( _)
+                  ( _)))
+        ＝
+          ( a *R 1/⟨1-r⟩) *R
+          ( ( one-R -R power-Commutative-Ring R n r) +R
+            ( power-Commutative-Ring R n r -R
+              power-Commutative-Ring R (succ-ℕ n) r))
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( ap-add-Commutative-Ring R
+                ( refl)
+                ( ap-right-subtraction-Commutative-Ring R
+                  ( left-unit-law-mul-Commutative-Ring R _)
+                  ( inv (power-succ-Commutative-Ring' R n r))))
+        ＝
+          ( a *R 1/⟨1-r⟩) *R
+          ( one-R -R power-Commutative-Ring R (succ-ℕ n) r)
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( add-right-subtraction-Commutative-Ring R _ _ _)
 ```

src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md

@@ -30,6 +30,7 @@ open import elementary-number-theory.ring-of-rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
 open import foundation.binary-transport
+open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types
 open import foundation.negated-equality
@@ -111,102 +112,14 @@ module _
     compute-sum-standard-geometric-fin-sequence-ℚ :
       (n : ℕ) →
       sum-standard-geometric-fin-sequence-ℚ a r n ＝
-      ( a *ℚ
-        ( (one-ℚ -ℚ power-ℚ n r) *ℚ
-          rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)))
-    compute-sum-standard-geometric-fin-sequence-ℚ 0 =
-      inv
-        ( equational-reasoning
-          a *ℚ ((one-ℚ -ℚ one-ℚ) *ℚ _)
-          ＝ a *ℚ (zero-ℚ *ℚ _)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-mul-ℚ (right-inverse-law-add-ℚ one-ℚ) refl)
-          ＝ a *ℚ zero-ℚ
-            by ap-mul-ℚ refl (left-zero-law-mul-ℚ _)
-          ＝ zero-ℚ
-            by right-zero-law-mul-ℚ a)
-    compute-sum-standard-geometric-fin-sequence-ℚ (succ-ℕ n) =
-      let
-        1/⟨1-r⟩ = rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)
-      in
-        equational-reasoning
-          sum-standard-geometric-fin-sequence-ℚ a r (succ-ℕ n)
-          ＝
-            sum-standard-geometric-fin-sequence-ℚ a r n +ℚ
-            seq-standard-geometric-sequence-ℚ a r n
-            by
-              cons-sum-fin-sequence-type-Commutative-Ring
-                ( commutative-ring-ℚ)
-                ( n)
-                ( _)
-                ( refl)
-          ＝
-            ( a *ℚ
-              ( (one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩)) +ℚ
-            ( a *ℚ power-ℚ n r)
-            by
-              ap-add-ℚ
-                ( compute-sum-standard-geometric-fin-sequence-ℚ n)
-                ( compute-standard-geometric-sequence-ℚ a r n)
-          ＝
-            a *ℚ
-            (((one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩) +ℚ power-ℚ n r)
-            by inv (left-distributive-mul-add-ℚ a _ _)
-          ＝
-            a *ℚ
-            ( (((one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩) +ℚ
-              (power-ℚ n r *ℚ (one-ℚ -ℚ r)) *ℚ 1/⟨1-r⟩))
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-add-ℚ
-                  ( refl)
-                  ( inv
-                    ( cancel-right-mul-div-ℚˣ _
-                      ( invertible-diff-neq-ℚ r one-ℚ r≠1))))
-          ＝
-            a *ℚ
-            ( ( (one-ℚ -ℚ power-ℚ n r) +ℚ (power-ℚ n r *ℚ (one-ℚ -ℚ r))) *ℚ
-              1/⟨1-r⟩)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( inv (right-distributive-mul-add-ℚ _ _ 1/⟨1-r⟩))
-          ＝
-            a *ℚ
-            ( ( one-ℚ -ℚ power-ℚ n r +ℚ
-                ((power-ℚ n r *ℚ one-ℚ) -ℚ (power-ℚ n r *ℚ r))) *ℚ
-              1/⟨1-r⟩)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-mul-ℚ
-                  ( ap-add-ℚ refl (left-distributive-mul-diff-ℚ _ _ _))
-                  ( refl))
-          ＝
-            a *ℚ
-            ( ( one-ℚ -ℚ power-ℚ n r +ℚ
-                ((power-ℚ n r -ℚ power-ℚ (succ-ℕ n) r))) *ℚ
-              1/⟨1-r⟩)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-mul-ℚ
-                  ( ap-add-ℚ
-                    ( refl)
-                    ( ap-diff-ℚ
-                      ( right-unit-law-mul-ℚ _)
-                      ( inv (power-succ-ℚ n r))))
-                  ( refl))
-          ＝ a *ℚ ((one-ℚ -ℚ power-ℚ (succ-ℕ n) r) *ℚ 1/⟨1-r⟩)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-mul-ℚ
-                  ( mul-right-div-Group group-add-ℚ _ _ _)
-                  ( refl))
+      ( (a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)) *ℚ
+        (one-ℚ -ℚ power-ℚ n r))
+    compute-sum-standard-geometric-fin-sequence-ℚ =
+      compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+        ( commutative-ring-ℚ)
+        ( a)
+        ( r)
+        ( pr2 (invertible-diff-neq-ℚ r one-ℚ r≠1))
 ```
 
 ### If `|r| < 1`, the sum of the standard geometric sequence `n ↦ arⁿ` is `a/(1-r)`
@@ -241,30 +154,24 @@ module _
           ( inv
             ( eq-htpy (compute-sum-standard-geometric-fin-sequence-ℚ a r r≠1)))
           ( equational-reasoning
-            a *ℚ
-            ( (one-ℚ -ℚ zero-ℚ) *ℚ
-              rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1))
+            a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1) *ℚ
+            (one-ℚ -ℚ zero-ℚ)
+            ＝
+              a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1) *ℚ one-ℚ
+              by ap-mul-ℚ refl (right-zero-law-diff-ℚ _)
             ＝
-              a *ℚ
-              ( one-ℚ *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1))
-              by ap-mul-ℚ refl (ap-mul-ℚ (right-zero-law-diff-ℚ one-ℚ) refl)
-            ＝ a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)
-              by ap-mul-ℚ refl (left-unit-law-mul-ℚ _))
-          ( uniformly-continuous-map-limit-sequence-Metric-Space
+              a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)
+              by right-unit-law-mul-ℚ _)
+          ( preserves-limits-sequence-uniformly-continuous-function-Metric-Space
             ( metric-space-ℚ)
             ( metric-space-ℚ)
             ( comp-uniformly-continuous-function-Metric-Space
               ( metric-space-ℚ)
               ( metric-space-ℚ)
               ( metric-space-ℚ)
-              ( uniformly-continuous-left-mul-ℚ a)
-              ( comp-uniformly-continuous-function-Metric-Space
-                ( metric-space-ℚ)
-                ( metric-space-ℚ)
-                ( metric-space-ℚ)
-                ( uniformly-continuous-right-mul-ℚ
-                  ( rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)))
-                ( uniformly-continuous-diff-ℚ one-ℚ)))
+              ( uniformly-continuous-left-mul-ℚ
+                ( a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)))
+              ( uniformly-continuous-diff-ℚ one-ℚ))
             ( λ n → power-ℚ n r)
             ( zero-ℚ)
             ( is-zero-limit-power-le-one-abs-ℚ r |r|<1))

src/elementary-number-theory/triangular-numbers.lagda.md

@@ -284,7 +284,7 @@ abstract
           by ap-mul-ℚ refl (right-zero-law-diff-ℚ one-ℚ)
         ＝ rational-ℕ 2
           by right-unit-law-mul-ℚ _)
-      ( uniformly-continuous-map-limit-sequence-Metric-Space
+      ( preserves-limits-sequence-uniformly-continuous-function-Metric-Space
         ( metric-space-ℚ)
         ( metric-space-ℚ)
         ( comp-uniformly-continuous-function-Metric-Space

src/literature/100-theorems.lagda.md

@@ -116,6 +116,16 @@ open import foundation.cantors-theorem using
   ( theorem-Cantor)
 ```
 
+### 66. Sum of a Geometric Series {#66}
+
+**Author:** [Louis Wasserman](https://github.com/lowasser)
+
+```agda
+open import real-numbers.geometric-sequences-real-numbers using
+  ( compute-sum-standard-geometric-fin-sequence-ℝ ;
+    compute-sum-standard-geometric-series-ℝ)
+```
+
 ### 68. Sum of an arithmetic series {#68}
 
 **Author:** [malarbol](http://www.github.com/malarbol)