Multiplication of real numbers (#1384)

Work-in-progress, not ready for review, but at least putting this here
to show how the parts fit together.

Will complete #1353 .

Author: lowasser

src/elementary-number-theory.lagda.md

@@ -9,6 +9,7 @@
 ```agda
 module elementary-number-theory where
 
+open import elementary-number-theory.absolute-value-closed-intervals-rational-numbers public
 open import elementary-number-theory.absolute-value-integers public
 open import elementary-number-theory.absolute-value-rational-numbers public
 open import elementary-number-theory.ackermann-function public
@@ -115,6 +116,7 @@ open import elementary-number-theory.kolakoski-sequence public
 open import elementary-number-theory.legendre-symbol public
 open import elementary-number-theory.lower-bounds-natural-numbers public
 open import elementary-number-theory.maximum-natural-numbers public
+open import elementary-number-theory.maximum-nonnegative-rational-numbers public
 open import elementary-number-theory.maximum-positive-rational-numbers public
 open import elementary-number-theory.maximum-rational-numbers public
 open import elementary-number-theory.maximum-standard-finite-types public

src/elementary-number-theory/absolute-value-closed-intervals-rational-numbers.lagda.md

@@ -0,0 +1,88 @@
+# Absolute value on closed intervals in the rational numbers
+
+```agda
+module elementary-number-theory.absolute-value-closed-intervals-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.absolute-value-rational-numbers
+open import elementary-number-theory.closed-intervals-rational-numbers
+open import elementary-number-theory.inequality-nonnegative-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.maximum-nonnegative-rational-numbers
+open import elementary-number-theory.maximum-rational-numbers
+open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.binary-transport
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+```
+
+</details>
+
+## Idea
+
+The
+[absolute value](elementary-number-theory.absolute-value-rational-numbers.md) of
+an element of a
+[closed interval](elementary-number-theory.closed-intervals-rational-numbers.md)
+`[a, b]` of [rational numbers](elementary-number-theory.rational-numbers.md) is
+bounded by `max(|a|, |b|)`.
+
+## Definition
+
+```agda
+max-abs-closed-interval-ℚ : closed-interval-ℚ → ℚ⁰⁺
+max-abs-closed-interval-ℚ ((p , q) , p≤q) = max-ℚ⁰⁺ (abs-ℚ p) (abs-ℚ q)
+
+rational-max-abs-closed-interval-ℚ : closed-interval-ℚ → ℚ
+rational-max-abs-closed-interval-ℚ [p,q] =
+  rational-ℚ⁰⁺ (max-abs-closed-interval-ℚ [p,q])
+```
+
+## Properties
+
+### If `r ∈ [p,q]`, then `|r| ≤ max(|p|, |q|)`
+
+```agda
+abstract
+  leq-max-abs-is-in-closed-interval-ℚ :
+    ([p,q] : closed-interval-ℚ) (r : ℚ) → is-in-closed-interval-ℚ [p,q] r →
+    leq-ℚ⁰⁺ (abs-ℚ r) (max-abs-closed-interval-ℚ [p,q])
+  leq-max-abs-is-in-closed-interval-ℚ ((p , q) , p≤q) r (p≤r , r≤q) =
+    rec-coproduct
+      ( λ r≤0 →
+        transitive-leq-ℚ
+          ( rational-abs-ℚ r)
+          ( rational-abs-ℚ p)
+          ( max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q))
+          ( leq-left-max-ℚ _ _)
+          ( leq-abs-leq-leq-neg-ℚ
+            ( r)
+            ( rational-abs-ℚ p)
+            ( transitive-leq-ℚ r zero-ℚ (rational-abs-ℚ p)
+              ( leq-zero-rational-ℚ⁰⁺ (abs-ℚ p))
+              ( r≤0))
+            ( transitive-leq-ℚ (neg-ℚ r) (neg-ℚ p) (rational-abs-ℚ p)
+              ( neg-leq-abs-ℚ p)
+              ( neg-leq-ℚ _ _ p≤r))))
+      ( λ 0≤r →
+        transitive-leq-ℚ
+          ( rational-abs-ℚ r)
+          ( rational-abs-ℚ q)
+          ( max-ℚ (rational-abs-ℚ p) (rational-abs-ℚ q))
+          ( leq-right-max-ℚ _ _)
+          ( binary-tr
+            ( leq-ℚ)
+            ( inv (rational-abs-zero-leq-ℚ r 0≤r))
+            ( inv
+              ( rational-abs-zero-leq-ℚ
+                ( q)
+                ( transitive-leq-ℚ zero-ℚ r q r≤q 0≤r)))
+            ( r≤q)))
+      ( linear-leq-ℚ r zero-ℚ)
+```

src/elementary-number-theory/absolute-value-rational-numbers.lagda.md

@@ -11,12 +11,14 @@ module elementary-number-theory.absolute-value-rational-numbers where
 ```agda
 open import elementary-number-theory.addition-nonnegative-rational-numbers
 open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.inequality-nonnegative-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.maximum-rational-numbers
 open import elementary-number-theory.multiplication-nonnegative-rational-numbers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
