Multiplication on closed intervals of rational numbers

src/elementary-number-theory.lagda.md

@@ -33,6 +33,7 @@ open import elementary-number-theory.binomial-theorem-integers public
 open import elementary-number-theory.binomial-theorem-natural-numbers public
 open import elementary-number-theory.bounded-sums-arithmetic-functions public
 open import elementary-number-theory.catalan-numbers public
+open import elementary-number-theory.closed-intervals-rational-numbers public
 open import elementary-number-theory.cofibonacci public
 open import elementary-number-theory.collatz-bijection public
 open import elementary-number-theory.collatz-conjecture public
@@ -97,10 +98,12 @@ 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-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.minimum-natural-numbers public
+open import elementary-number-theory.minimum-rational-numbers public
 open import elementary-number-theory.minimum-standard-finite-types public
 open import elementary-number-theory.modular-arithmetic public
 open import elementary-number-theory.modular-arithmetic-standard-finite-types public
@@ -121,7 +124,9 @@ open import elementary-number-theory.multiplicative-units-integers public
 open import elementary-number-theory.multiplicative-units-standard-cyclic-rings public
 open import elementary-number-theory.multiset-coefficients public
 open import elementary-number-theory.natural-numbers public
+open import elementary-number-theory.negative-integer-fractions public
 open import elementary-number-theory.negative-integers public
+open import elementary-number-theory.negative-rational-numbers public
 open import elementary-number-theory.nonnegative-integers public
 open import elementary-number-theory.nonpositive-integers public
 open import elementary-number-theory.nonzero-integers public

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

