diff --git a/src/functional-analysis.lagda.md b/src/functional-analysis.lagda.md index 485d15d2e3..7e96a1b208 100644 --- a/src/functional-analysis.lagda.md +++ b/src/functional-analysis.lagda.md @@ -6,13 +6,16 @@ module functional-analysis where open import functional-analysis.absolute-convergence-series-real-banach-spaces public open import functional-analysis.additive-complete-metric-abelian-groups-real-banach-spaces public open import functional-analysis.convergent-series-real-banach-spaces public +open import functional-analysis.differentiable-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces public open import functional-analysis.metric-abelian-groups-normed-real-vector-spaces public +open import functional-analysis.modulated-uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces public open import functional-analysis.ratio-test-series-real-banach-spaces public open import functional-analysis.real-banach-spaces public open import functional-analysis.real-hilbert-spaces public open import functional-analysis.series-real-banach-spaces public open import functional-analysis.standard-euclidean-hilbert-spaces public open import functional-analysis.sums-of-finite-sequences-of-elements-real-banach-spaces public +open import functional-analysis.uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces public ``` ## External links diff --git a/src/functional-analysis/differentiable-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces.lagda.md b/src/functional-analysis/differentiable-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces.lagda.md new file mode 100644 index 0000000000..7612a4047b --- /dev/null +++ b/src/functional-analysis/differentiable-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces.lagda.md @@ -0,0 +1,846 @@ +# Differentiable maps from proper closed intervals on ℝ to normed real vector spaces + +```agda +{-# OPTIONS --lossy-unification #-} + +module functional-analysis.differentiable-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.minimum-positive-rational-numbers +open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.dependent-products-propositions +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.inhabited-subtypes +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.universe-levels + +open import functional-analysis.modulated-uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces +open import functional-analysis.uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces + +open import group-theory.abelian-groups + +open import linear-algebra.normed-real-vector-spaces + +open import lists.sequences + +open import metric-spaces.limits-of-sequences-metric-spaces + +open import order-theory.large-posets + +open import real-numbers.absolute-value-real-numbers +open import real-numbers.accumulation-points-subsets-real-numbers +open import real-numbers.addition-nonnegative-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.apartness-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.distance-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.multiplication-nonnegative-real-numbers +open import real-numbers.multiplication-positive-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.multiplicative-inverses-nonzero-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.nonzero-real-numbers +open import real-numbers.proper-closed-intervals-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +Given a map `f` from a +[proper closed interval](real-numbers.proper-closed-intervals-real-numbers.md) +`[a, b]` of [real numbers](real-numbers.dedekind-real-numbers.md) to a +[normed real vector space](linear-algebra.normed-real-vector-spaces.md) `V`, `g` +is a +{{#concept "derivative" Disambiguation="of map from a proper closed interval in ℝ to a normed real vector space" WD="derivative" WDID=Q29175 Agda=is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space}} +of `f` if there [exists](foundation.existential-quantification.md) a modulus +function `μ` such that for `ε : ℚ⁺` and any `x` and `y` in `[a, b]` within a +`μ(ε)`-[neighborhood](real-numbers.metric-space-of-real-numbers.md) of each +other, we have $$∥f(y) - f(x) - (y - x)g(x)∥ ≤ ε|y - x|.$$ + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (f g : type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + where + + is-modulus-of-derivative-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + subtype (lsuc l1) (ℚ⁺ → ℚ⁺) + is-modulus-of-derivative-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + μ = + Π-Prop + ( ℚ⁺) + ( λ ε → + Π-Prop + ( type-proper-closed-interval-ℝ l1 [a,b]) + ( λ (x , x∈[a,b]) → + Π-Prop + ( type-proper-closed-interval-ℝ l1 [a,b]) + ( λ (y , y∈[a,b]) → + hom-Prop + ( neighborhood-prop-ℝ l1 (μ ε) x y) + ( leq-prop-ℝ + ( dist-Normed-ℝ-Vector-Space V + ( diff-Normed-ℝ-Vector-Space V + ( f (y , y∈[a,b])) + ( f (x , x∈[a,b]))) + ( mul-Normed-ℝ-Vector-Space V (y -ℝ x) (g (x , x∈[a,b])))) + ( real-ℚ⁺ ε *ℝ dist-ℝ y x))))) + + is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + (ℚ⁺ → ℚ⁺) → UU (lsuc l1) + is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + is-in-subtype + ( is-modulus-of-derivative-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + + is-derivative-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + Prop (lsuc l1) + is-derivative-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + is-inhabited-subtype-Prop + ( is-modulus-of-derivative-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + + is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + UU (lsuc l1) + is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + type-Prop + ( is-derivative-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + where + + is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + (type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) → + UU (lsuc l1 ⊔ l2) + is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space f = + Σ ( type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + ( is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f)) + + differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + UU (lsuc l1 ⊔ l2) + differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + Σ ( type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + ( is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + + map-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space → + type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V + map-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = pr1 + + map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space → + type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V + map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + pr1 ∘ pr2 + + is-derivative-map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + (f : differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) → + is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( map-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( f)) + ( map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( f)) + is-derivative-map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + pr2 ∘ pr2 +``` + +## Properties + +### Proving the derivative of a map from a modulus + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (f g : type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + where abstract + + is-derivative-modulus-of-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + ( (ε : ℚ⁺) → + Σ ( ℚ⁺) + ( λ δ → + (x y : type-proper-closed-interval-ℝ l1 [a,b]) → + neighborhood-ℝ l1 δ (pr1 x) (pr1 y) → + leq-ℝ + ( dist-Normed-ℝ-Vector-Space V + ( diff-Normed-ℝ-Vector-Space V (f y) (f x)) + ( mul-Normed-ℝ-Vector-Space V (pr1 y -ℝ pr1 x) (g x))) + ( real-ℚ⁺ ε *ℝ dist-ℝ (pr1 y) (pr1 x)))) → + is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( g) + is-derivative-modulus-of-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + M = + intro-exists (pr1 ∘ M) (pr2 ∘ M) +``` + +### If `g` is a derivative of `f`, and `aₙ` is a sequence accumulating to `x`, and the limit exists, then `g x` is equal to the limit of `(f aₙ - f x)/(aₙ - x)` as `n → ∞` + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (f : type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + ((x , x∈[a,b]) : type-proper-closed-interval-ℝ l1 [a,b]) + (y@(sequence-y , _) : + sequence-accumulating-to-point-subset-ℝ + ( subtype-proper-closed-interval-ℝ l1 [a,b]) + ( x)) + where + + sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space : + sequence (type-Normed-ℝ-Vector-Space V) + sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space + n = + mul-Normed-ℝ-Vector-Space + ( V) + ( real-inv-nonzero-ℝ + ( nonzero-diff-apart-ℝ + ( real-sequence-accumulating-to-point-subset-ℝ + ( subtype-proper-closed-interval-ℝ l1 [a,b]) + ( x) + ( y) + ( n)) + ( x) + ( apart-sequence-accumulating-to-point-subset-ℝ + ( subtype-proper-closed-interval-ℝ l1 [a,b]) + ( x) + ( y) + ( n)))) + ( diff-Normed-ℝ-Vector-Space V + ( f (sequence-y n)) + ( f (x , x∈[a,b]))) + +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (f g : type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + (x@(xℝ , xℝ∈[a,b]) : type-proper-closed-interval-ℝ l1 [a,b]) + (y@(seq-y , apart-y , lim-y→x) : + sequence-accumulating-to-point-subset-ℝ + ( subtype-proper-closed-interval-ℝ l1 [a,b]) + ( xℝ)) + where abstract + + is-limit-sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space : + is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( g) → + is-limit-sequence-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( x) + ( y)) + ( g x) + is-limit-sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space + is-derivative-f-g = + let + open + do-syntax-trunc-Prop + ( is-limit-prop-sequence-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( x) + ( y)) + ( g x)) + open inequality-reasoning-Large-Poset ℝ-Large-Poset + seq-deriv = + sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( x) + ( y) + nonzero-diff n = + nonzero-diff-apart-ℝ + ( real-sequence-accumulating-to-point-subset-ℝ + ( subtype-proper-closed-interval-ℝ l1 [a,b]) + ( xℝ) + ( y) + ( n)) + ( xℝ) + ( apart-sequence-accumulating-to-point-subset-ℝ + ( subtype-proper-closed-interval-ℝ l1 [a,b]) + ( xℝ) + ( y) + ( n)) + real-nonzero-diff n = real-nonzero-ℝ (nonzero-diff n) + dist-V = dist-Normed-ℝ-Vector-Space V + _*V_ = mul-Normed-ℝ-Vector-Space V + _-V_ = diff-Normed-ℝ-Vector-Space V + in do + (μ , is-mod-μ) ← + is-limit-sequence-accumulating-to-point-subset-ℝ + ( subtype-proper-closed-interval-ℝ l1 [a,b]) + ( xℝ) + ( y) + (ν , is-mod-ν) ← is-derivative-f-g + intro-exists + ( μ ∘ ν) + ( λ ε n N≤n → + chain-of-inequalities + dist-V (seq-deriv n) (g x) + ≤ dist-V + ( seq-deriv n) + ( raise-one-ℝ l1 *V g x) + by + leq-eq-ℝ + ( ap-binary + ( dist-V) + ( refl) + ( inv (left-unit-law-mul-Normed-ℝ-Vector-Space V (g x)))) + ≤ dist-V + ( real-inv-nonzero-ℝ (nonzero-diff n) *V (f (seq-y n) -V f x)) + ( ( real-inv-nonzero-ℝ (nonzero-diff n) *ℝ + real-nonzero-diff n) *V + ( g x)) + by + leq-eq-ℝ + ( ap-binary + ( dist-V) + ( refl) + ( ap-binary + ( _*V_) + ( inv + ( eq-left-inverse-law-mul-nonzero-ℝ (nonzero-diff n))) + ( refl))) + ≤ dist-V + ( real-inv-nonzero-ℝ (nonzero-diff n) *V (f (seq-y n) -V f x)) + ( ( real-inv-nonzero-ℝ (nonzero-diff n)) *V + ( real-nonzero-diff n *V g x)) + by + leq-eq-ℝ + ( ap-binary + ( dist-V) + ( refl) + ( associative-mul-Normed-ℝ-Vector-Space V _ _ _)) + ≤ ( abs-ℝ (real-inv-nonzero-ℝ (nonzero-diff n))) *ℝ + ( dist-V (f (seq-y n) -V f x) (real-nonzero-diff n *V g x)) + by + leq-eq-ℝ + ( inv + ( left-distributive-abs-mul-dist-Normed-ℝ-Vector-Space V + ( _) + ( _) + ( _))) + ≤ ( abs-ℝ (real-inv-nonzero-ℝ (nonzero-diff n))) *ℝ + ( real-ℚ⁺ ε *ℝ dist-ℝ (pr1 (seq-y n)) xℝ) + by + preserves-leq-left-mul-ℝ⁰⁺ + ( nonnegative-abs-ℝ _) + ( is-mod-ν + ( ε) + ( x) + ( seq-y n) + ( is-symmetric-neighborhood-ℝ + ( ν ε) + ( pr1 (seq-y n)) + ( xℝ) + ( is-mod-μ (ν ε) n N≤n))) + ≤ ( real-ℚ⁺ ε) *ℝ + ( ( abs-ℝ (real-inv-nonzero-ℝ (nonzero-diff n))) *ℝ + ( dist-ℝ (pr1 (seq-y n)) xℝ)) + by leq-eq-ℝ (left-swap-mul-ℝ _ _ _) + ≤ ( real-ℚ⁺ ε) *ℝ + ( abs-ℝ + ( real-inv-nonzero-ℝ (nonzero-diff n) *ℝ real-nonzero-diff n)) + by leq-eq-ℝ (ap-mul-ℝ refl (inv (abs-mul-ℝ _ _))) + ≤ real-ℚ⁺ ε *ℝ abs-ℝ one-ℝ + by + leq-sim-ℝ + ( preserves-sim-left-mul-ℝ (real-ℚ⁺ ε) _ _ + ( preserves-sim-abs-ℝ + ( left-inverse-law-mul-nonzero-ℝ (nonzero-diff n)))) + ≤ real-ℚ⁺ ε *ℝ one-ℝ + by leq-eq-ℝ (ap-mul-ℝ refl (abs-real-ℝ⁰⁺ one-ℝ⁰⁺)) + ≤ real-ℚ⁺ ε + by leq-eq-ℝ (right-unit-law-mul-ℝ _)) +``` + +### Any two derivatives of a map are homotopic + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (f g h : + type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + where abstract + + htpy-is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( g) → + is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( h) → + g ~ h + htpy-is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + Dg Dh x@(xℝ , x∈[a,b]) = + rec-trunc-Prop + ( Id-Prop (set-Normed-ℝ-Vector-Space V) (g x) (h x)) + ( λ y → + eq-limit-sequence-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( x) + ( y)) + ( g x) + ( h x) + ( is-limit-sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( g) + ( x) + ( y) + ( Dg)) + ( is-limit-sequence-derivative-accumulating-to-point-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( h) + ( x) + ( y) + ( Dh))) + ( is-sequential-accumulation-point-is-accumulation-point-subset-ℝ + ( subtype-proper-closed-interval-ℝ l1 [a,b]) + ( xℝ) + ( is-accumulation-point-is-in-proper-closed-interval-ℝ + ( [a,b]) + ( xℝ) + ( x∈[a,b]))) +``` + +### Being differentiable is a proposition + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (f : type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + where + + abstract + all-elements-equal-is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + all-elements-equal + ( is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f)) + all-elements-equal-is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + (g , Dg) (h , Dh) = + eq-type-subtype + ( is-derivative-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f)) + ( eq-htpy + ( htpy-is-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( g) + ( h) + ( Dg) + ( Dh))) + + is-prop-is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + is-prop + ( is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f)) + is-prop-is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + is-prop-all-elements-equal + ( all-elements-equal-is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + + is-differentiable-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + Prop (lsuc l1 ⊔ l2) + is-differentiable-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + ( is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) , + is-prop-is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) +``` + +### A derivative of a map from a proper closed interval to a normed real vector space is uniformly continuous + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (f f' : type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + (δf : ℚ⁺ → ℚ⁺) + (is-mod-derivative-f-f'-δf : + is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( f') + ( δf)) + where abstract + + apart-modulus-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + ℚ⁺ → ℚ⁺ + apart-modulus-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + δf ∘ modulus-le-double-le-ℚ⁺ + + is-apart-modulus-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + (ε : ℚ⁺) (x y : type-proper-closed-interval-ℝ l1 [a,b]) → + apart-ℝ (pr1 x) (pr1 y) → + neighborhood-ℝ _ + ( apart-modulus-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( ε)) + ( pr1 x) + ( pr1 y) → + neighborhood-Normed-ℝ-Vector-Space V ε (f' x) (f' y) + is-apart-modulus-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ε x@(xℝ , _) y@(yℝ , _) x#y Nμεxy = + let + (ε' , ε'+ε'<ε) = bound-double-le-ℚ⁺ ε + open inequality-reasoning-Large-Poset ℝ-Large-Poset + dist-V = dist-Normed-ℝ-Vector-Space V + _*V_ = mul-Normed-ℝ-Vector-Space V + _-V_ = diff-Normed-ℝ-Vector-Space V + neg-V = neg-Normed-ℝ-Vector-Space V + in + reflects-leq-left-mul-ℝ⁺ + ( dist-ℝ xℝ yℝ , is-positive-dist-apart-ℝ x#y) + ( _) + ( _) + ( chain-of-inequalities + dist-ℝ xℝ yℝ *ℝ dist-V (f' x) (f' y) + ≤ dist-V ((xℝ -ℝ yℝ) *V f' x) ((xℝ -ℝ yℝ) *V f' y) + by + leq-eq-ℝ + ( left-distributive-abs-mul-dist-Normed-ℝ-Vector-Space V + ( xℝ -ℝ yℝ) + ( f' x) + ( f' y)) + ≤ dist-V ((xℝ -ℝ yℝ) *V f' x) (f x -V f y) +ℝ + dist-V (f x -V f y) ((xℝ -ℝ yℝ) *V f' y) + by triangular-dist-Normed-ℝ-Vector-Space V _ _ _ + ≤ dist-V (f x -V f y) ((xℝ -ℝ yℝ) *V f' x) +ℝ + dist-V (f x -V f y) ((xℝ -ℝ yℝ) *V f' y) + by + leq-eq-ℝ + ( ap-add-ℝ (symmetric-dist-Normed-ℝ-Vector-Space V _ _) refl) + ≤ dist-V (neg-V (f x -V f y)) (neg-V ((xℝ -ℝ yℝ) *V f' x)) +ℝ + dist-V (f x -V f y) ((xℝ -ℝ yℝ) *V f' y) + by + leq-eq-ℝ + ( ap-add-ℝ (inv (dist-neg-Normed-ℝ-Vector-Space V _ _)) refl) + ≤ dist-V (f y -V f x) (neg-ℝ (xℝ -ℝ yℝ) *V f' x) +ℝ + dist-V (f x -V f y) ((xℝ -ℝ yℝ) *V f' y) + by + leq-eq-ℝ + ( ap-add-ℝ + ( ap-binary + ( dist-V) + ( neg-right-subtraction-Ab + ( ab-Normed-ℝ-Vector-Space V) + ( f x) + ( f y)) + ( inv (left-negative-law-mul-Normed-ℝ-Vector-Space V _ _))) + ( refl)) + ≤ dist-V (f y -V f x) ((yℝ -ℝ xℝ) *V f' x) +ℝ + dist-V (f x -V f y) ((xℝ -ℝ yℝ) *V f' y) + by + leq-eq-ℝ + ( ap-add-ℝ + ( ap-binary + ( dist-V) + ( refl) + ( ap-binary _*V_ (distributive-neg-diff-ℝ xℝ yℝ) refl)) + ( refl)) + ≤ ( real-ℚ⁺ ε' *ℝ dist-ℝ yℝ xℝ) +ℝ + ( real-ℚ⁺ ε' *ℝ dist-ℝ xℝ yℝ) + by + preserves-leq-add-ℝ + ( is-mod-derivative-f-f'-δf ε' x y Nμεxy) + ( is-mod-derivative-f-f'-δf ε' y x + ( is-symmetric-neighborhood-ℝ (δf ε') xℝ yℝ Nμεxy)) + ≤ ( real-ℚ⁺ ε' *ℝ dist-ℝ xℝ yℝ) +ℝ + ( real-ℚ⁺ ε' *ℝ dist-ℝ xℝ yℝ) + by + leq-eq-ℝ + ( ap-add-ℝ (ap-mul-ℝ refl (commutative-dist-ℝ yℝ xℝ)) refl) + ≤ (real-ℚ⁺ ε' +ℝ real-ℚ⁺ ε') *ℝ dist-ℝ xℝ yℝ + by leq-eq-ℝ (inv (right-distributive-mul-add-ℝ _ _ _)) + ≤ real-ℚ⁺ (ε' +ℚ⁺ ε') *ℝ dist-ℝ xℝ yℝ + by leq-eq-ℝ (ap-mul-ℝ (add-real-ℚ _ _) refl) + ≤ real-ℚ⁺ ε *ℝ dist-ℝ xℝ yℝ + by + preserves-leq-right-mul-ℝ⁰⁺ + ( nonnegative-dist-ℝ xℝ yℝ) + ( preserves-leq-real-ℚ (leq-le-ℚ ε'+ε'<ε)) + ≤ dist-ℝ xℝ yℝ *ℝ real-ℚ⁺ ε + by leq-eq-ℝ (commutative-mul-ℝ _ _)) + + is-uniformly-continuous-derivative-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + is-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f') + is-uniformly-continuous-derivative-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + is-uniformly-continuous-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + { l5 = l1} + ( V) + ( [a,b]) + ( f') + ( apart-modulus-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + ( is-apart-modulus-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (df@(f , f' , Df) : + differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b])) + where + + abstract + is-uniformly-continuous-map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + is-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( df)) + is-uniformly-continuous-map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + elim-exists + ( is-uniformly-continuous-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f')) + ( is-uniformly-continuous-derivative-is-modulus-of-derivative-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( f')) + ( Df) + + uniformly-continuous-map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( l1) + ( V) + ( [a,b]) + uniformly-continuous-map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + ( f' , + is-uniformly-continuous-map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) +``` + +### A differentiable map from a proper closed interval to a normed real vector space is uniformly continuous + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (f : type-proper-closed-interval-ℝ l1 [a,b] → type-Normed-ℝ-Vector-Space V) + ((f' , Df) : + is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f)) + where abstract + + is-uniformly-continuous-is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + is-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + is-uniformly-continuous-is-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + let + open + do-syntax-trunc-Prop + ( is-uniformly-continuous-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f)) + open inequality-reasoning-Large-Poset ℝ-Large-Poset + dist-V = dist-Normed-ℝ-Vector-Space V + norm-V = map-norm-Normed-ℝ-Vector-Space V + _-V_ = diff-Normed-ℝ-Vector-Space V + _*V_ = mul-Normed-ℝ-Vector-Space V + (max-|f'|⁰⁺@(max-|f'| , 0≤max-|f'|) , is-max-|f'|) = + nonnegative-upper-bound-norm-im-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( uniformly-continuous-map-derivative-differentiable-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f , f' , Df)) + in do + (q , |f'|+1Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-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.function-types +open import foundation.subtypes +open import foundation.universe-levels + +open import linear-algebra.normed-real-vector-spaces + +open import metric-spaces.modulated-uniformly-continuous-maps-metric-spaces + +open import order-theory.large-posets + +open import real-numbers.addition-real-numbers +open import real-numbers.apartness-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.proper-closed-intervals-real-numbers +open import real-numbers.rational-real-numbers +``` + + + +## Idea + +Given a map `f` from a +[proper closed interval](real-numbers.proper-closed-intervals-real-numbers.md) +`[a, b]` in the [real numbers](real-numbers.dedekind-real-numbers.md) to a +[normed real vector space](linear-algebra.normed-real-vector-spaces.md) `V`, a +{{#concept "modulus of uniform continuity" Disambiguation="for a map from a proper closed interval in ℝ to a normed real vector space" Agda=is-modulus-of-uniform-continuity-map-proper-closed-interval-real-Normed-ℝ-Vector-Space}} +for `f` is a +[modulus of uniform continuity](metric-spaces.modulated-uniformly-continuous-maps-metric-spaces.md) +of `f` from the [metric space](metric-spaces.metric-spaces.md) of `[a, b]` to +the metric space of `V`. + +## Definition + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l3 l4) + (f : type-proper-closed-interval-ℝ l5 [a,b] → type-Normed-ℝ-Vector-Space V) + where + + is-modulus-of-uniform-continuity-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + subtype (l1 ⊔ l3 ⊔ l4 ⊔ lsuc l5) (ℚ⁺ → ℚ⁺) + is-modulus-of-uniform-continuity-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + is-modulus-of-uniform-continuity-prop-map-Metric-Space + ( metric-space-proper-closed-interval-ℝ l5 [a,b]) + ( metric-space-Normed-ℝ-Vector-Space V) + ( f) + + is-modulus-of-uniform-continuity-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + (ℚ⁺ → ℚ⁺) → UU (l1 ⊔ l3 ⊔ l4 ⊔ lsuc l5) + is-modulus-of-uniform-continuity-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + is-in-subtype + ( is-modulus-of-uniform-continuity-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + + modulus-of-uniform-continuity-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + UU (l1 ⊔ l3 ⊔ l4 ⊔ lsuc l5) + modulus-of-uniform-continuity-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + type-subtype + ( is-modulus-of-uniform-continuity-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) +``` + +## Properties + +### To show a function on a proper closed interval of real numbers is uniformly continuous, it suffices to exhibit a modulus that applies when its arguments are apart + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l3 l4) + (f : + type-proper-closed-interval-ℝ (l3 ⊔ l4 ⊔ l5) [a,b] → + type-Normed-ℝ-Vector-Space V) + (μ : ℚ⁺ → ℚ⁺) + (H : + (ε : ℚ⁺) (x y : type-proper-closed-interval-ℝ (l3 ⊔ l4 ⊔ l5) [a,b]) → + apart-ℝ (pr1 x) (pr1 y) → + neighborhood-ℝ _ (μ ε) (pr1 x) (pr1 y) → + neighborhood-Normed-ℝ-Vector-Space V ε (f x) (f y)) + where abstract + + modulus-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + ℚ⁺ → ℚ⁺ + modulus-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + μ ∘ modulus-le-double-le-ℚ⁺ + + is-modulus-of-uniform-continuity-modulus-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + is-modulus-of-uniform-continuity-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + ( modulus-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + is-modulus-of-uniform-continuity-modulus-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + x ε y Nxy = + let + (ε' , 2ε'<ε) = bound-double-le-ℚ⁺ ε + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + elim-exists + ( neighborhood-prop-Normed-ℝ-Vector-Space V ε (f x) (f y)) + ( λ z (z#x , z#y , Nε'zx , Nε'zy) → + chain-of-inequalities + dist-Normed-ℝ-Vector-Space V (f x) (f y) + ≤ dist-Normed-ℝ-Vector-Space V (f x) (f z) +ℝ + dist-Normed-ℝ-Vector-Space V (f z) (f y) + by triangular-dist-Normed-ℝ-Vector-Space V (f x) (f z) (f y) + ≤ real-ℚ⁺ ε' +ℝ real-ℚ⁺ ε' + by + preserves-leq-add-ℝ + ( H ε' x z + ( symmetric-apart-ℝ z#x) + ( is-symmetric-neighborhood-ℝ (μ ε') (pr1 z) (pr1 x) Nε'zx)) + ( H ε' z y z#y Nε'zy) + ≤ real-ℚ⁺ (ε' +ℚ⁺ ε') + by leq-eq-ℝ (add-real-ℚ _ _) + ≤ real-ℚ⁺ ε + by preserves-leq-real-ℚ (leq-le-ℚ 2ε'<ε)) + ( exists-element-apart-from-both-in-neighborhood-proper-closed-interval-ℝ + ( l3 ⊔ l4 ⊔ l5) + ( [a,b]) + ( x) + ( y) + ( μ ε') + ( Nxy)) +``` diff --git a/src/functional-analysis/uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces.lagda.md b/src/functional-analysis/uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces.lagda.md new file mode 100644 index 0000000000..d576692315 --- /dev/null +++ b/src/functional-analysis/uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces.lagda.md @@ -0,0 +1,176 @@ +# Uniformly continuous maps from proper closed intervals in the real numbers to normed real vector spaces + +```agda +module functional-analysis.uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.inhabited-subtypes +open import foundation.subtypes +open import foundation.universe-levels + +open import functional-analysis.modulated-uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces + +open import linear-algebra.normed-real-vector-spaces + +open import metric-spaces.uniformly-continuous-maps-metric-spaces + +open import real-numbers.absolute-value-real-numbers +open import real-numbers.apartness-real-numbers +open import real-numbers.inequality-nonnegative-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.proper-closed-intervals-real-numbers +open import real-numbers.uniformly-continuous-real-maps-proper-closed-intervals-real-numbers +``` + +
+ +## Idea + +A map `f` from a +[proper closed interval](real-numbers.proper-closed-intervals-real-numbers.md) +`[a, b]` in the [real numbers](real-numbers.dedekind-real-numbers.md) to a +[normed real vector space](linear-algebra.normed-real-vector-spaces.md) `V` is +{{#concept "uniformly continuous" Disambiguation="uniformly continuous map from a proper closed interval in ℝ to a normed real vector space" Agda=uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space}} +if it is +[uniformly continuous](metric-spaces.uniformly-continuous-maps-metric-spaces.md) +as a map from the [metric space](metric-spaces.metric-spaces.md) of `[a, b]` to +the metric space of `V`. + +## Definition + +```agda +module _ + {l1 l2 l3 l4 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l3 l4) + where + + is-uniformly-continuous-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + {l5 : Level} → + subtype + ( l1 ⊔ l3 ⊔ l4 ⊔ lsuc l5) + ( type-proper-closed-interval-ℝ l5 [a,b] → type-Normed-ℝ-Vector-Space V) + is-uniformly-continuous-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + f = + is-inhabited-subtype-Prop + ( is-modulus-of-uniform-continuity-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f)) + + is-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + {l5 : Level} → + (type-proper-closed-interval-ℝ l5 [a,b] → type-Normed-ℝ-Vector-Space V) → + UU (l1 ⊔ l3 ⊔ l4 ⊔ lsuc l5) + is-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + is-in-subtype + ( is-uniformly-continuous-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space) + +uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + {l1 l2 l3 l4 : Level} (l5 : Level) → Normed-ℝ-Vector-Space l1 l2 → + proper-closed-interval-ℝ l3 l4 → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5) +uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + l5 V [a,b] = + type-subtype + ( is-uniformly-continuous-prop-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + { l5 = l5}) +``` + +## Properties + +### To show a function on a proper closed interval of real numbers is uniformly continuous, it suffices to exhibit a modulus that applies when its arguments are apart + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l3 l4) + (f : + type-proper-closed-interval-ℝ (l3 ⊔ l4 ⊔ l5) [a,b] → + type-Normed-ℝ-Vector-Space V) + (μ : ℚ⁺ → ℚ⁺) + (H : + (ε : ℚ⁺) (x y : type-proper-closed-interval-ℝ (l3 ⊔ l4 ⊔ l5) [a,b]) → + apart-ℝ (pr1 x) (pr1 y) → + neighborhood-ℝ _ (μ ε) (pr1 x) (pr1 y) → + neighborhood-Normed-ℝ-Vector-Space V ε (f x) (f y)) + where abstract + + is-uniformly-continuous-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + is-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( V) + ( [a,b]) + ( f) + is-uniformly-continuous-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + intro-exists + ( modulus-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + { l5 = l5} + ( V) + ( [a,b]) + ( f) + ( μ) + ( H)) + ( is-modulus-of-uniform-continuity-modulus-modulus-apart-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + { l5 = l5} + ( V) + ( [a,b]) + ( f) + ( μ) + ( H)) +``` + +### There is a bound on the norm of the image of a proper closed interval under a uniformly continuous real function + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + ([a,b] : proper-closed-interval-ℝ l1 l1) + (ucf@(f , is-uc-f) : + uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space + ( l1) + ( V) + ( [a,b])) + where abstract + + nonnegative-upper-bound-norm-im-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space : + Σ ( ℝ⁰⁺ l1) + ( λ b → + (x : type-proper-closed-interval-ℝ l1 [a,b]) → + leq-ℝ⁰⁺ (nonnegative-norm-Normed-ℝ-Vector-Space V (f x)) b) + nonnegative-upper-bound-norm-im-uniformly-continuous-map-proper-closed-interval-real-Normed-ℝ-Vector-Space = + let + (b , |||fx|||≤b) = + nonnegative-upper-bound-abs-im-uniformly-continuous-real-map-proper-closed-interval-ℝ + ( [a,b]) + ( comp-uniformly-continuous-map-Metric-Space + ( metric-space-proper-closed-interval-ℝ l1 [a,b]) + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-ℝ l1) + ( uniformly-continuous-map-norm-Normed-ℝ-Vector-Space V) + ( ucf)) + in + ( b , + λ x → + transitive-leq-ℝ⁰⁺ + ( nonnegative-norm-Normed-ℝ-Vector-Space V (f x)) + ( nonnegative-abs-ℝ (map-norm-Normed-ℝ-Vector-Space V (f x))) + ( b) + ( |||fx|||≤b x) + ( leq-abs-ℝ (map-norm-Normed-ℝ-Vector-Space V (f x)))) +``` + +## See also + +- [Modulated uniformly continuous maps from proper closed intervals in ℝ to normed real vector spaces](functional-analysis.modulated-uniformly-continuous-maps-on-proper-closed-intervals-real-numbers-normed-real-vector-spaces.md) diff --git a/src/group-theory/abelian-groups.lagda.md b/src/group-theory/abelian-groups.lagda.md index 962f85ee6e..d2fbd538f8 100644 --- a/src/group-theory/abelian-groups.lagda.md +++ b/src/group-theory/abelian-groups.lagda.md @@ -543,6 +543,24 @@ module _ is-unit-right-div-eq-Group (group-Ab A) ``` +### Unit laws of right subtraction + +```agda +module _ + {l : Level} (G : Ab l) (x : type-Ab G) + where abstract + + right-zero-law-right-subtraction-Ab : + right-subtraction-Ab G x (zero-Ab G) ＝ x + right-zero-law-right-subtraction-Ab = + right-unit-law-right-div-Group (group-Ab G) x + + left-unit-law-right-subtraction-Ab : + right-subtraction-Ab G (zero-Ab G) x ＝ neg-Ab G x + left-unit-law-right-subtraction-Ab = + left-unit-law-right-div-Group (group-Ab G) x +``` + ### If `x + y = 0`, then `y = -x` ```agda diff --git a/src/group-theory/groups.lagda.md b/src/group-theory/groups.lagda.md index 85bfdc1f95..a51374aa9d 100644 --- a/src/group-theory/groups.lagda.md +++ b/src/group-theory/groups.lagda.md @@ -652,6 +652,23 @@ module _ is-injective-mul-Group G x (p ∙ inv (right-unit-law-mul-Group G x)) ``` +### Unit laws of division + +```agda +module _ + {l : Level} (G : Group l) (x : type-Group G) + where abstract + + right-unit-law-right-div-Group : + right-div-Group G x (unit-Group G) ＝ x + right-unit-law-right-div-Group = + ap-mul-Group G refl (inv-unit-Group G) ∙ right-unit-law-mul-Group G x + + left-unit-law-right-div-Group : + right-div-Group G (unit-Group G) x ＝ inv-Group G x + left-unit-law-right-div-Group = left-unit-law-mul-Group G _ +``` + ### Multiplication of a list of elements in a group ```agda diff --git a/src/group-theory/homomorphisms-abelian-groups.lagda.md b/src/group-theory/homomorphisms-abelian-groups.lagda.md index 43fa154acc..ff48c6e169 100644 --- a/src/group-theory/homomorphisms-abelian-groups.lagda.md +++ b/src/group-theory/homomorphisms-abelian-groups.lagda.md @@ -195,3 +195,21 @@ right-unit-law-comp-hom-Ab : right-unit-law-comp-hom-Ab A B = right-unit-law-comp-hom-Semigroup (semigroup-Ab A) (semigroup-Ab B) ``` + +### Abelian group homomorphisms preserve subtraction + +```agda +module _ + {l1 l2 : Level} + (G : Ab l1) + (H : Ab l2) + (φ : hom-Ab G H) + where abstract + + preserves-right-subtraction-hom-Ab : + {x y : type-Ab G} → + map-hom-Ab G H φ (right-subtraction-Ab G x y) ＝ + right-subtraction-Ab H (map-hom-Ab G H φ x) (map-hom-Ab G H φ y) + preserves-right-subtraction-hom-Ab = + preserves-right-div-hom-Group (group-Ab G) (group-Ab H) φ +``` diff --git a/src/linear-algebra/left-modules-rings.lagda.md b/src/linear-algebra/left-modules-rings.lagda.md index b266313029..86bdf8c4a4 100644 --- a/src/linear-algebra/left-modules-rings.lagda.md +++ b/src/linear-algebra/left-modules-rings.lagda.md @@ -9,6 +9,7 @@ module linear-algebra.left-modules-rings where ```agda open import elementary-number-theory.ring-of-integers +open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types @@ -90,6 +91,16 @@ module _ (x y : type-left-module-Ring) → type-left-module-Ring add-left-module-Ring = add-Ab ab-left-module-Ring + ap-add-left-module-Ring : + {x x' : type-left-module-Ring} → x ＝ x' → + {y y' : type-left-module-Ring} → y ＝ y' → + add-left-module-Ring x y ＝ add-left-module-Ring x' y' + ap-add-left-module-Ring = ap-binary add-left-module-Ring + + diff-left-module-Ring : + (x y : type-left-module-Ring) → type-left-module-Ring + diff-left-module-Ring = right-subtraction-Ab ab-left-module-Ring + zero-left-module-Ring : type-left-module-Ring zero-left-module-Ring = zero-Ab ab-left-module-Ring @@ -207,6 +218,27 @@ module _ interchange-add-add-Ab (ab-left-module-Ring R M) ``` +### Interchange laws of addition and differences + +```agda +module _ + {l1 l2 : Level} + (R : Ring l1) + (M : left-module-Ring l2 R) + where abstract + + interchange-add-diff-left-module-Ring : + (x y z w : type-left-module-Ring R M) → + diff-left-module-Ring R M + ( add-left-module-Ring R M x y) + ( add-left-module-Ring R M z w) ＝ + add-left-module-Ring R M + ( diff-left-module-Ring R M x z) + ( diff-left-module-Ring R M y w) + interchange-add-diff-left-module-Ring = + interchange-add-right-subtraction-Ab (ab-left-module-Ring R M) +``` + ### Negation distributes over addition ```agda @@ -558,6 +590,53 @@ module _ left-module-hom-left-module-Ring R S h (left-module-ring-Ring S) ``` +### Left distributivity of scalar multiplication over differences + +```agda +module _ + {l1 l2 : Level} + (R : Ring l1) + (M : left-module-Ring l2 R) + where abstract + + left-distributive-mul-diff-left-module-Ring : + (r : type-Ring R) (x y : type-left-module-Ring R M) → + mul-left-module-Ring R M r (diff-left-module-Ring R M x y) ＝ + diff-left-module-Ring R M + ( mul-left-module-Ring R M r x) + ( mul-left-module-Ring R M r y) + left-distributive-mul-diff-left-module-Ring r x y = + ( left-distributive-mul-add-left-module-Ring R M + ( r) + ( x) + ( neg-left-module-Ring R M y)) ∙ + ( ap-add-left-module-Ring R M + ( refl) + ( right-negative-law-mul-left-module-Ring R M r y)) +``` + +### Right distributivity of scalar multiplication over differences + +```agda +module _ + {l1 l2 : Level} + (R : Ring l1) + (M : left-module-Ring l2 R) + where abstract + + right-distributive-mul-diff-left-module-Ring : + (r s : type-Ring R) (x : type-left-module-Ring R M) → + mul-left-module-Ring R M (diff-Ring R r s) x ＝ + diff-left-module-Ring R M + ( mul-left-module-Ring R M r x) + ( mul-left-module-Ring R M s x) + right-distributive-mul-diff-left-module-Ring r s x = + ( right-distributive-mul-add-left-module-Ring R M r (neg-Ring R s) x) ∙ + ( ap-add-left-module-Ring R M + ( refl) + ( left-negative-law-mul-left-module-Ring R M s x)) +``` + ## See also - [Left modules over commutative rings](linear-algebra.left-modules-commutative-rings.md) diff --git a/src/linear-algebra/normed-real-vector-spaces.lagda.md b/src/linear-algebra/normed-real-vector-spaces.lagda.md index 53a58db9b7..6110465fb0 100644 --- a/src/linear-algebra/normed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md @@ -9,9 +9,13 @@ module linear-algebra.normed-real-vector-spaces where
Imports ```agda +open import elementary-number-theory.positive-rational-numbers + open import foundation.action-on-identifications-functions +open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.dependent-products-propositions +open import foundation.function-extensionality open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions @@ -25,23 +29,33 @@ open import group-theory.abelian-groups open import linear-algebra.real-vector-spaces open import linear-algebra.seminormed-real-vector-spaces +open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.equality-of-metric-spaces open import metric-spaces.isometries-metric-spaces +open import metric-spaces.lipschitz-maps-metric-spaces open import metric-spaces.located-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.metrics open import metric-spaces.metrics-of-metric-spaces +open import metric-spaces.metrics-of-metric-spaces-are-uniformly-continuous +open import metric-spaces.rational-neighborhood-relations +open import metric-spaces.subspaces-metric-spaces +open import metric-spaces.uniformly-continuous-maps-metric-spaces + +open import order-theory.large-posets open import real-numbers.absolute-value-real-numbers 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.distance-real-numbers open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-nonnegative-real-numbers open import real-numbers.metric-space-of-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.negation-real-numbers open import real-numbers.nonnegative-real-numbers -open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.saturation-inequality-nonnegative-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.zero-real-numbers ``` @@ -126,140 +140,299 @@ module _ type-Normed-ℝ-Vector-Space : UU l2 type-Normed-ℝ-Vector-Space = type-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space +``` - add-Normed-ℝ-Vector-Space : - type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space → - type-Normed-ℝ-Vector-Space - add-Normed-ℝ-Vector-Space = - add-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space +### Properties inherited from the abelian group structure on addition - commutative-add-Normed-ℝ-Vector-Space : - (u v : type-Normed-ℝ-Vector-Space) → - add-Normed-ℝ-Vector-Space u v ＝ add-Normed-ℝ-Vector-Space v u - commutative-add-Normed-ℝ-Vector-Space = - commutative-add-Ab ab-Normed-ℝ-Vector-Space +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (let ab-V = ab-Normed-ℝ-Vector-Space V) + where + + add-Normed-ℝ-Vector-Space : + type-Normed-ℝ-Vector-Space V → type-Normed-ℝ-Vector-Space V → + type-Normed-ℝ-Vector-Space V + add-Normed-ℝ-Vector-Space = add-Ab ab-V diff-Normed-ℝ-Vector-Space : - type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space → - type-Normed-ℝ-Vector-Space - diff-Normed-ℝ-Vector-Space = - diff-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space + type-Normed-ℝ-Vector-Space V → type-Normed-ℝ-Vector-Space V → + type-Normed-ℝ-Vector-Space V + diff-Normed-ℝ-Vector-Space = right-subtraction-Ab ab-V neg-Normed-ℝ-Vector-Space : - type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space - neg-Normed-ℝ-Vector-Space = - neg-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space - - neg-neg-Normed-ℝ-Vector-Space : - (v : type-Normed-ℝ-Vector-Space) → - neg-Normed-ℝ-Vector-Space (neg-Normed-ℝ-Vector-Space v) ＝ v - neg-neg-Normed-ℝ-Vector-Space = - neg-neg-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space - - distributive-neg-add-Normed-ℝ-Vector-Space : - (v w : type-Normed-ℝ-Vector-Space) → - neg-Normed-ℝ-Vector-Space (add-Normed-ℝ-Vector-Space v w) ＝ - add-Normed-ℝ-Vector-Space - ( neg-Normed-ℝ-Vector-Space v) - ( neg-Normed-ℝ-Vector-Space w) - distributive-neg-add-Normed-ℝ-Vector-Space = - distributive-neg-add-Ab ab-Normed-ℝ-Vector-Space - - interchange-add-add-Normed-ℝ-Vector-Space : - (u v w x : type-Normed-ℝ-Vector-Space) → - add-Normed-ℝ-Vector-Space - ( add-Normed-ℝ-Vector-Space u v) - ( add-Normed-ℝ-Vector-Space w x) ＝ - add-Normed-ℝ-Vector-Space - ( add-Normed-ℝ-Vector-Space u w) - ( add-Normed-ℝ-Vector-Space v x) - interchange-add-add-Normed-ℝ-Vector-Space = - interchange-add-add-Ab ab-Normed-ℝ-Vector-Space - - zero-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space - zero-Normed-ℝ-Vector-Space = - zero-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space - - left-unit-law-add-Normed-ℝ-Vector-Space : - (v : type-Normed-ℝ-Vector-Space) → - add-Normed-ℝ-Vector-Space zero-Normed-ℝ-Vector-Space v ＝ v - left-unit-law-add-Normed-ℝ-Vector-Space = - left-unit-law-add-Ab ab-Normed-ℝ-Vector-Space - - right-inverse-law-add-Normed-ℝ-Vector-Space : - (v : type-Normed-ℝ-Vector-Space) → - diff-Normed-ℝ-Vector-Space v v ＝ zero-Normed-ℝ-Vector-Space - right-inverse-law-add-Normed-ℝ-Vector-Space = - right-inverse-law-add-Ab ab-Normed-ℝ-Vector-Space - - map-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → ℝ l1 - map-norm-Normed-ℝ-Vector-Space = pr1 (pr1 norm-Normed-ℝ-Vector-Space) - - nonnegative-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space → ℝ⁰⁺ l1 + type-Normed-ℝ-Vector-Space V → type-Normed-ℝ-Vector-Space V + neg-Normed-ℝ-Vector-Space = neg-Ab ab-V + + zero-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space V + zero-Normed-ℝ-Vector-Space = zero-Ab ab-V + + is-zero-prop-Normed-ℝ-Vector-Space : subtype l2 (type-Normed-ℝ-Vector-Space V) + is-zero-prop-Normed-ℝ-Vector-Space = is-zero-prop-Ab ab-V + + is-zero-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space V → UU l2 + is-zero-Normed-ℝ-Vector-Space = is-zero-Ab ab-V + + abstract + associative-add-Normed-ℝ-Vector-Space : + (u v w : type-Normed-ℝ-Vector-Space V) → + add-Normed-ℝ-Vector-Space + ( add-Normed-ℝ-Vector-Space u v) + ( w) ＝ + add-Normed-ℝ-Vector-Space + ( u) + ( add-Normed-ℝ-Vector-Space v w) + associative-add-Normed-ℝ-Vector-Space = associative-add-Ab ab-V + + left-unit-law-add-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + add-Normed-ℝ-Vector-Space zero-Normed-ℝ-Vector-Space v ＝ v + left-unit-law-add-Normed-ℝ-Vector-Space = left-unit-law-add-Ab ab-V + + right-unit-law-add-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + add-Normed-ℝ-Vector-Space v zero-Normed-ℝ-Vector-Space ＝ v + right-unit-law-add-Normed-ℝ-Vector-Space = right-unit-law-add-Ab ab-V + + left-inverse-law-add-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + add-Normed-ℝ-Vector-Space (neg-Normed-ℝ-Vector-Space v) v ＝ + zero-Normed-ℝ-Vector-Space + left-inverse-law-add-Normed-ℝ-Vector-Space = + left-inverse-law-add-Ab ab-V + + right-inverse-law-add-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + diff-Normed-ℝ-Vector-Space v v ＝ zero-Normed-ℝ-Vector-Space + right-inverse-law-add-Normed-ℝ-Vector-Space = + right-inverse-law-add-Ab ab-V + + commutative-add-Normed-ℝ-Vector-Space : + (u v : type-Normed-ℝ-Vector-Space V) → + add-Normed-ℝ-Vector-Space u v ＝ add-Normed-ℝ-Vector-Space v u + commutative-add-Normed-ℝ-Vector-Space = commutative-add-Ab ab-V + + neg-neg-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + neg-Normed-ℝ-Vector-Space (neg-Normed-ℝ-Vector-Space v) ＝ v + neg-neg-Normed-ℝ-Vector-Space = neg-neg-Ab ab-V + + distributive-neg-add-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space V) → + neg-Normed-ℝ-Vector-Space (add-Normed-ℝ-Vector-Space v w) ＝ + add-Normed-ℝ-Vector-Space + ( neg-Normed-ℝ-Vector-Space v) + ( neg-Normed-ℝ-Vector-Space w) + distributive-neg-add-Normed-ℝ-Vector-Space = distributive-neg-add-Ab ab-V + + interchange-add-add-Normed-ℝ-Vector-Space : + (u v w x : type-Normed-ℝ-Vector-Space V) → + add-Normed-ℝ-Vector-Space + ( add-Normed-ℝ-Vector-Space u v) + ( add-Normed-ℝ-Vector-Space w x) ＝ + add-Normed-ℝ-Vector-Space + ( add-Normed-ℝ-Vector-Space u w) + ( add-Normed-ℝ-Vector-Space v x) + interchange-add-add-Normed-ℝ-Vector-Space = + interchange-add-add-Ab ab-V + + eq-is-zero-diff-Normed-ℝ-Vector-Space : + {u v : type-Normed-ℝ-Vector-Space V} → + is-zero-Normed-ℝ-Vector-Space (diff-Normed-ℝ-Vector-Space u v) → + u ＝ v + eq-is-zero-diff-Normed-ℝ-Vector-Space = + eq-is-zero-right-subtraction-Ab ab-V + + interchange-add-diff-Normed-ℝ-Vector-Space : + (x y z w : type-Normed-ℝ-Vector-Space V) → + diff-Normed-ℝ-Vector-Space + ( add-Normed-ℝ-Vector-Space x y) + ( add-Normed-ℝ-Vector-Space z w) ＝ + add-Normed-ℝ-Vector-Space + ( diff-Normed-ℝ-Vector-Space x z) + ( diff-Normed-ℝ-Vector-Space y w) + interchange-add-diff-Normed-ℝ-Vector-Space = + interchange-add-right-subtraction-Ab ab-V +``` + +### Properties inherited from the vector space structure + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (let vector-space-V = vector-space-Normed-ℝ-Vector-Space V) + where + + mul-Normed-ℝ-Vector-Space : + ℝ l1 → type-Normed-ℝ-Vector-Space V → type-Normed-ℝ-Vector-Space V + mul-Normed-ℝ-Vector-Space = mul-ℝ-Vector-Space vector-space-V + + abstract + left-distributive-mul-add-Normed-ℝ-Vector-Space : + (c : ℝ l1) (v w : type-Normed-ℝ-Vector-Space V) → + mul-Normed-ℝ-Vector-Space c (add-Normed-ℝ-Vector-Space V v w) ＝ + add-Normed-ℝ-Vector-Space V + ( mul-Normed-ℝ-Vector-Space c v) + ( mul-Normed-ℝ-Vector-Space c w) + left-distributive-mul-add-Normed-ℝ-Vector-Space = + left-distributive-mul-add-ℝ-Vector-Space vector-space-V + + left-distributive-mul-diff-Normed-ℝ-Vector-Space : + (c : ℝ l1) (v w : type-Normed-ℝ-Vector-Space V) → + mul-Normed-ℝ-Vector-Space c (diff-Normed-ℝ-Vector-Space V v w) ＝ + diff-Normed-ℝ-Vector-Space V + ( mul-Normed-ℝ-Vector-Space c v) + ( mul-Normed-ℝ-Vector-Space c w) + left-distributive-mul-diff-Normed-ℝ-Vector-Space = + left-distributive-mul-diff-ℝ-Vector-Space vector-space-V + + right-distributive-mul-add-Normed-ℝ-Vector-Space : + (c d : ℝ l1) (v : type-Normed-ℝ-Vector-Space V) → + mul-Normed-ℝ-Vector-Space (c +ℝ d) v ＝ + add-Normed-ℝ-Vector-Space V + ( mul-Normed-ℝ-Vector-Space c v) + ( mul-Normed-ℝ-Vector-Space d v) + right-distributive-mul-add-Normed-ℝ-Vector-Space = + right-distributive-mul-add-ℝ-Vector-Space vector-space-V + + right-distributive-mul-diff-Normed-ℝ-Vector-Space : + (c d : ℝ l1) (v : type-Normed-ℝ-Vector-Space V) → + mul-Normed-ℝ-Vector-Space (c -ℝ d) v ＝ + diff-Normed-ℝ-Vector-Space V + ( mul-Normed-ℝ-Vector-Space c v) + ( mul-Normed-ℝ-Vector-Space d v) + right-distributive-mul-diff-Normed-ℝ-Vector-Space = + right-distributive-mul-diff-ℝ-Vector-Space vector-space-V + + associative-mul-Normed-ℝ-Vector-Space : + (c d : ℝ l1) (v : type-Normed-ℝ-Vector-Space V) → + mul-Normed-ℝ-Vector-Space (c *ℝ d) v ＝ + mul-Normed-ℝ-Vector-Space c (mul-Normed-ℝ-Vector-Space d v) + associative-mul-Normed-ℝ-Vector-Space = + associative-mul-ℝ-Vector-Space vector-space-V + + left-unit-law-mul-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + mul-Normed-ℝ-Vector-Space (raise-one-ℝ l1) v ＝ v + left-unit-law-mul-Normed-ℝ-Vector-Space = + left-unit-law-mul-ℝ-Vector-Space vector-space-V + + left-negative-law-mul-Normed-ℝ-Vector-Space : + (c : ℝ l1) (v : type-Normed-ℝ-Vector-Space V) → + mul-Normed-ℝ-Vector-Space (neg-ℝ c) v ＝ + neg-Normed-ℝ-Vector-Space V (mul-Normed-ℝ-Vector-Space c v) + left-negative-law-mul-Normed-ℝ-Vector-Space = + left-negative-law-mul-ℝ-Vector-Space vector-space-V +``` + +### Norms and distances in a normed vector space + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (let seminormed-V = seminormed-vector-space-Normed-ℝ-Vector-Space V) + where + + map-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space V → ℝ l1 + map-norm-Normed-ℝ-Vector-Space = pr1 (pr1 (norm-Normed-ℝ-Vector-Space V)) + + nonnegative-norm-Normed-ℝ-Vector-Space : type-Normed-ℝ-Vector-Space V → ℝ⁰⁺ l1 nonnegative-norm-Normed-ℝ-Vector-Space = - nonnegative-seminorm-Seminormed-ℝ-Vector-Space - ( seminormed-vector-space-Normed-ℝ-Vector-Space) + nonnegative-seminorm-Seminormed-ℝ-Vector-Space seminormed-V dist-Normed-ℝ-Vector-Space : - type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space → ℝ l1 - dist-Normed-ℝ-Vector-Space = - dist-Seminormed-ℝ-Vector-Space seminormed-vector-space-Normed-ℝ-Vector-Space + type-Normed-ℝ-Vector-Space V → type-Normed-ℝ-Vector-Space V → ℝ l1 + dist-Normed-ℝ-Vector-Space = dist-Seminormed-ℝ-Vector-Space seminormed-V nonnegative-dist-Normed-ℝ-Vector-Space : - type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space → ℝ⁰⁺ l1 + type-Normed-ℝ-Vector-Space V → type-Normed-ℝ-Vector-Space V → ℝ⁰⁺ l1 nonnegative-dist-Normed-ℝ-Vector-Space = - nonnegative-dist-Seminormed-ℝ-Vector-Space - ( seminormed-vector-space-Normed-ℝ-Vector-Space) + nonnegative-dist-Seminormed-ℝ-Vector-Space seminormed-V + + is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space : + (c : ℝ l1) (v : type-Normed-ℝ-Vector-Space V) → + map-norm-Normed-ℝ-Vector-Space (mul-Normed-ℝ-Vector-Space V c v) ＝ + abs-ℝ c *ℝ map-norm-Normed-ℝ-Vector-Space v + is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space = + is-absolutely-homogeneous-seminorm-Seminormed-ℝ-Vector-Space seminormed-V + + right-zero-law-dist-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + dist-Normed-ℝ-Vector-Space v (zero-Normed-ℝ-Vector-Space V) ＝ + map-norm-Normed-ℝ-Vector-Space v + right-zero-law-dist-Normed-ℝ-Vector-Space = + right-zero-law-dist-Seminormed-ℝ-Vector-Space seminormed-V +``` - abstract - is-extensional-norm-Normed-ℝ-Vector-Space : - (v : type-Normed-ℝ-Vector-Space) → - is-zero-ℝ (map-norm-Normed-ℝ-Vector-Space v) → - v ＝ zero-Normed-ℝ-Vector-Space - is-extensional-norm-Normed-ℝ-Vector-Space = pr2 norm-Normed-ℝ-Vector-Space - - is-extensional-dist-Normed-ℝ-Vector-Space : - (v w : type-Normed-ℝ-Vector-Space) → - is-zero-ℝ (dist-Normed-ℝ-Vector-Space v w) → - v ＝ w - is-extensional-dist-Normed-ℝ-Vector-Space v w |v-w|=0 = - eq-is-zero-right-subtraction-Ab - ( ab-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space) - ( is-extensional-norm-Normed-ℝ-Vector-Space - ( diff-Normed-ℝ-Vector-Space v w) - ( |v-w|=0)) - - refl-dist-Normed-ℝ-Vector-Space : - (v : type-Normed-ℝ-Vector-Space) → - is-zero-ℝ (dist-Normed-ℝ-Vector-Space v v) - refl-dist-Normed-ℝ-Vector-Space = - is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space - ( seminormed-vector-space-Normed-ℝ-Vector-Space) - - symmetric-dist-Normed-ℝ-Vector-Space : - (v w : type-Normed-ℝ-Vector-Space) → - dist-Normed-ℝ-Vector-Space v w ＝ dist-Normed-ℝ-Vector-Space w v - symmetric-dist-Normed-ℝ-Vector-Space = - symmetric-dist-Seminormed-ℝ-Vector-Space - ( seminormed-vector-space-Normed-ℝ-Vector-Space) - - triangular-norm-Normed-ℝ-Vector-Space : - (v w : type-Normed-ℝ-Vector-Space) → - leq-ℝ - ( map-norm-Normed-ℝ-Vector-Space (add-Normed-ℝ-Vector-Space v w)) - ( map-norm-Normed-ℝ-Vector-Space v +ℝ map-norm-Normed-ℝ-Vector-Space w) - triangular-norm-Normed-ℝ-Vector-Space = - triangular-seminorm-Seminormed-ℝ-Vector-Space - ( seminormed-vector-space-Normed-ℝ-Vector-Space) - - triangular-dist-Normed-ℝ-Vector-Space : - (u v w : type-Normed-ℝ-Vector-Space) → - leq-ℝ - ( dist-Normed-ℝ-Vector-Space u w) - ( dist-Normed-ℝ-Vector-Space u v +ℝ dist-Normed-ℝ-Vector-Space v w) - triangular-dist-Normed-ℝ-Vector-Space = - triangular-dist-Seminormed-ℝ-Vector-Space - ( seminormed-vector-space-Normed-ℝ-Vector-Space) +### The distance function in a normed vector space satisfies the properties of a metric + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + is-extensional-norm-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + is-zero-ℝ (map-norm-Normed-ℝ-Vector-Space V v) → + v ＝ zero-Normed-ℝ-Vector-Space V + is-extensional-norm-Normed-ℝ-Vector-Space = pr2 (norm-Normed-ℝ-Vector-Space V) + + is-extensional-dist-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space V) → + is-zero-ℝ (dist-Normed-ℝ-Vector-Space V v w) → + v ＝ w + is-extensional-dist-Normed-ℝ-Vector-Space v w |v-w|=0 = + eq-is-zero-diff-Normed-ℝ-Vector-Space V + ( is-extensional-norm-Normed-ℝ-Vector-Space + ( diff-Normed-ℝ-Vector-Space V v w) + ( |v-w|=0)) + + refl-dist-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + is-zero-ℝ (dist-Normed-ℝ-Vector-Space V v v) + refl-dist-Normed-ℝ-Vector-Space = + is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) + + symmetric-dist-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space V) → + dist-Normed-ℝ-Vector-Space V v w ＝ dist-Normed-ℝ-Vector-Space V w v + symmetric-dist-Normed-ℝ-Vector-Space = + symmetric-dist-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) + + triangular-norm-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space V) → + leq-ℝ + ( map-norm-Normed-ℝ-Vector-Space V (add-Normed-ℝ-Vector-Space V v w)) + ( map-norm-Normed-ℝ-Vector-Space V v +ℝ + map-norm-Normed-ℝ-Vector-Space V w) + triangular-norm-Normed-ℝ-Vector-Space = + triangular-seminorm-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) + + triangular-dist-Normed-ℝ-Vector-Space : + (u v w : type-Normed-ℝ-Vector-Space V) → + leq-ℝ + ( dist-Normed-ℝ-Vector-Space V u w) + ( dist-Normed-ℝ-Vector-Space V u v +ℝ dist-Normed-ℝ-Vector-Space V v w) + triangular-dist-Normed-ℝ-Vector-Space = + triangular-dist-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) + + is-metric-dist-Normed-ℝ-Vector-Space : + is-metric-distance-function + ( set-Normed-ℝ-Vector-Space V) + ( nonnegative-dist-Normed-ℝ-Vector-Space V) + is-metric-dist-Normed-ℝ-Vector-Space = + ( refl-dist-Normed-ℝ-Vector-Space , + ( λ v w → eq-ℝ⁰⁺ _ _ (symmetric-dist-Normed-ℝ-Vector-Space v w)) , + triangular-dist-Normed-ℝ-Vector-Space , + is-extensional-dist-Normed-ℝ-Vector-Space) ``` ### The metric space of a normed vector space @@ -269,21 +442,10 @@ module _ {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) where - abstract - is-metric-dist-Normed-ℝ-Vector-Space : - is-metric-distance-function - ( set-Normed-ℝ-Vector-Space V) - ( nonnegative-dist-Normed-ℝ-Vector-Space V) - is-metric-dist-Normed-ℝ-Vector-Space = - ( refl-dist-Normed-ℝ-Vector-Space V , - ( λ v w → eq-ℝ⁰⁺ _ _ (symmetric-dist-Normed-ℝ-Vector-Space V v w)) , - triangular-dist-Normed-ℝ-Vector-Space V , - is-extensional-dist-Normed-ℝ-Vector-Space V) - metric-Normed-ℝ-Vector-Space : Metric l1 (set-Normed-ℝ-Vector-Space V) metric-Normed-ℝ-Vector-Space = ( nonnegative-dist-Normed-ℝ-Vector-Space V , - is-metric-dist-Normed-ℝ-Vector-Space) + is-metric-dist-Normed-ℝ-Vector-Space V) metric-space-Normed-ℝ-Vector-Space : Metric-Space l2 l1 metric-space-Normed-ℝ-Vector-Space = @@ -296,28 +458,16 @@ module _ located-metric-space-Metric ( set-Normed-ℝ-Vector-Space V) ( metric-Normed-ℝ-Vector-Space) -``` -## Properties + neighborhood-prop-Normed-ℝ-Vector-Space : + Rational-Neighborhood-Relation l1 (type-Normed-ℝ-Vector-Space V) + neighborhood-prop-Normed-ℝ-Vector-Space = + neighborhood-prop-Metric-Space metric-space-Normed-ℝ-Vector-Space -### The real numbers are a normed vector space over themselves with norm `x ↦ |x|` - -```agda -normed-real-vector-space-ℝ : - (l : Level) → Normed-ℝ-Vector-Space l (lsuc l) -normed-real-vector-space-ℝ l = - ( real-vector-space-ℝ l , - ( abs-ℝ , triangle-inequality-abs-ℝ , abs-mul-ℝ) , - λ x |x|~0 → eq-raise-zero-is-zero-ℝ (is-zero-is-zero-abs-ℝ x |x|~0)) - -abstract - eq-metric-space-normed-real-vector-space-metric-space-ℝ : - (l : Level) → - metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l) ＝ - metric-space-ℝ l - eq-metric-space-normed-real-vector-space-metric-space-ℝ l = - eq-isometric-eq-Metric-Space _ _ - ( refl , λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y)) + neighborhood-Normed-ℝ-Vector-Space : + ℚ⁺ → Relation l1 (type-Normed-ℝ-Vector-Space V) + neighborhood-Normed-ℝ-Vector-Space = + neighborhood-Metric-Space metric-space-Normed-ℝ-Vector-Space ``` ### Negation is an isometry in the metric space of a normed vector space @@ -325,44 +475,49 @@ abstract ```agda module _ {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) - where - - abstract - is-isometry-neg-Normed-ℝ-Vector-Space : - is-isometry-Metric-Space - ( metric-space-Normed-ℝ-Vector-Space V) - ( metric-space-Normed-ℝ-Vector-Space V) - ( neg-Normed-ℝ-Vector-Space V) - is-isometry-neg-Normed-ℝ-Vector-Space = - is-isometry-sim-metric-Metric-Space - ( metric-space-Normed-ℝ-Vector-Space V) - ( metric-space-Normed-ℝ-Vector-Space V) - ( nonnegative-dist-Normed-ℝ-Vector-Space V) - ( nonnegative-dist-Normed-ℝ-Vector-Space V) - ( is-metric-metric-space-Metric - ( set-Normed-ℝ-Vector-Space V) - ( metric-Normed-ℝ-Vector-Space V)) - ( is-metric-metric-space-Metric - ( set-Normed-ℝ-Vector-Space V) - ( metric-Normed-ℝ-Vector-Space V)) - ( neg-Normed-ℝ-Vector-Space V) - ( λ x y → - sim-eq-ℝ - ( inv - ( equational-reasoning - dist-Normed-ℝ-Vector-Space V - ( neg-Normed-ℝ-Vector-Space V x) - ( neg-Normed-ℝ-Vector-Space V y) - ＝ dist-Normed-ℝ-Vector-Space V y x - by - ap - ( map-norm-Normed-ℝ-Vector-Space V) - ( right-subtraction-neg-Ab - ( ab-Normed-ℝ-Vector-Space V) - ( _) - ( _)) - ＝ dist-Normed-ℝ-Vector-Space V x y - by symmetric-dist-Normed-ℝ-Vector-Space V y x))) + where abstract + + dist-neg-Normed-ℝ-Vector-Space : + (x y : type-Normed-ℝ-Vector-Space V) → + dist-Normed-ℝ-Vector-Space V + ( neg-Normed-ℝ-Vector-Space V x) + ( neg-Normed-ℝ-Vector-Space V y) ＝ + dist-Normed-ℝ-Vector-Space V x y + dist-neg-Normed-ℝ-Vector-Space x y = + equational-reasoning + dist-Normed-ℝ-Vector-Space V + ( neg-Normed-ℝ-Vector-Space V x) + ( neg-Normed-ℝ-Vector-Space V y) + ＝ dist-Normed-ℝ-Vector-Space V y x + by + ap + ( map-norm-Normed-ℝ-Vector-Space V) + ( right-subtraction-neg-Ab + ( ab-Normed-ℝ-Vector-Space V) + ( _) + ( _)) + ＝ dist-Normed-ℝ-Vector-Space V x y + by symmetric-dist-Normed-ℝ-Vector-Space V y x + + is-isometry-neg-Normed-ℝ-Vector-Space : + is-isometry-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V) + ( neg-Normed-ℝ-Vector-Space V) + is-isometry-neg-Normed-ℝ-Vector-Space = + is-isometry-sim-metric-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V) + ( nonnegative-dist-Normed-ℝ-Vector-Space V) + ( nonnegative-dist-Normed-ℝ-Vector-Space V) + ( is-metric-metric-space-Metric + ( set-Normed-ℝ-Vector-Space V) + ( metric-Normed-ℝ-Vector-Space V)) + ( is-metric-metric-space-Metric + ( set-Normed-ℝ-Vector-Space V) + ( metric-Normed-ℝ-Vector-Space V)) + ( neg-Normed-ℝ-Vector-Space V) + ( λ x y → sim-eq-ℝ (inv (dist-neg-Normed-ℝ-Vector-Space x y))) ``` ### Left addition is an isometry in the metric space of a normed vector space @@ -407,6 +562,85 @@ module _ ### The norm of the zero vector is zero +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + norm-zero-Normed-ℝ-Vector-Space : + map-norm-Normed-ℝ-Vector-Space V (zero-Normed-ℝ-Vector-Space V) ＝ + raise-zero-ℝ l1 + norm-zero-Normed-ℝ-Vector-Space = + seminorm-zero-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) +``` + +### The distance between `cv` and `cw` is `|c|` times the distance between `v` and `w` + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (c : ℝ l1) + (v w : type-Normed-ℝ-Vector-Space V) + where abstract + + multiplicative-dist-Normed-ℝ-Vector-Space : + dist-Normed-ℝ-Vector-Space V + ( mul-Normed-ℝ-Vector-Space V c v) + ( mul-Normed-ℝ-Vector-Space V c w) ＝ + abs-ℝ c *ℝ dist-Normed-ℝ-Vector-Space V v w + multiplicative-dist-Normed-ℝ-Vector-Space = + ( ap + ( map-norm-Normed-ℝ-Vector-Space V) + ( inv (left-distributive-mul-diff-Normed-ℝ-Vector-Space V c v w))) ∙ + ( is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space V c _) +``` + +### The real numbers are a normed vector space over themselves with norm `x ↦ |x|` + +```agda +normed-real-vector-space-ℝ : + (l : Level) → Normed-ℝ-Vector-Space l (lsuc l) +normed-real-vector-space-ℝ l = + ( real-vector-space-ℝ l , + ( abs-ℝ , triangle-inequality-abs-ℝ , abs-mul-ℝ) , + λ x |x|~0 → eq-raise-zero-is-zero-ℝ (is-zero-is-zero-abs-ℝ x |x|~0)) + +abstract + eq-metric-space-normed-real-vector-space-metric-space-ℝ : + (l : Level) → + metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l) ＝ + metric-space-ℝ l + eq-metric-space-normed-real-vector-space-metric-space-ℝ l = + eq-isometric-eq-Metric-Space _ _ + ( refl , λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y)) +``` + +### The distance between `cx` and `cy` is `abs-ℝ c` times the distance between `x` and `y` + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where abstract + + left-distributive-abs-mul-dist-Normed-ℝ-Vector-Space : + (c : ℝ l1) (x y : type-Normed-ℝ-Vector-Space V) → + abs-ℝ c *ℝ dist-Normed-ℝ-Vector-Space V x y ＝ + dist-Normed-ℝ-Vector-Space V + ( mul-Normed-ℝ-Vector-Space V c x) + ( mul-Normed-ℝ-Vector-Space V c y) + left-distributive-abs-mul-dist-Normed-ℝ-Vector-Space c x y = + ( inv (is-absolutely-homogeneous-norm-Normed-ℝ-Vector-Space V c _)) ∙ + ( ap + ( map-norm-Normed-ℝ-Vector-Space V) + ( left-distributive-mul-diff-Normed-ℝ-Vector-Space V c x y)) +``` + +### The distance function is a uniformly continuous map from the product metric space to the nonnegative real numbers + ```agda module _ {l1 l2 : Level} @@ -414,12 +648,110 @@ module _ where abstract - eq-zero-norm-zero-Normed-ℝ-Vector-Space : - map-norm-Normed-ℝ-Vector-Space V (zero-Normed-ℝ-Vector-Space V) ＝ - raise-ℝ l1 zero-ℝ - eq-zero-norm-zero-Normed-ℝ-Vector-Space = - eq-zero-seminorm-zero-Seminormed-ℝ-Vector-Space - ( seminormed-vector-space-Normed-ℝ-Vector-Space V) + is-uniformly-continuous-map-nonnegative-dist-Normed-ℝ-Vector-Space : + is-uniformly-continuous-map-Metric-Space + ( product-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V)) + ( metric-space-ℝ⁰⁺ l1) + ( ind-Σ (nonnegative-dist-Normed-ℝ-Vector-Space V)) + is-uniformly-continuous-map-nonnegative-dist-Normed-ℝ-Vector-Space = + is-uniformly-continuous-map-metric-of-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( nonnegative-dist-Normed-ℝ-Vector-Space V) + ( is-metric-metric-space-Metric + ( set-Normed-ℝ-Vector-Space V) + ( metric-Normed-ℝ-Vector-Space V)) + + is-uniformly-continuous-map-nonnegative-norm-Normed-ℝ-Vector-Space : + is-uniformly-continuous-map-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-ℝ⁰⁺ l1) + ( nonnegative-norm-Normed-ℝ-Vector-Space V) + is-uniformly-continuous-map-nonnegative-norm-Normed-ℝ-Vector-Space = + tr + ( is-uniformly-continuous-map-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-ℝ⁰⁺ l1)) + ( eq-htpy + ( λ v → eq-ℝ⁰⁺ _ _ (right-zero-law-dist-Normed-ℝ-Vector-Space V v))) + ( is-uniformly-continuous-map-comp-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( product-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V)) + ( metric-space-ℝ⁰⁺ l1) + ( ind-Σ (nonnegative-dist-Normed-ℝ-Vector-Space V)) + ( _, zero-Normed-ℝ-Vector-Space V) + ( is-uniformly-continuous-map-nonnegative-dist-Normed-ℝ-Vector-Space) + ( is-uniformly-continuous-map-is-isometry-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( product-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V)) + ( _, zero-Normed-ℝ-Vector-Space V) + ( is-isometry-right-pair-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V) + ( zero-Normed-ℝ-Vector-Space V)))) + + uniformly-continuous-map-nonnegative-norm-Normed-ℝ-Vector-Space : + uniformly-continuous-map-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-ℝ⁰⁺ l1) + uniformly-continuous-map-nonnegative-norm-Normed-ℝ-Vector-Space = + ( nonnegative-norm-Normed-ℝ-Vector-Space V , + is-uniformly-continuous-map-nonnegative-norm-Normed-ℝ-Vector-Space) + + uniformly-continuous-map-norm-Normed-ℝ-Vector-Space : + uniformly-continuous-map-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-ℝ l1) + uniformly-continuous-map-norm-Normed-ℝ-Vector-Space = + comp-uniformly-continuous-map-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-ℝ⁰⁺ l1) + ( metric-space-ℝ l1) + ( uniformly-continuous-inclusion-subspace-Metric-Space + ( metric-space-ℝ l1) + ( is-nonnegative-prop-ℝ)) + ( uniformly-continuous-map-nonnegative-norm-Normed-ℝ-Vector-Space) +``` + +### For any `x y : V`, `∥x∥ ≤ ∥y∥ + ∥x - y∥` + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (x y : type-Normed-ℝ-Vector-Space V) + (let _+V_ = add-Normed-ℝ-Vector-Space V) + (let _-V_ = diff-Normed-ℝ-Vector-Space V) + where abstract + + open inequality-reasoning-Large-Poset ℝ-Large-Poset + + leq-norm-add-norm-dist-Normed-ℝ-Vector-Space : + leq-ℝ + ( map-norm-Normed-ℝ-Vector-Space V x) + ( map-norm-Normed-ℝ-Vector-Space V y +ℝ + dist-Normed-ℝ-Vector-Space V x y) + leq-norm-add-norm-dist-Normed-ℝ-Vector-Space = + chain-of-inequalities + map-norm-Normed-ℝ-Vector-Space V x + ≤ map-norm-Normed-ℝ-Vector-Space V (y +V (x -V y)) + by + leq-eq-ℝ + ( ap + ( map-norm-Normed-ℝ-Vector-Space V) + ( inv + ( is-identity-right-conjugation-Ab + ( ab-Normed-ℝ-Vector-Space V) + ( y) + ( x)))) + ≤ map-norm-Normed-ℝ-Vector-Space V y +ℝ + dist-Normed-ℝ-Vector-Space V x y + by triangular-norm-Normed-ℝ-Vector-Space V _ _ ``` ## See also diff --git a/src/linear-algebra/real-vector-spaces.lagda.md b/src/linear-algebra/real-vector-spaces.lagda.md index 526b466b41..2672295359 100644 --- a/src/linear-algebra/real-vector-spaces.lagda.md +++ b/src/linear-algebra/real-vector-spaces.lagda.md @@ -24,6 +24,7 @@ open import linear-algebra.vector-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.field-of-real-numbers open import real-numbers.multiplication-real-numbers open import real-numbers.negation-real-numbers @@ -84,8 +85,7 @@ module _ diff-ℝ-Vector-Space : type-ℝ-Vector-Space → type-ℝ-Vector-Space → type-ℝ-Vector-Space - diff-ℝ-Vector-Space v w = - add-ℝ-Vector-Space v (neg-ℝ-Vector-Space w) + diff-ℝ-Vector-Space = diff-Vector-Space (heyting-field-ℝ l1) V associative-add-ℝ-Vector-Space : (v w x : type-ℝ-Vector-Space) → @@ -128,6 +128,13 @@ module _ (v : type-ℝ-Vector-Space) → neg-ℝ-Vector-Space (neg-ℝ-Vector-Space v) ＝ v neg-neg-ℝ-Vector-Space = neg-neg-Ab ab-ℝ-Vector-Space + interchange-add-diff-ℝ-Vector-Space : + (x y z w : type-ℝ-Vector-Space) → + diff-ℝ-Vector-Space (add-ℝ-Vector-Space x y) (add-ℝ-Vector-Space z w) ＝ + add-ℝ-Vector-Space (diff-ℝ-Vector-Space x z) (diff-ℝ-Vector-Space y w) + interchange-add-diff-ℝ-Vector-Space = + interchange-add-diff-Vector-Space (heyting-field-ℝ l1) V + left-unit-law-mul-ℝ-Vector-Space : (v : type-ℝ-Vector-Space) → mul-ℝ-Vector-Space (raise-ℝ l1 one-ℝ) v ＝ v @@ -141,6 +148,13 @@ module _ left-distributive-mul-add-ℝ-Vector-Space = left-distributive-mul-add-Vector-Space (heyting-field-ℝ l1) V + left-distributive-mul-diff-ℝ-Vector-Space : + (r : ℝ l1) (v w : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space r (diff-ℝ-Vector-Space v w) ＝ + diff-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) (mul-ℝ-Vector-Space r w) + left-distributive-mul-diff-ℝ-Vector-Space = + left-distributive-mul-diff-Vector-Space (heyting-field-ℝ l1) V + right-distributive-mul-add-ℝ-Vector-Space : (r s : ℝ l1) (v : type-ℝ-Vector-Space) → mul-ℝ-Vector-Space (r +ℝ s) v ＝ @@ -148,6 +162,13 @@ module _ right-distributive-mul-add-ℝ-Vector-Space = right-distributive-mul-add-Vector-Space (heyting-field-ℝ l1) V + right-distributive-mul-diff-ℝ-Vector-Space : + (r s : ℝ l1) (v : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space (r -ℝ s) v ＝ + diff-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) (mul-ℝ-Vector-Space s v) + right-distributive-mul-diff-ℝ-Vector-Space = + right-distributive-mul-diff-Vector-Space (heyting-field-ℝ l1) V + associative-mul-ℝ-Vector-Space : (r s : ℝ l1) (v : type-ℝ-Vector-Space) → mul-ℝ-Vector-Space (r *ℝ s) v ＝ @@ -155,6 +176,13 @@ module _ associative-mul-ℝ-Vector-Space = associative-mul-Vector-Space (heyting-field-ℝ l1) V + left-swap-mul-ℝ-Vector-Space : + (r s : ℝ l1) (v : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space r (mul-ℝ-Vector-Space s v) ＝ + mul-ℝ-Vector-Space s (mul-ℝ-Vector-Space r v) + left-swap-mul-ℝ-Vector-Space = + left-swap-mul-Vector-Space (heyting-field-ℝ l1) V + left-zero-law-mul-ℝ-Vector-Space : (v : type-ℝ-Vector-Space) → mul-ℝ-Vector-Space (raise-ℝ l1 zero-ℝ) v ＝ zero-ℝ-Vector-Space diff --git a/src/linear-algebra/seminormed-real-vector-spaces.lagda.md b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md index 065ed1fba7..709623280c 100644 --- a/src/linear-algebra/seminormed-real-vector-spaces.lagda.md +++ b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md @@ -151,13 +151,15 @@ module _ vector-space-Seminormed-ℝ-Vector-Space : ℝ-Vector-Space l1 l2 vector-space-Seminormed-ℝ-Vector-Space = pr1 V + ab-Seminormed-ℝ-Vector-Space : Ab l2 + ab-Seminormed-ℝ-Vector-Space = + ab-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + set-Seminormed-ℝ-Vector-Space : Set l2 - set-Seminormed-ℝ-Vector-Space = - set-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + set-Seminormed-ℝ-Vector-Space = set-Ab ab-Seminormed-ℝ-Vector-Space type-Seminormed-ℝ-Vector-Space : UU l2 - type-Seminormed-ℝ-Vector-Space = - type-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + type-Seminormed-ℝ-Vector-Space = type-Ab ab-Seminormed-ℝ-Vector-Space seminorm-Seminormed-ℝ-Vector-Space : seminorm-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space @@ -169,23 +171,20 @@ module _ pr1 seminorm-Seminormed-ℝ-Vector-Space zero-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space - zero-Seminormed-ℝ-Vector-Space = - zero-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + zero-Seminormed-ℝ-Vector-Space = zero-Ab ab-Seminormed-ℝ-Vector-Space is-zero-prop-Seminormed-ℝ-Vector-Space : subtype l2 type-Seminormed-ℝ-Vector-Space is-zero-prop-Seminormed-ℝ-Vector-Space = - is-zero-prop-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + is-zero-prop-Ab ab-Seminormed-ℝ-Vector-Space is-zero-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space → UU l2 - is-zero-Seminormed-ℝ-Vector-Space = - is-zero-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + is-zero-Seminormed-ℝ-Vector-Space = is-zero-Ab ab-Seminormed-ℝ-Vector-Space add-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space - add-Seminormed-ℝ-Vector-Space = - add-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + add-Seminormed-ℝ-Vector-Space = add-Ab ab-Seminormed-ℝ-Vector-Space mul-Seminormed-ℝ-Vector-Space : ℝ l1 → type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space @@ -194,21 +193,20 @@ module _ neg-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space - neg-Seminormed-ℝ-Vector-Space = - neg-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + neg-Seminormed-ℝ-Vector-Space = neg-Ab ab-Seminormed-ℝ-Vector-Space diff-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space - diff-Seminormed-ℝ-Vector-Space v w = - add-Seminormed-ℝ-Vector-Space v (neg-Seminormed-ℝ-Vector-Space w) + diff-Seminormed-ℝ-Vector-Space = + right-subtraction-Ab ab-Seminormed-ℝ-Vector-Space right-inverse-law-add-Seminormed-ℝ-Vector-Space : (v : type-Seminormed-ℝ-Vector-Space) → add-Seminormed-ℝ-Vector-Space v (neg-Seminormed-ℝ-Vector-Space v) ＝ zero-Seminormed-ℝ-Vector-Space right-inverse-law-add-Seminormed-ℝ-Vector-Space = - right-inverse-law-add-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + right-inverse-law-add-Ab ab-Seminormed-ℝ-Vector-Space add-diff-Seminormed-ℝ-Vector-Space : (v w x : type-Seminormed-ℝ-Vector-Space) → @@ -223,7 +221,7 @@ module _ (v : type-Seminormed-ℝ-Vector-Space) → neg-Seminormed-ℝ-Vector-Space (neg-Seminormed-ℝ-Vector-Space v) ＝ v neg-neg-Seminormed-ℝ-Vector-Space = - neg-neg-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + neg-neg-Ab ab-Seminormed-ℝ-Vector-Space left-zero-law-mul-Seminormed-ℝ-Vector-Space : (v : type-Seminormed-ℝ-Vector-Space) → @@ -244,8 +242,7 @@ module _ neg-Seminormed-ℝ-Vector-Space (diff-Seminormed-ℝ-Vector-Space v w) ＝ diff-Seminormed-ℝ-Vector-Space w v distributive-neg-diff-Seminormed-ℝ-Vector-Space = - neg-right-subtraction-Ab - ( ab-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space) + neg-right-subtraction-Ab ab-Seminormed-ℝ-Vector-Space triangular-seminorm-Seminormed-ℝ-Vector-Space : (v w : type-Seminormed-ℝ-Vector-Space) → @@ -281,12 +278,12 @@ module _ where abstract - eq-zero-seminorm-zero-Seminormed-ℝ-Vector-Space : + seminorm-zero-Seminormed-ℝ-Vector-Space : map-seminorm-Seminormed-ℝ-Vector-Space ( V) ( zero-Seminormed-ℝ-Vector-Space V) ＝ raise-ℝ l1 zero-ℝ - eq-zero-seminorm-zero-Seminormed-ℝ-Vector-Space = + seminorm-zero-Seminormed-ℝ-Vector-Space = equational-reasoning map-seminorm-Seminormed-ℝ-Vector-Space ( V) @@ -330,7 +327,7 @@ module _ ( ap ( map-seminorm-Seminormed-ℝ-Vector-Space V) ( right-inverse-law-add-Seminormed-ℝ-Vector-Space V v)) ∙ - ( eq-zero-seminorm-zero-Seminormed-ℝ-Vector-Space) + ( seminorm-zero-Seminormed-ℝ-Vector-Space) is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space : (v : type-Seminormed-ℝ-Vector-Space V) → @@ -586,6 +583,23 @@ module _ pseudometric-structure-Seminormed-ℝ-Vector-Space) ``` +### Zero laws of distance in a seminormed vector space + +```agda +module _ + {l1 l2 : Level} (V : Seminormed-ℝ-Vector-Space l1 l2) + where abstract + + right-zero-law-dist-Seminormed-ℝ-Vector-Space : + (x : type-Seminormed-ℝ-Vector-Space V) → + dist-Seminormed-ℝ-Vector-Space V x (zero-Seminormed-ℝ-Vector-Space V) ＝ + map-seminorm-Seminormed-ℝ-Vector-Space V x + right-zero-law-dist-Seminormed-ℝ-Vector-Space x = + ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( right-zero-law-right-subtraction-Ab (ab-Seminormed-ℝ-Vector-Space V) x) +``` + ### The real numbers are a seminormed vector space over themselves with seminorm `x ↦ |x|` ```agda diff --git a/src/linear-algebra/vector-spaces.lagda.md b/src/linear-algebra/vector-spaces.lagda.md index f12b24dc0f..b018a99616 100644 --- a/src/linear-algebra/vector-spaces.lagda.md +++ b/src/linear-algebra/vector-spaces.lagda.md @@ -18,6 +18,7 @@ open import foundation.universe-levels open import group-theory.abelian-groups open import linear-algebra.left-modules-commutative-rings +open import linear-algebra.left-modules-rings ```
@@ -59,6 +60,9 @@ module _ add-Vector-Space : type-Vector-Space → type-Vector-Space → type-Vector-Space add-Vector-Space = add-Ab ab-Vector-Space + diff-Vector-Space : type-Vector-Space → type-Vector-Space → type-Vector-Space + diff-Vector-Space = right-subtraction-Ab ab-Vector-Space + zero-Vector-Space : type-Vector-Space zero-Vector-Space = zero-Ab ab-Vector-Space @@ -106,6 +110,13 @@ module _ (v w : type-Vector-Space) → add-Vector-Space v w ＝ add-Vector-Space w v commutative-add-Vector-Space = commutative-add-Ab ab-Vector-Space + interchange-add-diff-Vector-Space : + (x y z w : type-Vector-Space) → + diff-Vector-Space (add-Vector-Space x y) (add-Vector-Space z w) ＝ + add-Vector-Space (diff-Vector-Space x z) (diff-Vector-Space y w) + interchange-add-diff-Vector-Space = + interchange-add-diff-left-module-Ring (ring-Heyting-Field R) V + left-unit-law-mul-Vector-Space : (v : type-Vector-Space) → mul-Vector-Space (one-Heyting-Field R) v ＝ v @@ -123,6 +134,15 @@ module _ ( commutative-ring-Heyting-Field R) ( V) + left-distributive-mul-diff-Vector-Space : + (r : type-Heyting-Field R) (v w : type-Vector-Space) → + mul-Vector-Space r (diff-Vector-Space v w) ＝ + diff-Vector-Space (mul-Vector-Space r v) (mul-Vector-Space r w) + left-distributive-mul-diff-Vector-Space = + left-distributive-mul-diff-left-module-Ring + ( ring-Heyting-Field R) + ( V) + right-distributive-mul-add-Vector-Space : (r s : type-Heyting-Field R) (v : type-Vector-Space) → mul-Vector-Space (add-Heyting-Field R r s) v ＝ @@ -132,6 +152,15 @@ module _ ( commutative-ring-Heyting-Field R) ( V) + right-distributive-mul-diff-Vector-Space : + (r s : type-Heyting-Field R) (v : type-Vector-Space) → + mul-Vector-Space (diff-Heyting-Field R r s) v ＝ + diff-Vector-Space (mul-Vector-Space r v) (mul-Vector-Space s v) + right-distributive-mul-diff-Vector-Space = + right-distributive-mul-diff-left-module-Ring + ( ring-Heyting-Field R) + ( V) + associative-mul-Vector-Space : (r s : type-Heyting-Field R) (v : type-Vector-Space) → mul-Vector-Space (mul-Heyting-Field R r s) v ＝ @@ -141,6 +170,15 @@ module _ ( commutative-ring-Heyting-Field R) ( V) + left-swap-mul-Vector-Space : + (r s : type-Heyting-Field R) (v : type-Vector-Space) → + mul-Vector-Space r (mul-Vector-Space s v) ＝ + mul-Vector-Space s (mul-Vector-Space r v) + left-swap-mul-Vector-Space = + left-swap-mul-left-module-Commutative-Ring + ( commutative-ring-Heyting-Field R) + ( V) + left-zero-law-mul-Vector-Space : (v : type-Vector-Space) → is-zero-Vector-Space (mul-Vector-Space (zero-Heyting-Field R) v) diff --git a/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md b/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md index 241c102cdf..7b48e04148 100644 --- a/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md +++ b/src/metric-spaces/accumulation-points-subsets-located-metric-spaces.lagda.md @@ -208,6 +208,11 @@ module _ UU (l1 ⊔ l2 ⊔ l3) is-sequential-accumulation-point-subset-Located-Metric-Space = type-Prop is-sequential-accumulation-point-prop-subset-Located-Metric-Space + + sequence-accumulating-to-point-subset-Located-Metric-Space : UU (l1 ⊔ l2 ⊔ l3) + sequence-accumulating-to-point-subset-Located-Metric-Space = + type-subtype + ( is-sequence-accumulating-to-point-prop-subset-Located-Metric-Space) ``` ### If `x` is an accumulation point of `S`, it is a sequential accumulation point of `S` diff --git a/src/metric-spaces/cartesian-products-metric-spaces.lagda.md b/src/metric-spaces/cartesian-products-metric-spaces.lagda.md index b39eec2c5f..a24ac69300 100644 --- a/src/metric-spaces/cartesian-products-metric-spaces.lagda.md +++ b/src/metric-spaces/cartesian-products-metric-spaces.lagda.md @@ -161,3 +161,51 @@ module _ ( diagonal-product (type-Metric-Space X) , ( λ _ _ _ → ((λ N → (N , N)) , pr1))) ``` + +### Given a constant element `x : X`, the map `y ↦ (x , y)` is an isometry + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (x : type-Metric-Space X) + where + + abstract + is-isometry-left-pair-Metric-Space : + is-isometry-Metric-Space Y (product-Metric-Space X Y) (x ,_) + pr1 (is-isometry-left-pair-Metric-Space d y y') Ndyy' = + ( refl-neighborhood-Metric-Space X d x , Ndyy') + pr2 (is-isometry-left-pair-Metric-Space d x x') = pr2 + + isometry-left-pair-Metric-Space : + isometry-Metric-Space Y (product-Metric-Space X Y) + isometry-left-pair-Metric-Space = + ( (x ,_) , + is-isometry-left-pair-Metric-Space) +``` + +### Given a constant element `y : Y`, the map `x ↦ (x , y)` is an isometry + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (y : type-Metric-Space Y) + where + + abstract + is-isometry-right-pair-Metric-Space : + is-isometry-Metric-Space X (product-Metric-Space X Y) (_, y) + pr1 (is-isometry-right-pair-Metric-Space d x x') Ndxx' = + ( Ndxx' , refl-neighborhood-Metric-Space Y d y) + pr2 (is-isometry-right-pair-Metric-Space d x x') = pr1 + + isometry-right-pair-Metric-Space : + isometry-Metric-Space X (product-Metric-Space X Y) + isometry-right-pair-Metric-Space = + ( ( _, y) , + is-isometry-right-pair-Metric-Space) +``` diff --git a/src/metric-spaces/uniformly-continuous-maps-metric-spaces.lagda.md b/src/metric-spaces/uniformly-continuous-maps-metric-spaces.lagda.md index e9c63b9da2..3cf059bd1b 100644 --- a/src/metric-spaces/uniformly-continuous-maps-metric-spaces.lagda.md +++ b/src/metric-spaces/uniformly-continuous-maps-metric-spaces.lagda.md @@ -353,3 +353,10 @@ module _ ## See also - [Modulated uniformly continuous maps on metric spaces](metric-spaces.modulated-uniformly-continuous-maps-metric-spaces.md) + +## External links + +- [Uniform continuity](https://en.wikipedia.org/wiki/Uniform_continuity) on + Wikipedia +- [Uniformly continuous map](https://ncatlab.org/nlab/show/uniformly+continuous+map) + on $n$Lab diff --git a/src/real-numbers/apartness-real-numbers.lagda.md b/src/real-numbers/apartness-real-numbers.lagda.md index 7ecb7b8953..f29d2c3bf2 100644 --- a/src/real-numbers/apartness-real-numbers.lagda.md +++ b/src/real-numbers/apartness-real-numbers.lagda.md @@ -303,8 +303,8 @@ module _ ```agda module _ {l1 l2 : Level} - (x : ℝ l1) - (y : ℝ l2) + {x : ℝ l1} + {y : ℝ l2} where abstract @@ -372,8 +372,6 @@ module _ apart-located-metric-space-ℝ x y → apart-ℝ x y apart-apart-located-metric-space-ℝ x#y = apart-is-positive-dist-ℝ - ( x) - ( y) ( is-positive-exists-not-le-positive-rational-ℝ ( dist-ℝ x y) ( map-tot-exists diff --git a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md index 14a42db763..dfad36c7c7 100644 --- a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md +++ b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md @@ -134,6 +134,14 @@ module _ ( commutative-mul-ℝ _ _) ( right-inverse-law-mul-nonzero-ℝ) + eq-left-inverse-law-mul-nonzero-ℝ : + real-inv-nonzero-ℝ *ℝ real-nonzero-ℝ x ＝ raise-one-ℝ l + eq-left-inverse-law-mul-nonzero-ℝ = + eq-sim-ℝ + ( transitive-sim-ℝ _ _ _ + ( sim-raise-ℝ l one-ℝ) + ( left-inverse-law-mul-nonzero-ℝ)) + is-invertible-is-nonzero-ℝ : {l : Level} (x : ℝ l) → is-nonzero-ℝ x → is-invertible-element-Commutative-Ring (commutative-ring-ℝ l) x diff --git a/src/ring-theory/rings.lagda.md b/src/ring-theory/rings.lagda.md index 2a5ca889c4..14415ee686 100644 --- a/src/ring-theory/rings.lagda.md +++ b/src/ring-theory/rings.lagda.md @@ -119,6 +119,9 @@ module _ add-Ring' : type-Ring R → type-Ring R → type-Ring R add-Ring' = add-Ab' (ab-Ring R) + diff-Ring : type-Ring R → type-Ring R → type-Ring R + diff-Ring = right-subtraction-Ab (ab-Ring R) + ap-add-Ring : {x y x' y' : type-Ring R} → x ＝ x' → y ＝ y' → add-Ring x y ＝ add-Ring x' y'