Approximations in metric spaces

Content created by Louis Wasserman.

Created on 2025-08-30.
Last modified on 2025-10-19.

module metric-spaces.approximations-metric-spaces where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.cartesian-products-subtypes
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.full-subtypes
open import foundation.function-types
open import foundation.images
open import foundation.images-subtypes
open import foundation.inhabited-subtypes
open import foundation.inhabited-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.unions-subtypes
open import foundation.universe-levels

open import metric-spaces.cartesian-products-metric-spaces
open import metric-spaces.equality-of-metric-spaces
open import metric-spaces.functions-metric-spaces
open import metric-spaces.images-isometries-metric-spaces
open import metric-spaces.images-metric-spaces
open import metric-spaces.images-short-functions-metric-spaces
open import metric-spaces.images-uniformly-continuous-functions-metric-spaces
open import metric-spaces.isometries-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.modulated-uniformly-continuous-functions-metric-spaces
open import metric-spaces.short-functions-metric-spaces
open import metric-spaces.subspaces-metric-spaces
open import metric-spaces.uniformly-continuous-functions-metric-spaces

Idea

For an ε : ℚ⁺, an ε-approximation of a metric space X is a subset S of X such that every point in X is in an ε-neighborhood of some s ∈ S.

This terminology is taken from [BV06] section 2.2.

A finitely enumerable ε-approximation is called an ε-net.

Definitions

module _
  {l1 l2 l3 : Level} (X : Metric-Space l1 l2) (ε : ℚ⁺)
  (S : subset-Metric-Space l3 X)
  where

  is-approximation-prop-Metric-Space : Prop (l1 ⊔ l2 ⊔ l3)
  is-approximation-prop-Metric-Space =
    is-full-subtype-Prop
      ( union-family-of-subtypes
        { I = type-subtype S}
        ( λ (s , s∈S) → neighborhood-prop-Metric-Space X ε s))

  is-approximation-Metric-Space : UU (l1 ⊔ l2 ⊔ l3)
  is-approximation-Metric-Space =
    type-Prop is-approximation-prop-Metric-Space

approximation-Metric-Space :
  {l1 l2 : Level} (l3 : Level) (X : Metric-Space l1 l2) (ε : ℚ⁺) →
  UU (l1 ⊔ l2 ⊔ lsuc l3)
approximation-Metric-Space l3 X ε =
  type-subtype (is-approximation-prop-Metric-Space {l3 = l3} X ε)

module _
  {l1 l2 l3 : Level} (X : Metric-Space l1 l2) (ε : ℚ⁺)
  (S : approximation-Metric-Space l3 X ε)
  where

  subset-approximation-Metric-Space : subset-Metric-Space l3 X
  subset-approximation-Metric-Space = pr1 S

  type-approximation-Metric-Space : UU (l1 ⊔ l3)
  type-approximation-Metric-Space =
    type-subtype subset-approximation-Metric-Space

  is-approximation-approximation-Metric-Space :
    is-approximation-Metric-Space X ε subset-approximation-Metric-Space
  is-approximation-approximation-Metric-Space = pr2 S

Properties

If μ is a modulus of uniform continuity for f : X → Y and A is a (μ ε)-approximation of X, then im f A is an ε-approximation of im f X

