The sum of the reciprocals of the triangular numbers is 2 (#1665)

Completes #1606, the 42nd of the list of 100 theorems.

Author: lowasser

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

@@ -39,6 +39,15 @@ module _
   {l1 l2 : Level} (G : Metric-Ab l1 l2) (σ : series-Metric-Ab G)
   where
 
+  is-sum-prop-series-Metric-Ab : type-Metric-Ab G → Prop l2
+  is-sum-prop-series-Metric-Ab =
+    is-limit-prop-sequence-Metric-Space
+      ( metric-space-Metric-Ab G)
+      ( partial-sum-series-Metric-Ab G σ)
+
+  is-sum-series-Metric-Ab : type-Metric-Ab G → UU l2
+  is-sum-series-Metric-Ab s = type-Prop (is-sum-prop-series-Metric-Ab s)
+
   is-convergent-prop-series-Metric-Ab : Prop (l1 ⊔ l2)
   is-convergent-prop-series-Metric-Ab =
     subtype-convergent-sequence-Metric-Space

src/elementary-number-theory.lagda.md

@@ -122,6 +122,7 @@ open import elementary-number-theory.maximum-rational-numbers public
 open import elementary-number-theory.maximum-standard-finite-types public
 open import elementary-number-theory.mediant-integer-fractions public
 open import elementary-number-theory.mersenne-primes public
+open import elementary-number-theory.metric-additive-group-of-rational-numbers public
 open import elementary-number-theory.minima-and-maxima-rational-numbers public
 open import elementary-number-theory.minimum-natural-numbers public
 open import elementary-number-theory.minimum-positive-rational-numbers public

src/elementary-number-theory/addition-rational-numbers.lagda.md

@@ -325,9 +325,9 @@ abstract
 
 ```agda
 abstract
-  succ-rational-int-ℕ :
-    (n : ℕ) → succ-ℚ (rational-ℤ (int-ℕ n)) ＝ rational-ℤ (int-ℕ (succ-ℕ n))
-  succ-rational-int-ℕ n = succ-rational-ℤ _ ∙ ap rational-ℤ (succ-int-ℕ n)
+  succ-rational-ℕ :
+    (n : ℕ) → succ-ℚ (rational-ℕ n) ＝ rational-ℕ (succ-ℕ n)
+  succ-rational-ℕ n = succ-rational-ℤ _ ∙ ap rational-ℤ (succ-int-ℕ n)
 ```
 
 ## See also

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

@@ -153,7 +153,7 @@ module _
     compute-standard-arithmetic-sequence-ℚ⁺ (succ-ℕ n) =
       ( ap
         ( add-ℚ (rational-ℚ⁺ a))
-        ( ( ap (mul-ℚ' (rational-ℚ⁺ d)) (inv (succ-rational-int-ℕ n))) ∙
+        ( ( ap (mul-ℚ' (rational-ℚ⁺ d)) (inv (succ-rational-ℕ n))) ∙
           ( mul-left-succ-ℚ (rational-ℕ n) (rational-ℚ⁺ d)) ∙
           ( commutative-add-ℚ
             ( rational-ℚ⁺ d)

src/elementary-number-theory/difference-rational-numbers.lagda.md

@@ -187,3 +187,19 @@ abstract
       ＝ rational-ℤ (x -ℤ y)
         by add-rational-ℤ x (neg-ℤ y)
 ```
+
+### The difference of the successor of a rational number and the rational number is one
+
+```agda
+abstract
+  diff-succ-ℚ : (q : ℚ) → succ-ℚ q -ℚ q ＝ one-ℚ
+  diff-succ-ℚ q =
+    equational-reasoning
+      (one-ℚ +ℚ q) -ℚ q
+      ＝ one-ℚ +ℚ (q -ℚ q)
+        by associative-add-ℚ _ _ _
+      ＝ one-ℚ +ℚ zero-ℚ
+        by ap-add-ℚ refl (right-inverse-law-add-ℚ q)
+      ＝ one-ℚ
+        by right-unit-law-add-ℚ _
+```

src/elementary-number-theory/distance-rational-numbers.lagda.md

@@ -64,6 +64,22 @@ abstract
     inv (abs-neg-ℚ _) ∙ ap abs-ℚ (distributive-neg-diff-ℚ _ _)
 ```
 
+### Negation preserves distance
+
+```agda
+abstract
+  dist-neg-ℚ : (p q : ℚ) → dist-ℚ (neg-ℚ p) (neg-ℚ q) ＝ dist-ℚ p q
+  dist-neg-ℚ p q =
+    equational-reasoning
+      abs-ℚ (neg-ℚ p -ℚ neg-ℚ q)
+      ＝ abs-ℚ (neg-ℚ p +ℚ q)
+        by ap abs-ℚ (ap-add-ℚ refl (neg-neg-ℚ q))
+      ＝ abs-ℚ (q -ℚ p)
+        by ap abs-ℚ (commutative-add-ℚ _ _)
+      ＝ dist-ℚ p q
+        by commutative-dist-ℚ q p
+```
+
 ### A rational number's distance from itself is zero
 
 ```agda

src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md

@@ -0,0 +1,41 @@
+# The metric additive group of rational numbers
+
+```agda
+module elementary-number-theory.metric-additive-group-of-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.metric-abelian-groups
+
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.additive-group-of-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.metric-space-of-rational-numbers
+open import metric-spaces.metric-spaces
+```
+
+</details>
+
+## Idea
+
+[Addition](elementary-number-theory.addition-rational-numbers.md) on the
+[rational numbers](elementary-number-theory.rational-numbers.md) forms a
+[metric abelian group](analysis.metric-abelian-groups.md).
+
+## Definition
+
+```agda
+metric-ab-add-ℚ : Metric-Ab lzero lzero
+metric-ab-add-ℚ =
+  ( abelian-group-add-ℚ ,
+    pseudometric-structure-Metric-Space metric-space-ℚ ,
+    is-extensional-pseudometric-space-ℚ ,
+    is-isometry-neg-ℚ ,
+    is-isometry-add-ℚ)
+```

src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md

@@ -28,6 +28,7 @@ open import elementary-number-theory.strict-inequality-integers
 open import elementary-number-theory.strict-inequality-positive-rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
+open import foundation.action-on-identifications-binary-functions
 open import foundation.binary-transport
 open import foundation.dependent-pair-types
 open import foundation.empty-types
@@ -107,6 +108,10 @@ mul-ℚ⁺ = mul-Submonoid monoid-mul-ℚ submonoid-mul-ℚ⁺
 
 infixl 40 _*ℚ⁺_
 _*ℚ⁺_ = mul-ℚ⁺
+
+ap-mul-ℚ⁺ :
+  {x x' : ℚ⁺} → x ＝ x' → {y y' : ℚ⁺} → y ＝ y' → mul-ℚ⁺ x y ＝ mul-ℚ⁺ x' y'
+ap-mul-ℚ⁺ = ap-binary mul-ℚ⁺
 ```
 
 ## Properties
@@ -293,6 +298,14 @@ abstract
       ( preserves-leq-left-mul-ℚ⁺ p q r q≤r)
 ```
 
+### `2q = q + q`
+
+```agda
+abstract
+  mul-two-ℚ⁺ : (q : ℚ⁺) → two-ℚ⁺ *ℚ⁺ q ＝ q +ℚ⁺ q
+  mul-two-ℚ⁺ (q , _) = eq-ℚ⁺ (mul-two-ℚ q)
+```
+
 ### Multiplication of a positive rational by another positive rational less than 1 is a strictly deflationary map
 
 ```agda

src/elementary-number-theory/nonzero-natural-numbers.lagda.md

@@ -83,6 +83,9 @@ one-ℕ⁺ = one-nonzero-ℕ
 succ-nonzero-ℕ : nonzero-ℕ → nonzero-ℕ
 pr1 (succ-nonzero-ℕ (x , _)) = succ-ℕ x
 pr2 (succ-nonzero-ℕ (x , _)) = is-nonzero-succ-ℕ x
+
+succ-ℕ⁺ : ℕ⁺ → ℕ⁺
+succ-ℕ⁺ = succ-nonzero-ℕ
 ```
 
 ### The successor function from the natural numbers to the nonzero natural numbers
@@ -139,8 +142,7 @@ _+ℕ⁺_ = add-nonzero-ℕ
 ```agda
 mul-nonzero-ℕ : nonzero-ℕ → nonzero-ℕ → nonzero-ℕ
 pr1 (mul-nonzero-ℕ (p , p≠0) (q , q≠0)) = p *ℕ q
-pr2 (mul-nonzero-ℕ (p , p≠0) (q , q≠0)) pq=0 =
-  rec-coproduct p≠0 q≠0 (is-zero-summand-is-zero-mul-ℕ p q pq=0)
+pr2 (mul-nonzero-ℕ (p , p≠0) (q , q≠0)) = is-nonzero-mul-ℕ p q p≠0 q≠0
 
 infixl 40 _*ℕ⁺_
 _*ℕ⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺

src/elementary-number-theory/positive-rational-numbers.lagda.md

@@ -190,6 +190,9 @@ abstract
 ```agda
 positive-rational-ℕ⁺ : ℕ⁺ → ℚ⁺
 positive-rational-ℕ⁺ n = positive-rational-positive-ℤ (positive-int-ℕ⁺ n)
+
+two-ℚ⁺ : ℚ⁺
+two-ℚ⁺ = positive-rational-ℕ⁺ (2 , λ ())
 ```
 
 ### The rational image of a positive integer fraction is positive