Inequality on the rational numbers

Content created by Egbert Rijke, Fernando Chu, Fredrik Bakke and malarbol.

Created on 2023-04-08.
Last modified on 2024-02-27.

module elementary-number-theory.inequality-rational-numbers where
Imports
open import elementary-number-theory.cross-multiplication-difference-integer-fractions
open import elementary-number-theory.inequality-integer-fractions
open import elementary-number-theory.inequality-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.mediant-integer-fractions
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.binary-relations
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.universe-levels

Idea

A rational number x is less (or equal) to a rational number y if and only if the underlying fraction of x is less (or equal) than the underlying fraction of y.

Definition

Inequality on the rational numbers

leq-ℚ-Prop :     Prop lzero
leq-ℚ-Prop (x , px) (y , py) = leq-fraction-ℤ-Prop x y

leq-ℚ :     UU lzero
leq-ℚ x y = type-Prop (leq-ℚ-Prop x y)

is-prop-leq-ℚ : (x y : )  is-prop (leq-ℚ x y)
is-prop-leq-ℚ x y = is-prop-type-Prop (leq-ℚ-Prop x y)

infix 30 _≤-ℚ_
_≤-ℚ_ = leq-ℚ

Strict inequality on the rational numbers

le-ℚ-Prop :     Prop lzero
le-ℚ-Prop (x , px) (y , py) = le-fraction-ℤ-Prop x y

le-ℚ :     UU lzero
le-ℚ x y = type-Prop (le-ℚ-Prop x y)

is-prop-le-ℚ : (x y : )  is-prop (le-ℚ x y)
is-prop-le-ℚ x y = is-prop-type-Prop (le-ℚ-Prop x y)

Properties

Inequality on rational numbers is reflexive

refl-leq-ℚ : (x : )  leq-ℚ x x
refl-leq-ℚ x =
  refl-leq-ℤ (numerator-ℚ x *ℤ denominator-ℚ x)

Inequality on rational numbers is antisymmetric