@@ -127,6 +129,16 @@ opaque
         ( q≤0))
 ```
 
+### The absolute value of a positive rational number is the number itself
+
+```agda
+abstract
+  rational-abs-rational-ℚ⁺ :
+    (q : ℚ⁺) → rational-abs-ℚ (rational-ℚ⁺ q) ＝ rational-ℚ⁺ q
+  rational-abs-rational-ℚ⁺ q =
+    ap rational-ℚ⁰⁺ (abs-rational-ℚ⁰⁺ (nonnegative-ℚ⁺ q))
+```
+
 ### The absolute value of the negation of `q` is the absolute value of `q`
 
 ```agda
@@ -211,6 +223,14 @@ abstract
           { rational-abs-ℚ q}
           ( neg-leq-abs-ℚ p)
           ( neg-leq-abs-ℚ q)))
+
+  triangle-inequality-abs-diff-ℚ :
+    (p q : ℚ) → leq-ℚ⁰⁺ (abs-ℚ (p -ℚ q)) (abs-ℚ p +ℚ⁰⁺ abs-ℚ q)
+  triangle-inequality-abs-diff-ℚ p q =
+    tr
+      ( leq-ℚ⁰⁺ (abs-ℚ (p -ℚ q)))
+      ( ap-binary add-ℚ⁰⁺ (refl {x = abs-ℚ p}) (abs-neg-ℚ q))
+      ( triangle-inequality-abs-ℚ p (neg-ℚ q))
 ```
 
 ### `|ab| = |a||b|`
@@ -288,4 +308,9 @@ opaque
                   is-nonnegative-leq-zero-ℚ (neg-ℚ p) (neg-leq-ℚ p zero-ℚ p≤0)))
         ＝ rational-abs-ℚ p *ℚ rational-abs-ℚ q
           by ap (_*ℚ rational-abs-ℚ q) (inv (rational-abs-leq-zero-ℚ p p≤0)))
+
+abstract
+  rational-abs-mul-ℚ :
+    (p q : ℚ) → rational-abs-ℚ (p *ℚ q) ＝ rational-abs-ℚ p *ℚ rational-abs-ℚ q
+  rational-abs-mul-ℚ p q = ap rational-ℚ⁰⁺ (abs-mul-ℚ p q)
 ```

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

@@ -11,6 +11,7 @@ module elementary-number-theory.addition-rational-numbers where
 ```agda
 open import elementary-number-theory.addition-integer-fractions
 open import elementary-number-theory.addition-integers
+open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
 open import elementary-number-theory.natural-numbers
@@ -33,9 +34,9 @@ open import foundation.sections
 ## Idea
 
 We introduce
-{{#concept "addition" WDID=Q32043 WD="addition" Disambiguation="rational numbers" Agda=add-ℚ}}
-on the [rational numbers](elementary-number-theory.rational-numbers.md) and
-derive its basic properties.
+{{#concept "addition" Disambiguation="rational numbers" Agda=add-ℚ}} on the
+[rational numbers](elementary-number-theory.rational-numbers.md) and derive its
+basic properties.
 
 ## Definition
 
@@ -304,6 +305,15 @@ abstract
       by is-retraction-rational-fraction-ℚ (rational-ℤ (x +ℤ y))
 ```
 
+### The inclusion of natural numbers preserves addition
+
+```agda
+add-rational-ℕ :
+  (m n : ℕ) → rational-ℕ m +ℚ rational-ℕ n ＝ rational-ℕ (m +ℕ n)
+add-rational-ℕ m n =
+  add-rational-ℤ _ _ ∙ ap rational-ℤ (add-int-ℕ m n)
+```
+
 ### The rational successor of an integer is the successor of the integer
 
 ```agda

src/elementary-number-theory/archimedean-property-rational-numbers.lagda.md

@@ -25,6 +25,9 @@ open import foundation.dependent-pair-types
 open import foundation.existential-quantification
 open import foundation.identity-types
 open import foundation.propositional-truncations
+open import foundation.transport-along-identifications
+
+open import logic.functoriality-existential-quantification
 ```
 
 </details>
