diff --git a/src/elementary-number-theory/distance-rational-numbers.lagda.md b/src/elementary-number-theory/distance-rational-numbers.lagda.md index 9dd7d05eec..51ddf28395 100644 --- a/src/elementary-number-theory/distance-rational-numbers.lagda.md +++ b/src/elementary-number-theory/distance-rational-numbers.lagda.md @@ -29,9 +29,6 @@ open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.transport-along-identifications - -open import metric-spaces.metric-space-of-rational-numbers -open import metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods ``` @@ -93,6 +90,30 @@ abstract ```agda abstract + left-distributive-abs-mul-dist-ℚ : + (p q r : ℚ) → + abs-ℚ p *ℚ⁰⁺ dist-ℚ q r ＝ dist-ℚ (p *ℚ q) (p *ℚ r) + left-distributive-abs-mul-dist-ℚ p q r = + equational-reasoning + abs-ℚ p *ℚ⁰⁺ dist-ℚ q r + ＝ abs-ℚ (p *ℚ (q -ℚ r)) + by (inv (abs-mul-ℚ p (q -ℚ r))) + ＝ dist-ℚ (p *ℚ q) (p *ℚ r) + by ap abs-ℚ (left-distributive-mul-diff-ℚ p q r) + + right-distributive-abs-mul-dist-ℚ : + (p q r : ℚ) → + dist-ℚ q r *ℚ⁰⁺ abs-ℚ p ＝ dist-ℚ (q *ℚ p) (r *ℚ p) + right-distributive-abs-mul-dist-ℚ p q r = + equational-reasoning + dist-ℚ q r *ℚ⁰⁺ abs-ℚ p + ＝ abs-ℚ p *ℚ⁰⁺ dist-ℚ q r + by commutative-mul-ℚ⁰⁺ (dist-ℚ q r) (abs-ℚ p) + ＝ dist-ℚ (p *ℚ q) (p *ℚ r) + by left-distributive-abs-mul-dist-ℚ p q r + ＝ dist-ℚ (q *ℚ p) (r *ℚ p) + by ap-binary dist-ℚ (commutative-mul-ℚ p q) (commutative-mul-ℚ p r) + left-distributive-mul-dist-ℚ : (p : ℚ⁰⁺) (q r : ℚ) → p *ℚ⁰⁺ dist-ℚ q r ＝ dist-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r) @@ -165,122 +186,6 @@ abstract ( inv-tr (λ s → le-ℚ s r) (distributive-neg-diff-ℚ p q) q-pImports + +```agda +open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.identity-types +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.sequences +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import metric-spaces.functions-metric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.total-metric-spaces +open import metric-spaces.uniformly-continuous-functions-metric-spaces +``` + + + +## Idea + +A positive rational `α : ℚ⁺` is a +{{#concept "Lipschitz constant" Disambiguation="of a function between metric spaces" Agda=lipschitz-constant-function-Metric-Space}} +of a [function](metric-spaces.functions-metric-spaces.md) `f : A → B` between +[metric spaces](metric-spaces.metric-spaces.md) if for any `x y : A`, if `d` is +an upper bound of the distance between `x` and `y` in `A`, `α * d` is an upper +bound on the distance between `f x` and `f y` in `B`; in that case, `f` is +called an **α-Lipschitz** function. A function which admits a Lipschitz constant +is called a +{{#concept "Lipschitz function" Disambiguation="between metric spaces" WD="Lipschitz function" WDID=Q652707 Agda=lipschitz-function-Metric-Space}}. + +## Definitions + +### The property of being a Lipschitz constant of a map between metric spaces + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + (f : map-type-Metric-Space A B) + where + + is-lipschitz-constant-prop-function-Metric-Space : + ℚ⁺ → Prop (l1 ⊔ l2 ⊔ l2') + is-lipschitz-constant-prop-function-Metric-Space α = + Π-Prop + ( ℚ⁺) + ( λ d → + Π-Prop + ( type-Metric-Space A) + ( λ x → + Π-Prop + ( type-Metric-Space A) + ( λ y → + hom-Prop + ( structure-Metric-Space A d x y) + ( structure-Metric-Space B (α *ℚ⁺ d) (f x) (f y))))) + + is-lipschitz-constant-function-Metric-Space : ℚ⁺ → UU (l1 ⊔ l2 ⊔ l2') + is-lipschitz-constant-function-Metric-Space α = + type-Prop (is-lipschitz-constant-prop-function-Metric-Space α) + + is-prop-is-lipschitz-constant-function-Metric-Space : + (α : ℚ⁺) → + is-prop (is-lipschitz-constant-function-Metric-Space α) + is-prop-is-lipschitz-constant-function-Metric-Space α = + is-prop-type-Prop (is-lipschitz-constant-prop-function-Metric-Space α) + + lipschitz-constant-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l2') + lipschitz-constant-function-Metric-Space = + type-subtype is-lipschitz-constant-prop-function-Metric-Space +``` + +### The property of being a Lipschitz function + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + where + + is-lipschitz-function-prop-Metric-Space : + map-type-Metric-Space A B → Prop (l1 ⊔ l2 ⊔ l2') + is-lipschitz-function-prop-Metric-Space f = + is-inhabited-subtype-Prop + (is-lipschitz-constant-prop-function-Metric-Space A B f) + + is-lipschitz-function-Metric-Space : + map-type-Metric-Space A B → UU (l1 ⊔ l2 ⊔ l2') + is-lipschitz-function-Metric-Space f = + type-Prop (is-lipschitz-function-prop-Metric-Space f) + + is-prop-is-lipschitz-function-Metric-Space : + (f : map-type-Metric-Space A B) → + is-prop (is-lipschitz-function-Metric-Space f) + is-prop-is-lipschitz-function-Metric-Space f = + is-prop-type-Prop (is-lipschitz-function-prop-Metric-Space f) +``` + +### The type of Lipschitz functions between metric spaces + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + where + + lipschitz-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l1' ⊔ l2') + lipschitz-function-Metric-Space = + type-subtype (is-lipschitz-function-prop-Metric-Space A B) + +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + (f : lipschitz-function-Metric-Space A B) + where + + map-lipschitz-function-Metric-Space : + map-type-Metric-Space A B + map-lipschitz-function-Metric-Space = pr1 f + + is-lipschitz-map-lipschitz-function-Metric-Space : + is-lipschitz-function-Metric-Space A B map-lipschitz-function-Metric-Space + is-lipschitz-map-lipschitz-function-Metric-Space = pr2 f +``` + +## Properties + +### Constant functions are α-Lipschitz functions for all `α : ℚ⁺` + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + (f : map-type-Metric-Space A B) + where + + all-lipschitz-constant-is-constant-function-Metric-Space : + ( (x y : type-Metric-Space A) → f x ＝ f y) → + ( α : ℚ⁺) → + is-lipschitz-constant-function-Metric-Space A B f α + all-lipschitz-constant-is-constant-function-Metric-Space H α d x y _ = + indistinguishable-eq-Metric-Space B (f x) (f y) (H x y) (α *ℚ⁺ d) +``` + +### A function from a total metric space that is α-Lipschitz for all `α : ℚ⁺` is constant + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Total-Metric-Space l1 l2) (B : Metric-Space l1' l2') + (f : map-type-Metric-Space (metric-space-Total-Metric-Space A) B) + where + + is-constant-all-lipschitz-constant-function-Metric-Space : + ( (α : ℚ⁺) → + is-lipschitz-constant-function-Metric-Space + ( metric-space-Total-Metric-Space A) + ( B) + ( f) + ( α)) → + ( x y : type-Total-Metric-Space A) → + f x ＝ f y + is-constant-all-lipschitz-constant-function-Metric-Space H x y = + eq-indistinguishable-Metric-Space + ( B) + ( f x) + ( f y) + ( λ d → + rec-trunc-Prop + ( structure-Metric-Space B d (f x) (f y)) + ( λ (ε , Nεxy) → + tr + ( is-upper-bound-dist-Metric-Space B (f x) (f y)) + ( associative-mul-ℚ⁺ d (inv-ℚ⁺ ε) ε ∙ + ap (mul-ℚ⁺ d) (left-inverse-law-mul-ℚ⁺ ε) ∙ + right-unit-law-mul-ℚ⁺ d) + ( H (d *ℚ⁺ inv-ℚ⁺ ε) ε x y Nεxy)) + ( is-total-metric-space-Total-Metric-Space A x y)) +``` + +### Short functions are Lipschitz functions with Lipschitz constant equal to 1 + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + (f : map-type-Metric-Space A B) + where + + is-one-lipschitz-constant-is-short-function-Metric-Space : + is-short-function-Metric-Space A B f → + is-lipschitz-constant-function-Metric-Space A B f one-ℚ⁺ + is-one-lipschitz-constant-is-short-function-Metric-Space H d x y Nxy = + inv-tr + ( is-upper-bound-dist-Metric-Space B (f x) (f y)) + ( left-unit-law-mul-ℚ⁺ d) + ( H d x y Nxy) + + is-short-is-one-lipshitz-constant-function-Metric-Space : + is-lipschitz-constant-function-Metric-Space A B f one-ℚ⁺ → + is-short-function-Metric-Space A B f + is-short-is-one-lipshitz-constant-function-Metric-Space L d x y Nxy = + tr + ( is-upper-bound-dist-Metric-Space B (f x) (f y)) + ( left-unit-law-mul-ℚ⁺ d) + ( L d x y Nxy) +``` + +### Lipschitz functions are uniformly continuous + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + (f : map-type-Metric-Space A B) + where + + modulus-of-uniform-continuity-lipschitz-constant-function-Metric-Space : + lipschitz-constant-function-Metric-Space A B f → + modulus-of-uniform-continuity-map-Metric-Space A B f + modulus-of-uniform-continuity-lipschitz-constant-function-Metric-Space + (α , L) = + ( mul-ℚ⁺ (inv-ℚ⁺ α)) , + ( λ x d y H → + tr + ( is-upper-bound-dist-Metric-Space B (f x) (f y)) + ( ( inv (associative-mul-ℚ⁺ α (inv-ℚ⁺ α) d)) ∙ + ( ap (λ y → y *ℚ⁺ d) (right-inverse-law-mul-ℚ⁺ α)) ∙ + ( left-unit-law-mul-ℚ⁺ d)) + ( L (inv-ℚ⁺ α *ℚ⁺ d) x y H)) + + is-uniformly-continuous-is-lipschitz-function-Metric-Space : + is-lipschitz-function-Metric-Space A B f → + is-uniformly-continuous-map-Metric-Space A B f + is-uniformly-continuous-is-lipschitz-function-Metric-Space = + map-is-inhabited + modulus-of-uniform-continuity-lipschitz-constant-function-Metric-Space + +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + where + + uniformly-continuous-lipschitz-function-Metric-Space : + lipschitz-function-Metric-Space A B → + uniformly-continuous-map-Metric-Space A B + uniformly-continuous-lipschitz-function-Metric-Space f = + ( map-lipschitz-function-Metric-Space A B f) , + ( is-uniformly-continuous-is-lipschitz-function-Metric-Space + ( A) + ( B) + ( map-lipschitz-function-Metric-Space A B f) + ( is-lipschitz-map-lipschitz-function-Metric-Space A B f)) +``` + +### The product of Lipschitz constants of maps is a Lipschitz constant of their composition + +```agda +module _ + {la la' lb lb' lc lc' : Level} + (A : Metric-Space la la') + (B : Metric-Space lb lb') + (C : Metric-Space lc lc') + (g : map-type-Metric-Space B C) + (f : map-type-Metric-Space A B) + where + + mul-comp-lipschitz-constant-function-Metric-Space : + (α β : ℚ⁺) → + is-lipschitz-constant-function-Metric-Space B C g α → + is-lipschitz-constant-function-Metric-Space A B f β → + is-lipschitz-constant-function-Metric-Space A C (g ∘ f) (α *ℚ⁺ β) + mul-comp-lipschitz-constant-function-Metric-Space α β Hg Hf d x y Nxy = + inv-tr + ( λ ε → neighborhood-Metric-Space C ε (g (f x)) (g (f y))) + ( associative-mul-ℚ⁺ α β d) + ( Hg (β *ℚ⁺ d) (f x) (f y) (Hf d x y Nxy)) +``` + +### The composition of Lipschitz maps is Lipschitz + +```agda +module _ + {la la' lb lb' lc lc' : Level} + (A : Metric-Space la la') + (B : Metric-Space lb lb') + (C : Metric-Space lc lc') + where + + comp-is-lipschitz-function-Metric-Space : + (g : map-type-Metric-Space B C) → + (f : map-type-Metric-Space A B) → + is-lipschitz-function-Metric-Space B C g → + is-lipschitz-function-Metric-Space A B f → + is-lipschitz-function-Metric-Space A C (g ∘ f) + comp-is-lipschitz-function-Metric-Space g f Hg Hf = + rec-trunc-Prop + ( is-lipschitz-function-prop-Metric-Space A C (g ∘ f)) + ( λ (α , Lg) → + rec-trunc-Prop + ( is-lipschitz-function-prop-Metric-Space A C (g ∘ f)) + ( λ (β , Lf) → + unit-trunc-Prop + ( ( α *ℚ⁺ β) , + ( mul-comp-lipschitz-constant-function-Metric-Space + ( A) + ( B) + ( C) + ( g) + ( f) + ( α) + ( β) + ( Lg) + ( Lf)))) + ( Hf)) + ( Hg) +``` + +### Composition of Lipschitz functions + +```agda +module _ + {la la' lb lb' lc lc' : Level} + (A : Metric-Space la la') + (B : Metric-Space lb lb') + (C : Metric-Space lc lc') + where + + comp-lipschitz-function-Metric-Space : + lipschitz-function-Metric-Space B C → + lipschitz-function-Metric-Space A B → + lipschitz-function-Metric-Space A C + comp-lipschitz-function-Metric-Space g f = + ( map-lipschitz-function-Metric-Space B C g ∘ + map-lipschitz-function-Metric-Space A B f) , + ( comp-is-lipschitz-function-Metric-Space + ( A) + ( B) + ( C) + ( map-lipschitz-function-Metric-Space B C g) + ( map-lipschitz-function-Metric-Space A B f) + ( is-lipschitz-map-lipschitz-function-Metric-Space B C g) + ( is-lipschitz-map-lipschitz-function-Metric-Space A B f)) +``` + +### Being a Lipschitz map is homotopy invariant + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + (f g : map-type-Metric-Space A B) + (f~g : f ~ g) + where + + lipschitz-constant-htpy-function-Metric-Space : + lipschitz-constant-function-Metric-Space A B f → + lipschitz-constant-function-Metric-Space A B g + lipschitz-constant-htpy-function-Metric-Space = + tot + ( λ α H d x y N → + binary-tr + ( neighborhood-Metric-Space B (α *ℚ⁺ d)) + ( f~g x) + ( f~g y) + ( H d x y N)) + + is-lipschitz-htpy-function-Metric-Space : + is-lipschitz-function-Metric-Space A B f → + is-lipschitz-function-Metric-Space A B g + is-lipschitz-htpy-function-Metric-Space = + map-is-inhabited lipschitz-constant-htpy-function-Metric-Space +``` + +## External links + +- [Lipschitz maps](https://en.wikipedia.org/wiki/Lipschitz_continuity) at + Wikipedia diff --git a/src/metric-spaces/metric-space-of-lipschitz-functions-metric-spaces.lagda.md b/src/metric-spaces/metric-space-of-lipschitz-functions-metric-spaces.lagda.md new file mode 100644 index 0000000000..c2b2210036 --- /dev/null +++ b/src/metric-spaces/metric-space-of-lipschitz-functions-metric-spaces.lagda.md @@ -0,0 +1,45 @@ +# The metric space of Lipschitz functions between metric spaces + +```agda +module metric-spaces.metric-space-of-lipschitz-functions-metric-spaces where +``` + +
Imports + +```agda +open import foundation.universe-levels + +open import metric-spaces.lipschitz-functions-metric-spaces +open import metric-spaces.metric-space-of-functions-metric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.subspaces-metric-spaces +``` + +
+ +## Idea + +[Lipschitz functions](metric-spaces.lipschitz-functions-metric-spaces.md) +between [metric spaces](metric-spaces.metric-spaces.md) inherit the +[metric subspace](metric-spaces.subspaces-metric-spaces.md) structure of the +[function metric space](metric-spaces.metric-space-of-functions-metric-spaces.md). +This defines the +{{#concept "metric space of Lipschitz functions between metric spaces" Agda=metric-space-of-lipschitz-functions-Metric-Space}}. + +## Definitions + +### The metric space of Lipschitz functions between metric spaces + +```agda +module _ + {l1 l2 l1' l2' : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') + where + + metric-space-of-lipschitz-functions-Metric-Space : + Metric-Space (l1 ⊔ l2 ⊔ l1' ⊔ l2') (l1 ⊔ l2') + metric-space-of-lipschitz-functions-Metric-Space = + subspace-Metric-Space + ( metric-space-of-functions-Metric-Space A B) + ( is-lipschitz-function-prop-Metric-Space A B) +``` diff --git a/src/metric-spaces/metric-space-of-rational-numbers-with-open-neighborhoods.lagda.md b/src/metric-spaces/metric-space-of-rational-numbers-with-open-neighborhoods.lagda.md index 1d01b3be40..83a5a59bfe 100644 --- a/src/metric-spaces/metric-space-of-rational-numbers-with-open-neighborhoods.lagda.md +++ b/src/metric-spaces/metric-space-of-rational-numbers-with-open-neighborhoods.lagda.md @@ -11,6 +11,7 @@ module metric-spaces.metric-space-of-rational-numbers-with-open-neighborhoods wh ```agda open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.distance-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers @@ -23,6 +24,7 @@ open import foundation.empty-types open import foundation.equivalences open import foundation.function-types open import foundation.identity-types +open import foundation.logical-equivalences open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels @@ -149,6 +151,64 @@ pr1 metric-space-le-ℚ = premetric-space-le-ℚ pr2 metric-space-le-ℚ = is-metric-premetric-le-ℚ ``` +### Relationship to the distance on rational numbers + +```agda +abstract + le-dist-neighborhood-le-ℚ : + (ε : ℚ⁺) (p q : ℚ) → + neighborhood-le-ℚ ε p q → + le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) + le-dist-neighborhood-le-ℚ ε⁺@(ε , _) p q (H , K) = + le-dist-le-diff-ℚ + ( p) + ( q) + ( ε) + ( swap-right-diff-le-ℚ p ε q (le-transpose-right-add-ℚ p q ε K)) + ( swap-right-diff-le-ℚ q ε p (le-transpose-right-add-ℚ q p ε H)) + + neighborhood-le-le-dist-ℚ : + (ε : ℚ⁺) (p q : ℚ) → + le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) → + neighborhood-le-ℚ ε p q + neighborhood-le-le-dist-ℚ ε⁺@(ε , _) p q |p-q|<ε = + ( le-transpose-left-diff-ℚ + ( q) + ( ε) + ( p) + ( swap-right-diff-le-ℚ + ( q) + ( p) + ( ε) + ( concatenate-leq-le-ℚ + ( q -ℚ p) + ( rational-dist-ℚ p q) + ( ε) + ( leq-reversed-diff-dist-ℚ p q) + ( |p-q|<ε)))) , + ( le-transpose-left-diff-ℚ + ( p) + ( ε) + ( q) + ( swap-right-diff-le-ℚ + ( p) + ( q) + ( ε) + ( concatenate-leq-le-ℚ + ( p -ℚ q) + ( rational-dist-ℚ p q) + ( ε) + ( leq-diff-dist-ℚ p q) + ( |p-q|<ε)))) + +le-dist-iff-neighborhood-le-ℚ : + (ε : ℚ⁺) (p q : ℚ) → + le-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔ + neighborhood-le-ℚ ε p q +pr1 (le-dist-iff-neighborhood-le-ℚ ε p q) = neighborhood-le-le-dist-ℚ ε p q +pr2 (le-dist-iff-neighborhood-le-ℚ ε p q) = le-dist-neighborhood-le-ℚ ε p q +``` + ## See also - The standard diff --git a/src/metric-spaces/metric-space-of-rational-numbers.lagda.md b/src/metric-spaces/metric-space-of-rational-numbers.lagda.md index 6b959b335d..90caeaf96a 100644 --- a/src/metric-spaces/metric-space-of-rational-numbers.lagda.md +++ b/src/metric-spaces/metric-space-of-rational-numbers.lagda.md @@ -9,9 +9,13 @@ module metric-spaces.metric-space-of-rational-numbers where
Imports ```agda +open import elementary-number-theory.absolute-value-rational-numbers open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.distance-rational-numbers open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.nonnegative-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 @@ -27,6 +31,7 @@ open import foundation.function-types open import foundation.functoriality-cartesian-product-types open import foundation.identity-types open import foundation.logical-equivalences +open import foundation.propositional-truncations open import foundation.propositions open import foundation.transport-along-identifications open import foundation.universe-levels @@ -36,6 +41,7 @@ open import metric-spaces.convergent-cauchy-approximations-metric-spaces open import metric-spaces.extensional-premetric-structures open import metric-spaces.isometries-metric-spaces open import metric-spaces.limits-of-cauchy-approximations-premetric-spaces +open import metric-spaces.lipschitz-functions-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.metric-structures open import metric-spaces.monotonic-premetric-structures @@ -174,7 +180,65 @@ pr2 metric-space-leq-ℚ = is-metric-premetric-leq-ℚ ## Properties -### The standard saturated metric space of rationa numbers is saturated +### Relationship to the distance on rational numbers + +```agda +abstract + leq-dist-neighborhood-leq-ℚ : + (ε : ℚ⁺) (p q : ℚ) → + neighborhood-leq-ℚ ε p q → + leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) + leq-dist-neighborhood-leq-ℚ ε⁺@(ε , _) p q (H , K) = + leq-dist-leq-diff-ℚ + ( p) + ( q) + ( ε) + ( swap-right-diff-leq-ℚ p ε q (leq-transpose-right-add-ℚ p q ε K)) + ( swap-right-diff-leq-ℚ q ε p (leq-transpose-right-add-ℚ q p ε H)) + + neighborhood-leq-leq-dist-ℚ : + (ε : ℚ⁺) (p q : ℚ) → + leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) → + neighborhood-leq-ℚ ε p q + neighborhood-leq-leq-dist-ℚ ε⁺@(ε , _) p q |p-q|≤ε = + ( leq-transpose-left-diff-ℚ + ( q) + ( ε) + ( p) + ( swap-right-diff-leq-ℚ + ( q) + ( p) + ( ε) + ( transitive-leq-ℚ + ( q -ℚ p) + ( rational-dist-ℚ p q) + ( ε) + ( |p-q|≤ε) + ( leq-reversed-diff-dist-ℚ p q)))) , + ( leq-transpose-left-diff-ℚ + ( p) + ( ε) + ( q) + ( swap-right-diff-leq-ℚ + ( p) + ( q) + ( ε) + ( transitive-leq-ℚ + ( p -ℚ q) + ( rational-dist-ℚ p q) + ( ε) + ( |p-q|≤ε) + ( leq-diff-dist-ℚ p q)))) + +leq-dist-iff-neighborhood-leq-ℚ : + (ε : ℚ⁺) (p q : ℚ) → + leq-ℚ (rational-dist-ℚ p q) (rational-ℚ⁺ ε) ↔ + neighborhood-leq-ℚ ε p q +pr1 (leq-dist-iff-neighborhood-leq-ℚ ε p q) = neighborhood-leq-leq-dist-ℚ ε p q +pr2 (leq-dist-iff-neighborhood-leq-ℚ ε p q) = leq-dist-neighborhood-leq-ℚ ε p q +``` + +### The standard saturated metric space of rational numbers is saturated ```agda is-saturated-metric-space-leq-ℚ : @@ -256,6 +320,78 @@ module _ ( is-isometry-add-ℚ d y z) ``` +### Multiplication of rational numbers is Lipschitz + +```agda +module _ + (x : ℚ) + where + + abstract + is-lipschitz-constant-succ-abs-mul-ℚ : + is-lipschitz-constant-function-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℚ) + ( mul-ℚ x) + ( positive-succ-ℚ⁰⁺ (abs-ℚ x)) + is-lipschitz-constant-succ-abs-mul-ℚ d y z H = + neighborhood-leq-leq-dist-ℚ + ( positive-succ-ℚ⁰⁺ (abs-ℚ x) *ℚ⁺ d) + ( x *ℚ y) + ( x *ℚ z) + ( tr + ( λ q → + leq-ℚ + ( rational-ℚ⁰⁺ q) + ( rational-ℚ⁺ (positive-succ-ℚ⁰⁺ (abs-ℚ x) *ℚ⁺ d))) + ( left-distributive-abs-mul-dist-ℚ x y z) + ( transitive-leq-ℚ + ( rational-ℚ⁰⁺ (abs-ℚ x *ℚ⁰⁺ dist-ℚ y z)) + ( (succ-ℚ (rational-abs-ℚ x)) *ℚ (rational-dist-ℚ y z)) + ( rational-ℚ⁺ (positive-succ-ℚ⁰⁺ (abs-ℚ x) *ℚ⁺ d)) + ( preserves-leq-left-mul-ℚ⁺ + ( positive-succ-ℚ⁰⁺ (abs-ℚ x)) + ( rational-dist-ℚ y z) + ( rational-ℚ⁺ d) + ( leq-dist-neighborhood-leq-ℚ d y z H)) + ( preserves-leq-right-mul-ℚ⁰⁺ + ( dist-ℚ y z) + ( rational-abs-ℚ x) + ( succ-ℚ (rational-abs-ℚ x)) + ( succ-leq-ℚ (rational-abs-ℚ x))))) + + lipschitz-constant-succ-abs-mul-ℚ : + lipschitz-constant-function-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℚ) + ( mul-ℚ x) + lipschitz-constant-succ-abs-mul-ℚ = + ( positive-succ-ℚ⁰⁺ (abs-ℚ x)) , + ( is-lipschitz-constant-succ-abs-mul-ℚ) + + is-lipschitz-left-mul-ℚ : + ( is-lipschitz-function-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℚ) + ( mul-ℚ x)) + is-lipschitz-left-mul-ℚ = + unit-trunc-Prop lipschitz-constant-succ-abs-mul-ℚ + + is-lipschitz-right-mul-ℚ : + ( is-lipschitz-function-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℚ) + ( mul-ℚ' x)) + is-lipschitz-right-mul-ℚ = + is-lipschitz-htpy-function-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℚ) + ( mul-ℚ x) + ( mul-ℚ' x) + ( commutative-mul-ℚ x) + ( is-lipschitz-left-mul-ℚ) +``` + ### The convergent Cauchy approximation of the canonical inclusion of positive rational numbers into the rational numbers ```agda diff --git a/src/metric-spaces/metric-spaces.lagda.md b/src/metric-spaces/metric-spaces.lagda.md index 27701dbe35..926b30881f 100644 --- a/src/metric-spaces/metric-spaces.lagda.md +++ b/src/metric-spaces/metric-spaces.lagda.md @@ -147,6 +147,11 @@ module _ neighborhood-Metric-Space = neighborhood-Premetric-Space premetric-Metric-Space + is-upper-bound-dist-Metric-Space : + (x y : type-Metric-Space) → ℚ⁺ → UU l2 + is-upper-bound-dist-Metric-Space = + is-upper-bound-dist-Premetric-Space premetric-Metric-Space + is-reflexive-structure-Metric-Space : is-reflexive-Premetric structure-Metric-Space is-reflexive-structure-Metric-Space = diff --git a/src/metric-spaces/total-metric-spaces.lagda.md b/src/metric-spaces/total-metric-spaces.lagda.md new file mode 100644 index 0000000000..53d3342d7d --- /dev/null +++ b/src/metric-spaces/total-metric-spaces.lagda.md @@ -0,0 +1,76 @@ +# Total metric spaces + +```agda +module metric-spaces.total-metric-spaces where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.inhabited-subtypes +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.metric-spaces +``` + +
+ +## Idea + +A [metric space](metric-spaces.metric-spaces.md) is +{{#concept "total" Disambiguation="metric space" Agda=is-total-Metric-Space}} if +all elements are at bounded distance. + +## Definitions + +### The property of being a total metric space + +```agda +module _ + {l1 l2 : Level} (A : Metric-Space l1 l2) + where + + is-total-prop-Metric-Space : Prop (l1 ⊔ l2) + is-total-prop-Metric-Space = + Π-Prop + ( type-Metric-Space A) + ( λ x → + Π-Prop + ( type-Metric-Space A) + ( λ y → + is-inhabited-subtype-Prop + ( λ d → structure-Metric-Space A d x y))) + + is-total-Metric-Space : UU (l1 ⊔ l2) + is-total-Metric-Space = + type-Prop is-total-prop-Metric-Space +``` + +### The type of total metric spaces + +```agda +module _ + (l1 l2 : Level) + where + + Total-Metric-Space : UU (lsuc l1 ⊔ lsuc l2) + Total-Metric-Space = + type-subtype (is-total-prop-Metric-Space {l1} {l2}) + +module _ + {l1 l2 : Level} (M : Total-Metric-Space l1 l2) + where + + metric-space-Total-Metric-Space : Metric-Space l1 l2 + metric-space-Total-Metric-Space = pr1 M + + is-total-metric-space-Total-Metric-Space : + is-total-Metric-Space metric-space-Total-Metric-Space + is-total-metric-space-Total-Metric-Space = pr2 M + + type-Total-Metric-Space : UU l1 + type-Total-Metric-Space = type-Metric-Space metric-space-Total-Metric-Space +``` diff --git a/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md index ba1d0a1044..2089657c54 100644 --- a/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md @@ -11,6 +11,7 @@ open import elementary-number-theory.positive-rational-numbers open import foundation.function-types open import foundation.propositions +open import foundation.subtypes open import foundation.universe-levels open import metric-spaces.continuous-functions-metric-spaces @@ -32,6 +33,8 @@ if there exists a function `m : ℚ⁺ → ℚ⁺` such that for any `x : X`, wh ## Definitions +### The property of being a uniformly continuous function + ```agda module _ {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) @@ -46,6 +49,10 @@ module _ ( premetric-Metric-Space Y) ( f) + modulus-of-uniform-continuity-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) + modulus-of-uniform-continuity-map-Metric-Space = + type-subtype is-modulus-of-uniform-continuity-prop-Metric-Space + is-uniformly-continuous-map-prop-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4) is-uniformly-continuous-map-prop-Metric-Space = is-uniformly-continuous-map-prop-Premetric-Space @@ -70,6 +77,18 @@ module _ ( f) ``` +### The type of uniformly continuous functions between metric spaces + +```agda +module _ + {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4) + where + + uniformly-continuous-map-Metric-Space : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + uniformly-continuous-map-Metric-Space = + type-subtype (is-uniformly-continuous-map-prop-Metric-Space X Y) +``` + ## Properties ### The identity function is uniformly continuous diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 54359f5d72..5c7307e7d3 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -15,6 +15,7 @@ open import real-numbers.cauchy-completeness-dedekind-real-numbers public open import real-numbers.dedekind-real-numbers public open import real-numbers.difference-real-numbers public open import real-numbers.distance-real-numbers public +open import real-numbers.domain-extension-of-rational-real-functions public open import real-numbers.inequality-lower-dedekind-real-numbers public open import real-numbers.inequality-real-numbers public open import real-numbers.inequality-upper-dedekind-real-numbers public diff --git a/src/real-numbers/addition-real-numbers.lagda.md b/src/real-numbers/addition-real-numbers.lagda.md index 5abb105971..d9e0a2769f 100644 --- a/src/real-numbers/addition-real-numbers.lagda.md +++ b/src/real-numbers/addition-real-numbers.lagda.md @@ -341,7 +341,7 @@ module _ similarity-reasoning-ℝ x ~ℝ (x +ℝ z) +ℝ neg-ℝ z - by symmetric-sim-ℝ (cancel-right-add-diff-ℝ x z) + by inv-sim-ℝ (cancel-right-add-diff-ℝ x z) ~ℝ (y +ℝ z) +ℝ neg-ℝ z by preserves-sim-right-add-ℝ (neg-ℝ z) (x +ℝ z) (y +ℝ z) x+z≈y+z ~ℝ y by cancel-right-add-diff-ℝ y z @@ -442,9 +442,9 @@ module _ ( similarity-reasoning-ℝ neg-ℝ (x +ℝ y) ~ℝ neg-ℝ (x +ℝ y) +ℝ x +ℝ neg-ℝ x - by symmetric-sim-ℝ (cancel-right-add-diff-ℝ _ x) + by inv-sim-ℝ (cancel-right-add-diff-ℝ _ x) ~ℝ (((neg-ℝ (x +ℝ y) +ℝ x) +ℝ neg-ℝ x) +ℝ y) +ℝ neg-ℝ y - by symmetric-sim-ℝ (cancel-right-add-diff-ℝ _ y) + by inv-sim-ℝ (cancel-right-add-diff-ℝ _ y) ~ℝ (((neg-ℝ (x +ℝ y) +ℝ x) +ℝ y) +ℝ neg-ℝ x) +ℝ neg-ℝ y by sim-eq-ℝ (ap (_+ℝ neg-ℝ y) (right-swap-add-ℝ _ (neg-ℝ x) y)) ~ℝ ((neg-ℝ (x +ℝ y) +ℝ (x +ℝ y)) +ℝ neg-ℝ x) +ℝ neg-ℝ y diff --git a/src/real-numbers/domain-extension-of-rational-real-functions.lagda.md b/src/real-numbers/domain-extension-of-rational-real-functions.lagda.md new file mode 100644 index 0000000000..6be1192f82 --- /dev/null +++ b/src/real-numbers/domain-extension-of-rational-real-functions.lagda.md @@ -0,0 +1,375 @@ +# Domain extension of rational real functions + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.domain-extension-of-rational-real-functions where +``` + +
Imports + +```agda +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers + +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.existential-quantification +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.homotopies +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.negation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.metric-space-of-rational-numbers +open import metric-spaces.metric-spaces +open import metric-spaces.uniformly-continuous-functions-metric-spaces + +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +``` + +
+ +## Idea + +A [real](real-numbers.dedekind-real-numbers.md) function `g : ℝ → ℝ` is an +{{#concept "extension" Disambiguation="of rational real functions"}} of a +[rational](elementary-number-theory.rational-numbers.md) function `f : ℚ → ℝ` if +`g ∘ real-ℚ ~ f`. + +## Definitions + +### The property of being an extension of a rational real function + +```agda +module _ + {l : Level} (f : ℚ → ℝ l) + {l' : Level} (g : ℝ l' → ℝ (l ⊔ l')) + where + + is-extension-real-function-ℚ : UU (l ⊔ l') + is-extension-real-function-ℚ = + (q : ℚ) → sim-ℝ (g (raise-real-ℚ l' q)) (f q) + + opaque + unfolding sim-ℝ + + is-prop-is-extension-real-function-ℚ : + is-prop is-extension-real-function-ℚ + is-prop-is-extension-real-function-ℚ = + is-prop-Π + ( λ q → is-prop-type-Prop (sim-prop-ℝ (g (raise-real-ℚ l' q)) (f q))) + + is-extension-prop-real-function-ℚ : Prop (l ⊔ l') + is-extension-prop-real-function-ℚ = + is-extension-real-function-ℚ , + is-prop-is-extension-real-function-ℚ +``` + +### The type of extensions of rational real functions + +```agda +module _ + {l : Level} (f : ℚ → ℝ l) (l' : Level) + where + + extension-real-function-ℚ : UU (lsuc l ⊔ lsuc l') + extension-real-function-ℚ = + type-subtype (is-extension-prop-real-function-ℚ f {l'}) + + map-extension-real-function-ℚ : + extension-real-function-ℚ → ℝ l' → ℝ (l ⊔ l') + map-extension-real-function-ℚ = pr1 + + is-extention-map-extension-real-function-ℚ : + (H : extension-real-function-ℚ) → + is-extension-real-function-ℚ f (map-extension-real-function-ℚ H) + is-extention-map-extension-real-function-ℚ = pr2 +``` + +## Properties + +### If the extension of a rational real function is an isometry, so is the function + +```agda +module _ + {l : Level} (f : ℚ → ℝ l) + {l' : Level} (g : ℝ l' → ℝ (l ⊔ l')) + (ext-fg : is-extension-real-function-ℚ f g) + where + + is-isometry-is-isometry-is-extension-real-function-ℚ : + is-isometry-Metric-Space + ( metric-space-leq-ℝ l') + ( metric-space-leq-ℝ (l ⊔ l')) + ( g) → + is-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ l) + ( f) + is-isometry-is-isometry-is-extension-real-function-ℚ I d x y = + ( λ N → + preserves-neighborhood-sim-ℝ + ( d) + ( g (raise-real-ℚ l' x)) + ( g (raise-real-ℚ l' y)) + ( f x) + ( f y) + ( ext-fg x) + ( ext-fg y) + ( forward-implication + ( is-isometry-map-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ (l ⊔ l')) + ( comp-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ l') + ( metric-space-leq-ℝ (l ⊔ l')) + ( g , I) + ( isometry-metric-space-leq-raise-real-ℚ l')) + ( d) + ( x) + ( y)) + ( N))) , + ( λ N → + backward-implication + ( is-isometry-map-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ (l ⊔ l')) + ( comp-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ l') + ( metric-space-leq-ℝ (l ⊔ l')) + ( g , I) + ( isometry-metric-space-leq-raise-real-ℚ l')) + ( d) + ( x) + ( y)) + ( preserves-neighborhood-sim-ℝ + ( d) + ( f x) + ( f y) + ( g (raise-real-ℚ l' x)) + ( g (raise-real-ℚ l' y)) + ( symmetric-sim-ℝ (g (raise-real-ℚ l' x)) (f x) (ext-fg x)) + ( symmetric-sim-ℝ (g (raise-real-ℚ l' y)) (f y) (ext-fg y)) + ( N))) +``` + +### If the extension of a rational real function is short, so is the function + +TODO + +### If the extension of a rational real function is uniformly continuous so is the function + +TODO + +### Uniformly continuous extensions of rational real functions approximate the original function + +```agda +module _ + {l : Level} (f : ℚ → ℝ l) + {l' : Level} (g : ℝ l' → ℝ (l ⊔ l')) + (ext-fg : is-extension-real-function-ℚ f g) + where + + neighborhood-modulus-of-continuity-is-extension-real-function-ℚ : + ( uc-modulus-g : + modulus-of-uniform-continuity-map-Metric-Space + ( metric-space-leq-ℝ l') + ( metric-space-leq-ℝ (l ⊔ l')) + ( g)) + ( x : ℝ l') + ( y : ℚ) + ( ε : ℚ⁺) → + is-in-neighborhood-leq-ℝ + ( l') + ( pr1 uc-modulus-g ε) + ( x) + ( raise-real-ℚ l' y) → + is-in-neighborhood-leq-ℝ + ( l ⊔ l') + ( ε) + ( g x) + ( raise-ℝ l' (f y)) + neighborhood-modulus-of-continuity-is-extension-real-function-ℚ uc-g x y ε N = + preserves-neighborhood-sim-ℝ + ( ε) + ( g x) + ( g (raise-real-ℚ l' y)) + ( g x) + ( raise-ℝ l' (f y)) + ( refl-sim-ℝ (g x)) + ( transitive-sim-ℝ + ( g (raise-real-ℚ l' y)) + ( f y) + ( raise-ℝ l' (f y)) + ( sim-raise-ℝ l' (f y)) + ( ext-fg y)) + ( ( pr2 + ( uc-g) + ( x) + ( ε) + ( raise-real-ℚ l' y)) + ( N)) +``` + +### Uniformly continuous extensions of rational real functions are unique + +```agda +module _ + {l : Level} (f : ℚ → ℝ l) + {l' : Level} (g h : ℝ l' → ℝ (l ⊔ l')) + (ext-fg : is-extension-real-function-ℚ f g) + (ext-fh : is-extension-real-function-ℚ f h) + where + + sim-ev-modulus-of-uniform-continuity-is-extension-real-function-ℚ : + modulus-of-uniform-continuity-map-Metric-Space + ( metric-space-leq-ℝ l') + ( metric-space-leq-ℝ (l ⊔ l')) + ( g) → + modulus-of-uniform-continuity-map-Metric-Space + ( metric-space-leq-ℝ l') + ( metric-space-leq-ℝ (l ⊔ l')) + ( h) → + ( x : ℝ l') → + ( ε : ℚ⁺) → + is-in-neighborhood-leq-ℝ (l ⊔ l') ε (g x) (h x) + sim-ev-modulus-of-uniform-continuity-is-extension-real-function-ℚ + uc-g uc-h x ε = + tr + ( is-upper-bound-dist-Metric-Space + ( metric-space-leq-ℝ (l ⊔ l')) + ( g x) + ( h x)) + ( eq-add-split-ℚ⁺ ε) + ( elim-exists + ( premetric-leq-ℝ (l ⊔ l') (ε₁ +ℚ⁺ ε₂) (g x) (h x)) + ( λ y Nxy → + is-triangular-premetric-leq-ℝ + ( g x) + ( raise-ℝ l' (f y)) + ( h x) + ( ε₁) + ( ε₂) + ( is-symmetric-premetric-leq-ℝ + ( ε₂) + ( h x) + ( raise-ℝ l' (f y)) + ( lemma-approx-h y Nxy)) + ( lemma-approx-g y Nxy)) + ( is-dense-real-ℚ x δ)) + where + + ε₁ ε₂ δ : ℚ⁺ + ε₁ = left-summand-split-ℚ⁺ ε + ε₂ = right-summand-split-ℚ⁺ ε + δ = mediant-zero-min-ℚ⁺ (pr1 uc-g ε₁) (pr1 uc-h ε₂) + + lemma-approx-g : + (y : ℚ) → + is-in-neighborhood-leq-ℝ l' δ x (raise-real-ℚ l' y) → + is-in-neighborhood-leq-ℝ (l ⊔ l') ε₁ (g x) (raise-ℝ l' (f y)) + lemma-approx-g y Nxy = + neighborhood-modulus-of-continuity-is-extension-real-function-ℚ + ( f) + ( g) + ( ext-fg) + ( uc-g) + ( x) + ( y) + ( ε₁) + ( is-monotonic-structure-Metric-Space + ( metric-space-leq-ℝ l') + ( x) + ( raise-real-ℚ l' y) + ( δ) + ( pr1 uc-g ε₁) + ( le-left-mediant-zero-min-ℚ⁺ + ( pr1 uc-g ε₁) + ( pr1 uc-h ε₂)) + ( Nxy)) + + lemma-approx-h : + (y : ℚ) → + is-in-neighborhood-leq-ℝ l' δ x (raise-real-ℚ l' y) → + is-in-neighborhood-leq-ℝ (l ⊔ l') ε₂ (h x) (raise-ℝ l' (f y)) + lemma-approx-h y Nxy = + neighborhood-modulus-of-continuity-is-extension-real-function-ℚ + ( f) + ( h) + ( ext-fh) + ( uc-h) + ( x) + ( y) + ( ε₂) + ( is-monotonic-structure-Metric-Space + ( metric-space-leq-ℝ l') + ( x) + ( raise-real-ℚ l' y) + ( δ) + ( pr1 uc-h ε₂) + ( le-right-mediant-zero-min-ℚ⁺ + ( pr1 uc-g ε₁) + ( pr1 uc-h ε₂)) + ( Nxy)) + +module _ + { l : Level} (f : ℚ → ℝ l) + { l' : Level} (g h : ℝ l' → ℝ (l ⊔ l')) + ( ext-fg : is-extension-real-function-ℚ f g) + ( ext-fh : is-extension-real-function-ℚ f h) + ( uc-g : + is-uniformly-continuous-map-Metric-Space + (metric-space-leq-ℝ l') + (metric-space-leq-ℝ (l ⊔ l')) + ( g)) + ( uc-h : + is-uniformly-continuous-map-Metric-Space + (metric-space-leq-ℝ l') + (metric-space-leq-ℝ (l ⊔ l')) + ( h)) + where + + htpy-is-uniformly-continuous-real-extension-function-ℚ : g ~ h + htpy-is-uniformly-continuous-real-extension-function-ℚ x = + eq-indistinguishable-Metric-Space + ( metric-space-leq-ℝ (l ⊔ l')) + ( g x) + ( h x) + ( let + open + do-syntax-trunc-Prop + ( is-indistinguishable-prop-Metric-Space + ( metric-space-leq-ℝ (l ⊔ l')) + ( g x) + ( h x)) + in do + modulus-uc-g ← uc-g + modulus-uc-h ← uc-h + sim-ev-modulus-of-uniform-continuity-is-extension-real-function-ℚ + ( f) + ( g) + ( h) + ( ext-fg) + ( ext-fh) + ( modulus-uc-g) + ( modulus-uc-h) + ( x)) + + eq-is-uniformly-continuous-real-extension-function-ℚ : g ＝ h + eq-is-uniformly-continuous-real-extension-function-ℚ = + eq-htpy htpy-is-uniformly-continuous-real-extension-function-ℚ +``` diff --git a/src/real-numbers/maximum-real-numbers.lagda.md b/src/real-numbers/maximum-real-numbers.lagda.md index 984cef6207..6520eb2478 100644 --- a/src/real-numbers/maximum-real-numbers.lagda.md +++ b/src/real-numbers/maximum-real-numbers.lagda.md @@ -224,8 +224,8 @@ abstract ( a') ( b') ( max-ℝ a' b') - ( sim-leq-sim-ℝ (symmetric-sim-ℝ a~a')) - ( sim-leq-sim-ℝ (symmetric-sim-ℝ b~b')) + ( sim-leq-sim-ℝ (inv-sim-ℝ a~a')) + ( sim-leq-sim-ℝ (inv-sim-ℝ b~b')) ( is-least-binary-upper-bound-max-ℝ a' b'))) preserves-sim-left-max-ℝ : diff --git a/src/real-numbers/metric-space-of-real-numbers.lagda.md b/src/real-numbers/metric-space-of-real-numbers.lagda.md index 0ae8a26067..d494247341 100644 --- a/src/real-numbers/metric-space-of-real-numbers.lagda.md +++ b/src/real-numbers/metric-space-of-real-numbers.lagda.md @@ -28,6 +28,8 @@ open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels +open import logic.functoriality-existential-quantification + open import metric-spaces.extensional-premetric-structures open import metric-spaces.isometries-metric-spaces open import metric-spaces.metric-space-of-rational-numbers @@ -42,9 +44,11 @@ open import metric-spaces.symmetric-premetric-structures open import metric-spaces.triangular-premetric-structures open import real-numbers.addition-real-numbers +open import real-numbers.arithmetically-located-dedekind-cuts 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.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.strict-inequality-real-numbers @@ -312,31 +316,6 @@ module _ real-bound-is-in-lower-neighborhood-leq-ℝ d x y H ``` -### The canonical embedding from rational to real numbers is an isometry between metric spaces - -```agda -is-isometry-metric-space-leq-real-ℚ : - is-isometry-Metric-Space - ( metric-space-leq-ℚ) - ( metric-space-leq-ℝ lzero) - ( real-ℚ) -is-isometry-metric-space-leq-real-ℚ d x y = - pair - ( map-product - ( le-le-add-positive-leq-add-positive-ℚ x y d) - ( le-le-add-positive-leq-add-positive-ℚ y x d)) - ( map-product - ( leq-add-positive-le-le-add-positive-ℚ x y d) - ( leq-add-positive-le-le-add-positive-ℚ y x d)) - -isometry-metric-space-leq-real-ℚ : - isometry-Metric-Space - ( metric-space-leq-ℚ) - ( metric-space-leq-ℝ lzero) -isometry-metric-space-leq-real-ℚ = - ( real-ℚ , is-isometry-metric-space-leq-real-ℚ) -``` - ### Similarity of real numbers preserves neighborhoods ```agda @@ -378,6 +357,183 @@ module _ ( right-real-bound-neighborhood-leq-ℝ d x y H)) ``` +### The canonical embedding from rational to real numbers is an isometry between metric spaces + +```agda +is-isometry-metric-space-leq-real-ℚ : + is-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ lzero) + ( real-ℚ) +is-isometry-metric-space-leq-real-ℚ d x y = + pair + ( map-product + ( le-le-add-positive-leq-add-positive-ℚ x y d) + ( le-le-add-positive-leq-add-positive-ℚ y x d)) + ( map-product + ( leq-add-positive-le-le-add-positive-ℚ x y d) + ( leq-add-positive-le-le-add-positive-ℚ y x d)) + +isometry-metric-space-leq-real-ℚ : + isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ lzero) +isometry-metric-space-leq-real-ℚ = + ( real-ℚ , is-isometry-metric-space-leq-real-ℚ) +``` + +### Raising real numbers is an isometry + +```agda +module _ + {l0 : Level} (l : Level) + where + + is-isometry-metric-space-leq-raise-ℝ : + is-isometry-Metric-Space + ( metric-space-leq-ℝ l0) + ( metric-space-leq-ℝ (l0 ⊔ l)) + ( raise-ℝ l) + pr1 (is-isometry-metric-space-leq-raise-ℝ d x y) = + preserves-neighborhood-sim-ℝ + ( d) + ( x) + ( y) + ( raise-ℝ l x) + ( raise-ℝ l y) + ( sim-raise-ℝ l x) + ( sim-raise-ℝ l y) + pr2 (is-isometry-metric-space-leq-raise-ℝ d x y) = + preserves-neighborhood-sim-ℝ + ( d) + ( raise-ℝ l x) + ( raise-ℝ l y) + ( x) + ( y) + ( inv-sim-ℝ (sim-raise-ℝ l x)) + ( inv-sim-ℝ (sim-raise-ℝ l y)) + + isometry-metric-space-leq-raise-ℝ : + isometry-Metric-Space + ( metric-space-leq-ℝ l0) + ( metric-space-leq-ℝ (l0 ⊔ l)) + isometry-metric-space-leq-raise-ℝ = + ( raise-ℝ l , is-isometry-metric-space-leq-raise-ℝ) +``` + +### Raising rational numbers to real numbers is an isometry + +```agda +module _ + (l : Level) + where + + isometry-metric-space-leq-raise-real-ℚ : + isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ l) + isometry-metric-space-leq-raise-real-ℚ = + comp-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ lzero) + ( metric-space-leq-ℝ l) + ( isometry-metric-space-leq-raise-ℝ l) + ( isometry-metric-space-leq-real-ℚ) + + is-isometry-metric-space-leq-raise-real-ℚ : + is-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ l) + ( raise-real-ℚ l) + is-isometry-metric-space-leq-raise-real-ℚ = + is-isometry-map-isometry-Metric-Space + ( metric-space-leq-ℚ) + ( metric-space-leq-ℝ l) + ( isometry-metric-space-leq-raise-real-ℚ) +``` + +### The rational numbers are dense in the real nummbers + +```agda +module _ + {l : Level} (x : ℝ l) (δ : ℚ⁺) + where + + is-dense-real-ℚ : + exists + ( ℚ) + ( λ q → premetric-leq-ℝ l δ x (raise-real-ℚ l q)) + is-dense-real-ℚ = + map-exists + ( λ q → is-in-neighborhood-leq-ℝ l δ x (raise-real-ℚ l q)) + ( id) + ( λ q (H , K) → lemma-neighborhood-dense-real-ℚ q H K) + ( le-xδ) + where + + le-xδ : le-ℝ x (x +ℝ real-ℚ (rational-ℚ⁺ δ)) + le-xδ = + tr + ( λ z → le-ℝ z (x +ℝ real-ℚ (rational-ℚ⁺ δ))) + ( right-unit-law-add-ℝ x) + ( preserves-le-left-add-ℝ + ( x) + ( zero-ℝ) + ( real-ℚ (rational-ℚ⁺ δ)) + ( preserves-le-real-ℚ + ( zero-ℚ) + ( rational-ℚ⁺ δ) + ( le-zero-is-positive-ℚ + ( rational-ℚ⁺ δ) + ( is-positive-rational-ℚ⁺ δ)))) + + lemma-neighborhood-dense-real-ℚ : + (q : ℚ) → + is-in-upper-cut-ℝ x q → + is-in-lower-cut-ℝ (x +ℝ real-ℚ (rational-ℚ⁺ δ)) q → + is-in-neighborhood-leq-ℝ l δ x (raise-real-ℚ l q) + lemma-neighborhood-dense-real-ℚ q x