module _
  {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
  (f : type-function-Metric-Space X Y) {μ : ℚ⁺ → ℚ⁺}
  (is-modulus-ucont-f-μ :
    is-modulus-of-uniform-continuity-function-Metric-Space X Y f μ)
  (ε : ℚ⁺) (A : approximation-Metric-Space l5 X (μ ε))
  where

  abstract
    is-approximation-im-uniformly-continuous-function-approximation-Metric-Space :
      is-approximation-Metric-Space
        ( im-Metric-Space X Y f)
        ( ε)
        ( im-subtype
          ( map-unit-im f)
          ( subset-approximation-Metric-Space X (μ ε) A))
    is-approximation-im-uniformly-continuous-function-approximation-Metric-Space
      (y , ∃x:fx=y) =
        let
          open
            do-syntax-trunc-Prop
              ( ∃ _ (λ z → neighborhood-prop-Metric-Space Y ε (pr1 (pr1 z)) y))
        in do
          (x , fx=y) ← ∃x:fx=y
          ((a , a∈A) , Nμεax) ←
            is-approximation-approximation-Metric-Space X (μ ε) A x
          intro-exists
            ( map-unit-im
              ( map-unit-im f ∘
                inclusion-subtype
                  ( subset-approximation-Metric-Space X (μ ε) A))
              ( a , a∈A))
            ( tr
              ( neighborhood-Metric-Space Y ε (f a))
              ( fx=y)
              ( is-modulus-ucont-f-μ a ε x Nμεax))

  approximation-im-uniformly-continuous-function-approximation-Metric-Space :
    approximation-Metric-Space (l1 ⊔ l3 ⊔ l5) (im-Metric-Space X Y f) ε
  approximation-im-uniformly-continuous-function-approximation-Metric-Space =
    ( im-subtype (map-unit-im f) (subset-approximation-Metric-Space X (μ ε) A) ,
      is-approximation-im-uniformly-continuous-function-approximation-Metric-Space)

If f : X → Y is a short function and A is an ε-approximation of X, then im f A is an ε-approximation of im f X

module _
  {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
  (f : short-function-Metric-Space X Y)
  (ε : ℚ⁺) (A : approximation-Metric-Space l5 X ε)
  where

  approximation-im-short-function-approximation-Metric-Space :
    approximation-Metric-Space
      ( l1 ⊔ l3 ⊔ l5)
      ( im-short-function-Metric-Space X Y f)
      ( ε)
  approximation-im-short-function-approximation-Metric-Space =
    approximation-im-uniformly-continuous-function-approximation-Metric-Space
      ( X)
      ( Y)
      ( map-short-function-Metric-Space X Y f)
      ( is-modulus-of-uniform-continuity-id-is-short-function-Metric-Space
        ( X)
        ( Y)
        ( map-short-function-Metric-Space X Y f)
        ( is-short-map-short-function-Metric-Space X Y f))
      ( ε)
      ( A)

If f : X → Y is an isometry and A is an ε-approximation of X, then im f A is an ε-approximation of im f X

module _
  {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
  (f : isometry-Metric-Space X Y)
  (ε : ℚ⁺) (A : approximation-Metric-Space l5 X ε)
  where

  approximation-im-isometry-approximation-Metric-Space :
    approximation-Metric-Space
      ( l1 ⊔ l3 ⊔ l5)
      ( im-isometry-Metric-Space X Y f)
      ( ε)
  approximation-im-isometry-approximation-Metric-Space =
    approximation-im-short-function-approximation-Metric-Space X Y
      ( short-isometry-Metric-Space X Y f)
      ( ε)
      ( A)

If f : X ≃ Y is an isometric equivalence and A is an ε-approximation of X, then im f A is an ε-approximation of Y

module _
  {l1 l2 l3 l4 l5 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
  (f : isometric-equiv-Metric-Space X Y)
  (ε : ℚ⁺) (A : approximation-Metric-Space l5 X ε)
  where

  abstract
    is-approximation-im-isometric-equiv-approximation-Metric-Space :
      is-approximation-Metric-Space
        ( Y)
        ( ε)
        ( im-subtype
          ( map-isometric-equiv-Metric-Space X Y f)
          ( subset-approximation-Metric-Space X ε A))
    is-approximation-im-isometric-equiv-approximation-Metric-Space y =
      let
        open
          do-syntax-trunc-Prop
            ( ∃ _ (λ z → neighborhood-prop-Metric-Space Y ε (pr1 z) y))
      in do
        let x = map-inv-isometric-equiv-Metric-Space X Y f y
        ((a , a∈A) , Nεax) ← is-approximation-approximation-Metric-Space X ε A x
        intro-exists
          ( map-unit-im
            ( map-isometric-equiv-Metric-Space X Y f ∘
              inclusion-subtype (subset-approximation-Metric-Space X ε A))
            ( a , a∈A))
          ( tr
            ( neighborhood-Metric-Space Y ε
              ( map-isometric-equiv-Metric-Space X Y f a))
            ( is-section-map-inv-isometric-equiv-Metric-Space X Y f y)
            ( forward-implication
              ( is-isometry-map-isometric-equiv-Metric-Space X Y f ε _ _)
              ( Nεax)))

  approximation-im-isometric-equiv-approximation-Metric-Space :
    approximation-Metric-Space (l1 ⊔ l3 ⊔ l5) Y ε
  approximation-im-isometric-equiv-approximation-Metric-Space =
    ( im-subtype
        ( map-isometric-equiv-Metric-Space X Y f)
        ( subset-approximation-Metric-Space X ε A) ,
      is-approximation-im-isometric-equiv-approximation-Metric-Space)

If a metric space is inhabited, so is any approximation

module _
  {l1 l2 l3 : Level}
  (X : Metric-Space l1 l2) (|X| : is-inhabited (type-Metric-Space X))
  (ε : ℚ⁺) (S : subset-Metric-Space l3 X)
  where

  abstract
    is-inhabited-is-approximation-inhabited-Metric-Space :
      is-approximation-Metric-Space X ε S →
      is-inhabited-subtype S
    is-inhabited-is-approximation-inhabited-Metric-Space is-approx =
      let open do-syntax-trunc-Prop (is-inhabited-subtype-Prop S)
      in do
        x ← |X|
        (s , Nεsx) ← is-approx x
        unit-trunc-Prop s

Cartesian products of approximations

module _
  {l1 l2 l3 l4 l5 l6 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
  (ε : ℚ⁺)
  (A : approximation-Metric-Space l5 X ε)
  (B : approximation-Metric-Space l6 Y ε)
  where

  abstract
    is-approximation-product-approximation-Metric-Space :
      is-approximation-Metric-Space
        ( product-Metric-Space X Y)
        ( ε)
        ( product-subtype
          ( subset-approximation-Metric-Space X ε A)
          ( subset-approximation-Metric-Space Y ε B))
    is-approximation-product-approximation-Metric-Space (x , y) =
      let
        open
          do-syntax-trunc-Prop
            ( ∃
              ( type-product-subtype
                ( subset-approximation-Metric-Space X ε A)
                ( subset-approximation-Metric-Space Y ε B))
              ( λ (ab , _) →
                neighborhood-prop-Metric-Space
                  ( product-Metric-Space X Y)
                  ( ε)
                  ( ab)
                  ( x , y)))
      in do
        ((a , a∈A) , Nεax) ← is-approximation-approximation-Metric-Space X ε A x
        ((b , b∈B) , Nεby) ← is-approximation-approximation-Metric-Space Y ε B y
        intro-exists (((a , b) , a∈A , b∈B)) (Nεax , Nεby)

  product-approximation-Metric-Space :
    approximation-Metric-Space (l5 ⊔ l6) (product-Metric-Space X Y) ε
  product-approximation-Metric-Space =
    ( product-subtype
        ( subset-approximation-Metric-Space X ε A)
        ( subset-approximation-Metric-Space Y ε B) ,
      is-approximation-product-approximation-Metric-Space)

References

[BV06]
Douglas S. Bridges and Luminiţa Simona Vîţă. Techniques of Constructive Analysis. Springer-Verlag New York, 2006. ISBN 978-0-387-33646-6.

Recent changes