@@ -0,0 +1,169 @@
+# Closed intervals of rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.closed-intervals-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.maximum-rational-numbers
+open import elementary-number-theory.minimum-rational-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.negative-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
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [rational number](elementary-number-theory.rational-numbers.md) `p` is in a
+{{#concept "closed interval" Disambiguation="rational numbers" WDID=Q78240777 WD="closed interval" Agda=closed-interval-ℚ}}
+`[q , r]` if `q` is
+[less than or equal to](elementary-number-theory.inequality-rational-numbers.md)
+`p` and `p` is less than or equal to `r`.
+
+## Definition
+
+```agda
+module _
+  (p q : ℚ)
+  where
+
+  closed-interval-ℚ : subtype lzero ℚ
+  closed-interval-ℚ r = leq-ℚ-Prop p r ∧ leq-ℚ-Prop r q
+
+  is-in-closed-interval-ℚ : ℚ → UU lzero
+  is-in-closed-interval-ℚ r = type-Prop (closed-interval-ℚ r)
+
+unordered-closed-interval-ℚ : ℚ → ℚ → subtype lzero ℚ
+unordered-closed-interval-ℚ p q = closed-interval-ℚ (min-ℚ p q) (max-ℚ p q)
+
+is-in-unordered-closed-interval-ℚ : ℚ → ℚ → ℚ → UU lzero
+is-in-unordered-closed-interval-ℚ p q =
+  is-in-closed-interval-ℚ (min-ℚ p q) (max-ℚ p q)
+```
+
+## Properties
+
+### Multiplication of elements in a closed interval
+
+```agda
+abstract
+  left-mul-closed-interval-ℚ : (p q r s : ℚ) → is-in-closed-interval-ℚ p q r →
+    is-in-unordered-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s)
+  left-mul-closed-interval-ℚ p q r s (p≤r , r≤q) =
+    let
+      p≤q = transitive-leq-ℚ p r q r≤q p≤r
+    in
+      trichotomy-le-ℚ
+        ( s)
+        ( zero-ℚ)
+        ( λ s<0 →
+          let
+            s⁻ = s , is-negative-le-zero-ℚ s s<0
+            rs≤ps = reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r
+            qs≤ps = reverses-leq-right-mul-ℚ⁻ s⁻ p q p≤q
+            qs≤rs = reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q
+            min=qs = right-leq-left-min-ℚ (p *ℚ s) (q *ℚ s) qs≤ps
+            max=ps = right-leq-left-max-ℚ (p *ℚ s) (q *ℚ s) qs≤ps
+          in
+            inv-tr (λ t → leq-ℚ t (r *ℚ s)) min=qs qs≤rs ,
+            inv-tr (leq-ℚ (r *ℚ s)) max=ps rs≤ps)
+        ( λ s=0 →
+          let
+            ps=0 = ap (p *ℚ_) s=0 ∙ right-zero-law-mul-ℚ p
+            rs=0 = ap (r *ℚ_) s=0 ∙ right-zero-law-mul-ℚ r
+            qs=0 = ap (q *ℚ_) s=0 ∙ right-zero-law-mul-ℚ q
+            min=0 = ap-binary min-ℚ ps=0 qs=0 ∙ idempotent-min-ℚ zero-ℚ
+            max=0 = ap-binary max-ℚ ps=0 qs=0 ∙ idempotent-max-ℚ zero-ℚ
+          in leq-eq-ℚ _ _ (min=0 ∙ inv rs=0) , leq-eq-ℚ _ _ (rs=0 ∙ inv max=0))
+        ( λ 0<s →
+          let
+            s⁺ = s , is-positive-le-zero-ℚ s 0<s
+            ps≤rs = preserves-leq-right-mul-ℚ⁺ s⁺ p r p≤r
+            ps≤qs = preserves-leq-right-mul-ℚ⁺ s⁺ p q p≤q
+            rs≤qs = preserves-leq-right-mul-ℚ⁺ s⁺ r q r≤q
+            min=ps = left-leq-right-min-ℚ (p *ℚ s) (q *ℚ s) ps≤qs
+            max=qs = left-leq-right-max-ℚ (p *ℚ s) (q *ℚ s) ps≤qs
+          in
+            inv-tr (λ t → leq-ℚ t (r *ℚ s)) min=ps ps≤rs ,
+            inv-tr (leq-ℚ (r *ℚ s)) max=qs rs≤qs)
+
+  right-mul-closed-interval-ℚ :
+    (p q r s : ℚ) → is-in-closed-interval-ℚ p q r →
+    is-in-unordered-closed-interval-ℚ (s *ℚ p) (s *ℚ q) (s *ℚ r)
+  right-mul-closed-interval-ℚ p q r s r∈[p,q] =
+    tr
+      ( is-in-unordered-closed-interval-ℚ (s *ℚ p) (s *ℚ q))
+      ( commutative-mul-ℚ r s)
+      ( binary-tr
+        ( λ a b → is-in-unordered-closed-interval-ℚ a b (r *ℚ s))
+        ( commutative-mul-ℚ p s)
+        ( commutative-mul-ℚ q s)
+        ( left-mul-closed-interval-ℚ p q r s r∈[p,q]))
+
+  mul-closed-interval-closed-interval-ℚ :
+    (p q r s t u : ℚ) →
+    is-in-closed-interval-ℚ p q r → is-in-closed-interval-ℚ s t u →
+    is-in-closed-interval-ℚ
+      (min-ℚ (min-ℚ (p *ℚ s) (p *ℚ t)) (min-ℚ (q *ℚ s) (q *ℚ t)))
+      (max-ℚ (max-ℚ (p *ℚ s) (p *ℚ t)) (max-ℚ (q *ℚ s) (q *ℚ t)))
+      (r *ℚ u)
+  mul-closed-interval-closed-interval-ℚ p q r s t u r∈[p,q] u∈[s,t] =
+    let
+      (min-pu-qu≤ru , ru≤max-pu-qu) = left-mul-closed-interval-ℚ p q r u r∈[p,q]
+      (min-ps-pt≤pu , pu≤max-ps-pt) =
+        right-mul-closed-interval-ℚ s t u p u∈[s,t]
+      (min-qs-qt≤qu , qu≤max-qs-qt) =
+        right-mul-closed-interval-ℚ s t u q u∈[s,t]
+      max-pu-qu≤max-max-ps-pt-max-qs-qt =
+        max-leq-leq-ℚ
+          ( p *ℚ u)
+          ( max-ℚ (p *ℚ s) (p *ℚ t))
+          ( q *ℚ u)
+          ( max-ℚ (q *ℚ s) (q *ℚ t))
+          ( pu≤max-ps-pt)
+          ( qu≤max-qs-qt)
+      ru≤max-max-ps-pt-max-qs-qt =
+        transitive-leq-ℚ
+          ( r *ℚ u)
+          ( max-ℚ (p *ℚ u) (q *ℚ u))
+          ( max-ℚ (max-ℚ (p *ℚ s) (p *ℚ t)) (max-ℚ (q *ℚ s) (q *ℚ t)))
+          ( max-pu-qu≤max-max-ps-pt-max-qs-qt)
+          ( ru≤max-pu-qu)
+      min-min-ps-pt-min-qs-qt≤min-pu-qu =
+        min-leq-leq-ℚ
+          ( min-ℚ (p *ℚ s) (p *ℚ t))
+          ( p *ℚ u)
+          ( min-ℚ (q *ℚ s) (q *ℚ t))
+          ( q *ℚ u)
+          ( min-ps-pt≤pu)
+          ( min-qs-qt≤qu)
+      min-min-ps-pt-min-qs-qt≤ru =
+        transitive-leq-ℚ
+          ( min-ℚ (min-ℚ (p *ℚ s) (p *ℚ t)) (min-ℚ (q *ℚ s) (q *ℚ t)))
+          ( min-ℚ (p *ℚ u) (q *ℚ u))
+          ( r *ℚ u)
+          min-pu-qu≤ru
+          min-min-ps-pt-min-qs-qt≤min-pu-qu
+    in min-min-ps-pt-min-qs-qt≤ru , ru≤max-max-ps-pt-max-qs-qt
+```

src/elementary-number-theory/inequality-integer-fractions.lagda.md

@@ -24,6 +24,7 @@ open import elementary-number-theory.positive-integers
 open import elementary-number-theory.strict-inequality-integers
 
 open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
 open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.decidable-propositions
@@ -194,3 +195,18 @@ module _
             ( numerator-fraction-ℤ x)
             ( denominator-fraction-ℤ y))))
 ```
+
+### Negation reverses the order of inequality on integer fractions
+
+```agda
+neg-leq-fraction-ℤ :
+  (x y : fraction-ℤ) →
+  leq-fraction-ℤ x y →
+  leq-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ x)
+neg-leq-fraction-ℤ (m , n , p) (m' , n' , p') H =
+  binary-tr
+    ( leq-ℤ)
+    ( inv (left-negative-law-mul-ℤ m' n))
+    ( inv (left-negative-law-mul-ℤ m n'))
+    ( neg-leq-ℤ (m *ℤ n') (m' *ℤ n) H)
+```

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

@@ -285,6 +285,17 @@ module _
           ( I))
 ```
 
+### Negation of integers reverses inequality
+
+```agda
+neg-leq-ℤ : (x y : ℤ) → leq-ℤ x y → leq-ℤ (neg-ℤ y) (neg-ℤ x)
+neg-leq-ℤ x y =
+  tr
+    ( is-nonnegative-ℤ)
+    ( ap (_+ℤ neg-ℤ x) (inv (neg-neg-ℤ y)) ∙
+      commutative-add-ℤ (neg-ℤ (neg-ℤ y)) (neg-ℤ x))
+```
+
 ## See also
 
 - The decidable total order on the integers is defined in

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

@@ -1,6 +1,8 @@
 # Inequality on the rational numbers
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module elementary-number-theory.inequality-rational-numbers where
 ```
 
@@ -98,6 +100,9 @@ leq-ℚ-Decidable-Prop x y =
 refl-leq-ℚ : (x : ℚ) → leq-ℚ x x
 refl-leq-ℚ x =
   refl-leq-ℤ (numerator-ℚ x *ℤ denominator-ℚ x)
+
+leq-eq-ℚ : (x y : ℚ) → x ＝ y → leq-ℚ x y
+leq-eq-ℚ x y x=y = tr (leq-ℚ x) x=y (refl-leq-ℚ x)
 ```
 
 ### Inequality on the rational numbers is antisymmetric
@@ -338,6 +343,13 @@ preserves-leq-add-ℚ {a} {b} {c} {d} H K =
     ( preserves-leq-left-add-ℚ c a b H)
 ```
 
+### Negation of rational numbers reverses inequality
+
+```agda
+neg-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ (neg-ℚ y) (neg-ℚ x)
+neg-leq-ℚ x y = neg-leq-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)
+```
+
 ## See also
 
 - The decidable total order on the rational numbers is defined in

src/elementary-number-theory/integer-fractions.lagda.md

@@ -110,6 +110,14 @@ neg-fraction-ℤ (d , n) = (neg-ℤ d , n)
 
 ## Properties
 
+### The double negation of an integer fraction is the original fraction
+
+```agda
+abstract
+  neg-neg-fraction-ℤ : (x : fraction-ℤ) → neg-fraction-ℤ (neg-fraction-ℤ x) ＝ x
+  neg-neg-fraction-ℤ (n , d) = ap (_, d) (neg-neg-ℤ n)
+```
+
 ### Denominators are nonzero
 
 ```agda