Cauchy completeness of the Dedekind real numbers

Content created by Louis Wasserman.

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

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

module real-numbers.cauchy-completeness-dedekind-real-numbers where
Imports
open import elementary-number-theory.addition-rational-numbers
open import elementary-number-theory.additive-group-of-rational-numbers
open import elementary-number-theory.difference-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-functions
open import foundation.cartesian-product-types
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.empty-types
open import foundation.existential-quantification
open import foundation.functoriality-disjunction
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import metric-spaces.cauchy-approximations-metric-spaces
open import metric-spaces.cauchy-sequences-complete-metric-spaces
open import metric-spaces.complete-metric-spaces
open import metric-spaces.convergent-cauchy-approximations-metric-spaces
open import metric-spaces.limits-of-cauchy-approximations-in-premetric-spaces
open import metric-spaces.metric-spaces

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.lower-dedekind-real-numbers
open import real-numbers.metric-space-of-real-numbers
open import real-numbers.negation-real-numbers
open import real-numbers.positive-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.strict-inequality-real-numbers
open import real-numbers.transposition-addition-subtraction-cuts-dedekind-real-numbers
open import real-numbers.upper-dedekind-real-numbers

Idea

The metric space of the Dedekind real numbers is complete.

Definitions

Cauchy approximations in the real numbers

cauchy-approximation-leq-ℝ : (l : Level)  UU (lsuc l)
cauchy-approximation-leq-ℝ l =
  cauchy-approximation-Metric-Space (metric-space-leq-ℝ l)

map-cauchy-approximation-leq-ℝ :
  {l : Level}  (x : cauchy-approximation-leq-ℝ l)  ℚ⁺   l
map-cauchy-approximation-leq-ℝ {l} =
  map-cauchy-approximation-Metric-Space (metric-space-leq-ℝ l)

is-cauchy-map-cauchy-approximation-leq-ℝ :
  {l : Level}  (x : cauchy-approximation-leq-ℝ l) 
  (ε δ : ℚ⁺) 
  neighborhood-Metric-Space
    ( metric-space-leq-ℝ l)
    ( ε +ℚ⁺ δ)
    ( map-cauchy-approximation-leq-ℝ x ε)
    ( map-cauchy-approximation-leq-ℝ x δ)
is-cauchy-map-cauchy-approximation-leq-ℝ {l} x =
  is-cauchy-approximation-map-cauchy-approximation-Metric-Space
    ( metric-space-leq-ℝ l)
    ( x)

Properties

The limit of a Cauchy sequence