@@ -75,3 +78,17 @@ abstract
   archimedean-property-ℚ x y pos-x =
     unit-trunc-Prop (bound-archimedean-property-ℚ x y pos-x)
 ```
+
+## Corollaries
+
+### For any rational `q`, there exists a natural number `n` with `q < n`
+
+```agda
+abstract
+  exists-greater-natural-ℚ :
+    (q : ℚ) → exists ℕ (λ n → le-ℚ-Prop q (rational-ℕ n))
+  exists-greater-natural-ℚ q =
+    map-tot-exists
+      ( λ _ → tr (le-ℚ q) (right-unit-law-mul-ℚ _))
+      ( archimedean-property-ℚ one-ℚ q _)
+```

src/elementary-number-theory/closed-intervals-rational-numbers.lagda.md

@@ -8,6 +8,7 @@ module elementary-number-theory.closed-intervals-rational-numbers where
 
 ```agda
 open import elementary-number-theory.decidable-total-order-rational-numbers
+open import elementary-number-theory.distance-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.maximum-rational-numbers
 open import elementary-number-theory.minimum-rational-numbers
@@ -83,9 +84,17 @@ is-below-prop-closed-interval-ℚ :
   closed-interval-ℚ → subtype lzero ℚ
 is-below-prop-closed-interval-ℚ ((a , _) , _) b = le-ℚ-Prop b a
 
+is-below-closed-interval-ℚ : closed-interval-ℚ → ℚ → UU lzero
+is-below-closed-interval-ℚ [a,b] q =
+  type-Prop (is-below-prop-closed-interval-ℚ [a,b] q)
+
 is-above-prop-closed-interval-ℚ :
   closed-interval-ℚ → subtype lzero ℚ
 is-above-prop-closed-interval-ℚ ((_ , a) , _) b = le-ℚ-Prop a b
+
+is-above-closed-interval-ℚ : closed-interval-ℚ → ℚ → UU lzero
+is-above-closed-interval-ℚ [a,b] q =
+  type-Prop (is-above-prop-closed-interval-ℚ [a,b] q)
 ```
 
 ### The width of a closed interval
@@ -177,3 +186,26 @@ upper-bound-is-in-closed-interval-ℚ :
 upper-bound-is-in-closed-interval-ℚ =
   upper-bound-is-in-closed-interval-Poset ℚ-Poset
 ```
+
+### The distance between the lower and upper bounds of a closed interval is its width
+
+```agda
+abstract
+  eq-width-dist-lower-upper-bounds-closed-interval-ℚ :
+    ([a,b] : closed-interval-ℚ) →
+    rational-dist-ℚ
+      ( lower-bound-closed-interval-ℚ [a,b])
+      ( upper-bound-closed-interval-ℚ [a,b]) ＝
+    width-closed-interval-ℚ [a,b]
+  eq-width-dist-lower-upper-bounds-closed-interval-ℚ ((a , b) , a≤b) =
+    eq-dist-diff-leq-ℚ a b a≤b
+
+  eq-width-dist-upper-lower-bounds-closed-interval-ℚ :
+    ([a,b] : closed-interval-ℚ) →
+    rational-dist-ℚ
+      ( upper-bound-closed-interval-ℚ [a,b])
+      ( lower-bound-closed-interval-ℚ [a,b]) ＝
+    width-closed-interval-ℚ [a,b]
+  eq-width-dist-upper-lower-bounds-closed-interval-ℚ ((a , b) , a≤b) =
+    eq-dist-diff-leq-ℚ' b a a≤b
+```

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

@@ -64,6 +64,18 @@ abstract
     inv (abs-neg-ℚ _) ∙ ap abs-ℚ (distributive-neg-diff-ℚ _ _)
 ```
 
+### A rational number's distance from itself is zero
+
+```agda
+abstract
+  dist-self-ℚ : (q : ℚ) → dist-ℚ q q ＝ zero-ℚ⁰⁺
+  dist-self-ℚ q =
+    ap abs-ℚ (right-inverse-law-add-ℚ q) ∙ abs-rational-ℚ⁰⁺ zero-ℚ⁰⁺
+
+  rational-dist-self-ℚ : (q : ℚ) → rational-dist-ℚ q q ＝ zero-ℚ
+  rational-dist-self-ℚ q = ap rational-ℚ⁰⁺ (dist-self-ℚ q)
+```
+
 ### The differences of the arguments are less than or equal to their distance
 
 ```agda
@@ -225,6 +237,11 @@ abstract
             ( q -ℚ p)
             ( backward-implication (iff-translate-diff-leq-zero-ℚ p q) p≤q)
 
