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
@@ -123,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,227 @@
+# 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)
+
+is-in-unordered-closed-interval-is-in-closed-interval-ℚ :
+  (p q r : ℚ) →
+  is-in-closed-interval-ℚ p q r →
+  is-in-unordered-closed-interval-ℚ p q r
+is-in-unordered-closed-interval-is-in-closed-interval-ℚ p q r (p≤r , q≤r) =
+  transitive-leq-ℚ
+    ( min-ℚ p q)
+    ( p)
+    ( r)
+    ( p≤r)
+    ( leq-left-min-ℚ p q) ,
+  transitive-leq-ℚ
+    ( r)
+    ( q)
+    ( max-ℚ p q)
+    ( leq-right-max-ℚ p q)
+    ( q≤r)
+
+is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ :
+  (p q r : ℚ) → is-in-closed-interval-ℚ p q r →
+  is-in-unordered-closed-interval-ℚ q p r
+is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ
+  p q r (p≤r , q≤r) =
+  transitive-leq-ℚ
+    ( min-ℚ q p)
+    ( p)
+    ( r)
+    ( p≤r)
+    ( leq-right-min-ℚ q p) ,
+  transitive-leq-ℚ
+    ( r)
+    ( q)
+    ( max-ℚ q p)
+    ( leq-left-max-ℚ q p)
+    ( q≤r)
+```
+
+## Properties
+
+### Multiplication of elements in a closed interval
+
+```agda
+abstract
+  left-mul-negative-closed-interval-ℚ :
+    (p q r s : ℚ) →
+    is-in-closed-interval-ℚ p q r → is-negative-ℚ s →
+    is-in-closed-interval-ℚ (q *ℚ s) (p *ℚ s) (r *ℚ s)
+  left-mul-negative-closed-interval-ℚ p q r s (p≤r , r≤q) neg-s =
+    let
+      s⁻ = s , neg-s
+    in
+      reverses-leq-right-mul-ℚ⁻ s⁻ r q r≤q ,
+      reverses-leq-right-mul-ℚ⁻ s⁻ p r p≤r
+
+  left-mul-positive-closed-interval-ℚ :
+    (p q r s : ℚ) →
+    is-in-closed-interval-ℚ p q r → is-positive-ℚ s →
+    is-in-closed-interval-ℚ (p *ℚ s) (q *ℚ s) (r *ℚ s)
+  left-mul-positive-closed-interval-ℚ p q r s (p≤r , r≤q) pos-s =
+    let
+      s⁺ = s , pos-s
+    in
+      preserves-leq-right-mul-ℚ⁺ s⁺ p r p≤r ,
+      preserves-leq-right-mul-ℚ⁺ s⁺ r q r≤q
+
+  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 H@(p≤r , r≤q) =
+    let
+      p≤q = transitive-leq-ℚ p r q r≤q p≤r
+    in
+      trichotomy-le-ℚ
+        ( s)
+        ( zero-ℚ)
+        ( λ s<0 →
+          is-in-reversed-unordered-closed-interval-is-in-closed-interval-ℚ
+            (q *ℚ s)
+            (p *ℚ s)
+            (r *ℚ s)
+            ( left-mul-negative-closed-interval-ℚ p q r s H
+              ( is-negative-le-zero-ℚ s s<0)))
+        ( λ 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
+          in
+            leq-eq-ℚ
+              ( _)
+              ( _)
+              ( ap-binary min-ℚ ps=0 qs=0 ∙
+                idempotent-min-ℚ zero-ℚ ∙ inv rs=0) ,
+            leq-eq-ℚ
+              ( _)
+              ( _)
+              ( rs=0 ∙
+                inv (ap-binary max-ℚ ps=0 qs=0 ∙ idempotent-max-ℚ zero-ℚ)))
+        ( λ 0<s →
+          is-in-unordered-closed-interval-is-in-closed-interval-ℚ
+            ( p *ℚ s)
+            ( q *ℚ s)
+            ( r *ℚ s)
+            ( left-mul-positive-closed-interval-ℚ p q r s H
+              ( is-positive-le-zero-ℚ s 0<s)))
+
+abstract
+  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]))
+
+abstract
+  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]
+    in
+      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-leq-leq-ℚ
+          ( min-ℚ (p *ℚ s) (p *ℚ t))
+          ( p *ℚ u)
+          ( min-ℚ (q *ℚ s) (q *ℚ t))
+          ( q *ℚ u)
+          ( min-ps-pt≤pu)
+          ( min-qs-qt≤qu)) ,
+      transitive-leq-ℚ
+        ( r *ℚ u)
+        ( max-ℚ (p *ℚ u) (q *ℚ u))
+        ( max-ℚ (max-ℚ (p *ℚ s) (p *ℚ t)) (max-ℚ (q *ℚ s) (q *ℚ t)))
+        ( 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-pu-qu)
+```

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

@@ -104,6 +104,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
@@ -412,6 +415,13 @@ pr1 (leq-iff-transpose-left-diff-ℚ x y z) = leq-transpose-left-diff-ℚ x y z
 pr2 (leq-iff-transpose-left-diff-ℚ x y z) = leq-transpose-right-add-ℚ x z y
 ```
 
+### 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