Absolute value of real numbers (#1385)

Doesn't have nearly as much content as #1381 , but that's because we
don't even have addition yet on the real numbers. Still, this is, I
think, enough to continue on #1353 .

---------

Co-authored-by: Fredrik Bakke <[email protected]>

Author: lowasser

src/elementary-number-theory/absolute-value-integers.lagda.md

@@ -28,8 +28,9 @@ open import foundation.unit-type
 
 ## Idea
 
-The {{#concept "absolute value" Disambiguation="of an integer" Agda=abs-ℤ}} of
-an integer is the natural number with the same distance from `0`.
+The
+{{#concept "absolute value" Disambiguation="of an integer" Agda=abs-ℤ WD="absolute value" WDID=Q120812}}
+of an integer is the natural number with the same distance from `0`.
 
 ## Definition
 

src/order-theory/least-upper-bounds-large-posets.lagda.md

@@ -8,7 +8,9 @@ module order-theory.least-upper-bounds-large-posets where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.logical-equivalences
+open import foundation.type-arithmetic-cartesian-product-types
 open import foundation.universe-levels
 
 open import order-theory.dependent-products-large-posets
@@ -39,6 +41,15 @@ Similarly, a
 of a family of elements `a : I → P` in a large poset `P` is an element `x` in
 `P` such that the logical equivalence
 
+```text
+  is-binary-upper-bound-Large-Poset P a b y ↔ (x ≤ y)
+```
+
+holds for every `y` in `P`.
+
+Similarly, a least upper bound of a family of elements `a : I → P` in a large
+poset `P` is an element `x` in `P` such that the logical equivalence
+
 ```text
   is-upper-bound-family-of-elements-Large-Poset P a y ↔ (x ≤ y)
 ```
@@ -130,6 +141,24 @@ module _
     backward-implication (H _) (refl-leq-Large-Poset P _)
 ```
 
+### The least upper bound of `x` and `y` is the least upper bound of `y` and `x`
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (P : Large-Poset α β)
+  {l1 l2 : Level} (a : type-Large-Poset P l1) (b : type-Large-Poset P l2)
+  where
+
+  abstract
+    is-binary-least-upper-bound-swap-Large-Poset :
+      {l3 : Level} (y : type-Large-Poset P l3) →
+      is-least-binary-upper-bound-Large-Poset P a b y →
+      is-least-binary-upper-bound-Large-Poset P b a y
+    is-binary-least-upper-bound-swap-Large-Poset _ H z =
+      H z ∘iff iff-equiv commutative-product
+```
+
 ### Binary least upper bounds are unique up to similarity of elements
 
 ```agda

src/real-numbers.lagda.md

@@ -5,6 +5,7 @@
 ```agda
 module real-numbers where
 
+open import real-numbers.absolute-value-real-numbers public
 open import real-numbers.addition-lower-dedekind-real-numbers public
 open import real-numbers.addition-upper-dedekind-real-numbers public
 open import real-numbers.apartness-real-numbers public
@@ -23,6 +24,7 @@ open import real-numbers.minimum-real-numbers public
 open import real-numbers.minimum-upper-dedekind-real-numbers public
 open import real-numbers.negation-lower-upper-dedekind-real-numbers public
 open import real-numbers.negation-real-numbers public
+open import real-numbers.nonnegative-real-numbers public
 open import real-numbers.raising-universe-levels-real-numbers public
 open import real-numbers.rational-lower-dedekind-real-numbers public
 open import real-numbers.rational-real-numbers public

src/real-numbers/absolute-value-real-numbers.lagda.md

@@ -0,0 +1,92 @@
+# The absolute value of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.absolute-value-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.maximum-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.nonnegative-real-numbers
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "absolute value" Disambiguation="of a real number" Agda=abs-ℝ WD="absolute value" WDID=Q120812}}
+of a [real number](real-numbers.dedekind-real-numbers.md) is the
+[maximum](real-numbers.maximum-real-numbers.md) of it and its
+[negation](real-numbers.negation-real-numbers.md).
+
+```agda
+abs-ℝ : {l : Level} → ℝ l → ℝ l
+abs-ℝ x = binary-max-ℝ x (neg-ℝ x)
+```
+
+## Properties
+
+### The absolute value of a real number is nonnegative
+
+```agda
+abstract
+  is-nonnegative-abs-ℝ : {l : Level} → (x : ℝ l) → is-nonnegative-ℝ (abs-ℝ x)
+  is-nonnegative-abs-ℝ x q q<0 =
+    elim-disjunction
+      ( lower-cut-ℝ (abs-ℝ x) q)
+      ( id)
+      ( λ (x<0 , 0<x) → ex-falso (is-disjoint-cut-ℝ x zero-ℚ (0<x , x<0)))
+      ( is-located-lower-upper-cut-ℝ (abs-ℝ x) q zero-ℚ q<0)
+```
+
+### The absolute value of the negation of a real number is its absolute value
+
+```agda
+abstract
+  abs-neg-ℝ : {l : Level} → (x : ℝ l) → abs-ℝ (neg-ℝ x) ＝ abs-ℝ x
+  abs-neg-ℝ x =
+    ap (binary-max-ℝ (neg-ℝ x)) (neg-neg-ℝ x) ∙ commutative-binary-max-ℝ _ _
+```
+
+### `x` is between `-|x|` and `|x|`
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  abstract
+    leq-abs-ℝ : leq-ℝ x (abs-ℝ x)
+    leq-abs-ℝ = leq-left-binary-max-ℝ x (neg-ℝ x)
+
+    neg-leq-abs-ℝ : leq-ℝ (neg-ℝ x) (abs-ℝ x)
+    neg-leq-abs-ℝ = leq-right-binary-max-ℝ x (neg-ℝ x)
+
+    leq-neg-abs-ℝ : leq-ℝ (neg-ℝ (abs-ℝ x)) x
+    leq-neg-abs-ℝ =
+      tr
+        ( leq-ℝ (neg-ℝ (abs-ℝ x)))
+        ( neg-neg-ℝ x)
+        ( neg-leq-ℝ (neg-ℝ x) (abs-ℝ x) neg-leq-abs-ℝ)
+
+    neg-leq-neg-abs-ℝ : leq-ℝ (neg-ℝ (abs-ℝ x)) (neg-ℝ x)
+    neg-leq-neg-abs-ℝ = neg-leq-ℝ x (abs-ℝ x) leq-abs-ℝ
+```

src/real-numbers/inequality-real-numbers.lagda.md

@@ -16,6 +16,7 @@ open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.existential-quantification
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.propositions
@@ -75,41 +76,47 @@ module _
   leq-ℝ' : UU (l1 ⊔ l2)
   leq-ℝ' = type-Prop leq-ℝ-Prop'
 
-  leq-iff-ℝ' : leq-ℝ x y ↔ leq-ℝ'
-  pr1 (leq-iff-ℝ') lx⊆ly q q-in-uy =
-    elim-exists
-      ( upper-cut-ℝ x q)
-      ( λ p (p<q , p≮y) →
-        subset-upper-cut-upper-complement-lower-cut-ℝ
-          ( x)
-          ( q)
-          ( intro-exists
-            ( p)
-            ( p<q ,
-              reverses-order-complement-subtype
-                ( lower-cut-ℝ x)
-                ( lower-cut-ℝ y)
-                ( lx⊆ly)
-                ( p)
-                ( p≮y))))
-      ( subset-upper-complement-lower-cut-upper-cut-ℝ y q q-in-uy)
-  pr2 leq-iff-ℝ' uy⊆ux p p-in-lx =
-    elim-exists
-      ( lower-cut-ℝ y p)
-      ( λ q (p<q , x≮q) →
-        subset-lower-cut-lower-complement-upper-cut-ℝ
-          ( y)
-          ( p)
-          ( intro-exists
+  abstract
+    leq'-leq-ℝ : leq-ℝ x y → leq-ℝ'
+    leq'-leq-ℝ lx⊆ly q y<q =
+      elim-exists
+        ( upper-cut-ℝ x q)
+        ( λ p (p<q , p≮y) →
+          subset-upper-cut-upper-complement-lower-cut-ℝ
+            ( x)
             ( q)
-            ( p<q ,
-              reverses-order-complement-subtype
-                ( upper-cut-ℝ y)
-                ( upper-cut-ℝ x)
-                ( uy⊆ux)
-                ( q)
-                ( x≮q))))
-      ( subset-lower-complement-upper-cut-lower-cut-ℝ x p p-in-lx)
+            ( intro-exists
+              ( p)
+              ( p<q ,
+                reverses-order-complement-subtype
+                  ( lower-cut-ℝ x)
+                  ( lower-cut-ℝ y)
+                  ( lx⊆ly)
+                  ( p)
+                  ( p≮y))))
+        ( subset-upper-complement-lower-cut-upper-cut-ℝ y q y<q)
+
+    leq-leq'-ℝ : leq-ℝ' → leq-ℝ x y
+    leq-leq'-ℝ uy⊆ux p p<x =
+      elim-exists
+        ( lower-cut-ℝ y p)
+        ( λ q (p<q , x≮q) →
+          subset-lower-cut-lower-complement-upper-cut-ℝ
+            ( y)
+            ( p)
+            ( intro-exists
+              ( q)
+              ( p<q ,
+                reverses-order-complement-subtype
+                  ( upper-cut-ℝ y)
+                  ( upper-cut-ℝ x)
+                  ( uy⊆ux)
+                  ( q)
+                  ( x≮q))))
+        ( subset-lower-complement-upper-cut-lower-cut-ℝ x p p<x)
+
+    leq-iff-ℝ' : leq-ℝ x y ↔ leq-ℝ'
+    leq-iff-ℝ' = (leq'-leq-ℝ , leq-leq'-ℝ)
 ```
 
 ### Inequality on the real numbers is reflexive
@@ -186,6 +193,17 @@ iff-leq-real-ℚ : (x y : ℚ) → leq-ℚ x y ↔ leq-ℝ (real-ℚ x) (real-
 iff-leq-real-ℚ = iff-leq-lower-real-ℚ
 ```
 
+### Negation reverses inequality on the real numbers
+
+```agda
+module _
+  {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
+  where
+
+  neg-leq-ℝ : leq-ℝ x y → leq-ℝ (neg-ℝ y) (neg-ℝ x)
+  neg-leq-ℝ x≤y = leq-leq'-ℝ (neg-ℝ y) (neg-ℝ x) (x≤y ∘ neg-ℚ)
+```
+
 ## References
 
 {{#bibliography}}

src/real-numbers/maximum-real-numbers.lagda.md

@@ -12,6 +12,7 @@ module real-numbers.maximum-real-numbers where
 open import foundation.dependent-pair-types
 open import foundation.disjunction
 open import foundation.empty-types
+open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels
 
@@ -23,6 +24,7 @@ open import real-numbers.inequality-real-numbers
 open import real-numbers.lower-dedekind-real-numbers
 open import real-numbers.maximum-lower-dedekind-real-numbers
 open import real-numbers.maximum-upper-dedekind-real-numbers
+open import real-numbers.similarity-real-numbers
 open import real-numbers.upper-dedekind-real-numbers
 ```
 
@@ -111,6 +113,61 @@ module _
       ( lower-real-ℝ z)
 ```
 
+### The binary maximum is a binary upper bound
+
+```agda
+module _
+  {l1 l2 : Level}
+  (x : ℝ l1) (y : ℝ l2)
+  where
+
+  abstract
+    leq-left-binary-max-ℝ : leq-ℝ x (binary-max-ℝ x y)
+    leq-left-binary-max-ℝ =
+      pr1
+        ( is-binary-upper-bound-is-least-binary-upper-bound-Large-Poset
+          ( ℝ-Large-Poset)
+          ( x)
+          ( y)
+          ( is-least-binary-upper-bound-binary-max-ℝ x y))
+
+    leq-right-binary-max-ℝ : leq-ℝ y (binary-max-ℝ x y)
+    leq-right-binary-max-ℝ =
+      pr2
+        ( is-binary-upper-bound-is-least-binary-upper-bound-Large-Poset
+          ( ℝ-Large-Poset)
+          ( x)
+          ( y)
+          ( is-least-binary-upper-bound-binary-max-ℝ x y))
+```
+
+### The binary maximum is commutative
+
+```agda
+module _
+  {l1 l2 : Level}
+  (x : ℝ l1) (y : ℝ l2)
+  where
+
+  opaque
+    unfolding sim-ℝ
+
+    commutative-binary-max-ℝ : binary-max-ℝ x y ＝ binary-max-ℝ y x
+    commutative-binary-max-ℝ =
+      eq-sim-ℝ
+        ( sim-is-least-binary-upper-bound-Large-Poset
+          ( ℝ-Large-Poset)
+          ( x)
+          ( y)
+          ( is-least-binary-upper-bound-binary-max-ℝ x y)
+          ( is-binary-least-upper-bound-swap-Large-Poset
+            ( ℝ-Large-Poset)
+            ( y)
+            ( x)
+            ( binary-max-ℝ y x)
+            ( is-least-binary-upper-bound-binary-max-ℝ y x)))
+```
+
 ### The large poset of real numbers has joins
 
 ```agda

src/real-numbers/nonnegative-real-numbers.lagda.md

@@ -0,0 +1,40 @@
+# Nonnegative real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.nonnegative-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.rational-real-numbers
+```
+
+</details>
+
+## Idea
+
+A real number `x` is
+{{#concept "nonnegative" Disambiguation="real number" Agda=is-nonnegative-ℝ}} if
+`0 ≤ x`.
+
+## Definitions
+
+```agda
+is-nonnegative-ℝ : {l : Level} → ℝ l → UU l
+is-nonnegative-ℝ = leq-ℝ zero-ℝ
+
+is-nonnegative-prop-ℝ : {l : Level} → ℝ l → Prop l
+is-nonnegative-prop-ℝ = leq-ℝ-Prop zero-ℝ
+
+nonnegative-ℝ : (l : Level) → UU (lsuc l)
+nonnegative-ℝ l = type-subtype (is-nonnegative-prop-ℝ {l})
+```