The binary maximum of real numbers

Content created by Louis Wasserman.

Created on 2025-09-02.
Last modified on 2025-09-02.

{-# OPTIONS --lossy-unification #-}

module real-numbers.binary-maximum-real-numbers where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.binary-transport
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.empty-types
open import foundation.functoriality-disjunction
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.universe-levels

open import metric-spaces.metric-space-of-short-functions-metric-spaces
open import metric-spaces.short-functions-metric-spaces

open import order-theory.join-semilattices
open import order-theory.large-join-semilattices
open import order-theory.least-upper-bounds-large-posets

open import real-numbers.addition-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.difference-real-numbers
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.metric-space-of-real-numbers
open import real-numbers.positive-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.strict-inequality-real-numbers
open import real-numbers.upper-dedekind-real-numbers

Idea

The maximum of two Dedekind real numbers x and y is the Dedekind real number max-ℝ x y with lower cut equal to the union of x and y’s lower cuts, and upper cut equal to the intersection of their upper cuts.

For any x : ℝ, max-ℝ x is a short function ℝ → ℝ for the standard real metric structure. Moreover, the map x ↦ max-ℝ x is a short function from ℝ into the metric space of short functions of ℝ.

Definition

module _
  {l1 l2 : Level}
  (x : ℝ l1) (y : ℝ l2)
  where

  lower-real-max-ℝ : lower-ℝ (l1 ⊔ l2)
  lower-real-max-ℝ = binary-max-lower-ℝ (lower-real-ℝ x) (lower-real-ℝ y)

  upper-real-max-ℝ : upper-ℝ (l1 ⊔ l2)
  upper-real-max-ℝ = binary-max-upper-ℝ (upper-real-ℝ x) (upper-real-ℝ y)

  abstract
    is-disjoint-lower-upper-max-ℝ :
      is-disjoint-lower-upper-ℝ lower-real-max-ℝ upper-real-max-ℝ
    is-disjoint-lower-upper-max-ℝ q (q<x∨q<y , x<q , y<q) =
      elim-disjunction
        ( empty-Prop)
        ( λ q<x → is-disjoint-cut-ℝ x q (q<x , x<q))
        ( λ q<y → is-disjoint-cut-ℝ y q (q<y , y<q))
        ( q<x∨q<y)

    is-located-lower-upper-max-ℝ :
      is-located-lower-upper-ℝ lower-real-max-ℝ upper-real-max-ℝ
    is-located-lower-upper-max-ℝ p q p<q =
      elim-disjunction
        ( claim)
        ( λ p<x → inl-disjunction (inl-disjunction p<x))
        ( λ x<q →
          map-disjunction
            ( λ p<y → inr-disjunction p<y)
            ( x<q ,_)
            ( is-located-lower-upper-cut-ℝ y p q p<q))
        ( is-located-lower-upper-cut-ℝ x p q p<q)
      where
        claim : Prop (l1 ⊔ l2)
        claim =
          cut-lower-ℝ lower-real-max-ℝ p ∨
          cut-upper-ℝ upper-real-max-ℝ q

  opaque
    max-ℝ : ℝ (l1 ⊔ l2)
    max-ℝ =
      real-lower-upper-ℝ
        ( lower-real-max-ℝ)
        ( upper-real-max-ℝ)
        ( is-disjoint-lower-upper-max-ℝ)
        ( is-located-lower-upper-max-ℝ)

Properties

The binary maximum is a least upper bound

module _
  {l1 l2 : Level}
  (x : ℝ l1) (y : ℝ l2)
  where

  opaque
    unfolding leq-ℝ max-ℝ

    is-least-binary-upper-bound-max-ℝ :
      is-least-binary-upper-bound-Large-Poset
        ( ℝ-Large-Poset)
        ( x)
        ( y)
        ( max-ℝ x y)
    is-least-binary-upper-bound-max-ℝ z =
      is-least-binary-upper-bound-binary-max-lower-ℝ
        ( lower-real-ℝ x)
        ( lower-real-ℝ y)
        ( lower-real-ℝ z)

    leq-max-leq-leq-ℝ :
      {l3 : Level} (z : ℝ l3) → leq-ℝ x z → leq-ℝ y z → leq-ℝ (max-ℝ x y) z
    leq-max-leq-leq-ℝ z x≤z y≤z =
      forward-implication (is-least-binary-upper-bound-max-ℝ z) (x≤z , y≤z)

The binary maximum is a binary upper bound

module _
  {l1 l2 : Level}
  (x : ℝ l1) (y : ℝ l2)
  where

  abstract
    leq-left-max-ℝ : leq-ℝ x (max-ℝ x y)
    leq-left-max-ℝ =
      pr1
        ( is-binary-upper-bound-is-least-binary-upper-bound-Large-Poset
          ( ℝ-Large-Poset)
          ( x)
          ( y)
          ( is-least-binary-upper-bound-max-ℝ x y))

    leq-right-max-ℝ : leq-ℝ y (max-ℝ x y)
    leq-right-max-ℝ =
      pr2
        ( is-binary-upper-bound-is-least-binary-upper-bound-Large-Poset
          ( ℝ-Large-Poset)
          ( x)
          ( y)
          ( is-least-binary-upper-bound-max-ℝ x y))

The binary maximum is commutative

module _
  {l1 l2 : Level}
  (x : ℝ l1) (y : ℝ l2)
  where

  opaque
    unfolding leq-ℝ sim-ℝ

    commutative-max-ℝ : max-ℝ x y ＝ max-ℝ y x
    commutative-max-ℝ =
      eq-sim-ℝ
        ( sim-is-least-binary-upper-bound-Large-Poset
          ( ℝ-Large-Poset)
          ( x)
          ( y)
          ( is-least-binary-upper-bound-max-ℝ x y)
          ( is-binary-least-upper-bound-swap-Large-Poset
            ( ℝ-Large-Poset)
            ( y)
            ( x)
            ( max-ℝ y x)
            ( is-least-binary-upper-bound-max-ℝ y x)))

The large poset of real numbers has joins

has-joins-ℝ-Large-Poset : has-joins-Large-Poset ℝ-Large-Poset
join-has-joins-Large-Poset has-joins-ℝ-Large-Poset = max-ℝ
is-least-binary-upper-bound-join-has-joins-Large-Poset
  has-joins-ℝ-Large-Poset = is-least-binary-upper-bound-max-ℝ

The real numbers at a specific universe level are a join semilattice

ℝ-Order-Theoretic-Join-Semilattice :
  (l : Level) → Order-Theoretic-Join-Semilattice (lsuc l) l
ℝ-Order-Theoretic-Join-Semilattice l =
  ( ℝ-Poset l , λ x y → (max-ℝ x y , is-least-binary-upper-bound-max-ℝ x y))

The binary maximum preserves similarity

abstract
  preserves-sim-max-ℝ :
    {l1 l2 l3 l4 : Level} →
    (a : ℝ l1) (a' : ℝ l2) → sim-ℝ a a' →
    (b : ℝ l3) (b' : ℝ l4) → sim-ℝ b b' →
    sim-ℝ (max-ℝ a b) (max-ℝ a' b')
  preserves-sim-max-ℝ a a' a~a' b b' b~b' =
    sim-sim-leq-ℝ
      ( sim-is-least-binary-upper-bound-Large-Poset
        ( ℝ-Large-Poset)
        ( a)
        ( b)
        ( is-least-binary-upper-bound-max-ℝ a b)
        ( preserves-is-least-binary-upper-bound-sim-Large-Poset
          ( ℝ-Large-Poset)
          ( a')
          ( b')
          ( max-ℝ a' b')
          ( sim-leq-sim-ℝ (symmetric-sim-ℝ a~a'))
          ( sim-leq-sim-ℝ (symmetric-sim-ℝ b~b'))
          ( is-least-binary-upper-bound-max-ℝ a' b')))

  preserves-sim-left-max-ℝ :
    {l1 l2 l3 : Level} →
    (a : ℝ l1) (a' : ℝ l2) → sim-ℝ a a' →
    (b : ℝ l3) →
    sim-ℝ (max-ℝ a b) (max-ℝ a' b)
  preserves-sim-left-max-ℝ a a' a~a' b =
    preserves-sim-max-ℝ a a' a~a' b b (refl-sim-ℝ b)

  preserves-sim-right-max-ℝ :
    {l1 l2 l3 : Level} →
    (a : ℝ l1) →
    (b : ℝ l2) (b' : ℝ l3) → sim-ℝ b b' →
    sim-ℝ (max-ℝ a b) (max-ℝ a b')
  preserves-sim-right-max-ℝ a = preserves-sim-max-ℝ a a (refl-sim-ℝ a)

The binary maximum preserves lower neighborhoods

module _
  {l1 l2 l3 : Level} (d : ℚ⁺)
  (x : ℝ l1) (y : ℝ l2) (z : ℝ l3)
  where

  abstract
    preserves-lower-neighborhood-leq-left-max-ℝ :
      leq-ℝ y (z +ℝ real-ℚ⁺ d) →
      leq-ℝ
        ( max-ℝ x y)
        ( (max-ℝ x z) +ℝ real-ℚ⁺ d)
    preserves-lower-neighborhood-leq-left-max-ℝ z≤y+d =
      leq-is-least-binary-upper-bound-Large-Poset
        ( ℝ-Large-Poset)
        ( x)
        ( y)
        ( is-least-binary-upper-bound-max-ℝ x y)
        ( (max-ℝ x z) +ℝ real-ℚ⁺ d)
        ( ( transitive-leq-ℝ
            ( x)
            ( max-ℝ x z)
            ( max-ℝ x z +ℝ real-ℚ⁺ d)
            ( leq-le-ℝ
              ( max-ℝ x z)
              ( max-ℝ x z +ℝ real-ℚ⁺ d)
              ( le-left-add-real-ℝ⁺
                ( max-ℝ x z)
                ( positive-real-ℚ⁺ d)))
            ( leq-left-max-ℝ x z)) ,
          ( transitive-leq-ℝ
            ( y)
            ( z +ℝ real-ℚ⁺ d)
            ( max-ℝ x z +ℝ real-ℚ⁺ d)
            ( preserves-leq-right-add-ℝ
              ( real-ℚ⁺ d)
              ( z)
              ( max-ℝ x z)
              ( leq-right-max-ℝ x z))
            ( z≤y+d)))

    preserves-lower-neighborhood-leq-right-max-ℝ :
      leq-ℝ y (z +ℝ real-ℚ⁺ d) →
      leq-ℝ
        ( max-ℝ y x)
        ( (max-ℝ z x) +ℝ real-ℚ⁺ d)
    preserves-lower-neighborhood-leq-right-max-ℝ z≤y+d =
      binary-tr
        ( λ u v → leq-ℝ u (v +ℝ real-ℚ⁺ d))
        ( commutative-max-ℝ x y)
        ( commutative-max-ℝ x z)
        ( preserves-lower-neighborhood-leq-left-max-ℝ z≤y+d)

The maximum with a real number is a short function ℝ → ℝ

module _
  {l1 l2 : Level} (x : ℝ l1)
  where

  abstract
    is-short-function-left-max-ℝ :
      is-short-function-Metric-Space
        ( metric-space-ℝ l2)
        ( metric-space-ℝ (l1 ⊔ l2))
        ( max-ℝ x)
    is-short-function-left-max-ℝ d y z Nyz =
      neighborhood-real-bound-each-leq-ℝ
        ( d)
        ( max-ℝ x y)
        ( max-ℝ x z)
        ( preserves-lower-neighborhood-leq-left-max-ℝ d x y z
          ( left-leq-real-bound-neighborhood-ℝ d y z Nyz))
        ( preserves-lower-neighborhood-leq-left-max-ℝ d x z y
          ( right-leq-real-bound-neighborhood-ℝ d y z Nyz))

  short-left-max-ℝ :
    short-function-Metric-Space
      ( metric-space-ℝ l2)
      ( metric-space-ℝ (l1 ⊔ l2))
  short-left-max-ℝ =
    (max-ℝ x , is-short-function-left-max-ℝ)

The binary maximum is a short function from ℝ to the metric space of short functions ℝ → ℝ

module _
  {l1 l2 : Level}
  where

  abstract
    is-short-function-short-left-max-ℝ :
      is-short-function-Metric-Space
        ( metric-space-ℝ l1)
        ( metric-space-of-short-functions-Metric-Space
          ( metric-space-ℝ l2)
          ( metric-space-ℝ (l1 ⊔ l2)))
        ( short-left-max-ℝ)
    is-short-function-short-left-max-ℝ d x y Nxy z =
      neighborhood-real-bound-each-leq-ℝ
        ( d)
        ( max-ℝ x z)
        ( max-ℝ y z)
        ( preserves-lower-neighborhood-leq-right-max-ℝ d z x y
          ( left-leq-real-bound-neighborhood-ℝ d x y Nxy))
        ( preserves-lower-neighborhood-leq-right-max-ℝ d z y x
          ( right-leq-real-bound-neighborhood-ℝ d x y Nxy))

  short-max-ℝ :
    short-function-Metric-Space
      ( metric-space-ℝ l1)
      ( metric-space-of-short-functions-Metric-Space
        ( metric-space-ℝ l2)
        ( metric-space-ℝ (l1 ⊔ l2)))
  short-max-ℝ =
    (short-left-max-ℝ , is-short-function-short-left-max-ℝ)

For any ε : ℚ⁺, (max-ℝ x y - ε < x) ∨ (max-ℝ x y - ε < y)

module _
  {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
  where

  abstract
    approximate-below-max-ℝ :
      (ε : ℚ⁺) →
      disjunction-type
        ( le-ℝ (max-ℝ x y -ℝ real-ℚ⁺ ε) x)
        ( le-ℝ (max-ℝ x y -ℝ real-ℚ⁺ ε) y)
    approximate-below-max-ℝ ε⁺@(ε , _) =
      let
        motive =
          ( le-prop-ℝ (max-ℝ x y -ℝ real-ℚ ε) x) ∨
          ( le-prop-ℝ (max-ℝ x y -ℝ real-ℚ ε) y)
        open do-syntax-trunc-Prop motive
      in do
        (q , max-ε<q , q<max) ←
          dense-rational-le-ℝ
            ( max-ℝ x y -ℝ real-ℚ ε)
            ( max-ℝ x y)
            ( le-diff-real-ℝ⁺ (max-ℝ x y) (positive-real-ℚ⁺ ε⁺))
        (r , q-<ℝ-r , r<max) ← dense-rational-le-ℝ (real-ℚ q) (max-ℝ x y) q<max
        let q<r = reflects-le-real-ℚ q r q-<ℝ-r
        map-disjunction
          ( λ q<x →
            transitive-le-ℝ
              ( max-ℝ x y -ℝ real-ℚ ε)
              ( real-ℚ q)
              ( x)
              ( le-real-is-in-lower-cut-ℚ q x q<x)
              ( max-ε<q))
          ( λ x<r →
            elim-disjunction
              ( le-prop-ℝ (max-ℝ x y -ℝ real-ℚ ε) y)
              ( λ q<y →
                transitive-le-ℝ
                  ( max-ℝ x y -ℝ real-ℚ ε)
                  ( real-ℚ q)
                  ( y)
                  ( le-real-is-in-lower-cut-ℚ q y q<y)
                  ( max-ε<q))
              ( λ y<r →
                ex-falso
                  ( irreflexive-le-ℝ
                    ( max-ℝ x y)
                    ( concatenate-leq-le-ℝ (max-ℝ x y) (real-ℚ r) (max-ℝ x y)
                      ( leq-max-leq-leq-ℝ x y (real-ℚ r)
                        ( leq-le-ℝ x (real-ℚ r)
                          ( le-real-is-in-upper-cut-ℚ r x x<r))
                        ( leq-le-ℝ y (real-ℚ r)
                          ( le-real-is-in-upper-cut-ℚ r y y<r)))
                      ( r<max))))
              ( is-located-lower-upper-cut-ℝ y q r q<r))
          ( is-located-lower-upper-cut-ℝ x q r q<r)

Recent changes