+  eq-dist-diff-leq-ℚ' : (p q : ℚ) → leq-ℚ q p → rational-dist-ℚ p q ＝ p -ℚ q
+  eq-dist-diff-leq-ℚ' p q q≤p =
+    ap rational-ℚ⁰⁺ (commutative-dist-ℚ _ _) ∙
+    eq-dist-diff-leq-ℚ q p q≤p
+
   eq-dist-diff-max-min-ℚ :
     (p q : ℚ) → rational-dist-ℚ p q ＝ max-ℚ p q -ℚ min-ℚ p q
   eq-dist-diff-max-min-ℚ p q =

src/elementary-number-theory/inequality-integers.lagda.md

@@ -215,20 +215,37 @@ reflects-leq-right-add-ℤ z x y =
   is-nonnegative-eq-ℤ (left-translation-diff-ℤ y x z)
 ```
 
-### The inclusion of ℕ into ℤ preserves inequality
+### The inclusion of ℕ into ℤ preserves and reflects inequality
 
 ```agda
-leq-int-ℕ : (x y : ℕ) → leq-ℕ x y → leq-ℤ (int-ℕ x) (int-ℕ y)
-leq-int-ℕ zero-ℕ y H =
-  tr
-    ( is-nonnegative-ℤ)
-    ( inv (right-unit-law-add-ℤ (int-ℕ y)))
-    ( is-nonnegative-int-ℕ y)
-leq-int-ℕ (succ-ℕ x) (succ-ℕ y) H = tr (is-nonnegative-ℤ)
-  ( inv (diff-succ-ℤ (int-ℕ y) (int-ℕ x)) ∙
-    ( ap (_-ℤ (succ-ℤ (int-ℕ x))) (succ-int-ℕ y) ∙
-      ap ((int-ℕ (succ-ℕ y)) -ℤ_) (succ-int-ℕ x)))
-  ( leq-int-ℕ x y H)
+abstract
+  leq-int-ℕ : (x y : ℕ) → leq-ℕ x y → leq-ℤ (int-ℕ x) (int-ℕ y)
+  leq-int-ℕ zero-ℕ y H =
+    tr
+      ( is-nonnegative-ℤ)
+      ( inv (right-unit-law-add-ℤ (int-ℕ y)))
+      ( is-nonnegative-int-ℕ y)
+  leq-int-ℕ (succ-ℕ x) (succ-ℕ y) H =
+    tr
+      ( is-nonnegative-ℤ)
+      ( ( inv (diff-succ-ℤ (int-ℕ y) (int-ℕ x))) ∙
+        ( ap (_-ℤ (succ-ℤ (int-ℕ x))) (succ-int-ℕ y)) ∙
+        ( ap ((int-ℕ (succ-ℕ y)) -ℤ_) (succ-int-ℕ x)))
+      ( leq-int-ℕ x y H)
+
+  reflects-leq-int-ℕ : (x y : ℕ) → leq-ℤ (int-ℕ x) (int-ℕ y) → leq-ℕ x y
+  reflects-leq-int-ℕ zero-ℕ y x≤y = star
+  reflects-leq-int-ℕ (succ-ℕ x) (succ-ℕ y) x≤y =
+    reflects-leq-int-ℕ x y
+      ( tr
+        ( is-nonnegative-ℤ)
+        ( ap-diff-ℤ (inv (succ-int-ℕ y)) (inv (succ-int-ℕ x)) ∙
+          diff-succ-ℤ (int-ℕ y) (int-ℕ x))
+        ( x≤y))
+
+  iff-leq-int-ℕ : (x y : ℕ) → leq-ℕ x y ↔ leq-ℤ (int-ℕ x) (int-ℕ y)
+  pr1 (iff-leq-int-ℕ x y) = leq-int-ℕ x y
+  pr2 (iff-leq-int-ℕ x y) = reflects-leq-int-ℕ x y
 ```
 
 ### An integer `x` is nonnegative if and only if `0 ≤ x`

src/elementary-number-theory/inequality-nonnegative-rational-numbers.lagda.md

@@ -7,12 +7,15 @@ module elementary-number-theory.inequality-nonnegative-rational-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.decidable-total-order-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.nonnegative-rational-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.propositions
 open import foundation.universe-levels
+
+open import order-theory.decidable-total-orders
 ```
 
 </details>
@@ -36,3 +39,15 @@ leq-prop-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ-Prop p q
 leq-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → UU lzero
 leq-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ p q
 ```
+
+## Properties
+
+### The decidable total order of nonnegative rational numbers
+
+```agda
+decidable-total-order-ℚ⁰⁺ : Decidable-Total-Order lzero lzero
+decidable-total-order-ℚ⁰⁺ =
+  decidable-total-order-Decidable-Total-Suborder
+    ℚ-Decidable-Total-Order
+    is-nonnegative-prop-ℚ
+```