Multiplication of closed intervals on rational numbers is subdistributive over addition (UniMath#1567)

Continuing to try to break off small chunks of UniMath#1384.

Author: lowasser

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

@@ -12,8 +12,10 @@ open import elementary-number-theory.additive-group-of-rational-numbers
 open import elementary-number-theory.closed-intervals-rational-numbers
 open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.poset-closed-intervals-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.existential-quantification
@@ -90,6 +92,15 @@ abstract
               inv (is-section-diff-ℚ _ _)))
         ( linear-leq-ℚ q (a +ℚ d))
 
+  is-in-add-interval-add-is-in-closed-interval-ℚ :
+    ([a,b] [c,d] : closed-interval-ℚ) (s t : ℚ) →
+    is-in-closed-interval-ℚ [a,b] s → is-in-closed-interval-ℚ [c,d] t →
+    is-in-closed-interval-ℚ (add-closed-interval-ℚ [a,b] [c,d]) (s +ℚ t)
+  is-in-add-interval-add-is-in-closed-interval-ℚ
+    ((a , b) , _) ((c , d) , _) s t (a≤s , s≤b) (c≤t , t≤d) =
+    ( preserves-leq-add-ℚ a≤s c≤t ,
+      preserves-leq-add-ℚ s≤b t≤d)
+
   is-in-add-interval-is-in-minkowski-sum-ℚ :
     ([a,b] [c,d] : closed-interval-ℚ) →
     (q : ℚ) →
@@ -103,17 +114,19 @@ abstract
       ( add-closed-interval-ℚ [a,b] [c,d])
       ( q)
   is-in-add-interval-is-in-minkowski-sum-ℚ
-    [a,b]@((a , b) , a≤b) [c,d]@((c , d) , c≤d) q q∈[a,b]+[c,d] =
+    [a,b] [c,d] q q∈[a,b]+[c,d] =
       let
         open
           do-syntax-trunc-Prop
-            ( subtype-closed-interval-ℚ
-              ( add-closed-interval-ℚ [a,b] [c,d])
-              ( q))
+            ( subtype-closed-interval-ℚ (add-closed-interval-ℚ [a,b] [c,d]) q)
       in do
-        ((s , t) , (a≤s , s≤b) , (c≤t , t≤d) , q=s+t) ← q∈[a,b]+[c,d]
-        ( inv-tr (leq-ℚ (a +ℚ c)) q=s+t (preserves-leq-add-ℚ a≤s c≤t) ,
-          inv-tr (λ r → leq-ℚ r (b +ℚ d)) q=s+t (preserves-leq-add-ℚ s≤b t≤d))
+        ((s , t) , s∈[a,b] , t∈[c,d] , q=s+t) ← q∈[a,b]+[c,d]
+        inv-tr
+          ( is-in-closed-interval-ℚ (add-closed-interval-ℚ [a,b] [c,d]))
+          ( q=s+t)
+          ( is-in-add-interval-add-is-in-closed-interval-ℚ [a,b] [c,d] s t
+            ( s∈[a,b])
+            ( t∈[c,d]))
 
 has-same-elements-minkowski-add-closed-interval-ℚ :
   ([a,b] [c,d] : closed-interval-ℚ) →
