diff --git a/src/analysis.lagda.md b/src/analysis.lagda.md index 99788b360c..143ec1cb78 100644 --- a/src/analysis.lagda.md +++ b/src/analysis.lagda.md @@ -3,7 +3,16 @@ ```agda module analysis where +open import analysis.complete-metric-abelian-groups public +open import analysis.complete-metric-abelian-groups-real-banach-spaces public +open import analysis.convergent-series-complete-metric-abelian-groups public open import analysis.convergent-series-metric-abelian-groups public +open import analysis.convergent-series-real-banach-spaces public +open import analysis.convergent-series-real-numbers public open import analysis.metric-abelian-groups public +open import analysis.metric-abelian-groups-normed-real-vector-spaces public +open import analysis.series-complete-metric-abelian-groups public open import analysis.series-metric-abelian-groups public +open import analysis.series-real-banach-spaces public +open import analysis.series-real-numbers public ``` diff --git a/src/analysis/complete-metric-abelian-groups-real-banach-spaces.lagda.md b/src/analysis/complete-metric-abelian-groups-real-banach-spaces.lagda.md new file mode 100644 index 0000000000..40aa017885 --- /dev/null +++ b/src/analysis/complete-metric-abelian-groups-real-banach-spaces.lagda.md @@ -0,0 +1,63 @@ +# Complete metric abelian groups of real Banach spaces + +```agda +module analysis.complete-metric-abelian-groups-real-banach-spaces where +``` + +
Imports + +```agda +open import analysis.complete-metric-abelian-groups +open import analysis.metric-abelian-groups +open import analysis.metric-abelian-groups-normed-real-vector-spaces + +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.subtypes +open import foundation.universe-levels + +open import linear-algebra.real-banach-spaces + +open import real-numbers.metric-additive-group-of-real-numbers +``` + +
+ +## Idea + +Every [real Banach space](linear-algebra.real-banach-spaces.md) forms a +[complete metric abelian group](analysis.complete-metric-abelian-groups.md) +under addition. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + where + + metric-ab-add-ℝ-Banach-Space : Metric-Ab l2 l1 + metric-ab-add-ℝ-Banach-Space = + metric-ab-Normed-ℝ-Vector-Space (normed-vector-space-ℝ-Banach-Space V) + + complete-metric-ab-add-ℝ-Banach-Space : Complete-Metric-Ab l2 l1 + complete-metric-ab-add-ℝ-Banach-Space = + ( metric-ab-add-ℝ-Banach-Space , is-complete-metric-space-ℝ-Banach-Space V) +``` + +## Properties + +### The complete metric abelian group from the reals as a real Banach space equals the standard complete metric abelian group of the reals under addition + +```agda +abstract + eq-complete-metric-ab-ℝ : + (l : Level) → + complete-metric-ab-add-ℝ-Banach-Space (real-banach-space-ℝ l) ＝ + complete-metric-ab-add-ℝ l + eq-complete-metric-ab-ℝ l = + eq-type-subtype + ( is-complete-prop-Metric-Ab) + ( eq-metric-ab-normed-real-vector-space-metric-ab-ℝ l) +``` diff --git a/src/analysis/complete-metric-abelian-groups.lagda.md b/src/analysis/complete-metric-abelian-groups.lagda.md new file mode 100644 index 0000000000..e629810ef1 --- /dev/null +++ b/src/analysis/complete-metric-abelian-groups.lagda.md @@ -0,0 +1,65 @@ +# Complete metric abelian groups + +```agda +module analysis.complete-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.metric-abelian-groups + +open import foundation.dependent-pair-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.complete-metric-spaces +open import metric-spaces.metric-spaces +``` + +
+ +## Idea + +A {{#concept "complete metric abelian group" Agda=Complete-Metric-Ab}} is a +[metric abelian group](analysis.metric-abelian-groups.md) whose associated +[metric space](metric-spaces.metric-spaces.md) is +[complete](metric-spaces.complete-metric-spaces.md). + +## Definition + +```agda +is-complete-prop-Metric-Ab : {l1 l2 : Level} → Metric-Ab l1 l2 → Prop (l1 ⊔ l2) +is-complete-prop-Metric-Ab G = + is-complete-prop-Metric-Space (metric-space-Metric-Ab G) + +is-complete-Metric-Ab : {l1 l2 : Level} → Metric-Ab l1 l2 → UU (l1 ⊔ l2) +is-complete-Metric-Ab G = is-complete-Metric-Space (metric-space-Metric-Ab G) + +Complete-Metric-Ab : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Complete-Metric-Ab l1 l2 = type-subtype (is-complete-prop-Metric-Ab {l1} {l2}) +``` + +## Properties + +```agda +module _ + {l1 l2 : Level} + (G : Complete-Metric-Ab l1 l2) + where + + metric-ab-Complete-Metric-Ab : Metric-Ab l1 l2 + metric-ab-Complete-Metric-Ab = pr1 G + + metric-space-Complete-Metric-Ab : Metric-Space l1 l2 + metric-space-Complete-Metric-Ab = + metric-space-Metric-Ab metric-ab-Complete-Metric-Ab + + complete-metric-space-Complete-Metric-Ab : Complete-Metric-Space l1 l2 + complete-metric-space-Complete-Metric-Ab = + ( metric-space-Complete-Metric-Ab , pr2 G) + + type-Complete-Metric-Ab : UU l1 + type-Complete-Metric-Ab = type-Metric-Ab metric-ab-Complete-Metric-Ab +``` diff --git a/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md b/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md new file mode 100644 index 0000000000..49b1ac0dcc --- /dev/null +++ b/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md @@ -0,0 +1,79 @@ +# Convergent series in complete metric abelian groups + +```agda +module analysis.convergent-series-complete-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.complete-metric-abelian-groups +open import analysis.convergent-series-metric-abelian-groups +open import analysis.series-complete-metric-abelian-groups + +open import foundation.dependent-pair-types +open import foundation.propositions +open import foundation.universe-levels + +open import metric-spaces.cauchy-sequences-complete-metric-spaces +open import metric-spaces.cauchy-sequences-metric-spaces +``` + +
+ +## Idea + +A [series](analysis.series-metric-abelian-groups.md) +[converges](analysis.convergent-series-metric-abelian-groups.md) in a +[complete metric abelian group](analysis.complete-metric-abelian-groups.md) if +its partial sums form a +[Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md). + +A slightly modified converse is also true: if a series converges, there +[exists](foundation.existential-quantification.md) a modulus making it a Cauchy +sequence. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Complete-Metric-Ab l1 l2) + (σ : series-Complete-Metric-Ab G) + where + + is-sum-prop-series-Complete-Metric-Ab : type-Complete-Metric-Ab G → Prop l2 + is-sum-prop-series-Complete-Metric-Ab = is-sum-prop-series-Metric-Ab σ + + is-sum-series-Complete-Metric-Ab : type-Complete-Metric-Ab G → UU l2 + is-sum-series-Complete-Metric-Ab = is-sum-series-Metric-Ab σ + + is-convergent-prop-series-Complete-Metric-Ab : Prop (l1 ⊔ l2) + is-convergent-prop-series-Complete-Metric-Ab = + is-convergent-prop-series-Metric-Ab σ + + is-convergent-series-Complete-Metric-Ab : UU (l1 ⊔ l2) + is-convergent-series-Complete-Metric-Ab = is-convergent-series-Metric-Ab σ +``` + +## Properties + +### If the partial sums of a series form a Cauchy sequence, the series converges + +```agda +module _ + {l1 l2 : Level} + (G : Complete-Metric-Ab l1 l2) + (σ : series-Complete-Metric-Ab G) + where + + is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab : + is-cauchy-sequence-Metric-Space + ( metric-space-Complete-Metric-Ab G) + ( partial-sum-series-Complete-Metric-Ab G σ) → + is-convergent-series-Complete-Metric-Ab G σ + is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab H = + has-limit-cauchy-sequence-Complete-Metric-Space + ( complete-metric-space-Complete-Metric-Ab G) + ( partial-sum-series-Complete-Metric-Ab G σ , H) +``` diff --git a/src/analysis/convergent-series-real-banach-spaces.lagda.md b/src/analysis/convergent-series-real-banach-spaces.lagda.md new file mode 100644 index 0000000000..6ef12cc4ec --- /dev/null +++ b/src/analysis/convergent-series-real-banach-spaces.lagda.md @@ -0,0 +1,79 @@ +# Convergent series in real Banach spaces + +```agda +module analysis.convergent-series-real-banach-spaces where +``` + +
Imports + +```agda +open import analysis.complete-metric-abelian-groups-banach-spaces +open import analysis.convergent-series-complete-metric-abelian-groups +open import analysis.convergent-series-metric-abelian-groups +open import analysis.series-real-banach-spaces + +open import foundation.propositions +open import foundation.universe-levels + +open import linear-algebra.real-banach-spaces + +open import metric-spaces.cauchy-sequences-metric-spaces +``` + +
+ +## Idea + +A [series](analysis.series-real-banach-spaces.md) +[converges](analysis.convergent-series-metric-abelian-groups.md) in a +[real Banach space](linear-algebra.real-banach-spaces.md) if its partial sums +form a [Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md). + +A slightly modified converse is also true: if a series converges, there +[exists](foundation.existential-quantification.md) a modulus making it a Cauchy +sequence. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + (σ : series-ℝ-Banach-Space V) + where + + is-sum-prop-series-ℝ-Banach-Space : type-ℝ-Banach-Space V → Prop l1 + is-sum-prop-series-ℝ-Banach-Space = is-sum-prop-series-Metric-Ab σ + + is-sum-series-ℝ-Banach-Space : type-ℝ-Banach-Space V → UU l1 + is-sum-series-ℝ-Banach-Space = is-sum-series-Metric-Ab σ + + is-convergent-prop-series-ℝ-Banach-Space : Prop (l1 ⊔ l2) + is-convergent-prop-series-ℝ-Banach-Space = + is-convergent-prop-series-Metric-Ab σ + + is-convergent-series-ℝ-Banach-Space : UU (l1 ⊔ l2) + is-convergent-series-ℝ-Banach-Space = is-convergent-series-Metric-Ab σ +``` + +## Properties + +### If the partial sums of a series form a Cauchy sequence, the series converges + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + (σ : series-ℝ-Banach-Space V) + where + + is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space : + is-cauchy-sequence-Metric-Space + ( metric-space-ℝ-Banach-Space V) + ( partial-sum-series-ℝ-Banach-Space V σ) → + is-convergent-series-ℝ-Banach-Space V σ + is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space = + is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab + ( complete-metric-ab-add-ℝ-Banach-Space V) + ( σ) +``` diff --git a/src/analysis/convergent-series-real-numbers.lagda.md b/src/analysis/convergent-series-real-numbers.lagda.md new file mode 100644 index 0000000000..a7c911dd9e --- /dev/null +++ b/src/analysis/convergent-series-real-numbers.lagda.md @@ -0,0 +1,74 @@ +# Convergent series in the real numbers + +```agda +module analysis.convergent-series-real-numbers where +``` + +
Imports + +```agda +open import analysis.convergent-series-complete-metric-abelian-groups +open import analysis.convergent-series-metric-abelian-groups +open import analysis.series-real-numbers + +open import foundation.propositions +open import foundation.universe-levels + +open import real-numbers.cauchy-sequences-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-additive-group-of-real-numbers +``` + +
+ +## Idea + +A [series of real numbers](analysis.series-real-numbers.md) is +{{#concept "convergent" Disambiguation="series in 𝐑" Agda=is-convergent-series-ℝ Agda=convergent-series-ℝ WDID=Q1211057 WD="convergent series"}} +if its partial sums converge in the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md). + +## Definition + +```agda +module _ + {l : Level} + (σ : series-ℝ l) + where + + is-sum-prop-series-ℝ : ℝ l → Prop l + is-sum-prop-series-ℝ = is-sum-prop-series-Metric-Ab σ + + is-sum-series-ℝ : ℝ l → UU l + is-sum-series-ℝ = is-sum-series-Metric-Ab σ + + is-convergent-prop-series-ℝ : Prop (lsuc l) + is-convergent-prop-series-ℝ = + is-convergent-prop-series-Metric-Ab σ + + is-convergent-series-ℝ : UU (lsuc l) + is-convergent-series-ℝ = is-convergent-series-Metric-Ab σ +``` + +## Properties + +### If the partial sums of a series form a Cauchy sequence, the series converges + +```agda +module _ + {l : Level} + (σ : series-ℝ l) + where + + is-convergent-is-cauchy-sequence-partial-sum-series-ℝ : + is-cauchy-sequence-ℝ (partial-sum-series-ℝ σ) → + is-convergent-series-ℝ σ + is-convergent-is-cauchy-sequence-partial-sum-series-ℝ = + is-convergent-is-cauchy-sequence-partial-sum-series-Complete-Metric-Ab + ( complete-metric-ab-add-ℝ l) + ( σ) +``` + +## External links + +- [Convergent series](https://en.wikipedia.org/wiki/Ratio_test) on Wikipedia diff --git a/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md b/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md new file mode 100644 index 0000000000..4ee09d54d5 --- /dev/null +++ b/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md @@ -0,0 +1,94 @@ +# Metric abelian groups of normed real vector spaces + +```agda +module analysis.metric-abelian-groups-normed-real-vector-spaces where +``` + +
Imports + +```agda +open import analysis.metric-abelian-groups + +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.abelian-groups + +open import linear-algebra.normed-real-vector-spaces + +open import metric-spaces.extensionality-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations + +open import real-numbers.dedekind-real-numbers +open import real-numbers.distance-real-numbers +open import real-numbers.large-additive-group-of-real-numbers +open import real-numbers.metric-additive-group-of-real-numbers +``` + +
+ +## Idea + +A [normed](linear-algebra.normed-real-vector-spaces.md) +[real vector space](linear-algebra.real-vector-spaces.md) forms a +[metric abelian group](analysis.metric-abelian-groups.md) under addition. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + ab-metric-ab-Normed-ℝ-Vector-Space : Ab l2 + ab-metric-ab-Normed-ℝ-Vector-Space = ab-Normed-ℝ-Vector-Space V + + type-metric-ab-Normed-ℝ-Vector-Space : UU l2 + type-metric-ab-Normed-ℝ-Vector-Space = type-Normed-ℝ-Vector-Space V + + pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space : + Pseudometric-Structure l1 type-metric-ab-Normed-ℝ-Vector-Space + pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space = + pseudometric-structure-Metric-Space (metric-space-Normed-ℝ-Vector-Space V) + + pseudometric-space-metric-ab-Normed-ℝ-Vector-Space : + Pseudometric-Space l2 l1 + pseudometric-space-metric-ab-Normed-ℝ-Vector-Space = + pseudometric-Metric-Space (metric-space-Normed-ℝ-Vector-Space V) + + metric-ab-Normed-ℝ-Vector-Space : Metric-Ab l2 l1 + metric-ab-Normed-ℝ-Vector-Space = + ( ab-metric-ab-Normed-ℝ-Vector-Space , + pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space , + is-extensional-pseudometric-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) , + is-isometry-neg-Normed-ℝ-Vector-Space V , + is-isometry-left-add-Normed-ℝ-Vector-Space V) +``` + +## Properties + +### The metric abelian group associated with `ℝ` as a normed vector space over `ℝ` is equal to the metric additive group of `ℝ` + +```agda +abstract + eq-metric-ab-normed-real-vector-space-metric-ab-ℝ : + (l : Level) → + metric-ab-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l) ＝ + metric-ab-add-ℝ l + eq-metric-ab-normed-real-vector-space-metric-ab-ℝ l = + eq-pair-eq-fiber + ( eq-type-subtype + ( λ M → is-metric-ab-prop-Ab-Pseudometric-Structure (ab-add-ℝ l) M) + ( eq-type-subtype + ( is-pseudometric-prop-Rational-Neighborhood-Relation (ℝ l)) + ( eq-Eq-Rational-Neighborhood-Relation _ _ + ( λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y))))) +``` diff --git a/src/analysis/metric-abelian-groups.lagda.md b/src/analysis/metric-abelian-groups.lagda.md index 3306202936..fe8317d466 100644 --- a/src/analysis/metric-abelian-groups.lagda.md +++ b/src/analysis/metric-abelian-groups.lagda.md @@ -12,8 +12,10 @@ open import elementary-number-theory.positive-rational-numbers open import foundation.action-on-identifications-binary-functions open import foundation.binary-relations open import foundation.cartesian-product-types +open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.identity-types +open import foundation.propositions open import foundation.universe-levels open import group-theory.abelian-groups @@ -39,18 +41,25 @@ and negation operation are ## Definition ```agda +is-metric-ab-prop-Ab-Pseudometric-Structure : + {l1 l2 : Level} (G : Ab l1) (M : Pseudometric-Structure l2 (type-Ab G)) → + Prop (l1 ⊔ l2) +is-metric-ab-prop-Ab-Pseudometric-Structure G M = + let + MS = (type-Ab G , M) + in + is-extensional-prop-Pseudometric-Space MS ∧ + is-isometry-prop-Pseudometric-Space MS MS (neg-Ab G) ∧ + Π-Prop + ( type-Ab G) + ( λ x → is-isometry-prop-Pseudometric-Space MS MS (add-Ab G x)) + Metric-Ab : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Metric-Ab l1 l2 = Σ ( Ab l1) ( λ G → Σ ( Pseudometric-Structure l2 (type-Ab G)) - ( λ M → - let MS = (type-Ab G , M) - in - is-extensional-Pseudometric-Space MS × - is-isometry-Pseudometric-Space MS MS (neg-Ab G) × - ( (x : type-Ab G) → - is-isometry-Pseudometric-Space MS MS (add-Ab G x)))) + ( λ M → type-Prop (is-metric-ab-prop-Ab-Pseudometric-Structure G M))) module _ {l1 l2 : Level} (MG : Metric-Ab l1 l2) diff --git a/src/analysis/series-complete-metric-abelian-groups.lagda.md b/src/analysis/series-complete-metric-abelian-groups.lagda.md new file mode 100644 index 0000000000..bb936a8eb0 --- /dev/null +++ b/src/analysis/series-complete-metric-abelian-groups.lagda.md @@ -0,0 +1,49 @@ +# Series in complete metric abelian groups + +```agda +module analysis.series-complete-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.complete-metric-abelian-groups +open import analysis.series-metric-abelian-groups + +open import foundation.universe-levels + +open import lists.sequences +``` + +
+ +## Idea + +A [series](analysis.series-metric-abelian-groups.md) in a +[complete metric abelian group](analysis.complete-metric-abelian-groups.md) is a +series in the underlying +[metric abelian group](analysis.metric-abelian-groups.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Complete-Metric-Ab l1 l2) + where + + series-Complete-Metric-Ab : UU l1 + series-Complete-Metric-Ab = series-Metric-Ab (metric-ab-Complete-Metric-Ab G) + + series-terms-Complete-Metric-Ab : + sequence (type-Complete-Metric-Ab G) → series-Complete-Metric-Ab + series-terms-Complete-Metric-Ab = series-terms-Metric-Ab + + term-series-Complete-Metric-Ab : + series-Complete-Metric-Ab → sequence (type-Complete-Metric-Ab G) + term-series-Complete-Metric-Ab = term-series-Metric-Ab + + partial-sum-series-Complete-Metric-Ab : + series-Complete-Metric-Ab → sequence (type-Complete-Metric-Ab G) + partial-sum-series-Complete-Metric-Ab = partial-sum-series-Metric-Ab +``` diff --git a/src/analysis/series-real-banach-spaces.lagda.md b/src/analysis/series-real-banach-spaces.lagda.md new file mode 100644 index 0000000000..7c17414d98 --- /dev/null +++ b/src/analysis/series-real-banach-spaces.lagda.md @@ -0,0 +1,58 @@ +# Series in real Banach spaces + +```agda +module analysis.series-real-banach-spaces where +``` + +
Imports + +```agda +open import analysis.metric-abelian-groups-normed-real-vector-spaces +open import analysis.series-metric-abelian-groups + +open import foundation.universe-levels + +open import linear-algebra.real-banach-spaces + +open import lists.sequences +``` + +
+ +## Idea + +A +{{#concept "series" Disambiguation="in a real Banach space" Agda=series-ℝ-Banach-Space}} +is a [series](analysis.series-metric-abelian-groups.md) in the +[metric abelian group](analysis.metric-abelian-groups.md) +[associated](analysis.metric-abelian-groups-normed-real-vector-spaces.md) with +the underlying +[normed real vector space](linear-algebra.normed-real-vector-spaces.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + where + + series-ℝ-Banach-Space : UU l2 + series-ℝ-Banach-Space = + series-Metric-Ab + ( metric-ab-Normed-ℝ-Vector-Space (normed-vector-space-ℝ-Banach-Space V)) + + series-terms-ℝ-Banach-Space : + sequence (type-ℝ-Banach-Space V) → series-ℝ-Banach-Space + series-terms-ℝ-Banach-Space = series-terms-Metric-Ab + + term-series-ℝ-Banach-Space : + series-ℝ-Banach-Space → sequence (type-ℝ-Banach-Space V) + term-series-ℝ-Banach-Space = term-series-Metric-Ab + + partial-sum-series-ℝ-Banach-Space : + series-ℝ-Banach-Space → sequence (type-ℝ-Banach-Space V) + partial-sum-series-ℝ-Banach-Space = + partial-sum-series-Metric-Ab + ( metric-ab-Normed-ℝ-Vector-Space (normed-vector-space-ℝ-Banach-Space V)) +``` diff --git a/src/analysis/series-real-numbers.lagda.md b/src/analysis/series-real-numbers.lagda.md new file mode 100644 index 0000000000..6b7455caa6 --- /dev/null +++ b/src/analysis/series-real-numbers.lagda.md @@ -0,0 +1,44 @@ +# Series in the real numbers + +```agda +module analysis.series-real-numbers where +``` + +
Imports + +```agda +open import analysis.series-complete-metric-abelian-groups +open import analysis.series-metric-abelian-groups + +open import foundation.universe-levels + +open import lists.sequences + +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-additive-group-of-real-numbers +``` + +
+ +## Idea + +A {{#concept "series" Disambiguation="of real numbers" Agda=series-ℝ}} in the +[real numbers](real-numbers.dedekind-real-numbers.md) is a +[series](analysis.series-metric-abelian-groups.md) in the +[metric additive group of real numbers](real-numbers.metric-additive-group-of-real-numbers.md). + +## Definition + +```agda +series-ℝ : (l : Level) → UU (lsuc l) +series-ℝ l = series-Complete-Metric-Ab (complete-metric-ab-add-ℝ l) + +series-terms-ℝ : {l : Level} → sequence (ℝ l) → series-ℝ l +series-terms-ℝ = series-terms-Metric-Ab + +term-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l) +term-series-ℝ = term-series-Metric-Ab + +partial-sum-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l) +partial-sum-series-ℝ {l} = partial-sum-series-Metric-Ab +``` diff --git a/src/group-theory/abelian-groups.lagda.md b/src/group-theory/abelian-groups.lagda.md index afd0152826..cd3e651b39 100644 --- a/src/group-theory/abelian-groups.lagda.md +++ b/src/group-theory/abelian-groups.lagda.md @@ -622,6 +622,52 @@ module _ add-right-subtraction-Ab = mul-right-div-Group (group-Ab A) ``` +### `(-x) - (-y) = y - x` + +```agda +module _ + {l : Level} (A : Ab l) + where + + abstract + right-subtraction-neg-Ab : + (x y : type-Ab A) → + right-subtraction-Ab A (neg-Ab A x) (neg-Ab A y) ＝ + right-subtraction-Ab A y x + right-subtraction-neg-Ab x y = + equational-reasoning + right-subtraction-Ab A (neg-Ab A x) (neg-Ab A y) + ＝ add-Ab A (neg-Ab A x) y + by ap-add-Ab A refl (neg-neg-Ab A y) + ＝ right-subtraction-Ab A y x + by commutative-add-Ab A _ _ +``` + +### `(x + y) - (x + z) = y - z` + +```agda +module _ + {l : Level} (A : Ab l) + where + + abstract + right-subtraction-left-add-Ab : + (x y z : type-Ab A) → + right-subtraction-Ab A (add-Ab A x y) (add-Ab A x z) ＝ + right-subtraction-Ab A y z + right-subtraction-left-add-Ab x y z = + equational-reasoning + right-subtraction-Ab A (add-Ab A x y) (add-Ab A x z) + ＝ add-Ab A (add-Ab A x y) (add-Ab A (neg-Ab A x) (neg-Ab A z)) + by ap-add-Ab A refl (distributive-neg-add-Ab A x z) + ＝ add-Ab A (right-subtraction-Ab A x x) (right-subtraction-Ab A y z) + by interchange-add-add-Ab A _ _ _ _ + ＝ add-Ab A (zero-Ab A) (right-subtraction-Ab A y z) + by ap-add-Ab A (right-inverse-law-add-Ab A x) refl + ＝ right-subtraction-Ab A y z + by left-unit-law-add-Ab A _ +``` + ### Conjugation is the identity function **Proof:** Consider two elements `x` and `y` of an abelian group. Then diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index bc84732dbb..18b98d8f6b 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -32,13 +32,16 @@ open import linear-algebra.linear-spans-left-modules-rings public open import linear-algebra.matrices public open import linear-algebra.matrices-on-rings public open import linear-algebra.multiplication-matrices public +open import linear-algebra.normed-real-vector-spaces public open import linear-algebra.preimages-of-left-module-structures-along-homomorphisms-of-rings public open import linear-algebra.rational-modules public +open import linear-algebra.real-banach-spaces public open import linear-algebra.real-vector-spaces public open import linear-algebra.right-modules-rings public open import linear-algebra.scalar-multiplication-matrices public open import linear-algebra.scalar-multiplication-tuples public open import linear-algebra.scalar-multiplication-tuples-on-rings public +open import linear-algebra.seminormed-real-vector-spaces public open import linear-algebra.subsets-left-modules-rings public open import linear-algebra.transposition-matrices public open import linear-algebra.tuples-on-commutative-monoids public diff --git a/src/linear-algebra/normed-real-vector-spaces.lagda.md b/src/linear-algebra/normed-real-vector-spaces.lagda.md new file mode 100644 index 0000000000..798b3ca6c8 --- /dev/null +++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md @@ -0,0 +1,396 @@ +# Normed real vector spaces + +```agda +{-# OPTIONS --lossy-unification #-} + +module linear-algebra.normed-real-vector-spaces where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +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.equality-of-metric-spaces +open import metric-spaces.isometries-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 real-numbers.absolute-value-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.distance-real-numbers +open import real-numbers.metric-space-of-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 +``` + +
+ +## Idea + +A +{{#concept "norm" WDID=Q956437 WD="norm" Disambiguation="on a real vector space" Agda=norm-ℝ-Vector-Space}} +on a [real vector space](linear-algebra.real-vector-spaces.md) `V` is a +[seminorm](linear-algebra.seminormed-real-vector-spaces.md) `p` on `V` that is +**extensional**: if `p v = 0`, then `v` is the zero vector. + +A real vector space equipped with such a norm is called a +{{#concept "normed vector space" Disambiguation="normed real vector space" WDID=Q726210 WD="normed vector space" Agda=Normed-ℝ-Vector-Space}}. + +A norm on a real vector space induces a +[located](metric-spaces.located-metric-spaces.md) +[metric space](metric-spaces.metric-spaces.md) on the vector space, defined by +the neighborhood relation that `v` and `w` are in an `ε`-neighborhood of each +other if `p (v - w) ≤ ε`. + +## Definition + +```agda +module _ + {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2) (p : seminorm-ℝ-Vector-Space V) + where + + is-norm-prop-seminorm-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2) + is-norm-prop-seminorm-ℝ-Vector-Space = + Π-Prop + ( type-ℝ-Vector-Space V) + ( λ v → + hom-Prop + ( Id-Prop (ℝ-Set l1) (pr1 p v) (raise-ℝ l1 zero-ℝ)) + ( is-zero-prop-ℝ-Vector-Space V v)) + + is-norm-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2) + is-norm-seminorm-ℝ-Vector-Space = + type-Prop is-norm-prop-seminorm-ℝ-Vector-Space + +norm-ℝ-Vector-Space : {l1 l2 : Level} → ℝ-Vector-Space l1 l2 → UU (lsuc l1 ⊔ l2) +norm-ℝ-Vector-Space V = type-subtype (is-norm-prop-seminorm-ℝ-Vector-Space V) + +Normed-ℝ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Normed-ℝ-Vector-Space l1 l2 = Σ (ℝ-Vector-Space l1 l2) norm-ℝ-Vector-Space +``` + +## Properties + +```agda +module _ + {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) + where + + vector-space-Normed-ℝ-Vector-Space : ℝ-Vector-Space l1 l2 + vector-space-Normed-ℝ-Vector-Space = pr1 V + + ab-Normed-ℝ-Vector-Space : Ab l2 + ab-Normed-ℝ-Vector-Space = + ab-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space + + norm-Normed-ℝ-Vector-Space : + norm-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space + norm-Normed-ℝ-Vector-Space = pr2 V + + seminorm-Normed-ℝ-Vector-Space : + seminorm-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space + seminorm-Normed-ℝ-Vector-Space = pr1 norm-Normed-ℝ-Vector-Space + + seminormed-vector-space-Normed-ℝ-Vector-Space : + Seminormed-ℝ-Vector-Space l1 l2 + seminormed-vector-space-Normed-ℝ-Vector-Space = + ( vector-space-Normed-ℝ-Vector-Space , seminorm-Normed-ℝ-Vector-Space) + + set-Normed-ℝ-Vector-Space : Set l2 + set-Normed-ℝ-Vector-Space = + set-ℝ-Vector-Space vector-space-Normed-ℝ-Vector-Space + + 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 + + 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 + + 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 + + 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 + nonnegative-norm-Normed-ℝ-Vector-Space = + nonnegative-seminorm-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space) + + 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 + + nonnegative-dist-Normed-ℝ-Vector-Space : + type-Normed-ℝ-Vector-Space → type-Normed-ℝ-Vector-Space → ℝ⁰⁺ l1 + nonnegative-dist-Normed-ℝ-Vector-Space = + nonnegative-dist-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space) + + is-extensional-norm-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space) → + map-norm-Normed-ℝ-Vector-Space v ＝ raise-ℝ l1 zero-ℝ → + 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) → + dist-Normed-ℝ-Vector-Space v w ＝ raise-ℝ l1 zero-ℝ → + 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)) + + commutative-dist-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space) → + dist-Normed-ℝ-Vector-Space v w ＝ dist-Normed-ℝ-Vector-Space w v + commutative-dist-Normed-ℝ-Vector-Space = + commutative-dist-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space) +``` + +### The metric space of a normed vector space + +```agda +module _ + {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) + where + + refl-norm-Normed-ℝ-Vector-Space : + (v : type-Normed-ℝ-Vector-Space V) → + sim-ℝ zero-ℝ (dist-Normed-ℝ-Vector-Space V v v) + refl-norm-Normed-ℝ-Vector-Space v = + inv-tr + ( sim-ℝ zero-ℝ) + ( is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) + ( v)) + ( sim-raise-ℝ l1 zero-ℝ) + + metric-Normed-ℝ-Vector-Space : Metric l1 (set-Normed-ℝ-Vector-Space V) + metric-Normed-ℝ-Vector-Space = + ( nonnegative-dist-Normed-ℝ-Vector-Space V , + refl-norm-Normed-ℝ-Vector-Space , + ( λ v w → eq-ℝ⁰⁺ _ _ (commutative-dist-Normed-ℝ-Vector-Space V v w)) , + triangular-dist-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) , + ( λ v w 0~dvw → + is-extensional-dist-Normed-ℝ-Vector-Space V v w + ( eq-sim-ℝ + ( transitive-sim-ℝ _ _ _ + ( sim-raise-ℝ l1 zero-ℝ) + ( symmetric-sim-ℝ 0~dvw))))) + + metric-space-Normed-ℝ-Vector-Space : Metric-Space l2 l1 + metric-space-Normed-ℝ-Vector-Space = + metric-space-Metric + ( set-Normed-ℝ-Vector-Space V) + ( metric-Normed-ℝ-Vector-Space) + + located-metric-space-Normed-ℝ-Vector-Space : Located-Metric-Space l2 l1 + located-metric-space-Normed-ℝ-Vector-Space = + located-metric-space-Metric + ( set-Normed-ℝ-Vector-Space V) + ( metric-Normed-ℝ-Vector-Space) +``` + +## Properties + +### 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-ℝ) , + eq-raise-zero-eq-raise-zero-abs-ℝ) + +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)) +``` + +### Negation is an isometry in the metric space of a normed vector space + +```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 commutative-dist-Normed-ℝ-Vector-Space V y x))) +``` + +### Addition is an isometry in the metric space of a normed vector space + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + (u : type-Normed-ℝ-Vector-Space V) + where + + abstract + is-isometry-left-add-Normed-ℝ-Vector-Space : + is-isometry-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) + ( metric-space-Normed-ℝ-Vector-Space V) + ( add-Normed-ℝ-Vector-Space V u) + is-isometry-left-add-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)) + ( add-Normed-ℝ-Vector-Space V u) + ( λ v w → + sim-eq-ℝ + ( ap + ( map-norm-Normed-ℝ-Vector-Space V) + ( inv + ( right-subtraction-left-add-Ab + ( ab-Normed-ℝ-Vector-Space V) + ( u) + ( v) + ( w))))) +``` + +## See also + +- [Real Banach spaces](linear-algebra.real-banach-spaces.md), normed real vector + spaces for which the induced metric space is + [complete](metric-spaces.complete-metric-spaces.md) + +## External links + +- [Normed vector space](https://en.wikipedia.org/wiki/Normed_vector_space) on + Wikipedia diff --git a/src/linear-algebra/real-banach-spaces.lagda.md b/src/linear-algebra/real-banach-spaces.lagda.md new file mode 100644 index 0000000000..a1fe26c2c7 --- /dev/null +++ b/src/linear-algebra/real-banach-spaces.lagda.md @@ -0,0 +1,130 @@ +# Real Banach spaces + +```agda +{-# OPTIONS --lossy-unification #-} + +module linear-algebra.real-banach-spaces where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import linear-algebra.normed-real-vector-spaces + +open import lists.sequences + +open import metric-spaces.cauchy-sequences-complete-metric-spaces +open import metric-spaces.cauchy-sequences-metric-spaces +open import metric-spaces.complete-metric-spaces +open import metric-spaces.limits-of-sequences-metric-spaces +open import metric-spaces.metric-spaces + +open import real-numbers.cauchy-completeness-dedekind-real-numbers +open import real-numbers.dedekind-real-numbers +``` + +
+ +## Idea + +A real +{{#concept "Banach space" WDID=Q194397 WD="Banach space" Disambiguation="over ℝ" Agda=ℝ-Banach-Space}} +is a [normed](linear-algebra.normed-real-vector-spaces.md) +[real vector space](linear-algebra.real-vector-spaces.md) such that the +[metric space](metric-spaces.metric-spaces.md) induced by the norm is +[complete](metric-spaces.complete-metric-spaces.md). + +## Definition + +```agda +is-banach-prop-Normed-ℝ-Vector-Space : + {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) → Prop (l1 ⊔ l2) +is-banach-prop-Normed-ℝ-Vector-Space V = + is-complete-prop-Metric-Space (metric-space-Normed-ℝ-Vector-Space V) + +is-banach-Normed-ℝ-Vector-Space : + {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) → UU (l1 ⊔ l2) +is-banach-Normed-ℝ-Vector-Space V = + type-Prop (is-banach-prop-Normed-ℝ-Vector-Space V) + +ℝ-Banach-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +ℝ-Banach-Space l1 l2 = + type-subtype (is-banach-prop-Normed-ℝ-Vector-Space {l1} {l2}) + +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + where + + normed-vector-space-ℝ-Banach-Space : Normed-ℝ-Vector-Space l1 l2 + normed-vector-space-ℝ-Banach-Space = pr1 V + + metric-space-ℝ-Banach-Space : Metric-Space l2 l1 + metric-space-ℝ-Banach-Space = + metric-space-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space + + is-complete-metric-space-ℝ-Banach-Space : + is-complete-Metric-Space metric-space-ℝ-Banach-Space + is-complete-metric-space-ℝ-Banach-Space = pr2 V + + complete-metric-space-ℝ-Banach-Space : Complete-Metric-Space l2 l1 + complete-metric-space-ℝ-Banach-Space = + ( metric-space-ℝ-Banach-Space , is-complete-metric-space-ℝ-Banach-Space) + + type-ℝ-Banach-Space : UU l2 + type-ℝ-Banach-Space = + type-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space + + map-norm-ℝ-Banach-Space : type-ℝ-Banach-Space → ℝ l1 + map-norm-ℝ-Banach-Space = + map-norm-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space + + cauchy-sequence-ℝ-Banach-Space : UU (l1 ⊔ l2) + cauchy-sequence-ℝ-Banach-Space = + cauchy-sequence-Metric-Space metric-space-ℝ-Banach-Space + + is-cauchy-sequence-ℝ-Banach-Space : + sequence type-ℝ-Banach-Space → UU l1 + is-cauchy-sequence-ℝ-Banach-Space = + is-cauchy-sequence-Metric-Space metric-space-ℝ-Banach-Space + + map-cauchy-sequence-ℝ-Banach-Space : + cauchy-sequence-ℝ-Banach-Space → sequence type-ℝ-Banach-Space + map-cauchy-sequence-ℝ-Banach-Space = pr1 + + has-limit-sequence-ℝ-Banach-Space : + sequence type-ℝ-Banach-Space → UU (l1 ⊔ l2) + has-limit-sequence-ℝ-Banach-Space = + has-limit-sequence-Metric-Space metric-space-ℝ-Banach-Space + + has-limit-cauchy-sequence-ℝ-Banach-Space : + (σ : cauchy-sequence-ℝ-Banach-Space) → + has-limit-sequence-ℝ-Banach-Space (map-cauchy-sequence-ℝ-Banach-Space σ) + has-limit-cauchy-sequence-ℝ-Banach-Space = + has-limit-cauchy-sequence-Complete-Metric-Space + ( complete-metric-space-ℝ-Banach-Space) +``` + +## Properties + +### The real numbers are a real Banach space with norm `x ↦ |x|` + +```agda +real-banach-space-ℝ : (l : Level) → ℝ-Banach-Space l (lsuc l) +real-banach-space-ℝ l = + ( normed-real-vector-space-ℝ l , + inv-tr + ( is-complete-Metric-Space) + ( eq-metric-space-normed-real-vector-space-metric-space-ℝ l) + ( is-complete-metric-space-ℝ l)) +``` + +## External links + +- [Banach space](https://en.wikipedia.org/wiki/Banach_space) on Wikipedia diff --git a/src/linear-algebra/real-vector-spaces.lagda.md b/src/linear-algebra/real-vector-spaces.lagda.md index bc1d8cd6f2..526b466b41 100644 --- a/src/linear-algebra/real-vector-spaces.lagda.md +++ b/src/linear-algebra/real-vector-spaces.lagda.md @@ -1,17 +1,24 @@ # Real vector spaces ```agda +{-# OPTIONS --lossy-unification #-} + module linear-algebra.real-vector-spaces where ```
Imports ```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-functions open import foundation.identity-types open import foundation.sets +open import foundation.subtypes open import foundation.universe-levels open import group-theory.abelian-groups +open import group-theory.multiples-of-elements-abelian-groups open import linear-algebra.vector-spaces @@ -63,12 +70,23 @@ module _ zero-ℝ-Vector-Space : type-ℝ-Vector-Space zero-ℝ-Vector-Space = zero-Ab ab-ℝ-Vector-Space + is-zero-prop-ℝ-Vector-Space : subtype l2 type-ℝ-Vector-Space + is-zero-prop-ℝ-Vector-Space = is-zero-prop-Ab ab-ℝ-Vector-Space + + is-zero-ℝ-Vector-Space : type-ℝ-Vector-Space → UU l2 + is-zero-ℝ-Vector-Space = is-zero-Ab ab-ℝ-Vector-Space + neg-ℝ-Vector-Space : type-ℝ-Vector-Space → type-ℝ-Vector-Space neg-ℝ-Vector-Space = neg-Ab ab-ℝ-Vector-Space mul-ℝ-Vector-Space : ℝ l1 → type-ℝ-Vector-Space → type-ℝ-Vector-Space mul-ℝ-Vector-Space = mul-Vector-Space (heyting-field-ℝ l1) V + 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) + associative-add-ℝ-Vector-Space : (v w x : type-ℝ-Vector-Space) → add-ℝ-Vector-Space (add-ℝ-Vector-Space v w) x ＝ @@ -100,6 +118,16 @@ module _ add-ℝ-Vector-Space v w ＝ add-ℝ-Vector-Space w v commutative-add-ℝ-Vector-Space = commutative-add-Ab ab-ℝ-Vector-Space + add-diff-ℝ-Vector-Space : + (v w x : type-ℝ-Vector-Space) → + add-ℝ-Vector-Space (diff-ℝ-Vector-Space v w) (diff-ℝ-Vector-Space w x) ＝ + diff-ℝ-Vector-Space v x + add-diff-ℝ-Vector-Space = add-right-subtraction-Ab ab-ℝ-Vector-Space + + neg-neg-ℝ-Vector-Space : + (v : type-ℝ-Vector-Space) → neg-ℝ-Vector-Space (neg-ℝ-Vector-Space v) ＝ v + neg-neg-ℝ-Vector-Space = neg-neg-Ab ab-ℝ-Vector-Space + left-unit-law-mul-ℝ-Vector-Space : (v : type-ℝ-Vector-Space) → mul-ℝ-Vector-Space (raise-ℝ l1 one-ℝ) v ＝ v @@ -158,6 +186,56 @@ module _ mul-ℝ-Vector-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝ neg-ℝ-Vector-Space v mul-neg-one-ℝ-Vector-Space = mul-neg-one-Vector-Space (heyting-field-ℝ l1) V + + ap-add-ℝ-Vector-Space : + {x x' y y' : type-ℝ-Vector-Space} → x ＝ x' → y ＝ y' → + add-ℝ-Vector-Space x y ＝ add-ℝ-Vector-Space x' y' + ap-add-ℝ-Vector-Space = ap-add-Ab ab-ℝ-Vector-Space +``` + +## Properties + +### Multiplication by a natural number is iterated addition + +```agda +module _ + {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2) + where + + abstract + left-mul-real-ℕ-ℝ-Vector-Space : + (n : ℕ) (v : type-ℝ-Vector-Space V) → + mul-ℝ-Vector-Space V (raise-ℝ l1 (real-ℕ n)) v ＝ + multiple-Ab (ab-ℝ-Vector-Space V) n v + left-mul-real-ℕ-ℝ-Vector-Space 0 v = + left-zero-law-mul-ℝ-Vector-Space V v + left-mul-real-ℕ-ℝ-Vector-Space 1 v = + left-unit-law-mul-ℝ-Vector-Space V v + left-mul-real-ℕ-ℝ-Vector-Space (succ-ℕ n@(succ-ℕ _)) v = + equational-reasoning + mul-ℝ-Vector-Space V (raise-ℝ l1 (real-ℕ (succ-ℕ n))) v + ＝ mul-ℝ-Vector-Space V (raise-ℝ l1 (real-ℕ n) +ℝ raise-ℝ l1 one-ℝ) v + by + ap + ( λ c → mul-ℝ-Vector-Space V c v) + ( equational-reasoning + raise-ℝ l1 (real-ℕ (succ-ℕ n)) + ＝ raise-ℝ l1 (real-ℕ n +ℝ one-ℝ) + by ap (raise-ℝ l1) (inv (add-real-ℕ n 1)) + ＝ raise-ℝ l1 (real-ℕ n) +ℝ raise-ℝ l1 one-ℝ + by distributive-raise-add-ℝ l1 (real-ℕ n) one-ℝ) + ＝ + add-ℝ-Vector-Space V + ( mul-ℝ-Vector-Space V (raise-ℝ l1 (real-ℕ n)) v) + ( mul-ℝ-Vector-Space V (raise-ℝ l1 one-ℝ) v) + by right-distributive-mul-add-ℝ-Vector-Space V _ _ _ + ＝ + multiple-Ab (ab-ℝ-Vector-Space V) (succ-ℕ n) v + by + ap-add-ℝ-Vector-Space + ( V) + ( left-mul-real-ℕ-ℝ-Vector-Space n v) + ( left-unit-law-mul-ℝ-Vector-Space V v) ``` ### The real numbers are a real vector space @@ -172,3 +250,4 @@ real-vector-space-ℝ l = ## See also - [Vector spaces](linear-algebra.vector-spaces.md) +- [Normed real vector spaces](linear-algebra.normed-real-vector-spaces.md) diff --git a/src/linear-algebra/seminormed-real-vector-spaces.lagda.md b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md new file mode 100644 index 0000000000..2baea3c63b --- /dev/null +++ b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md @@ -0,0 +1,608 @@ +# Seminormed real vector spaces + +```agda +{-# OPTIONS --lossy-unification #-} + +module linear-algebra.seminormed-real-vector-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-relations +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import group-theory.abelian-groups + +open import linear-algebra.real-vector-spaces + +open import metric-spaces.pseudometric-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.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.multiplication-positive-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.positive-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.strict-inequality-real-numbers +``` + +
+ +## Idea + +A +{{#concept "seminorm" WDID=Q1416088 WD="seminorm" Disambiguation="on a real vector space" Agda=seminorm-ℝ-Vector-Space}} +on a [real vector space](linear-algebra.real-vector-spaces.md) `V` is a +[real](real-numbers.dedekind-real-numbers.md)-valued function `p` on the vector +space such that `p (x + y) ≤ p x + p y` for all `x` and `y` in `V`, and +`p (c * x) = |c| * p x` for all real numbers `c` and `x` in `V`. + +These conditions imply that `p 0 = 0` and that `p` is nonnegative. + +A real vector space equipped with such a seminorm is called a +{{#concept "seminormed space" WD="seminormed space" WDID=Q63793693 Agda=Seminormed-ℝ-Vector-Space}}. +A seminormed space has an induced +[pseudometric structure](metric-spaces.pseudometric-spaces.md) defined by the +neighborhood relation that `v` and `w` are in an `ε`-neighborhood of each other +if `p (v - w) ≤ ε`. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Vector-Space l1 l2) + (p : type-ℝ-Vector-Space V → ℝ l1) + where + + is-triangular-prop-seminorm-ℝ-Vector-Space : Prop (l1 ⊔ l2) + is-triangular-prop-seminorm-ℝ-Vector-Space = + Π-Prop + ( type-ℝ-Vector-Space V) + ( λ x → + Π-Prop + ( type-ℝ-Vector-Space V) + ( λ y → leq-prop-ℝ (p (add-ℝ-Vector-Space V x y)) (p x +ℝ p y))) + + is-triangular-seminorm-ℝ-Vector-Space : UU (l1 ⊔ l2) + is-triangular-seminorm-ℝ-Vector-Space = + type-Prop is-triangular-prop-seminorm-ℝ-Vector-Space + + is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2) + is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space = + Π-Prop + ( ℝ l1) + ( λ c → + Π-Prop + ( type-ℝ-Vector-Space V) + ( λ x → + Id-Prop + ( ℝ-Set l1) + ( p (mul-ℝ-Vector-Space V c x)) + ( abs-ℝ c *ℝ p x))) + + is-absolutely-homogeneous-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2) + is-absolutely-homogeneous-seminorm-ℝ-Vector-Space = + type-Prop is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space + + is-seminorm-prop-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2) + is-seminorm-prop-ℝ-Vector-Space = + is-triangular-prop-seminorm-ℝ-Vector-Space ∧ + is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space + + is-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2) + is-seminorm-ℝ-Vector-Space = type-Prop is-seminorm-prop-ℝ-Vector-Space + +seminorm-ℝ-Vector-Space : + {l1 l2 : Level} → ℝ-Vector-Space l1 l2 → UU (lsuc l1 ⊔ l2) +seminorm-ℝ-Vector-Space V = + type-subtype (is-seminorm-prop-ℝ-Vector-Space V) + +Seminormed-ℝ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Seminormed-ℝ-Vector-Space l1 l2 = + Σ (ℝ-Vector-Space l1 l2) seminorm-ℝ-Vector-Space +``` + +## Properties + +### Vector space properties + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + vector-space-Seminormed-ℝ-Vector-Space : ℝ-Vector-Space l1 l2 + vector-space-Seminormed-ℝ-Vector-Space = pr1 V + + set-Seminormed-ℝ-Vector-Space : Set l2 + set-Seminormed-ℝ-Vector-Space = + set-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + type-Seminormed-ℝ-Vector-Space : UU l2 + type-Seminormed-ℝ-Vector-Space = + type-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + seminorm-Seminormed-ℝ-Vector-Space : + seminorm-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + seminorm-Seminormed-ℝ-Vector-Space = pr2 V + + map-seminorm-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space → ℝ l1 + map-seminorm-Seminormed-ℝ-Vector-Space = + 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 + + 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-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space → UU l2 + is-zero-Seminormed-ℝ-Vector-Space = + is-zero-ℝ-Vector-Space vector-space-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 + + mul-Seminormed-ℝ-Vector-Space : + ℝ l1 → type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space + mul-Seminormed-ℝ-Vector-Space = + mul-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + neg-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space + neg-Seminormed-ℝ-Vector-Space = + neg-ℝ-Vector-Space vector-space-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) + + 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 + + add-diff-Seminormed-ℝ-Vector-Space : + (v w x : type-Seminormed-ℝ-Vector-Space) → + add-Seminormed-ℝ-Vector-Space + ( diff-Seminormed-ℝ-Vector-Space v w) + ( diff-Seminormed-ℝ-Vector-Space w x) ＝ + diff-Seminormed-ℝ-Vector-Space v x + add-diff-Seminormed-ℝ-Vector-Space = + add-diff-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + neg-neg-Seminormed-ℝ-Vector-Space : + (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 + + left-zero-law-mul-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space) → + mul-Seminormed-ℝ-Vector-Space (raise-ℝ l1 zero-ℝ) v ＝ + zero-Seminormed-ℝ-Vector-Space + left-zero-law-mul-Seminormed-ℝ-Vector-Space = + left-zero-law-mul-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + mul-neg-one-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space) → + mul-Seminormed-ℝ-Vector-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝ + neg-Seminormed-ℝ-Vector-Space v + mul-neg-one-Seminormed-ℝ-Vector-Space = + mul-neg-one-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + distributive-neg-diff-Seminormed-ℝ-Vector-Space : + (v w : type-Seminormed-ℝ-Vector-Space) → + 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) + + triangular-Seminormed-ℝ-Vector-Space : + (v w : type-Seminormed-ℝ-Vector-Space) → + leq-ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( add-Seminormed-ℝ-Vector-Space v w)) + ( map-seminorm-Seminormed-ℝ-Vector-Space v +ℝ + map-seminorm-Seminormed-ℝ-Vector-Space w) + triangular-Seminormed-ℝ-Vector-Space = + pr1 (pr2 seminorm-Seminormed-ℝ-Vector-Space) + + is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space : + (c : ℝ l1) (v : type-Seminormed-ℝ-Vector-Space) → + map-seminorm-Seminormed-ℝ-Vector-Space + ( mul-Seminormed-ℝ-Vector-Space c v) ＝ + abs-ℝ c *ℝ map-seminorm-Seminormed-ℝ-Vector-Space v + is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space = + pr2 (pr2 seminorm-Seminormed-ℝ-Vector-Space) + + dist-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space → ℝ l1 + dist-Seminormed-ℝ-Vector-Space v w = + map-seminorm-Seminormed-ℝ-Vector-Space + ( diff-Seminormed-ℝ-Vector-Space v w) +``` + +### The seminorm of the zero vector in a seminormed real vector space is zero + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + abstract + is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space : + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) ＝ + raise-ℝ l1 zero-ℝ + is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space = + eq-sim-ℝ + ( similarity-reasoning-ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) + ~ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( mul-Seminormed-ℝ-Vector-Space + ( V) + ( raise-ℝ l1 zero-ℝ) + ( zero-Seminormed-ℝ-Vector-Space V)) + by + sim-eq-ℝ + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( inv (left-zero-law-mul-Seminormed-ℝ-Vector-Space V _))) + ~ℝ + ( abs-ℝ (raise-ℝ l1 zero-ℝ)) *ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V)) + by + sim-eq-ℝ + ( is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space V _ _) + ~ℝ + ( abs-ℝ zero-ℝ) *ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V)) + by + preserves-sim-right-mul-ℝ _ _ _ + ( preserves-sim-abs-ℝ (sim-raise-ℝ' l1 zero-ℝ)) + ~ℝ + ( zero-ℝ) *ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V)) + by sim-eq-ℝ (ap-mul-ℝ abs-zero-ℝ refl) + ~ℝ zero-ℝ + by left-zero-law-mul-ℝ _ + ~ℝ raise-ℝ l1 zero-ℝ + by sim-raise-ℝ l1 zero-ℝ) + + is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space V) → + dist-Seminormed-ℝ-Vector-Space V v v ＝ raise-ℝ l1 zero-ℝ + is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space v = + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( right-inverse-law-add-Seminormed-ℝ-Vector-Space V v)) ∙ + ( is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space) +``` + +### The seminorm of the negation of a vector is equal to the seminorm of the vector + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + abstract + seminorm-neg-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space V) → + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( neg-Seminormed-ℝ-Vector-Space V v) ＝ + map-seminorm-Seminormed-ℝ-Vector-Space V v + seminorm-neg-Seminormed-ℝ-Vector-Space v = + eq-sim-ℝ + ( similarity-reasoning-ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( neg-Seminormed-ℝ-Vector-Space V v) + ~ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( mul-Seminormed-ℝ-Vector-Space + ( V) + ( neg-ℝ (raise-ℝ l1 one-ℝ)) + ( v)) + by + sim-eq-ℝ + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( inv (mul-neg-one-Seminormed-ℝ-Vector-Space V v))) + ~ℝ + ( abs-ℝ (neg-ℝ (raise-ℝ l1 one-ℝ))) *ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space V v) + by + sim-eq-ℝ + ( is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space V _ _) + ~ℝ + ( abs-ℝ (raise-ℝ l1 one-ℝ)) *ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space V v) + by sim-eq-ℝ (ap-mul-ℝ (abs-neg-ℝ _) refl) + ~ℝ abs-ℝ one-ℝ *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by + preserves-sim-right-mul-ℝ _ _ _ + ( preserves-sim-abs-ℝ (sim-raise-ℝ' l1 one-ℝ)) + ~ℝ one-ℝ *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by + sim-eq-ℝ (ap-mul-ℝ (abs-real-ℝ⁺ one-ℝ⁺) refl) + ~ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by sim-eq-ℝ (left-unit-law-mul-ℝ _)) + + commutative-dist-Seminormed-ℝ-Vector-Space : + (v w : type-Seminormed-ℝ-Vector-Space V) → + dist-Seminormed-ℝ-Vector-Space V v w ＝ + dist-Seminormed-ℝ-Vector-Space V w v + commutative-dist-Seminormed-ℝ-Vector-Space v w = + ( inv + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( distributive-neg-diff-Seminormed-ℝ-Vector-Space V w v))) ∙ + ( seminorm-neg-Seminormed-ℝ-Vector-Space _) +``` + +### The distance function on a seminormed vector space satisfies the triangle inequality + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + abstract + triangular-dist-Seminormed-ℝ-Vector-Space : + (v w x : type-Seminormed-ℝ-Vector-Space V) → + leq-ℝ + ( dist-Seminormed-ℝ-Vector-Space V v x) + ( dist-Seminormed-ℝ-Vector-Space V v w +ℝ + dist-Seminormed-ℝ-Vector-Space V w x) + triangular-dist-Seminormed-ℝ-Vector-Space v w x = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + chain-of-inequalities + dist-Seminormed-ℝ-Vector-Space V v x + ≤ map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( add-Seminormed-ℝ-Vector-Space + ( V) + ( diff-Seminormed-ℝ-Vector-Space V v w) + ( diff-Seminormed-ℝ-Vector-Space V w x)) + by + leq-eq-ℝ + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( inv (add-diff-Seminormed-ℝ-Vector-Space V v w x))) + ≤ ( dist-Seminormed-ℝ-Vector-Space V v w) +ℝ + ( dist-Seminormed-ℝ-Vector-Space V w x) + by triangular-Seminormed-ℝ-Vector-Space V _ _ +``` + +### The seminorm of a vector in a seminormed vector space is nonnegative + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + abstract + is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space V) → + is-nonnegative-ℝ (map-seminorm-Seminormed-ℝ-Vector-Space V v) + is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space v = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + reflects-leq-left-mul-ℝ⁺ + ( positive-real-ℕ⁺ (2 , λ ())) + ( zero-ℝ) + ( map-seminorm-Seminormed-ℝ-Vector-Space V v) + ( chain-of-inequalities + real-ℝ⁺ (positive-real-ℕ⁺ (2 , (λ ()))) *ℝ zero-ℝ + ≤ zero-ℝ + by leq-sim-ℝ (right-zero-law-mul-ℝ _) + ≤ raise-ℝ l1 zero-ℝ + by leq-sim-ℝ (sim-raise-ℝ l1 zero-ℝ) + ≤ dist-Seminormed-ℝ-Vector-Space V v v + by + leq-eq-ℝ + ( inv (is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space V v)) + ≤ ( map-seminorm-Seminormed-ℝ-Vector-Space V v) +ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( neg-Seminormed-ℝ-Vector-Space V v)) + by triangular-Seminormed-ℝ-Vector-Space V _ _ + ≤ ( map-seminorm-Seminormed-ℝ-Vector-Space V v) +ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space V v) + by + leq-eq-ℝ + ( ap-add-ℝ + ( refl) + ( seminorm-neg-Seminormed-ℝ-Vector-Space V v)) + ≤ real-ℕ 2 *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by leq-eq-ℝ (inv (left-mul-real-ℕ 2 _))) + + nonnegative-seminorm-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space V → ℝ⁰⁺ l1 + nonnegative-seminorm-Seminormed-ℝ-Vector-Space v = + ( map-seminorm-Seminormed-ℝ-Vector-Space V v , + is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space v) +``` + +### The pseudometric space induced by a seminorm + +```agda +module _ + {l1 l2 : Level} (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + nonnegative-dist-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space V → type-Seminormed-ℝ-Vector-Space V → ℝ⁰⁺ l1 + nonnegative-dist-Seminormed-ℝ-Vector-Space v w = + ( dist-Seminormed-ℝ-Vector-Space V v w , + is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space V _) + + neighborhood-prop-Seminormed-ℝ-Vector-Space : + ℚ⁺ → Relation-Prop l1 (type-Seminormed-ℝ-Vector-Space V) + neighborhood-prop-Seminormed-ℝ-Vector-Space ε v w = + leq-prop-ℝ + ( dist-Seminormed-ℝ-Vector-Space V v w) + ( real-ℚ⁺ ε) + + neighborhood-Seminormed-ℝ-Vector-Space : + ℚ⁺ → Relation l1 (type-Seminormed-ℝ-Vector-Space V) + neighborhood-Seminormed-ℝ-Vector-Space d = + type-Relation-Prop (neighborhood-prop-Seminormed-ℝ-Vector-Space d) + + abstract + refl-neighborhood-Seminormed-ℝ-Vector-Space : + (ε : ℚ⁺) (v : type-Seminormed-ℝ-Vector-Space V) → + neighborhood-Seminormed-ℝ-Vector-Space ε v v + refl-neighborhood-Seminormed-ℝ-Vector-Space ε v = + leq-le-ℝ + ( preserves-le-left-sim-ℝ + ( real-ℚ⁺ ε) + ( zero-ℝ) + ( dist-Seminormed-ℝ-Vector-Space V v v) + ( similarity-reasoning-ℝ + zero-ℝ + ~ℝ raise-ℝ l1 zero-ℝ + by sim-raise-ℝ l1 zero-ℝ + ~ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) + by + sim-eq-ℝ + ( inv (is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space V)) + ~ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( diff-Seminormed-ℝ-Vector-Space V v v) + by + sim-eq-ℝ + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( inv + ( right-inverse-law-add-Seminormed-ℝ-Vector-Space V v)))) + ( preserves-is-positive-real-ℚ (is-positive-rational-ℚ⁺ ε))) + + symmetric-neighborhood-Seminormed-ℝ-Vector-Space : + (d : ℚ⁺) (v w : type-Seminormed-ℝ-Vector-Space V) → + neighborhood-Seminormed-ℝ-Vector-Space d v w → + neighborhood-Seminormed-ℝ-Vector-Space d w v + symmetric-neighborhood-Seminormed-ℝ-Vector-Space d v w = + tr + ( λ z → leq-ℝ z (real-ℚ⁺ d)) + ( commutative-dist-Seminormed-ℝ-Vector-Space V v w) + + triangular-neighborhood-Seminormed-ℝ-Vector-Space : + (v w x : type-Seminormed-ℝ-Vector-Space V) (d1 d2 : ℚ⁺) → + neighborhood-Seminormed-ℝ-Vector-Space d2 w x → + neighborhood-Seminormed-ℝ-Vector-Space d1 v w → + neighborhood-Seminormed-ℝ-Vector-Space (d1 +ℚ⁺ d2) v x + triangular-neighborhood-Seminormed-ℝ-Vector-Space + v w x d1 d2 Nd2wx Nd1vw = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + chain-of-inequalities + dist-Seminormed-ℝ-Vector-Space V v x + ≤ ( dist-Seminormed-ℝ-Vector-Space V v w) +ℝ + ( dist-Seminormed-ℝ-Vector-Space V w x) + by triangular-dist-Seminormed-ℝ-Vector-Space V v w x + ≤ real-ℚ⁺ d1 +ℝ real-ℚ⁺ d2 + by preserves-leq-add-ℝ Nd1vw Nd2wx + ≤ real-ℚ⁺ (d1 +ℚ⁺ d2) + by leq-eq-ℝ (add-real-ℚ _ _) + + saturated-neighborhood-Seminormed-ℝ-Vector-Space : + (d : ℚ⁺) (v w : type-Seminormed-ℝ-Vector-Space V) → + ((δ : ℚ⁺) → neighborhood-Seminormed-ℝ-Vector-Space (d +ℚ⁺ δ) v w) → + neighborhood-Seminormed-ℝ-Vector-Space d v w + saturated-neighborhood-Seminormed-ℝ-Vector-Space d v w H = + saturated-leq-ℝ⁰⁺ + ( nonnegative-dist-Seminormed-ℝ-Vector-Space v w) + ( nonnegative-real-ℚ⁺ d) + ( λ δ → + inv-tr + ( leq-ℝ (dist-Seminormed-ℝ-Vector-Space V v w)) + ( add-real-ℚ _ _) + ( H δ)) + + pseudometric-structure-Seminormed-ℝ-Vector-Space : + Pseudometric-Structure l1 (type-Seminormed-ℝ-Vector-Space V) + pseudometric-structure-Seminormed-ℝ-Vector-Space = + ( neighborhood-prop-Seminormed-ℝ-Vector-Space , + refl-neighborhood-Seminormed-ℝ-Vector-Space , + symmetric-neighborhood-Seminormed-ℝ-Vector-Space , + triangular-neighborhood-Seminormed-ℝ-Vector-Space , + saturated-neighborhood-Seminormed-ℝ-Vector-Space) + + pseudometric-space-Seminormed-ℝ-Vector-Space : Pseudometric-Space l2 l1 + pseudometric-space-Seminormed-ℝ-Vector-Space = + ( type-Seminormed-ℝ-Vector-Space V , + pseudometric-structure-Seminormed-ℝ-Vector-Space) +``` + +### The real numbers are a seminormed vector space over themselves with seminorm `x ↦ |x|` + +```agda +seminormed-real-vector-space-ℝ : + (l : Level) → Seminormed-ℝ-Vector-Space l (lsuc l) +seminormed-real-vector-space-ℝ l = + ( real-vector-space-ℝ l , abs-ℝ , triangle-inequality-abs-ℝ , abs-mul-ℝ) +``` diff --git a/src/metric-spaces/metrics-of-metric-spaces.lagda.md b/src/metric-spaces/metrics-of-metric-spaces.lagda.md index ea6ba29759..f3b1b5bcff 100644 --- a/src/metric-spaces/metrics-of-metric-spaces.lagda.md +++ b/src/metric-spaces/metrics-of-metric-spaces.lagda.md @@ -21,13 +21,17 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.equality-of-metric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.isometries-metric-spaces open import metric-spaces.located-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.metrics +open import metric-spaces.short-functions-metric-spaces open import real-numbers.addition-nonnegative-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.inequality-nonnegative-real-numbers +open import real-numbers.inequality-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.saturation-inequality-nonnegative-real-numbers @@ -109,7 +113,7 @@ module _ is-reflexive-is-metric-of-Metric-Space : is-reflexive-distance-function (set-Metric-Space M) ρ is-reflexive-is-metric-of-Metric-Space x = - sim-zero-le-positive-rational-ℝ⁰⁺ + sim-zero-leq-positive-rational-ℝ⁰⁺ ( ρ x x) ( λ ε → forward-implication @@ -266,6 +270,109 @@ module _ ( isometric-equiv-metric-is-metric-of-Metric-Space M ρ is-metric-M-ρ) ``` +### If `M` and `N` are metric spaces with metrics `dM` and `dN`, a function `f : M → N` is an isometry if and only if `dM x y` is similar to `dN (f x) (f y)` for all `x, y : M` + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (M : Metric-Space l1 l2) + (N : Metric-Space l3 l4) + (dM : distance-function l5 (set-Metric-Space M)) + (dN : distance-function l6 (set-Metric-Space N)) + (is-metric-dM : is-metric-of-Metric-Space M dM) + (is-metric-dN : is-metric-of-Metric-Space N dN) + (f : type-function-Metric-Space M N) + where + + abstract + is-isometry-sim-metric-Metric-Space : + ((x y : type-Metric-Space M) → sim-ℝ⁰⁺ (dM x y) (dN (f x) (f y))) → + is-isometry-Metric-Space M N f + is-isometry-sim-metric-Metric-Space H d x y = + logical-equivalence-reasoning + neighborhood-Metric-Space M d x y + ↔ leq-ℝ (real-ℝ⁰⁺ (dM x y)) (real-ℚ⁺ d) + by is-metric-dM d x y + ↔ leq-ℝ (real-ℝ⁰⁺ (dN (f x) (f y))) (real-ℚ⁺ d) + by leq-iff-left-sim-ℝ (H x y) + ↔ neighborhood-Metric-Space N d (f x) (f y) + by inv-iff (is-metric-dN d (f x) (f y)) + + sim-metric-is-isometry-Metric-Space : + is-isometry-Metric-Space M N f → + (x y : type-Metric-Space M) → + sim-ℝ⁰⁺ (dM x y) (dN (f x) (f y)) + sim-metric-is-isometry-Metric-Space H x y = + sim-leq-same-positive-rational-ℝ⁰⁺ + ( dM x y) + ( dN (f x) (f y)) + ( λ d → + logical-equivalence-reasoning + leq-ℝ (real-ℝ⁰⁺ (dM x y)) (real-ℚ⁺ d) + ↔ neighborhood-Metric-Space M d x y + by inv-iff (is-metric-dM d x y) + ↔ neighborhood-Metric-Space N d (f x) (f y) + by H d x y + ↔ leq-ℝ (real-ℝ⁰⁺ (dN (f x) (f y))) (real-ℚ⁺ d) + by is-metric-dN d (f x) (f y)) + + is-isometry-iff-sim-metric-Metric-Space : + is-isometry-Metric-Space M N f ↔ + ((x y : type-Metric-Space M) → sim-ℝ⁰⁺ (dM x y) (dN (f x) (f y))) + is-isometry-iff-sim-metric-Metric-Space = + ( sim-metric-is-isometry-Metric-Space , + is-isometry-sim-metric-Metric-Space) +``` + +### If `M` and `N` are metric spaces with metrics `dM` and `dN`, a function `f : M → N` is short if and only if `dN (f x) (f y) ≤ dM x y` for all `x, y : M` + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (M : Metric-Space l1 l2) + (N : Metric-Space l3 l4) + (dM : distance-function l5 (set-Metric-Space M)) + (dN : distance-function l6 (set-Metric-Space N)) + (is-metric-dM : is-metric-of-Metric-Space M dM) + (is-metric-dN : is-metric-of-Metric-Space N dN) + (f : type-function-Metric-Space M N) + where + + abstract + is-short-function-leq-metric-Metric-Space : + ((x y : type-Metric-Space M) → leq-ℝ⁰⁺ (dN (f x) (f y)) (dM x y)) → + is-short-function-Metric-Space M N f + is-short-function-leq-metric-Metric-Space H d x y Ndxy = + backward-implication + ( is-metric-dN d (f x) (f y)) + ( transitive-leq-ℝ + ( real-ℝ⁰⁺ (dN (f x) (f y))) + ( real-ℝ⁰⁺ (dM x y)) + ( real-ℚ⁺ d) + ( forward-implication (is-metric-dM d x y) Ndxy) + ( H x y)) + + leq-metric-is-short-function-Metric-Space : + is-short-function-Metric-Space M N f → + (x y : type-Metric-Space M) → + leq-ℝ⁰⁺ (dN (f x) (f y)) (dM x y) + leq-metric-is-short-function-Metric-Space H x y = + leq-leq-positive-rational-ℝ⁰⁺ + ( dN (f x) (f y)) + ( dM x y) + ( λ d dMxy≤d → + forward-implication + ( is-metric-dN d (f x) (f y)) + ( H d x y (backward-implication (is-metric-dM d x y) dMxy≤d))) + + is-short-function-iff-leq-metric-Metric-Space : + is-short-function-Metric-Space M N f ↔ + ((x y : type-Metric-Space M) → leq-ℝ⁰⁺ (dN (f x) (f y)) (dM x y)) + is-short-function-iff-leq-metric-Metric-Space = + ( leq-metric-is-short-function-Metric-Space , + is-short-function-leq-metric-Metric-Space) +``` + ## See also - [Metrics of metric spaces are uniformly continuous](metric-spaces.metrics-of-metric-spaces-are-uniformly-continuous.md) diff --git a/src/metric-spaces/metrics.lagda.md b/src/metric-spaces/metrics.lagda.md index 6ed22735b3..67cc1c541a 100644 --- a/src/metric-spaces/metrics.lagda.md +++ b/src/metric-spaces/metrics.lagda.md @@ -297,7 +297,7 @@ module _ is-tight-Pseudometric-Space (pseudometric-space-Metric X μ) is-tight-pseudometric-space-Metric x y H = is-extensional-dist-Metric X μ x y - ( sim-zero-le-positive-rational-ℝ⁰⁺ (dist-Metric X μ x y) H) + ( sim-zero-leq-positive-rational-ℝ⁰⁺ (dist-Metric X μ x y) H) ``` ### The pseudometric space induced by a metric is extensional diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index 538d9ef259..c4bcb8c5a7 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -103,6 +103,7 @@ open import order-theory.maximal-chains-preorders public open import order-theory.meet-semilattices public open import order-theory.meet-suplattices public open import order-theory.meets-finite-families-meet-semilattices public +open import order-theory.monotonic-sequences-posets public open import order-theory.nuclei-large-locales public open import order-theory.opposite-large-posets public open import order-theory.opposite-large-preorders public diff --git a/src/order-theory/monotonic-sequences-posets.lagda.md b/src/order-theory/monotonic-sequences-posets.lagda.md new file mode 100644 index 0000000000..048129132b --- /dev/null +++ b/src/order-theory/monotonic-sequences-posets.lagda.md @@ -0,0 +1,84 @@ +# Monotonic sequences in posets + +```agda +module order-theory.monotonic-sequences-posets where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import lists.sequences + +open import order-theory.order-preserving-maps-posets +open import order-theory.posets +``` + +
+ +## Idea + +A +{{#concept "monotonic sequence" Agda=monotonic-sequence-Poset Disambiguation="in a poset"}} +in a [poset](order-theory.posets.md) `P` is a [sequence](lists.sequences.md) +`aₙ` such that whenever `m ≤ n`, `aₘ ≤ aₙ`. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + is-monotonic-prop-sequence-Poset : subtype l2 (sequence (type-Poset P)) + is-monotonic-prop-sequence-Poset a = preserves-order-prop-Poset ℕ-Poset P a + + is-monotonic-sequence-Poset : sequence (type-Poset P) → UU l2 + is-monotonic-sequence-Poset a = type-Prop (is-monotonic-prop-sequence-Poset a) +``` + +## Properties + +### If `aₙ ≤ aₙ₊₁` for all `n`, then the sequence `aₙ` is monotonic + +```agda +module _ + {l1 l2 : Level} + (P : Poset l1 l2) + where + + abstract + is-monotonic-sequence-is-increasing-Poset : + (a : sequence (type-Poset P)) → + ((n : ℕ) → leq-Poset P (a n) (a (succ-ℕ n))) → + is-monotonic-sequence-Poset P a + is-monotonic-sequence-is-increasing-Poset a H m n m≤n = + let + (l , l+m=n) = subtraction-leq-ℕ m n m≤n + in + tr + ( λ k → leq-Poset P (a m) (a k)) + ( commutative-add-ℕ m l ∙ l+m=n) + ( lemma l) + where + lemma : (k : ℕ) → leq-Poset P (a m) (a (m +ℕ k)) + lemma 0 = refl-leq-Poset P (a m) + lemma (succ-ℕ k) = + transitive-leq-Poset P + ( a m) + ( a (m +ℕ k)) + ( a (m +ℕ succ-ℕ k)) + ( H (m +ℕ k)) + ( lemma k) +``` diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 26bb420996..eb9471d10b 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -22,7 +22,6 @@ open import real-numbers.binary-minimum-real-numbers public open import real-numbers.cauchy-completeness-dedekind-real-numbers public open import real-numbers.cauchy-sequences-real-numbers public open import real-numbers.closed-intervals-real-numbers public -open import real-numbers.convergent-series-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 @@ -58,7 +57,7 @@ open import real-numbers.maximum-finite-families-real-numbers public open import real-numbers.maximum-inhabited-finitely-enumerable-subsets-real-numbers public open import real-numbers.maximum-lower-dedekind-real-numbers public open import real-numbers.maximum-upper-dedekind-real-numbers public -open import real-numbers.metric-abelian-group-of-real-numbers public +open import real-numbers.metric-additive-group-of-real-numbers public open import real-numbers.metric-space-of-nonnegative-real-numbers public open import real-numbers.metric-space-of-real-numbers public open import real-numbers.minimum-finite-families-real-numbers public @@ -92,7 +91,6 @@ open import real-numbers.real-numbers-from-upper-dedekind-real-numbers public open import real-numbers.real-sequences-approximating-zero public open import real-numbers.saturation-inequality-nonnegative-real-numbers public open import real-numbers.saturation-inequality-real-numbers public -open import real-numbers.series-real-numbers public open import real-numbers.short-function-binary-maximum-real-numbers public open import real-numbers.short-function-binary-minimum-real-numbers public open import real-numbers.similarity-nonnegative-real-numbers public diff --git a/src/real-numbers/absolute-value-real-numbers.lagda.md b/src/real-numbers/absolute-value-real-numbers.lagda.md index 6e56c70a08..120e455dd4 100644 --- a/src/real-numbers/absolute-value-real-numbers.lagda.md +++ b/src/real-numbers/absolute-value-real-numbers.lagda.md @@ -14,6 +14,7 @@ open import elementary-number-theory.rational-numbers open import elementary-number-theory.squares-rational-numbers open import foundation.action-on-identifications-functions +open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.empty-types @@ -39,6 +40,7 @@ open import real-numbers.negative-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.positive-and-negative-real-numbers open import real-numbers.positive-real-numbers +open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.saturation-inequality-real-numbers open import real-numbers.similarity-real-numbers @@ -90,6 +92,23 @@ abstract opaque preserves-sim-max-ℝ _ _ x~x' _ _ (preserves-sim-neg-ℝ x~x') ``` +### The absolute value commutes with raising the universe level of a real number + +```agda +abstract + abs-raise-ℝ : + {l1 : Level} (l2 : Level) (x : ℝ l1) → + abs-ℝ (raise-ℝ l2 x) ＝ raise-ℝ l2 (abs-ℝ x) + abs-raise-ℝ l2 x = + eq-sim-ℝ + ( similarity-reasoning-ℝ + abs-ℝ (raise-ℝ l2 x) + ~ℝ abs-ℝ x + by preserves-sim-abs-ℝ (sim-raise-ℝ' l2 x) + ~ℝ raise-ℝ l2 (abs-ℝ x) + by sim-raise-ℝ l2 (abs-ℝ x)) +``` + ### The absolute value of a real number is nonnegative ```agda @@ -183,6 +202,34 @@ module _ ### If `|x| ＝ 0` then `x ＝ 0` ```agda +module _ + {l : Level} (x : ℝ l) (|x|~0 : sim-ℝ (abs-ℝ x) zero-ℝ) + where + + abstract + sim-zero-sim-zero-abs-ℝ : sim-ℝ x zero-ℝ + sim-zero-sim-zero-abs-ℝ = + sim-sim-leq-ℝ + ( transitive-leq-ℝ _ _ _ (leq-sim-ℝ |x|~0) (leq-abs-ℝ x) , + binary-tr + ( leq-ℝ) + ( neg-zero-ℝ) + ( neg-neg-ℝ x) + ( neg-leq-ℝ + ( transitive-leq-ℝ _ _ _ (leq-sim-ℝ |x|~0) (neg-leq-abs-ℝ x)))) + +abstract + eq-raise-zero-eq-raise-zero-abs-ℝ : + {l : Level} (x : ℝ l) → abs-ℝ x ＝ raise-ℝ l zero-ℝ → x ＝ raise-ℝ l zero-ℝ + eq-raise-zero-eq-raise-zero-abs-ℝ {l} x |x|=0 = + eq-sim-ℝ + ( transitive-sim-ℝ _ _ _ + ( sim-raise-ℝ l zero-ℝ) + ( sim-zero-sim-zero-abs-ℝ x + ( transitive-sim-ℝ _ _ _ + ( sim-raise-ℝ' l zero-ℝ) + ( sim-eq-ℝ |x|=0)))) + module _ (x : ℝ lzero) (|x|=0 : abs-ℝ x ＝ zero-ℝ) where @@ -190,14 +237,7 @@ module _ abstract is-zero-is-zero-abs-ℝ : x ＝ zero-ℝ is-zero-is-zero-abs-ℝ = - antisymmetric-leq-ℝ - ( x) - ( zero-ℝ) - ( tr (leq-ℝ x) |x|=0 (leq-abs-ℝ x)) - ( tr - ( λ y → leq-ℝ y x) - ( (ap neg-ℝ |x|=0) ∙ neg-zero-ℝ) - ( leq-neg-abs-ℝ x)) + eq-sim-ℝ (sim-zero-sim-zero-abs-ℝ x (sim-eq-ℝ |x|=0)) ``` ### If `|x| ≤ 0` then `|x| ＝ 0` and `x ＝ 0` diff --git a/src/real-numbers/addition-real-numbers.lagda.md b/src/real-numbers/addition-real-numbers.lagda.md index 8f67041ac9..681da0f83d 100644 --- a/src/real-numbers/addition-real-numbers.lagda.md +++ b/src/real-numbers/addition-real-numbers.lagda.md @@ -9,8 +9,12 @@ module real-numbers.addition-real-numbers where
Imports ```agda +open import elementary-number-theory.addition-integers +open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers @@ -385,6 +389,23 @@ module _ pr2 iff-translate-left-sim-ℝ = reflects-sim-left-add-ℝ z x y ``` +### Raising the universe level of real numbers distributes over addition + +```agda +abstract + distributive-raise-add-ℝ : + {l1 l2 : Level} (l3 : Level) (x : ℝ l1) (y : ℝ l2) → + raise-ℝ l3 (x +ℝ y) ＝ raise-ℝ l3 x +ℝ raise-ℝ l3 y + distributive-raise-add-ℝ l3 x y = + eq-sim-ℝ + ( similarity-reasoning-ℝ + raise-ℝ l3 (x +ℝ y) + ~ℝ x +ℝ y + by sim-raise-ℝ' l3 (x +ℝ y) + ~ℝ raise-ℝ l3 x +ℝ raise-ℝ l3 y + by preserves-sim-add-ℝ (sim-raise-ℝ l3 x) (sim-raise-ℝ l3 y)) +``` + ### The inclusion of rational numbers preserves addition ```agda @@ -427,6 +448,34 @@ abstract ＝ x +ℝ real-ℚ (p +ℚ q) by ap (x +ℝ_) (add-real-ℚ p q) ``` +### The inclusion of integers preserves addition + +```agda +abstract + add-real-ℤ : (x y : ℤ) → real-ℤ x +ℝ real-ℤ y ＝ real-ℤ (x +ℤ y) + add-real-ℤ x y = + equational-reasoning + real-ℤ x +ℝ real-ℤ y + ＝ real-ℚ (rational-ℤ x +ℚ rational-ℤ y) + by add-real-ℚ _ _ + ＝ real-ℤ (x +ℤ y) + by ap real-ℚ (add-rational-ℤ x y) +``` + +### The inclusion of natural numbers preserves addition + +```agda +abstract + add-real-ℕ : (x y : ℕ) → real-ℕ x +ℝ real-ℕ y ＝ real-ℕ (x +ℕ y) + add-real-ℕ x y = + equational-reasoning + real-ℕ x +ℝ real-ℕ y + ＝ real-ℤ (int-ℕ x +ℤ int-ℕ y) + by add-real-ℤ _ _ + ＝ real-ℕ (x +ℕ y) + by ap real-ℤ (add-int-ℕ x y) +``` + ### Interchange laws for addition on real numbers ```agda diff --git a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md index 6876201386..a7d81021a9 100644 --- a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md +++ b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md @@ -11,6 +11,8 @@ module real-numbers.cauchy-sequences-real-numbers where ```agda open import foundation.universe-levels +open import lists.sequences + open import metric-spaces.cartesian-products-metric-spaces open import metric-spaces.cauchy-sequences-complete-metric-spaces open import metric-spaces.cauchy-sequences-metric-spaces @@ -39,6 +41,9 @@ is a [Cauchy sequence](metric-spaces.cauchy-sequences-metric-spaces.md) in the ## Definition ```agda +is-cauchy-sequence-ℝ : {l : Level} → sequence (ℝ l) → UU l +is-cauchy-sequence-ℝ {l} = is-cauchy-sequence-Metric-Space (metric-space-ℝ l) + cauchy-sequence-ℝ : (l : Level) → UU (lsuc l) cauchy-sequence-ℝ l = cauchy-sequence-Metric-Space (metric-space-ℝ l) ``` diff --git a/src/real-numbers/convergent-series-real-numbers.lagda.md b/src/real-numbers/convergent-series-real-numbers.lagda.md deleted file mode 100644 index 9c8b3bd2db..0000000000 --- a/src/real-numbers/convergent-series-real-numbers.lagda.md +++ /dev/null @@ -1,40 +0,0 @@ -# Convergent series of real numbers - -```agda -{-# OPTIONS --lossy-unification #-} - -module real-numbers.convergent-series-real-numbers where -``` - -
Imports - -```agda -open import analysis.convergent-series-metric-abelian-groups - -open import foundation.propositions -open import foundation.universe-levels - -open import real-numbers.dedekind-real-numbers -open import real-numbers.series-real-numbers -``` - -
- -## Idea - -A [series](real-numbers.series-real-numbers.md) of -[real numbers](real-numbers.dedekind-real-numbers.md) -{{#concept "converges" Disambiguation="series of real numbers" Agda=is-sum-series-ℝ}} -to `x` if the sequence of its partial sums -[converges](metric-spaces.limits-of-sequences-metric-spaces.md) to `x` in the -[standard metric space of real numbers](real-numbers.metric-space-of-real-numbers.md). - -## Definition - -```agda -is-sum-prop-series-ℝ : {l : Level} → series-ℝ l → ℝ l → Prop l -is-sum-prop-series-ℝ = is-sum-prop-series-Metric-Ab - -is-sum-series-ℝ : {l : Level} → series-ℝ l → ℝ l → UU l -is-sum-series-ℝ = is-sum-series-Metric-Ab -``` diff --git a/src/real-numbers/geometric-sequences-real-numbers.lagda.md b/src/real-numbers/geometric-sequences-real-numbers.lagda.md index a868836657..f5625e7f4e 100644 --- a/src/real-numbers/geometric-sequences-real-numbers.lagda.md +++ b/src/real-numbers/geometric-sequences-real-numbers.lagda.md @@ -9,6 +9,9 @@ module real-numbers.geometric-sequences-real-numbers where
Imports ```agda +open import analysis.convergent-series-real-numbers +open import analysis.series-real-numbers + open import commutative-algebra.geometric-sequences-commutative-rings open import elementary-number-theory.natural-numbers @@ -27,7 +30,6 @@ open import metric-spaces.uniformly-continuous-functions-metric-spaces open import real-numbers.absolute-value-real-numbers open import real-numbers.apartness-real-numbers -open import real-numbers.convergent-series-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers open import real-numbers.isometry-difference-real-numbers @@ -41,7 +43,6 @@ open import real-numbers.nonzero-real-numbers open import real-numbers.powers-real-numbers open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers -open import real-numbers.series-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.strict-inequality-real-numbers open import real-numbers.uniformly-continuous-functions-real-numbers diff --git a/src/real-numbers/inequality-real-numbers.lagda.md b/src/real-numbers/inequality-real-numbers.lagda.md index 1d9d46febf..d44ee49da3 100644 --- a/src/real-numbers/inequality-real-numbers.lagda.md +++ b/src/real-numbers/inequality-real-numbers.lagda.md @@ -328,6 +328,21 @@ module _ preserves-leq-right-sim-ℝ : leq-ℝ z x → leq-ℝ z y preserves-leq-right-sim-ℝ z≤x q qImports ```agda +open import analysis.complete-metric-abelian-groups open import analysis.metric-abelian-groups open import foundation.dependent-pair-types @@ -16,6 +17,7 @@ open import foundation.universe-levels open import metric-spaces.pseudometric-spaces +open import real-numbers.cauchy-completeness-dedekind-real-numbers open import real-numbers.isometry-addition-real-numbers open import real-numbers.isometry-negation-real-numbers open import real-numbers.large-additive-group-of-real-numbers @@ -34,11 +36,16 @@ The [Dedekind real numbers](real-numbers.dedekind-real-numbers.md) form a ## Definition ```agda -metric-ab-ℝ : (l : Level) → Metric-Ab (lsuc l) l -metric-ab-ℝ l = +metric-ab-add-ℝ : (l : Level) → Metric-Ab (lsuc l) l +metric-ab-add-ℝ l = ( ab-add-ℝ l , structure-Pseudometric-Space (pseudometric-space-ℝ l) , is-extensional-pseudometric-space-ℝ , is-isometry-neg-ℝ , is-isometry-left-add-ℝ) + +complete-metric-ab-add-ℝ : (l : Level) → Complete-Metric-Ab (lsuc l) l +complete-metric-ab-add-ℝ l = + ( metric-ab-add-ℝ l , + is-complete-metric-space-ℝ l) ``` diff --git a/src/real-numbers/positive-real-numbers.lagda.md b/src/real-numbers/positive-real-numbers.lagda.md index e0b81e741e..d14d3b0658 100644 --- a/src/real-numbers/positive-real-numbers.lagda.md +++ b/src/real-numbers/positive-real-numbers.lagda.md @@ -9,6 +9,10 @@ module real-numbers.positive-real-numbers where
Imports ```agda +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.positive-integers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-positive-rational-numbers @@ -253,6 +257,32 @@ one-ℝ⁺ : ℝ⁺ lzero one-ℝ⁺ = positive-real-ℚ⁺ one-ℚ⁺ ``` +### The canonical embedding of integers preserves positivity + +```agda +abstract + preserves-is-positive-real-ℤ : + {x : ℤ} → is-positive-ℤ x → is-positive-ℝ (real-ℤ x) + preserves-is-positive-real-ℤ pos-x = + preserves-is-positive-real-ℚ (is-positive-rational-ℤ pos-x) + +positive-real-ℤ⁺ : ℤ⁺ → ℝ⁺ lzero +positive-real-ℤ⁺ (x , pos-x) = (real-ℤ x , preserves-is-positive-real-ℤ pos-x) +``` + +### The canonical embedding of a nonzero natural number is positive + +```agda +abstract + is-positive-real-is-nonzero-ℕ : + {n : ℕ} → is-nonzero-ℕ n → is-positive-ℝ (real-ℕ n) + is-positive-real-is-nonzero-ℕ n≠0 = + preserves-is-positive-real-ℤ (is-positive-int-is-nonzero-ℕ _ n≠0) + +positive-real-ℕ⁺ : ℕ⁺ → ℝ⁺ lzero +positive-real-ℕ⁺ (n , n≠0) = (real-ℕ n , is-positive-real-is-nonzero-ℕ n≠0) +``` + ### `x` is positive if and only if there exists a positive rational number it is not less than or equal to ```agda diff --git a/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md b/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md index 69f3a5fb11..ef8ef84722 100644 --- a/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/saturation-inequality-nonnegative-real-numbers.lagda.md @@ -57,15 +57,16 @@ module _ ### If a nonnegative real number is less than or equal to all positive rational numbers, it is similar to zero ```agda -sim-zero-le-positive-rational-ℝ⁰⁺ : - {l : Level} (x : ℝ⁰⁺ l) → - ((ε : ℚ⁺) → leq-ℝ⁰⁺ x (nonnegative-real-ℚ⁺ ε)) → - sim-zero-ℝ⁰⁺ x -sim-zero-le-positive-rational-ℝ⁰⁺ x H = - sim-sim-leq-ℝ - ( leq-zero-ℝ⁰⁺ x , - saturated-leq-ℝ⁰⁺ - ( x) - ( zero-ℝ⁰⁺) - ( λ ε → inv-tr (leq-ℝ⁰⁺ x) (left-unit-law-add-ℝ⁰⁺ _) (H ε))) +abstract + sim-zero-leq-positive-rational-ℝ⁰⁺ : + {l : Level} (x : ℝ⁰⁺ l) → + ((ε : ℚ⁺) → leq-ℝ⁰⁺ x (nonnegative-real-ℚ⁺ ε)) → + sim-zero-ℝ⁰⁺ x + sim-zero-leq-positive-rational-ℝ⁰⁺ x H = + sim-sim-leq-ℝ + ( leq-zero-ℝ⁰⁺ x , + saturated-leq-ℝ⁰⁺ + ( x) + ( zero-ℝ⁰⁺) + ( λ ε → inv-tr (leq-ℝ⁰⁺ x) (left-unit-law-add-ℝ⁰⁺ _) (H ε))) ``` diff --git a/src/real-numbers/series-real-numbers.lagda.md b/src/real-numbers/series-real-numbers.lagda.md deleted file mode 100644 index f3d0ecf21e..0000000000 --- a/src/real-numbers/series-real-numbers.lagda.md +++ /dev/null @@ -1,42 +0,0 @@ -# Series of real numbers - -```agda -{-# OPTIONS --lossy-unification #-} - -module real-numbers.series-real-numbers where -``` - -
Imports - -```agda -open import analysis.series-metric-abelian-groups - -open import foundation.universe-levels - -open import lists.sequences - -open import real-numbers.dedekind-real-numbers -open import real-numbers.metric-abelian-group-of-real-numbers -``` - -
- -## Idea - -A {{#concept "series" Disambiguation="of real numbers" Agda=series-ℝ}} of -[real numbers](real-numbers.dedekind-real-numbers.md) is an infinite sum -$$∑_{n=0}^∞ a_n$$, which is evaluated for convergence in the -[metric abelian group of real numbers](real-numbers.metric-abelian-group-of-real-numbers.md). - -## Definition - -```agda -series-ℝ : (l : Level) → UU (lsuc l) -series-ℝ l = series-Metric-Ab (metric-ab-ℝ l) - -series-terms-ℝ : {l : Level} → sequence (ℝ l) → series-ℝ l -series-terms-ℝ = series-terms-Metric-Ab - -terms-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l) -terms-series-ℝ = term-series-Metric-Ab -```