Rational approximates of real numbers

Content created by Louis Wasserman.

Created on 2025-12-27.
Last modified on 2025-12-27.

module real-numbers.rational-approximates-of-real-numbers where
Imports 
open import elementary-number-theory.addition-positive-rational-numbers
open import elementary-number-theory.addition-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.dependent-pair-types
open import foundation.existential-quantification
open import foundation.propositional-truncations
open import foundation.raising-universe-levels
open import foundation.universe-levels

open import metric-spaces.dense-subsets-metric-spaces

open import real-numbers.arithmetically-located-dedekind-cuts
open import real-numbers.dedekind-real-numbers
open import real-numbers.metric-space-of-real-numbers
open import real-numbers.rational-real-numbers

Idea

A rational approximate of a real number x to some positive rational ε is a rational number whose canonical embedding in the real numbers is within an ε-neighborhood of x in the metric space of real numbers.

Definition

rational-approximate-ℝ : {l : Level} → ℝ l → ℚ⁺ → UU l
rational-approximate-ℝ {l} x ε =
  Σ ℚ (λ q → neighborhood-ℝ l ε x (raise-real-ℚ l q))

Properties

Any real number can be approximated to any positive rational ε

abstract opaque
  unfolding neighborhood-ℝ real-ℚ

  exists-rational-approximate-ℝ :
    {l : Level} (x : ℝ l) (ε : ℚ⁺) →
    exists ℚ (λ q → neighborhood-prop-ℝ l ε x (raise-real-ℚ l q))
  exists-rational-approximate-ℝ {l} x ε⁺@(ε , _) =
    let
      open
        do-syntax-trunc-Prop
          ( ∃ ℚ (λ q → neighborhood-prop-ℝ l ε⁺ x (raise-real-ℚ l q)))
    in do
      ((p , q) , q<p+ε , p<x , x<q) ← is-arithmetically-located-ℝ x ε⁺
      intro-exists
        ( p)
        ( ( λ r r+ε<p →
            le-lower-cut-ℝ
              ( x)
              ( transitive-le-ℚ
                ( r)
                ( r +ℚ ε)
                ( p)
                ( map-inv-raise r+ε<p)
                ( le-right-add-rational-ℚ⁺ r ε⁺))
              ( p<x)) ,
          ( λ r r+ε<x →
            map-raise
              ( reflects-le-left-add-ℚ
                ( ε)
                ( r)
                ( p)
                ( transitive-le-ℚ
                  ( r +ℚ ε)
                  ( q)
                  ( p +ℚ ε)
                  ( q<p+ε)
                  ( le-lower-upper-cut-ℝ x r+ε<x x<q)))))

Recent changes