@@ -221,3 +234,59 @@ commutative-monoid-add-closed-interval-ℚ =
   ( monoid-add-closed-interval-ℚ ,
     commutative-add-closed-interval-ℚ)
 ```
+
+### Containment on rational intervals is preserved by addition
+
+```agda
+abstract
+  preserves-leq-left-add-closed-interval-ℚ :
+    ([c,d] [a,b] [a',b'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [a,b] [a',b'] →
+    leq-closed-interval-ℚ
+      ( add-closed-interval-ℚ [a,b] [c,d])
+      ( add-closed-interval-ℚ [a',b'] [c,d])
+  preserves-leq-left-add-closed-interval-ℚ
+    ((c , d) , _) ((a , b) , _) ((a' , b') , _) (a'≤a , b≤b') =
+    ( preserves-leq-left-add-ℚ c a' a a'≤a ,
+      preserves-leq-left-add-ℚ d b b' b≤b')
+
+  preserves-leq-right-add-closed-interval-ℚ :
+    ([a,b] [c,d] [c',d'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [c,d] [c',d'] →
+    leq-closed-interval-ℚ
+      ( add-closed-interval-ℚ [a,b] [c,d])
+      ( add-closed-interval-ℚ [a,b] [c',d'])
+  preserves-leq-right-add-closed-interval-ℚ [a,b] [c,d] [c',d'] [c,d]⊆[c',d'] =
+    binary-tr
+      ( leq-closed-interval-ℚ)
+      ( commutative-add-closed-interval-ℚ [c,d] [a,b])
+      ( commutative-add-closed-interval-ℚ [c',d'] [a,b])
+      ( preserves-leq-left-add-closed-interval-ℚ
+        ( [a,b])
+        ( [c,d])
+        ( [c',d'])
+        ( [c,d]⊆[c',d']))
+
+  preserves-leq-add-closed-interval-ℚ :
+    ([a,b] [a',b'] [c,d] [c',d'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [a,b] [a',b'] → leq-closed-interval-ℚ [c,d] [c',d'] →
+    leq-closed-interval-ℚ
+      ( add-closed-interval-ℚ [a,b] [c,d])
+      ( add-closed-interval-ℚ [a',b'] [c',d'])
+  preserves-leq-add-closed-interval-ℚ
+    [a,b] [a',b'] [c,d] [c',d'] [a,b]⊆[a',b'] [c,d]⊆[c',d'] =
+    transitive-leq-closed-interval-ℚ
+      ( add-closed-interval-ℚ [a,b] [c,d])
+      ( add-closed-interval-ℚ [a,b] [c',d'])
+      ( add-closed-interval-ℚ [a',b'] [c',d'])
+      ( preserves-leq-left-add-closed-interval-ℚ
+        ( [c',d'])
+        ( [a,b])
+        ( [a',b'])
+        ( [a,b]⊆[a',b']))
+      ( preserves-leq-right-add-closed-interval-ℚ
+        ( [a,b])
+        ( [c,d])
+        ( [c',d'])
+        ( [c,d]⊆[c',d']))
+```

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

@@ -22,6 +22,7 @@ open import elementary-number-theory.multiplicative-group-of-positive-rational-n
 open import elementary-number-theory.multiplicative-group-of-rational-numbers
 open import elementary-number-theory.multiplicative-monoid-of-rational-numbers
 open import elementary-number-theory.negative-rational-numbers
+open import elementary-number-theory.poset-closed-intervals-rational-numbers
 open import elementary-number-theory.positive-and-negative-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
@@ -753,3 +754,137 @@ commutative-monoid-mul-closed-interval-ℚ =
   ( monoid-mul-closed-interval-ℚ ,
     commutative-mul-closed-interval-ℚ)
 ```
+
+### Multiplication of closed intervals is subdistributive
+
+```agda
+abstract
+  left-subdistributive-mul-add-closed-interval-ℚ :
+    ([a,b] [c,d] [e,f] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] (add-closed-interval-ℚ [c,d] [e,f]))
+      ( add-closed-interval-ℚ
+        ( mul-closed-interval-ℚ [a,b] [c,d])
+        ( mul-closed-interval-ℚ [a,b] [e,f]))
+  left-subdistributive-mul-add-closed-interval-ℚ [a,b] [c,d] [e,f] =
+    leq-closed-interval-leq-subtype-ℚ
+      ( mul-closed-interval-ℚ [a,b] (add-closed-interval-ℚ [c,d] [e,f]))
+      ( add-closed-interval-ℚ
+        ( mul-closed-interval-ℚ [a,b] [c,d])
+        ( mul-closed-interval-ℚ [a,b] [e,f]))
+      ( λ q q∈[a,b]⟨[c,d]+[e,f]⟩ →
+        let
+          open
+            do-syntax-trunc-Prop
+              ( subtype-closed-interval-ℚ
+                ( add-closed-interval-ℚ
+                  ( mul-closed-interval-ℚ [a,b] [c,d])
+                  ( mul-closed-interval-ℚ [a,b] [e,f]))
+                ( q))
+        in do
+          ((qab , qcdef) , qab∈[a,b] , qcdef∈[c,d]+[e,f] , q=qab*qcdef) ←
+            is-in-minkowski-product-is-in-mul-closed-interval-ℚ
+              ( [a,b])
+              ( add-closed-interval-ℚ [c,d] [e,f])
+              ( q)
+              ( q∈[a,b]⟨[c,d]+[e,f]⟩)
+          ((qcd , qef) , qcd∈[c,d] , qef∈[e,f] , qcdef=qcd+qef) ←
+            is-in-minkowski-sum-is-in-add-closed-interval-ℚ
+              ( [c,d])
+              ( [e,f])
+              ( qcdef)
+              ( qcdef∈[c,d]+[e,f])
+          inv-tr
+            ( is-in-closed-interval-ℚ
+              ( add-closed-interval-ℚ
+                ( mul-closed-interval-ℚ [a,b] [c,d])
+                ( mul-closed-interval-ℚ [a,b] [e,f])))
+            ( ( q=qab*qcdef) ∙
+              ( ap-mul-ℚ refl qcdef=qcd+qef) ∙
+              ( left-distributive-mul-add-ℚ qab qcd qef))
+            ( is-in-add-interval-add-is-in-closed-interval-ℚ
+              ( mul-closed-interval-ℚ [a,b] [c,d])
+              ( mul-closed-interval-ℚ [a,b] [e,f])
+              ( qab *ℚ qcd)
+              ( qab *ℚ qef)
+              ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                  ( [a,b])
+                  ( [c,d])
+                  ( qab)
+                  ( qcd)
+                  ( qab∈[a,b])
+                  ( qcd∈[c,d]))
+              ( is-in-mul-interval-mul-is-in-closed-interval-ℚ
+                  ( [a,b])
+                  ( [e,f])
+                  ( qab)
+                  ( qef)
+                  ( qab∈[a,b])
+                  ( qef∈[e,f]))))
+```
+
+### Containment of intervals is preserved by multiplication
+
+```agda
+abstract
+  preserves-leq-left-mul-closed-interval-ℚ :
+    ([c,d] [a,b] [a',b'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [a,b] [a',b'] →
+    leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a',b'] [c,d])
+  preserves-leq-left-mul-closed-interval-ℚ [c,d] [a,b] [a',b'] [a,b]⊆[a',b'] =
+    leq-closed-interval-leq-subtype-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a',b'] [c,d])
+      ( binary-tr
+        ( _⊆_)
+        ( eq-minkowski-mul-closed-interval-ℚ [a,b] [c,d])
+        ( eq-minkowski-mul-closed-interval-ℚ [a',b'] [c,d])
+        ( preserves-leq-left-minkowski-mul-Commutative-Monoid
+          ( commutative-monoid-mul-ℚ)
+          ( subtype-closed-interval-ℚ [c,d])
+          ( subtype-closed-interval-ℚ [a,b])
+          ( subtype-closed-interval-ℚ [a',b'])
+          ( leq-subtype-leq-closed-interval-ℚ [a,b] [a',b'] [a,b]⊆[a',b'])))
+
+  preserves-leq-right-mul-closed-interval-ℚ :
+    ([a,b] [c,d] [c',d'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [c,d] [c',d'] →
+    leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a,b] [c',d'])
+  preserves-leq-right-mul-closed-interval-ℚ [a,b] [c,d] [c',d'] [c,d]⊆[c',d'] =
+    binary-tr
+      ( leq-closed-interval-ℚ)
+      ( commutative-mul-closed-interval-ℚ [c,d] [a,b])
+      ( commutative-mul-closed-interval-ℚ [c',d'] [a,b])
+      ( preserves-leq-left-mul-closed-interval-ℚ
+        ( [a,b])
+        ( [c,d])
+        ( [c',d'])
+        ( [c,d]⊆[c',d']))
+
+  preserves-leq-mul-closed-interval-ℚ :
+    ([a,b] [a',b'] [c,d] [c',d'] : closed-interval-ℚ) →
+    leq-closed-interval-ℚ [a,b] [a',b'] → leq-closed-interval-ℚ [c,d] [c',d'] →
+    leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a',b'] [c',d'])
+  preserves-leq-mul-closed-interval-ℚ
+    [a,b] [a',b'] [c,d] [c',d'] [a,b]⊆[a',b'] [c,d]⊆[c',d'] =
+    transitive-leq-closed-interval-ℚ
+      ( mul-closed-interval-ℚ [a,b] [c,d])
+      ( mul-closed-interval-ℚ [a,b] [c',d'])
+      ( mul-closed-interval-ℚ [a',b'] [c',d'])
+      ( preserves-leq-left-mul-closed-interval-ℚ
+        ( [c',d'])
+        ( [a,b])
+        ( [a',b'])
+        ( [a,b]⊆[a',b']))
+      ( preserves-leq-right-mul-closed-interval-ℚ
+        ( [a,b])
+        ( [c,d])
+        ( [c',d'])
+        ( [c,d]⊆[c',d']))
+```

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

@@ -11,6 +11,8 @@ open import elementary-number-theory.closed-intervals-rational-numbers
 open import elementary-number-theory.decidable-total-order-rational-numbers
 
 open import foundation.binary-relations
+open import foundation.logical-equivalences
+open import foundation.subtypes
 open import foundation.universe-levels
 
 open import order-theory.closed-intervals-total-orders
@@ -60,3 +62,28 @@ abstract
 poset-closed-interval-ℚ : Poset lzero lzero
 poset-closed-interval-ℚ = poset-closed-interval-Total-Order ℚ-Total-Order
 ```
+
+### Containment of closed intervals is equivalent to containment of subtypes
+
+```agda
+abstract
+  leq-subtype-iff-leq-closed-interval-ℚ :
+    ([a,b] [c,d] : closed-interval-ℚ) →
+    ( leq-closed-interval-ℚ [a,b] [c,d] ↔
+      ( subtype-closed-interval-ℚ [a,b] ⊆ subtype-closed-interval-ℚ [c,d]))
+  leq-subtype-iff-leq-closed-interval-ℚ =
+    leq-subtype-iff-leq-closed-interval-Total-Order ℚ-Total-Order
+
+  leq-subtype-leq-closed-interval-ℚ :
+    ([a,b] [c,d] : closed-interval-ℚ) → leq-closed-interval-ℚ [a,b] [c,d] →
+    subtype-closed-interval-ℚ [a,b] ⊆ subtype-closed-interval-ℚ [c,d]
+  leq-subtype-leq-closed-interval-ℚ =
+    leq-subtype-leq-closed-interval-Total-Order ℚ-Total-Order
+
+  leq-closed-interval-leq-subtype-ℚ :
+    ([a,b] [c,d] : closed-interval-ℚ) →
+    subtype-closed-interval-ℚ [a,b] ⊆ subtype-closed-interval-ℚ [c,d] →
+    leq-closed-interval-ℚ [a,b] [c,d]
+  leq-closed-interval-leq-subtype-ℚ =
+    leq-closed-interval-leq-subtype-Total-Order ℚ-Total-Order
+```