module _
  {l : Level} (x : cauchy-approximation-leq-ℝ l)
  where

  lower-cut-lim-cauchy-approximation-leq-ℝ : subtype l 
  lower-cut-lim-cauchy-approximation-leq-ℝ q =
     ( ℚ⁺ × ℚ⁺)
      ( λ (ε , θ) 
        lower-cut-ℝ
          ( map-cauchy-approximation-leq-ℝ x ε)
          ( q +ℚ rational-ℚ⁺ (ε +ℚ⁺ θ)))

  upper-cut-lim-cauchy-approximation-leq-ℝ : subtype l 
  upper-cut-lim-cauchy-approximation-leq-ℝ q =
     ( ℚ⁺ × ℚ⁺)
      ( λ (ε , θ) 
        upper-cut-ℝ
          ( map-cauchy-approximation-leq-ℝ x ε)
          ( q -ℚ (rational-ℚ⁺ (ε +ℚ⁺ θ))))

  abstract
    is-inhabited-lower-cut-lim-cauchy-approximation-leq-ℝ :
      exists  lower-cut-lim-cauchy-approximation-leq-ℝ
    is-inhabited-lower-cut-lim-cauchy-approximation-leq-ℝ =
      let
        open do-syntax-trunc-Prop (  lower-cut-lim-cauchy-approximation-leq-ℝ)
        x1 = map-cauchy-approximation-leq-ℝ x one-ℚ⁺
        two-ℚ = one-ℚ +ℚ one-ℚ
      in do
        p , p<x1  is-inhabited-lower-cut-ℝ x1
        intro-exists
          ( p -ℚ two-ℚ)
          ( intro-exists
            ( one-ℚ⁺ , one-ℚ⁺)
            ( inv-tr
              ( is-in-lower-cut-ℝ x1)
              ( is-section-diff-ℚ two-ℚ p)
              ( p<x1)))

    is-inhabited-upper-cut-lim-cauchy-approximation-leq-ℝ :
      exists  upper-cut-lim-cauchy-approximation-leq-ℝ
    is-inhabited-upper-cut-lim-cauchy-approximation-leq-ℝ =
      let
        open do-syntax-trunc-Prop (  upper-cut-lim-cauchy-approximation-leq-ℝ)
        x1 = map-cauchy-approximation-leq-ℝ x one-ℚ⁺
        two-ℚ = one-ℚ +ℚ one-ℚ
      in do
        q , x1<q  is-inhabited-upper-cut-ℝ x1
        intro-exists
          ( q +ℚ two-ℚ)
          ( intro-exists
            ( one-ℚ⁺ , one-ℚ⁺)
            ( inv-tr
              ( is-in-upper-cut-ℝ x1)
              ( is-retraction-diff-ℚ two-ℚ q)
              ( x1<q)))

    forward-implication-is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ :
      (q : ) 
      is-in-subtype lower-cut-lim-cauchy-approximation-leq-ℝ q 
      exists
        ( )
        ( λ r  le-ℚ-Prop q r  lower-cut-lim-cauchy-approximation-leq-ℝ r)
    forward-implication-is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ
      q q<lim =
        let
          open
            do-syntax-trunc-Prop
              ( 
                ( )
                ( λ r 
                  le-ℚ-Prop q r  lower-cut-lim-cauchy-approximation-leq-ℝ r))
        in do
          (ε⁺@(ε , _) , θ⁺@(θ , _)) , q+ε+θ<xε  q<lim
          let  = map-cauchy-approximation-leq-ℝ x ε⁺
          r , q+ε+θ<r , r<xε 
            forward-implication
              ( is-rounded-lower-cut-ℝ
                ( map-cauchy-approximation-leq-ℝ x ε⁺)
                ( q +ℚ (ε +ℚ θ)))
              ( q+ε+θ<xε)
          intro-exists
            ( r -ℚ (ε +ℚ θ))
            ( le-transpose-left-add-ℚ q (ε +ℚ θ) r q+ε+θ<r ,
              intro-exists
                ( ε⁺ , θ⁺)
                ( inv-tr
                  ( is-in-lower-cut-ℝ )
                  ( is-section-diff-ℚ (ε +ℚ θ) r)
                  ( r<xε)))

    backward-implication-is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ :
      (q : ) 
      exists
        ( )
        ( λ r  le-ℚ-Prop q r  lower-cut-lim-cauchy-approximation-leq-ℝ r) 
      is-in-subtype lower-cut-lim-cauchy-approximation-leq-ℝ q
    backward-implication-is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ
      q ∃r =
        let
          open do-syntax-trunc-Prop (lower-cut-lim-cauchy-approximation-leq-ℝ q)
        in do
          r , q<r , r<lim  ∃r
          (ε⁺@(ε , _) , θ⁺@(θ , _)) , r+ε+θ<xε  r<lim
          let  = map-cauchy-approximation-leq-ℝ x ε⁺
          intro-exists
            ( ε⁺ , θ⁺)
            ( le-lower-cut-ℝ
              ( )
              ( q +ℚ (ε +ℚ θ))
              ( r +ℚ (ε +ℚ θ))
              ( preserves-le-left-add-ℚ (ε +ℚ θ) q r q<r)
              ( r+ε+θ<xε))

    is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ :
      (q : ) 
      is-in-subtype lower-cut-lim-cauchy-approximation-leq-ℝ q 
      exists
        ( )
        ( λ r  le-ℚ-Prop q r  lower-cut-lim-cauchy-approximation-leq-ℝ r)
    is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ q =
      ( forward-implication-is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ
          ( q) ,
        backward-implication-is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ
          ( q))

    forward-implication-is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ :
      (q : ) 
      is-in-subtype upper-cut-lim-cauchy-approximation-leq-ℝ q 
      exists
        ( )
        ( λ p  le-ℚ-Prop p q  upper-cut-lim-cauchy-approximation-leq-ℝ p)
    forward-implication-is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ
      q lim<q =
        let
          open
            do-syntax-trunc-Prop
              ( 
                ( )
                ( λ p 
                  le-ℚ-Prop p q  upper-cut-lim-cauchy-approximation-leq-ℝ p))
        in do
          (ε⁺@(ε , _) , θ⁺@(θ , _)) , xε<q-ε-θ  lim<q
          let  = map-cauchy-approximation-leq-ℝ x ε⁺
          p , p<q-ε-θ , xε<p 
            forward-implication
              ( is-rounded-upper-cut-ℝ  (q -ℚ (ε +ℚ θ)))
              ( xε<q-ε-θ)
          intro-exists
            ( p +ℚ (ε +ℚ θ))
            ( le-transpose-right-diff-ℚ p q (ε +ℚ θ) p<q-ε-θ ,
              intro-exists
                ( ε⁺ , θ⁺)
                ( inv-tr
                  ( is-in-upper-cut-ℝ )
                  ( is-retraction-diff-ℚ (ε +ℚ θ) p)
                  ( xε<p)))

    backward-implication-is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ :
      (q : ) 
      exists
        ( )
        ( λ p  le-ℚ-Prop p q  upper-cut-lim-cauchy-approximation-leq-ℝ p) 
      is-in-subtype upper-cut-lim-cauchy-approximation-leq-ℝ q
    backward-implication-is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ
      q ∃p =
        let
          open do-syntax-trunc-Prop (upper-cut-lim-cauchy-approximation-leq-ℝ q)
        in do
          p , p<q , lim<p  ∃p
          (ε⁺@(ε , _) , θ⁺@(θ , _)) , xε<p-ε-θ  lim<p
          let  = map-cauchy-approximation-leq-ℝ x ε⁺
          intro-exists
            ( ε⁺ , θ⁺)
            ( le-upper-cut-ℝ
              ( )
              ( p -ℚ (ε +ℚ θ))
              ( q -ℚ (ε +ℚ θ))
              ( preserves-le-left-add-ℚ (neg-ℚ (ε +ℚ θ)) p q p<q)
              ( xε<p-ε-θ))

    is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ :
      (q : ) 
      is-in-subtype upper-cut-lim-cauchy-approximation-leq-ℝ q 
      exists
        ( )
        ( λ p  le-ℚ-Prop p q  upper-cut-lim-cauchy-approximation-leq-ℝ p)
    is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ q =
      ( forward-implication-is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ
        ( q) ,
        backward-implication-is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ
        ( q))

  lower-real-lim-cauchy-approximation-leq-ℝ : lower-ℝ l
  lower-real-lim-cauchy-approximation-leq-ℝ =
    lower-cut-lim-cauchy-approximation-leq-ℝ ,
    is-inhabited-lower-cut-lim-cauchy-approximation-leq-ℝ ,
    is-rounded-lower-cut-lim-cauchy-approximation-leq-ℝ

  upper-real-lim-cauchy-approximation-leq-ℝ : upper-ℝ l
  upper-real-lim-cauchy-approximation-leq-ℝ =
    upper-cut-lim-cauchy-approximation-leq-ℝ ,
    is-inhabited-upper-cut-lim-cauchy-approximation-leq-ℝ ,
    is-rounded-upper-cut-lim-cauchy-approximation-leq-ℝ

  abstract
    is-disjoint-cut-lim-cauchy-approximation-leq-ℝ :
      (q : ) 
      ¬ ( is-in-subtype lower-cut-lim-cauchy-approximation-leq-ℝ q ×
          is-in-subtype upper-cut-lim-cauchy-approximation-leq-ℝ q)
    is-disjoint-cut-lim-cauchy-approximation-leq-ℝ q (q<lim , lim<q) =
      let
        open do-syntax-trunc-Prop empty-Prop
      in do
        (εl⁺@(εl , _) , θl⁺@(θl , _)) , q+εl+θl<xεl  q<lim
        (εu⁺@(εu , _) , θu⁺@(θu , _)) , xεu<q-εu-θu  lim<q
        let
          xεl = map-cauchy-approximation-leq-ℝ x εl⁺
          xεu = map-cauchy-approximation-leq-ℝ x εu⁺
          q-εu+θl<xεu : is-in-lower-cut-ℝ xεu ((q -ℚ εu) +ℚ θl)
          q-εu+θl<xεu =
            pr2
              ( is-cauchy-map-cauchy-approximation-leq-ℝ x εl⁺ εu⁺)
              ( (q -ℚ εu) +ℚ θl)
              ( inv-tr
                ( is-in-lower-cut-ℝ xεl)
                ( equational-reasoning
                    ((q -ℚ εu) +ℚ θl) +ℚ (εl +ℚ εu)
                     ((q +ℚ θl) -ℚ εu) +ℚ (εu +ℚ εl)
                      by
                        ap-add-ℚ
                          ( right-swap-add-ℚ q (neg-ℚ εu) θl)
                          ( commutative-add-ℚ εl εu)
                     ((q +ℚ θl) -ℚ εu) +ℚ εu +ℚ εl
                      by inv (associative-add-ℚ _ _ _)
                     (q +ℚ θl) +ℚ εl by ap (_+ℚ εl) (is-section-diff-ℚ _ _)
                     q +ℚ (θl +ℚ εl) by associative-add-ℚ _ _ _
                     q +ℚ (εl +ℚ θl) by ap (q +ℚ_) (commutative-add-ℚ _ _))
                ( q+εl+θl<xεl))
        is-disjoint-cut-ℝ
          ( xεu)
          ( q -ℚ εu)
          ( le-lower-cut-ℝ
              ( xεu)
              ( q -ℚ εu)
              ( (q -ℚ εu) +ℚ θl)
              ( le-right-add-rational-ℚ⁺ (q -ℚ εu) θl⁺)
              ( q-εu+θl<xεu) ,
            tr
              ( is-in-upper-cut-ℝ xεu)
              ( equational-reasoning
                (q -ℚ (εu +ℚ θu)) +ℚ θu
                 (q +ℚ (neg-ℚ εu +ℚ neg-ℚ θu)) +ℚ θu
                  by ap  r  (q +ℚ r) +ℚ θu) (distributive-neg-add-ℚ εu θu)
                 ((q -ℚ εu) -ℚ θu) +ℚ θu
                  by ap (_+ℚ θu) (inv (associative-add-ℚ _ _ _))
                 q -ℚ εu by is-section-diff-ℚ θu _)
              ( le-upper-cut-ℝ
                ( xεu)
                ( q -ℚ (εu +ℚ θu))
                ( (q -ℚ (εu +ℚ θu)) +ℚ θu)
                ( le-right-add-rational-ℚ⁺ (q -ℚ (εu +ℚ θu)) θu⁺)
                ( xεu<q-εu-θu)))

    is-located-lower-upper-cut-lim-cauchy-approximation-leq-ℝ :
      is-located-lower-upper-ℝ
        ( lower-real-lim-cauchy-approximation-leq-ℝ)
        ( upper-real-lim-cauchy-approximation-leq-ℝ)
    is-located-lower-upper-cut-lim-cauchy-approximation-leq-ℝ p q p<q =
      let
        open
          do-syntax-trunc-Prop
            ( lower-cut-lim-cauchy-approximation-leq-ℝ p 
              upper-cut-lim-cauchy-approximation-leq-ℝ q)
      in do
        ε'⁺@(ε' , _) , 2ε'⁺<q-p  double-le-ℚ⁺ (positive-diff-le-ℚ p q p<q)
        ε⁺@(ε , _) , 2ε⁺<ε'⁺  double-le-ℚ⁺ ε'⁺
        let
          2ε' = ε' +ℚ ε'
           = ε +ℚ ε
           =  +ℚ 
           = map-cauchy-approximation-leq-ℝ x ε⁺
        map-disjunction
          ( lower-cut-ℝ  (p +ℚ ))
          ( lower-cut-lim-cauchy-approximation-leq-ℝ p)
          ( upper-cut-ℝ  (q -ℚ ))
          ( upper-cut-lim-cauchy-approximation-leq-ℝ q)
          ( intro-exists (ε⁺ , ε⁺))
          ( intro-exists (ε⁺ , ε⁺))
          ( is-located-lower-upper-cut-ℝ
            ( map-cauchy-approximation-leq-ℝ x ε⁺)
            ( p +ℚ )
            ( q -ℚ )
            ( le-transpose-left-add-ℚ
              ( p +ℚ )
              ( )
              ( q)
              ( inv-tr
                ( λ r  le-ℚ r q)
                ( associative-add-ℚ p    commutative-add-ℚ p )
                ( le-transpose-right-diff-ℚ
                  ( )
                  ( q)
                  ( p)
                  ( transitive-le-ℚ
                    ( )
                    ( 2ε')
                    ( q -ℚ p)
                    ( 2ε'⁺<q-p)
                    ( preserves-le-add-ℚ {} {ε'} {} {ε'}
                      ( 2ε⁺<ε'⁺)
                      ( 2ε⁺<ε'⁺)))))))

  lim-cauchy-approximation-leq-ℝ :  l
  lim-cauchy-approximation-leq-ℝ =
    real-lower-upper-ℝ
      ( lower-real-lim-cauchy-approximation-leq-ℝ)
      ( upper-real-lim-cauchy-approximation-leq-ℝ)
      ( is-disjoint-cut-lim-cauchy-approximation-leq-ℝ)
      ( is-located-lower-upper-cut-lim-cauchy-approximation-leq-ℝ)

The limit satisfies the definition of a limit of a Cauchy approximation

module _
  {l : Level} (x : cauchy-approximation-leq-ℝ l)
  where

  is-limit-lim-cauchy-approximation-leq-ℝ :
    is-limit-cauchy-approximation-Premetric-Space
      ( premetric-space-leq-ℝ l)
      ( x)
      ( lim-cauchy-approximation-leq-ℝ x)
  is-limit-lim-cauchy-approximation-leq-ℝ ε⁺@(ε , _) θ⁺@(θ , _) =
    let
      open
        do-syntax-trunc-Prop
          ( premetric-leq-ℝ
            ( l)
            ( ε⁺ +ℚ⁺ θ⁺)
            ( map-cauchy-approximation-leq-ℝ x ε⁺)
            ( lim-cauchy-approximation-leq-ℝ x))
      lim = lim-cauchy-approximation-leq-ℝ x
       = map-cauchy-approximation-leq-ℝ x ε⁺
      θ'⁺@(θ' , _) = left-summand-split-ℚ⁺ θ⁺
      θ''⁺@(θ'' , _) = right-summand-split-ℚ⁺ θ⁺
      ε+θ'+θ''=ε+θ =
        associative-add-ℚ _ _ _ 
        ap (ε +ℚ_) (ap rational-ℚ⁺ (eq-add-split-ℚ⁺ θ⁺))
    in do
      ( r , xε+ε+θ'<r , r<xε+ε+θ) 
        tr
          ( le-ℝ ( +ℝ real-ℚ (ε +ℚ θ')))
          ( associative-add-ℝ _ _ _ 
            ap (  +ℝ_) (add-real-ℚ _ _  ap real-ℚ ε+θ'+θ''=ε+θ))
          ( le-left-add-real-ℝ⁺
            (  +ℝ (real-ℚ (ε +ℚ θ')))
            ( positive-real-ℚ⁺ θ''⁺))
      ( q , xε-ε-θ<q , q<xε-ε-θ') 
        tr
          ( λ y  le-ℝ y ( -ℝ real-ℚ (ε +ℚ θ')))
          ( associative-add-ℝ _ _ _ 
            ap
              (  +ℝ_)
              ( inv (distributive-neg-add-ℝ _ _) 
                ap neg-ℝ (add-real-ℚ _ _  ap real-ℚ ε+θ'+θ''=ε+θ)))
          ( le-diff-real-ℝ⁺ ( -ℝ real-ℚ (ε +ℚ θ')) (positive-real-ℚ⁺ θ''⁺))
      neighborhood-real-bound-each-leq-ℝ
        ( ε⁺ +ℚ⁺ θ⁺)
        ( )
        ( lim)
        ( leq-le-ℝ
          ( )
          ( lim +ℝ real-ℚ (ε +ℚ θ))
          ( le-transpose-left-diff-ℝ
            ( )
            ( real-ℚ (ε +ℚ θ))
            ( lim)
            ( transitive-le-ℝ
              (  -ℝ real-ℚ (ε +ℚ θ))
              ( real-ℚ q)
              ( lim)
              ( le-real-is-in-lower-cut-ℚ
                ( q)
                ( lim)
                ( intro-exists
                  ( ε⁺ , θ'⁺)
                  ( transpose-is-in-lower-cut-diff-ℝ  (ε +ℚ θ') q q<xε-ε-θ')))
              ( le-real-is-in-upper-cut-ℚ q ( -ℝ real-ℚ (ε +ℚ θ)) xε-ε-θ<q))))
        ( leq-le-ℝ
          ( lim)
          (  +ℝ real-ℚ (ε +ℚ θ))
          ( transitive-le-ℝ
            ( lim)
            ( real-ℚ r)
            (  +ℝ real-ℚ (ε +ℚ θ))
            ( le-real-is-in-lower-cut-ℚ r ( +ℝ real-ℚ (ε +ℚ θ)) r<xε+ε+θ)
            ( le-real-is-in-upper-cut-ℚ
              ( r)
              ( lim)
              ( intro-exists
                ( ε⁺ , θ'⁺)
                ( transpose-is-in-upper-cut-add-ℝ  (ε +ℚ θ') r xε+ε+θ'<r)))))

  is-convergent-cauchy-approximation-leq-ℝ :
    is-convergent-cauchy-approximation-Metric-Space
      ( metric-space-leq-ℝ l)
      ( x)
  is-convergent-cauchy-approximation-leq-ℝ =
    ( lim-cauchy-approximation-leq-ℝ x ,
      is-limit-lim-cauchy-approximation-leq-ℝ)

The standard metric space of real numbers is complete

is-complete-metric-space-leq-ℝ :
  (l : Level)  is-complete-Metric-Space (metric-space-leq-ℝ l)
is-complete-metric-space-leq-ℝ _ = is-convergent-cauchy-approximation-leq-ℝ

complete-metric-space-leq-ℝ :
  (l : Level)  Complete-Metric-Space (lsuc l) l
pr1 (complete-metric-space-leq-ℝ l) = metric-space-leq-ℝ l
pr2 (complete-metric-space-leq-ℝ l) = is-complete-metric-space-leq-ℝ l

Limits of Cauchy sequences in

cauchy-sequence-ℝ : (l : Level)  UU (lsuc l)
cauchy-sequence-ℝ l =
  cauchy-sequence-Complete-Metric-Space (complete-metric-space-leq-ℝ l)

lim-cauchy-sequence-ℝ : {l : Level}  cauchy-sequence-ℝ l   l
lim-cauchy-sequence-ℝ {l} =
  limit-cauchy-sequence-Complete-Metric-Space (complete-metric-space-leq-ℝ l)

Recent changes