antisymmetric-leq-ℚ : (x y : )  leq-ℚ x y  leq-ℚ y x  x  y
antisymmetric-leq-ℚ x y H H' =
  ( inv (in-fraction-fraction-ℚ x)) 
  ( eq-ℚ-sim-fractions-ℤ
    ( fraction-ℚ x)
    ( fraction-ℚ y)
    ( is-sim-antisymmetric-leq-fraction-ℤ
      ( fraction-ℚ x)
      ( fraction-ℚ y)
      ( H)
      ( H'))) 
  ( in-fraction-fraction-ℚ y)

Strict inequality on rationals is asymmetric

asymmetric-le-ℚ : (x y : )  le-ℚ x y  ¬ (le-ℚ y x)
asymmetric-le-ℚ x y =
  asymmetric-le-fraction-ℤ
    ( fraction-ℚ x)
    ( fraction-ℚ y)

irreflexive-le-ℚ : (x : )  ¬ (le-ℚ x x)
irreflexive-le-ℚ =
  is-irreflexive-is-asymmetric le-ℚ asymmetric-le-ℚ

Transitivity properties

module _
  (x y z : )
  where

  transitive-leq-ℚ : leq-ℚ x y  leq-ℚ y z  leq-ℚ x z
  transitive-leq-ℚ =
    transitive-leq-fraction-ℤ
      ( fraction-ℚ x)
      ( fraction-ℚ y)
      ( fraction-ℚ z)

  transitive-le-ℚ : le-ℚ x y  le-ℚ y z  le-ℚ x z
  transitive-le-ℚ =
    transitive-le-fraction-ℤ
      ( fraction-ℚ x)
      ( fraction-ℚ y)
      ( fraction-ℚ z)

  concatenate-le-leq-ℚ : le-ℚ x y  leq-ℚ y z  le-ℚ x z
  concatenate-le-leq-ℚ =
    concatenate-le-leq-fraction-ℤ
      ( fraction-ℚ x)
      ( fraction-ℚ y)
      ( fraction-ℚ z)

  concatenate-leq-le-ℚ : leq-ℚ x y  le-ℚ y z  le-ℚ x z
  concatenate-leq-le-ℚ =
    concatenate-leq-le-fraction-ℤ
      ( fraction-ℚ x)
      ( fraction-ℚ y)
      ( fraction-ℚ z)

Strict inequality on the rational numbers reflects strict inequality on the underlying fractions

module _
  (x : ) (p : fraction-ℤ)
  where

  right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ :
    le-fraction-ℤ (fraction-ℚ x) p 
    le-ℚ x (in-fraction-ℤ p)
  right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ H =
    concatenate-le-sim-fraction-ℤ
      ( fraction-ℚ x)
      ( p)
      ( fraction-ℚ ( in-fraction-ℤ p))
      ( H)
      ( sim-reduced-fraction-ℤ p)

  left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ :
    le-fraction-ℤ p (fraction-ℚ x) 
    le-ℚ (in-fraction-ℤ p) x
  left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ =
    concatenate-sim-le-fraction-ℤ
      ( fraction-ℚ ( in-fraction-ℤ p))
      ( p)
      ( fraction-ℚ x)
      ( symmetric-sim-fraction-ℤ
        ( p)
        ( fraction-ℚ ( in-fraction-ℤ p))
        ( sim-reduced-fraction-ℤ p))

The rational numbers have no lower or upper bound

module _
  (x : )
  where

  left-∃-le-ℚ :    q  le-ℚ q x)
  left-∃-le-ℚ = intro-∃
    ( in-fraction-ℤ frac)
    ( left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac
      ( le-fraction-le-numerator-fraction-ℤ
        ( frac)
        ( fraction-ℚ x)
        ( refl)
        ( le-pred-ℤ (numerator-ℚ x))))
    where
    frac : fraction-ℤ
    frac = pred-ℤ (numerator-ℚ x) , positive-denominator-ℚ x

  right-∃-le-ℚ :    r  le-ℚ x r)
  right-∃-le-ℚ = intro-∃
    ( in-fraction-ℤ frac)
    ( right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac
      ( le-fraction-le-numerator-fraction-ℤ
        ( fraction-ℚ x)
        ( frac)
        ( refl)
        ( le-succ-ℤ (numerator-ℚ x))))
    where
    frac : fraction-ℤ
    frac = succ-ℤ (numerator-ℚ x) , positive-denominator-ℚ x

Decidability of strict inequality on the rationals

decide-le-leq-ℚ : (x y : )  le-ℚ x y + leq-ℚ y x
decide-le-leq-ℚ x y =
  map-coproduct
    ( id)
    ( is-nonnegative-eq-ℤ
      ( skew-commutative-cross-mul-diff-fraction-ℤ
        ( fraction-ℚ x)
        ( fraction-ℚ y)))
    ( decide-is-positive-ℤ
      { cross-mul-diff-fraction-ℤ
        ( fraction-ℚ x)
        ( fraction-ℚ y)})

It remains to fully formalize that strict inequality is decidable.

Trichotomy on the rationals

trichotomy-le-ℚ :
  {l : Level} {A : UU l} (x y : ) 
  ( le-ℚ x y  A) 
  ( Id x y  A) 
  ( le-ℚ y x  A) 
  A
trichotomy-le-ℚ x y left eq right with decide-le-leq-ℚ x y | decide-le-leq-ℚ y x
... | inl I | _ = left I
... | inr I | inl I' = right I'
... | inr I | inr I' = eq (antisymmetric-leq-ℚ x y I' I)

The mediant of two rationals is between them

module _
  (x y : ) (H : le-ℚ x y)
  where

  le-left-mediant-ℚ : le-ℚ x (mediant-ℚ x y)
  le-left-mediant-ℚ =
    right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x
      ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
      ( le-left-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H)

  le-right-mediant-ℚ : le-ℚ (mediant-ℚ x y) y
  le-right-mediant-ℚ =
    left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ y
      ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
      ( le-right-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H)

Strict inequality on the rationals is dense

module _
  (x y : ) (H : le-ℚ x y)
  where

  dense-le-ℚ :    r  le-ℚ x r × le-ℚ r y)
  dense-le-ℚ =
    intro-∃
      ( mediant-ℚ x y)
      ( le-left-mediant-ℚ x y H , le-right-mediant-ℚ x y H)

The strict order on the rationals is located

located-le-ℚ : (x y z : )  le-ℚ y z  (le-ℚ-Prop y x)  (le-ℚ-Prop x z)
located-le-ℚ x y z H =
  unit-trunc-Prop
    ( map-coproduct
      ( id)
      ( λ p  concatenate-leq-le-ℚ x y z p H)
      ( decide-le-leq-ℚ y x))

Recent changes