diff --git a/config/codespell-dictionary.txt b/config/codespell-dictionary.txt index 42eb42d013..67d1419ed8 100644 --- a/config/codespell-dictionary.txt +++ b/config/codespell-dictionary.txt @@ -79,3 +79,4 @@ morphsims->morphisms outout->output ringr->ring ringrs->rings +semiorm->seminorm diff --git a/src/analysis.lagda.md b/src/analysis.lagda.md index c3893468cc..1e84df96c0 100644 --- a/src/analysis.lagda.md +++ b/src/analysis.lagda.md @@ -3,8 +3,22 @@ ```agda module analysis where +open import analysis.absolute-convergence-series-real-banach-spaces public +open import analysis.absolute-convergence-series-real-numbers public +open import analysis.comparison-test-series-real-numbers public +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.derivatives-of-real-functions-on-proper-closed-intervals public open import analysis.metric-abelian-groups public +open import analysis.metric-abelian-groups-normed-real-vector-spaces public +open import analysis.ratio-test-series-real-banach-spaces public +open import analysis.ratio-test-series-real-numbers 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/absolute-convergence-series-real-banach-spaces.lagda.md b/src/analysis/absolute-convergence-series-real-banach-spaces.lagda.md new file mode 100644 index 0000000000..bf41a0115c --- /dev/null +++ b/src/analysis/absolute-convergence-series-real-banach-spaces.lagda.md @@ -0,0 +1,202 @@ +# Absolute convergence of series in real Banach spaces + +```agda +module analysis.absolute-convergence-series-real-banach-spaces where +``` + +
Imports + +```agda +open import analysis.convergent-series-real-banach-spaces +open import analysis.convergent-series-real-numbers +open import analysis.series-real-banach-spaces +open import analysis.series-real-numbers + +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 elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import linear-algebra.real-banach-spaces +open import linear-algebra.sums-of-finite-sequences-of-elements-real-banach-spaces + +open import order-theory.large-posets + +open import real-numbers.cauchy-sequences-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.distance-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.rational-real-numbers +``` + +
+ +## Idea + +A [series](analysis.series-real-banach-spaces.md) `Σ aₙ` in a +[real Banach space](linear-algebra.real-banach-spaces.md) is said to +{{#concept "absolutely converge" WDID=Q332465 WD="absolute convergence" Agda=is-absolutely-convergent-prop-series-ℝ-Banach-Space Disambiguation="series in a real Banach space"}} +if the series of norms `Σ ∥aₙ∥` is a +[convergent series](analysis.convergent-series-real-numbers.md) of +[real numbers](real-numbers.dedekind-real-numbers.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + (σ : series-ℝ-Banach-Space V) + where + + is-absolutely-convergent-prop-series-ℝ-Banach-Space : Prop (lsuc l1) + is-absolutely-convergent-prop-series-ℝ-Banach-Space = + is-convergent-prop-series-ℝ (map-norm-series-ℝ-Banach-Space V σ) + + is-absolutely-convergent-series-ℝ-Banach-Space : UU (lsuc l1) + is-absolutely-convergent-series-ℝ-Banach-Space = + type-Prop is-absolutely-convergent-prop-series-ℝ-Banach-Space +``` + +## Properties + +### If a series is absolutely convergent, it is convergent + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + (σ : series-ℝ-Banach-Space V) + where + + is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space : + is-absolutely-convergent-series-ℝ-Banach-Space V σ → + is-convergent-series-ℝ-Banach-Space V σ + is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space (lim-Σnorm , H) = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + open + do-syntax-trunc-Prop + ( is-convergent-prop-series-ℝ-Banach-Space V σ) + in do + cauchy-mod ← + exists-cauchy-modulus-has-limit-sequence-ℝ + ( partial-sum-series-ℝ (map-norm-series-ℝ-Banach-Space V σ)) + ( lim-Σnorm , H) + let + μ = pr1 ∘ cauchy-mod + is-mod-μ = pr2 ∘ cauchy-mod + lemma : + (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (μ ε) n → + leq-ℝ + ( dist-ℝ-Banach-Space V + ( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ k)) + ( partial-sum-series-ℝ-Banach-Space V σ n)) + ( real-ℚ⁺ ε) + lemma ε n k με≤n = + chain-of-inequalities + dist-ℝ-Banach-Space V + ( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ k)) + ( partial-sum-series-ℝ-Banach-Space V σ n) + ≤ map-norm-ℝ-Banach-Space V + ( partial-sum-series-ℝ-Banach-Space V + ( drop-series-ℝ-Banach-Space V n σ) + ( k)) + by + leq-eq-ℝ + ( ap + ( map-norm-ℝ-Banach-Space V) + ( inv (partial-sum-drop-series-ℝ-Banach-Space V n σ k))) + ≤ partial-sum-series-ℝ + ( map-norm-series-ℝ-Banach-Space V + ( drop-series-ℝ-Banach-Space V n σ)) + ( k) + by + triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space + ( V) + ( k) + ( _) + ≤ ( partial-sum-series-ℝ + ( map-norm-series-ℝ-Banach-Space V σ) + ( n +ℕ k)) -ℝ + ( partial-sum-series-ℝ (map-norm-series-ℝ-Banach-Space V σ) n) + by + leq-eq-ℝ + ( partial-sum-drop-series-ℝ + ( n) + ( map-norm-series-ℝ-Banach-Space V σ) + ( k)) + ≤ dist-ℝ + ( partial-sum-series-ℝ + ( map-norm-series-ℝ-Banach-Space V σ) + ( n +ℕ k)) + ( partial-sum-series-ℝ + ( map-norm-series-ℝ-Banach-Space V σ) + ( n)) + by leq-diff-dist-ℝ _ _ + ≤ real-ℚ⁺ ε + by + leq-dist-neighborhood-ℝ + ( ε) + ( _) + ( _) + ( is-mod-μ + ( ε) + ( n +ℕ k) + ( n) + ( transitive-leq-ℕ (μ ε) n (n +ℕ k) (leq-add-ℕ n k) με≤n) + ( με≤n)) + lemma' : + (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (μ ε) n → leq-ℕ n k → + leq-ℝ + ( dist-ℝ-Banach-Space V + ( partial-sum-series-ℝ-Banach-Space V σ k) + ( partial-sum-series-ℝ-Banach-Space V σ n)) + ( real-ℚ⁺ ε) + lemma' ε n k με≤n n≤k = + let + (l , l+n=k) = subtraction-leq-ℕ n k n≤k + in + tr + ( λ p → + leq-ℝ + ( dist-ℝ-Banach-Space V + ( partial-sum-series-ℝ-Banach-Space V σ p) + ( _)) + ( _)) + ( commutative-add-ℕ n l ∙ l+n=k) + ( lemma ε n l με≤n) + is-convergent-is-cauchy-sequence-partial-sum-series-ℝ-Banach-Space + ( V) + ( σ) + ( λ ε → + ( μ ε , + λ a b με≤a με≤b → + rec-coproduct + ( λ a≤b → + tr + ( λ d → leq-ℝ d (real-ℚ⁺ ε)) + ( commutative-dist-ℝ-Banach-Space V _ _) + ( lemma' ε a b με≤a a≤b)) + ( lemma' ε b a με≤b) + ( linear-leq-ℕ a b))) +``` + +## See also + +- [Absolute convergence of series of real numbers](analysis.absolute-convergence-series-real-numbers.md) + +## External links + +- [Absolute convergence of series in Banach spaces](https://en.wikipedia.org/wiki/Absolute_convergence#Proof_that_any_absolutely_convergent_series_in_a_Banach_space_is_convergent) + on Wikipedia diff --git a/src/analysis/absolute-convergence-series-real-numbers.lagda.md b/src/analysis/absolute-convergence-series-real-numbers.lagda.md new file mode 100644 index 0000000000..309cbb81ea --- /dev/null +++ b/src/analysis/absolute-convergence-series-real-numbers.lagda.md @@ -0,0 +1,80 @@ +# Absolute convergence of series in the real numbers + +```agda +module analysis.absolute-convergence-series-real-numbers where +``` + +
Imports + +```agda +open import analysis.absolute-convergence-series-real-banach-spaces +open import analysis.convergent-series-real-banach-spaces +open import analysis.convergent-series-real-numbers +open import analysis.series-real-banach-spaces +open import analysis.series-real-numbers + +open import foundation.propositions +open import foundation.universe-levels + +open import linear-algebra.real-banach-spaces +``` + +
+ +## Idea + +A [series](analysis.series-real-numbers.md) `Σ aₙ` of +[real numbers](real-numbers.dedekind-real-numbers.md) is said to +{{#concept "absolutely converge" WDID=Q332465 WD="absolute convergence" Agda=is-absolutely-convergent-prop-series-ℝ Disambiguation="series of real numbers"}} +if the series of absolute values `Σ |aₙ|` +[converges](analysis.convergent-series-real-numbers.md). + +## Definition + +```agda +module _ + {l : Level} + (σ : series-ℝ l) + where + + is-absolutely-convergent-prop-series-ℝ : Prop (lsuc l) + is-absolutely-convergent-prop-series-ℝ = + is-convergent-prop-series-ℝ (map-abs-series-ℝ σ) + + is-absolutely-convergent-series-ℝ : UU (lsuc l) + is-absolutely-convergent-series-ℝ = + type-Prop is-absolutely-convergent-prop-series-ℝ +``` + +## Properties + +### If a series of real numbers is absolutely convergent, it is convergent + +```agda +module _ + {l : Level} + (σ : series-ℝ l) + where + + is-convergent-is-absolutely-convergent-series-ℝ : + is-absolutely-convergent-series-ℝ σ → + is-convergent-series-ℝ σ + is-convergent-is-absolutely-convergent-series-ℝ H = + is-convergent-real-is-convergent-real-banach-space-ℝ + ( term-series-ℝ σ) + ( is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space + ( real-banach-space-ℝ l) + ( series-terms-ℝ-Banach-Space + ( real-banach-space-ℝ l) + ( term-series-ℝ σ)) + ( H)) +``` + +## See also + +- [Absolute convergence of series in real Banach spaces](analysis.absolute-convergence-series-real-banach-spaces.md) + +## External links + +- [Absolute convergence](https://en.wikipedia.org/wiki/Absolute_convergence) on + Wikipedia diff --git a/src/analysis/comparison-test-series-real-numbers.lagda.md b/src/analysis/comparison-test-series-real-numbers.lagda.md new file mode 100644 index 0000000000..dbc9581cb5 --- /dev/null +++ b/src/analysis/comparison-test-series-real-numbers.lagda.md @@ -0,0 +1,199 @@ +# Comparison test for series in the real numbers + +```agda +module analysis.comparison-test-series-real-numbers where +``` + +
Imports + +```agda +open import analysis.convergent-series-real-numbers +open import analysis.series-real-numbers + +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.binary-transport +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.universe-levels + +open import metric-spaces.cauchy-sequences-metric-spaces + +open import order-theory.large-posets + +open import real-numbers.difference-real-numbers +open import real-numbers.distance-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.sums-of-finite-sequences-of-real-numbers + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +A [series](analysis.series-real-numbers.md) `∑ aₙ` of +[nonnegative](real-numbers.nonnegative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) +[converges](analysis.convergent-series-real-numbers.md) if there +[exists](foundation.existential-quantification.md) a convergent series `∑ bₙ` +such that `aₙ ≤ bₙ` for all `n`. + +## Definition + +```agda +module _ + {l1 : Level} + (l2 : Level) + (σ : series-ℝ l1) + where + + comparison-test-prop-series-ℝ : Prop (l1 ⊔ lsuc l2) + comparison-test-prop-series-ℝ = + ( is-nonnegative-prop-series-ℝ σ) ∧ + ( ∃ + ( convergent-series-ℝ l2) + ( λ τ → + Π-Prop + ( ℕ) + ( λ n → + leq-prop-ℝ (term-series-ℝ σ n) (term-convergent-series-ℝ τ n)))) + + comparison-test-series-ℝ : UU (l1 ⊔ lsuc l2) + comparison-test-series-ℝ = + type-Prop comparison-test-prop-series-ℝ +``` + +## Properties + +### The comparison test implies convergence + +```agda +module _ + {l1 l2 : Level} + (σ : series-ℝ l1) + (τ : convergent-series-ℝ l2) + where + + abstract + is-convergent-is-nonnegative-is-bounded-by-convergent-series-ℝ : + ((n : ℕ) → is-nonnegative-ℝ (term-series-ℝ σ n)) → + ((n : ℕ) → leq-ℝ (term-series-ℝ σ n) (term-convergent-series-ℝ τ n)) → + is-convergent-series-ℝ σ + is-convergent-is-nonnegative-is-bounded-by-convergent-series-ℝ 0≤σₙ σₙ≤τₙ = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + open do-syntax-trunc-Prop (is-convergent-prop-series-ℝ σ) + in do + lim-modulus-τ ← is-sum-sum-convergent-series-ℝ τ + let + cauchy-mod-partial-sum-τ = + is-cauchy-has-limit-modulus-sequence-Metric-Space + ( metric-space-ℝ l2) + ( partial-sum-convergent-series-ℝ τ) + ( sum-convergent-series-ℝ τ) + ( lim-modulus-τ) + μ = pr1 ∘ cauchy-mod-partial-sum-τ + is-mod-μ = pr2 ∘ cauchy-mod-partial-sum-τ + is-mod'-μ ε n k με≤n = + neighborhood-dist-ℝ ε _ _ + ( leq-dist-leq-diff-ℝ _ _ _ + ( chain-of-inequalities + partial-sum-series-ℝ σ (n +ℕ k) -ℝ partial-sum-series-ℝ σ n + ≤ partial-sum-series-ℝ (drop-series-ℝ n σ) k + by leq-eq-ℝ (inv (partial-sum-drop-series-ℝ n σ k)) + ≤ partial-sum-series-ℝ + ( drop-series-ℝ n (series-convergent-series-ℝ τ)) + ( k) + by + leq-sum-fin-sequence-ℝ k _ _ + ( λ m → σₙ≤τₙ (n +ℕ nat-Fin k m)) + ≤ ( partial-sum-convergent-series-ℝ τ (n +ℕ k)) -ℝ + ( partial-sum-convergent-series-ℝ τ n) + by + leq-eq-ℝ + ( partial-sum-drop-series-ℝ + ( n) + ( series-convergent-series-ℝ τ) + ( k)) + ≤ dist-ℝ + ( partial-sum-convergent-series-ℝ τ (n +ℕ k)) + ( partial-sum-convergent-series-ℝ τ n) + by leq-diff-dist-ℝ _ _ + ≤ real-ℚ⁺ ε + by + leq-dist-neighborhood-ℝ ε _ _ + ( is-mod-μ + ( ε) + ( n +ℕ k) + ( n) + ( transitive-leq-ℕ + ( μ ε) + ( n) + ( n +ℕ k) + ( leq-add-ℕ n k) + ( με≤n)) + ( με≤n))) + ( transitive-leq-ℝ + ( partial-sum-series-ℝ σ n -ℝ partial-sum-series-ℝ σ (n +ℕ k)) + ( zero-ℝ) + ( real-ℚ⁺ ε) + ( is-nonnegative-real-ℝ⁰⁺ (nonnegative-real-ℚ⁺ ε)) + ( binary-tr + ( leq-ℝ) + ( distributive-neg-diff-ℝ _ _) + ( neg-zero-ℝ) + ( neg-leq-ℝ + ( is-nonnegative-diff-leq-ℝ + ( is-monotonic-partial-sum-is-nonnegative-term-series-ℝ + ( σ) + ( 0≤σₙ) + ( n) + ( n +ℕ k) + ( leq-add-ℕ n k))))))) + is-convergent-is-cauchy-sequence-partial-sum-series-ℝ + σ + ( λ ε → + ( μ ε , + is-cauchy-modulus-is-cauchy-modulus-sequence-Metric-Space' + ( metric-space-ℝ l1) + ( partial-sum-series-ℝ σ) + ( ε) + ( μ ε) + ( is-mod'-μ ε))) + +module _ + {l1 l2 : Level} + (σ : series-ℝ l1) + where + + is-convergent-comparison-test-series-ℝ : + {l2 : Level} → comparison-test-series-ℝ l2 σ → is-convergent-series-ℝ σ + is-convergent-comparison-test-series-ℝ (0≤σₙ , ∃τ) = + rec-trunc-Prop + ( is-convergent-prop-series-ℝ σ) + ( λ (τ , σₙ≤τₙ) → + is-convergent-is-nonnegative-is-bounded-by-convergent-series-ℝ + ( σ) + ( τ) + ( 0≤σₙ) + ( σₙ≤τₙ)) + ( ∃τ) +``` + +## External links + +- [Direct comparison test](https://en.wikipedia.org/wiki/Direct_comparison_test) + on Wikipedia 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..f4a8f90448 --- /dev/null +++ b/src/analysis/convergent-series-complete-metric-abelian-groups.lagda.md @@ -0,0 +1,85 @@ +# 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.subtypes +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 σ + +convergent-series-Complete-Metric-Ab : + {l1 l2 : Level} (G : Complete-Metric-Ab l1 l2) → UU (l1 ⊔ l2) +convergent-series-Complete-Metric-Ab G = + type-subtype (is-convergent-prop-series-Complete-Metric-Ab G) +``` + +## 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-metric-abelian-groups.lagda.md b/src/analysis/convergent-series-metric-abelian-groups.lagda.md index d78cf2b8bd..30673b9085 100644 --- a/src/analysis/convergent-series-metric-abelian-groups.lagda.md +++ b/src/analysis/convergent-series-metric-abelian-groups.lagda.md @@ -10,9 +10,19 @@ module analysis.convergent-series-metric-abelian-groups where open import analysis.metric-abelian-groups open import analysis.series-metric-abelian-groups +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.action-on-identifications-functions +open import foundation.binary-transport open import foundation.dependent-pair-types +open import foundation.functoriality-propositional-truncation +open import foundation.identity-types +open import foundation.logical-equivalences open import foundation.propositions open import foundation.subtypes +open import foundation.transport-along-identifications open import foundation.universe-levels open import lists.sequences @@ -79,7 +89,7 @@ module _ partial-sum-series-Metric-Ab series-convergent-series-Metric-Ab ``` -## The partial sums of a convergent series have a limit, the sum of the series +### The partial sums of a convergent series have a limit, the sum of the series ```agda module _ @@ -111,3 +121,79 @@ module _ ( partial-sum-convergent-series-Metric-Ab G σ) ( has-limit-partial-sum-convergent-series-Metric-Ab) ``` + +### A series converges if and only if it converges after dropping a finite number of terms + +```agda +module _ + {l1 l2 : Level} + {G : Metric-Ab l1 l2} + (σ : series-Metric-Ab G) + (k : ℕ) + where + + is-convergent-is-convergent-drop-series-ℝ : + is-convergent-series-Metric-Ab (drop-series-Metric-Ab k σ) → + is-convergent-series-Metric-Ab σ + is-convergent-is-convergent-drop-series-ℝ (lim-drop , is-lim-drop) = + ( add-Metric-Ab G (partial-sum-series-Metric-Ab σ k) lim-drop , + map-trunc-Prop + ( λ (μ , is-mod-μ) → + ( ( λ ε → μ ε +ℕ k) , + ( λ ε n με+k≤n → + let + (l , l+k=n) = + subtraction-leq-ℕ + ( k) + ( n) + ( transitive-leq-ℕ + ( k) + ( μ ε +ℕ k) + ( n) + ( με+k≤n) + ( leq-add-ℕ' k (μ ε))) + in + tr + ( λ x → neighborhood-Metric-Ab G ε x _) + ( equational-reasoning + add-Metric-Ab G + ( partial-sum-series-Metric-Ab σ k) + ( partial-sum-series-Metric-Ab + ( drop-series-Metric-Ab k σ) + ( l)) + ＝ + add-Metric-Ab G + ( partial-sum-series-Metric-Ab σ k) + ( diff-Metric-Ab G + ( partial-sum-series-Metric-Ab σ (k +ℕ l)) + ( partial-sum-series-Metric-Ab σ k)) + by + ap-add-Metric-Ab G + ( refl) + ( partial-sum-drop-series-Metric-Ab k σ l) + ＝ partial-sum-series-Metric-Ab σ (k +ℕ l) + by is-identity-right-conjugation-Metric-Ab G _ _ + ＝ partial-sum-series-Metric-Ab σ n + by + ap + ( partial-sum-series-Metric-Ab σ) + ( commutative-add-ℕ k l ∙ l+k=n)) + ( forward-implication + ( is-isometry-add-Metric-Ab + ( G) + ( partial-sum-series-Metric-Ab σ k) + ( ε) + ( partial-sum-series-Metric-Ab + ( drop-series-Metric-Ab k σ) + ( l)) + ( lim-drop)) + ( is-mod-μ + ( ε) + ( l) + ( reflects-leq-left-add-ℕ + ( k) + ( μ ε) + ( l) + ( inv-tr (leq-ℕ (μ ε +ℕ k)) l+k=n με+k≤n))))))) + ( is-lim-drop)) +``` 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..3b590b5416 --- /dev/null +++ b/src/analysis/convergent-series-real-banach-spaces.lagda.md @@ -0,0 +1,140 @@ +# Convergent series in real Banach spaces + +```agda +module analysis.convergent-series-real-banach-spaces where +``` + +
Imports + +```agda +open import analysis.complete-metric-abelian-groups-real-banach-spaces +open import analysis.convergent-series-complete-metric-abelian-groups +open import analysis.convergent-series-metric-abelian-groups +open import analysis.convergent-series-real-numbers +open import analysis.series-real-banach-spaces +open import analysis.series-real-numbers + +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.logical-equivalences +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import linear-algebra.normed-real-vector-spaces +open import linear-algebra.real-banach-spaces + +open import lists.sequences + +open import metric-spaces.cauchy-sequences-metric-spaces +open import metric-spaces.limits-of-sequences-metric-spaces + +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.sums-of-finite-sequences-of-real-numbers + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## 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 σ + +convergent-series-ℝ-Banach-Space : + {l1 l2 : Level} (V : ℝ-Banach-Space l1 l2) → UU (l1 ⊔ l2) +convergent-series-ℝ-Banach-Space V = + type-subtype (is-convergent-prop-series-ℝ-Banach-Space V) +``` + +## 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) + ( σ) +``` + +### A series in the real Banach space of real numbers converges if and only if its corresponding series of real numbers converges + +```agda +module _ + {l : Level} + (σ : sequence (ℝ l)) + where + + is-convergent-real-is-convergent-real-banach-space-ℝ : + is-convergent-series-ℝ-Banach-Space + ( real-banach-space-ℝ l) + ( series-terms-ℝ-Banach-Space (real-banach-space-ℝ l) σ) → + is-convergent-series-ℝ (series-terms-ℝ σ) + is-convergent-real-is-convergent-real-banach-space-ℝ (lim , is-lim) = + ( lim , + preserves-limits-sequence-isometry-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l)) + ( metric-space-ℝ l) + ( id , λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y)) + ( λ n → sum-fin-sequence-ℝ n (σ ∘ nat-Fin n)) + ( lim) + ( is-lim)) + + is-convergent-real-banach-space-is-convergent-ℝ : + is-convergent-series-ℝ (series-terms-ℝ σ) → + is-convergent-series-ℝ-Banach-Space + ( real-banach-space-ℝ l) + ( series-terms-ℝ-Banach-Space (real-banach-space-ℝ l) σ) + is-convergent-real-banach-space-is-convergent-ℝ (lim , is-lim) = + ( lim , + preserves-limits-sequence-isometry-Metric-Space + ( metric-space-ℝ l) + ( metric-space-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l)) + ( id , λ d x y → neighborhood-iff-leq-dist-ℝ d x y) + ( λ n → sum-fin-sequence-ℝ n (σ ∘ nat-Fin n)) + ( lim) + ( is-lim)) +``` 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..9979c39ed9 --- /dev/null +++ b/src/analysis/convergent-series-real-numbers.lagda.md @@ -0,0 +1,103 @@ +# 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.dependent-pair-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import lists.sequences + +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 σ + +convergent-series-ℝ : (l : Level) → UU (lsuc l) +convergent-series-ℝ l = type-subtype (is-convergent-prop-series-ℝ {l}) + +module _ + {l : Level} + (σ : convergent-series-ℝ l) + where + + series-convergent-series-ℝ : series-ℝ l + series-convergent-series-ℝ = pr1 σ + + term-convergent-series-ℝ : sequence (ℝ l) + term-convergent-series-ℝ = term-series-ℝ series-convergent-series-ℝ + + sum-convergent-series-ℝ : ℝ l + sum-convergent-series-ℝ = pr1 (pr2 σ) + + is-sum-sum-convergent-series-ℝ : + is-sum-series-ℝ series-convergent-series-ℝ sum-convergent-series-ℝ + is-sum-sum-convergent-series-ℝ = pr2 (pr2 σ) + + partial-sum-convergent-series-ℝ : sequence (ℝ l) + partial-sum-convergent-series-ℝ = + partial-sum-series-ℝ series-convergent-series-ℝ +``` + +## 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..5cdee85e20 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) @@ -98,6 +107,11 @@ module _ commutative-add-Metric-Ab : (x y : type-Metric-Ab MG) → add-Metric-Ab x y ＝ add-Metric-Ab y x commutative-add-Metric-Ab = commutative-add-Ab (ab-Metric-Ab MG) + + is-identity-right-conjugation-Metric-Ab : + (x y : type-Metric-Ab MG) → add-Metric-Ab x (diff-Metric-Ab y x) ＝ y + is-identity-right-conjugation-Metric-Ab = + is-identity-right-conjugation-Ab (ab-Metric-Ab MG) ``` ### Metric properties of metric abelian groups diff --git a/src/analysis/ratio-test-series-real-banach-spaces.lagda.md b/src/analysis/ratio-test-series-real-banach-spaces.lagda.md new file mode 100644 index 0000000000..53ccad85e8 --- /dev/null +++ b/src/analysis/ratio-test-series-real-banach-spaces.lagda.md @@ -0,0 +1,115 @@ +# The ratio test for series in real Banach spaces + +```agda +module analysis.ratio-test-series-real-banach-spaces where +``` + +
Imports + +```agda +open import analysis.absolute-convergence-series-real-banach-spaces +open import analysis.convergent-series-real-banach-spaces +open import analysis.ratio-test-series-real-numbers +open import analysis.series-real-banach-spaces + +open import elementary-number-theory.natural-numbers + +open import foundation.binary-transport +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.propositions +open import foundation.universe-levels + +open import linear-algebra.real-banach-spaces + +open import logic.functoriality-existential-quantification + +open import real-numbers.absolute-value-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.strict-inequality-nonnegative-real-numbers +``` + +
+ +## Idea + +To prove that a [series](analysis.series-real-banach-spaces.md) `∑ aₙ` in a +[real Banach space](linear-algebra.real-banach-spaces.md) +[converges](analysis.series-real-numbers.md), it is sufficient to show that +[there exists](foundation.existential-quantification.md) a +[nonnegative](real-numbers.nonnegative-real-numbers.md) real number `r` +[less than](real-numbers.strict-inequality-real-numbers.md) 1 such that for all +`n`, `∥aₙ₊₁∥ ≤ r∥aₙ∥`. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + (σ : series-ℝ-Banach-Space V) + where + + ratio-test-prop-series-ℝ-Banach-Space : Prop (lsuc l1) + ratio-test-prop-series-ℝ-Banach-Space = + ∃ ( ℝ⁰⁺ l1) + ( λ r → + le-prop-ℝ⁰⁺ r one-ℝ⁰⁺ ∧ + Π-Prop + ( ℕ) + ( λ n → + leq-prop-ℝ + ( map-norm-ℝ-Banach-Space V + ( term-series-ℝ-Banach-Space V σ (succ-ℕ n))) + ( ( real-ℝ⁰⁺ r) *ℝ + ( map-norm-ℝ-Banach-Space V + ( term-series-ℝ-Banach-Space V σ n))))) + + ratio-test-series-ℝ-Banach-Space : UU (lsuc l1) + ratio-test-series-ℝ-Banach-Space = + type-Prop ratio-test-prop-series-ℝ-Banach-Space +``` + +## Properties + +### The ratio test implies convergence + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + (σ : series-ℝ-Banach-Space V) + where + + abstract + is-convergent-ratio-test-series-ℝ-Banach-Space : + ratio-test-series-ℝ-Banach-Space V σ → + is-convergent-series-ℝ-Banach-Space V σ + is-convergent-ratio-test-series-ℝ-Banach-Space H = + is-convergent-is-absolutely-convergent-series-ℝ-Banach-Space + ( V) + ( σ) + ( is-convergent-ratio-test-series-ℝ + ( map-norm-series-ℝ-Banach-Space V σ) + ( map-tot-exists + ( λ r (r<1 , K) → + ( r<1 , + λ n → + binary-tr + ( leq-ℝ) + ( inv (abs-real-ℝ⁰⁺ (nonnegative-norm-ℝ-Banach-Space V _))) + ( ap-mul-ℝ + ( refl) + ( inv + ( abs-real-ℝ⁰⁺ (nonnegative-norm-ℝ-Banach-Space V _)))) + ( K n))) + ( H))) +``` + +## See also + +- [The ratio test for series of real numbers](analysis.ratio-test-series-real-numbers.md) diff --git a/src/analysis/ratio-test-series-real-numbers.lagda.md b/src/analysis/ratio-test-series-real-numbers.lagda.md new file mode 100644 index 0000000000..13d7ff672b --- /dev/null +++ b/src/analysis/ratio-test-series-real-numbers.lagda.md @@ -0,0 +1,142 @@ +# The ratio test for series in the real numbers + +```agda +module analysis.ratio-test-series-real-numbers where +``` + +
Imports + +```agda +open import analysis.absolute-convergence-series-real-numbers +open import analysis.comparison-test-series-real-numbers +open import analysis.convergent-series-real-numbers +open import analysis.series-real-numbers + +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.natural-numbers + +open import foundation.cartesian-product-types +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import order-theory.large-posets + +open import real-numbers.absolute-value-real-numbers +open import real-numbers.geometric-sequences-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.multiplication-nonnegative-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.powers-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-nonnegative-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +To prove that a [series](analysis.series-real-numbers.md) `∑ aₙ` of +[real numbers](real-numbers.dedekind-real-numbers.md) +[converges](analysis.convergent-series-real-numbers.md), it is sufficient to +show that [there exists](foundation.existential-quantification.md) a +[nonnegative](real-numbers.nonnegative-real-numbers.md) real number `r` +[less than](real-numbers.strict-inequality-real-numbers.md) 1 such that for all +`n`, `|aₙ₊₁| ≤ r|aₙ|`. + +## Definition + +```agda +module _ + {l : Level} + (σ : series-ℝ l) + where + + ratio-test-prop-series-ℝ : Prop (lsuc l) + ratio-test-prop-series-ℝ = + ∃ ( ℝ⁰⁺ l) + ( λ r → + le-prop-ℝ⁰⁺ r one-ℝ⁰⁺ ∧ + Π-Prop + ( ℕ) + ( λ n → + ( leq-prop-ℝ + ( abs-ℝ (term-series-ℝ σ (succ-ℕ n))) + ( real-ℝ⁰⁺ r *ℝ abs-ℝ (term-series-ℝ σ n))))) + + ratio-test-series-ℝ : UU (lsuc l) + ratio-test-series-ℝ = type-Prop ratio-test-prop-series-ℝ +``` + +## Properties + +### The ratio test implies convergence + +```agda +module _ + {l : Level} + (σ : series-ℝ l) + where + + abstract + is-convergent-ratio-test-series-ℝ : + ratio-test-series-ℝ σ → is-convergent-series-ℝ σ + is-convergent-ratio-test-series-ℝ H = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + open do-syntax-trunc-Prop (is-convergent-prop-series-ℝ σ) + in do + (r⁰⁺@(r , 0≤r) , r<1 , K) ← H + let |σ₀| = abs-ℝ (term-series-ℝ σ 0) + is-convergent-is-absolutely-convergent-series-ℝ + ( σ) + ( is-convergent-is-nonnegative-is-bounded-by-convergent-series-ℝ + ( map-abs-series-ℝ σ) + ( convergent-standard-geometric-series-ℝ + ( |σ₀|) + ( r) + ( inv-tr (λ x → le-ℝ x one-ℝ) (abs-real-ℝ⁰⁺ r⁰⁺) r<1)) + ( λ _ → is-nonnegative-abs-ℝ _) + ( ind-ℕ + ( refl-leq-ℝ _) + ( λ n |σₙ|≤arⁿ → + chain-of-inequalities + abs-ℝ (term-series-ℝ σ (succ-ℕ n)) + ≤ r *ℝ abs-ℝ (term-series-ℝ σ n) + by K n + ≤ r *ℝ seq-standard-geometric-sequence-ℝ |σ₀| r n + by preserves-leq-left-mul-ℝ⁰⁺ r⁰⁺ |σₙ|≤arⁿ + ≤ r *ℝ (|σ₀| *ℝ power-ℝ n r) + by + leq-eq-ℝ + ( ap-mul-ℝ + ( refl) + ( compute-standard-geometric-sequence-ℝ |σ₀| r n)) + ≤ |σ₀| *ℝ (r *ℝ power-ℝ n r) + by leq-eq-ℝ (left-swap-mul-ℝ _ _ _) + ≤ |σ₀| *ℝ power-ℝ (succ-ℕ n) r + by leq-eq-ℝ (ap-mul-ℝ refl (inv (power-succ-ℝ' n r))) + ≤ seq-standard-geometric-sequence-ℝ |σ₀| r (succ-ℕ n) + by + leq-eq-ℝ + ( inv + ( compute-standard-geometric-sequence-ℝ + ( |σ₀|) + ( r) + ( succ-ℕ n)))))) +``` + +## See also + +- [The ratio test for series in real Banach spaces](analysis.ratio-test-series-real-banach-spaces.md) + +## External links + +- [Ratio test](https://en.wikipedia.org/wiki/Ratio_test) on Wikipedia 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..12f7c30508 --- /dev/null +++ b/src/analysis/series-real-banach-spaces.lagda.md @@ -0,0 +1,111 @@ +# 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 analysis.series-real-numbers + +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.natural-numbers + +open import foundation.function-types +open import foundation.identity-types +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 +``` + +## Properties + +### The series of norms + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + (σ : series-ℝ-Banach-Space V) + where + + map-norm-series-ℝ-Banach-Space : series-ℝ l1 + map-norm-series-ℝ-Banach-Space = + series-terms-ℝ (map-norm-ℝ-Banach-Space V ∘ term-series-ℝ-Banach-Space V σ) +``` + +### Dropping terms from a series + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + where + + drop-series-ℝ-Banach-Space : + ℕ → series-ℝ-Banach-Space V → series-ℝ-Banach-Space V + drop-series-ℝ-Banach-Space = drop-series-Metric-Ab +``` + +### The partial sums of a series after dropping terms + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + where + + abstract + partial-sum-drop-series-ℝ-Banach-Space : + (n : ℕ) (σ : series-ℝ-Banach-Space V) (i : ℕ) → + partial-sum-series-ℝ-Banach-Space V + ( drop-series-ℝ-Banach-Space V n σ) + ( i) ＝ + diff-ℝ-Banach-Space V + ( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ i)) + ( partial-sum-series-ℝ-Banach-Space V σ n) + partial-sum-drop-series-ℝ-Banach-Space = partial-sum-drop-series-Metric-Ab +``` diff --git a/src/analysis/series-real-numbers.lagda.md b/src/analysis/series-real-numbers.lagda.md new file mode 100644 index 0000000000..a797c5ca4f --- /dev/null +++ b/src/analysis/series-real-numbers.lagda.md @@ -0,0 +1,124 @@ +# 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 elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.universe-levels + +open import lists.sequences + +open import order-theory.monotonic-sequences-posets + +open import real-numbers.absolute-value-real-numbers +open import real-numbers.addition-nonnegative-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-additive-group-of-real-numbers +open import real-numbers.nonnegative-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 +``` + +## Properties + +### The proposition that the terms of a series are nonnegative + +```agda +is-nonnegative-prop-series-ℝ : {l : Level} → series-ℝ l → Prop l +is-nonnegative-prop-series-ℝ σ = + Π-Prop ℕ (λ n → is-nonnegative-prop-ℝ (term-series-ℝ σ n)) + +is-nonnegative-series-ℝ : {l : Level} → series-ℝ l → UU l +is-nonnegative-series-ℝ σ = type-Prop (is-nonnegative-prop-series-ℝ σ) +``` + +### If the terms of a series of real numbers are nonnegative, the partial sums are monotonic + +```agda +abstract + is-monotonic-partial-sum-is-nonnegative-term-series-ℝ : + {l : Level} (σ : series-ℝ l) → + is-nonnegative-series-ℝ σ → + is-monotonic-sequence-Poset (ℝ-Poset l) (partial-sum-series-ℝ σ) + is-monotonic-partial-sum-is-nonnegative-term-series-ℝ {l} σ H = + is-monotonic-sequence-is-increasing-Poset + ( ℝ-Poset l) + ( partial-sum-series-ℝ σ) + ( λ n → leq-left-add-real-ℝ⁰⁺ _ (term-series-ℝ σ n , H n)) +``` + +### The series of absolute values + +```agda +module _ + {l : Level} + (σ : series-ℝ l) + where + + map-abs-series-ℝ : series-ℝ l + map-abs-series-ℝ = series-terms-ℝ (abs-ℝ ∘ term-series-ℝ σ) +``` + +### Dropping terms from a series + +```agda +module _ + {l : Level} + where + + drop-series-ℝ : ℕ → series-ℝ l → series-ℝ l + drop-series-ℝ = drop-series-Metric-Ab +``` + +### The partial sums of a series after dropping terms + +```agda +module _ + {l : Level} + where + + abstract + partial-sum-drop-series-ℝ : + (n : ℕ) (σ : series-ℝ l) (i : ℕ) → + partial-sum-series-ℝ (drop-series-ℝ n σ) i ＝ + partial-sum-series-ℝ σ (n +ℕ i) -ℝ partial-sum-series-ℝ σ n + partial-sum-drop-series-ℝ = partial-sum-drop-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..6c63a8f58d 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -32,14 +32,19 @@ 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.sums-of-finite-sequences-of-elements-normed-real-vector-spaces public +open import linear-algebra.sums-of-finite-sequences-of-elements-real-banach-spaces public open import linear-algebra.transposition-matrices public open import linear-algebra.tuples-on-commutative-monoids public open import linear-algebra.tuples-on-commutative-rings 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..e980a017df --- /dev/null +++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md @@ -0,0 +1,424 @@ +# 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.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.distance-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.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) + + triangular-Normed-ℝ-Vector-Space : + (v w : type-Normed-ℝ-Vector-Space) → + leq-ℝ + ( map-norm-Normed-ℝ-Vector-Space (add-Normed-ℝ-Vector-Space v w)) + ( map-norm-Normed-ℝ-Vector-Space v +ℝ map-norm-Normed-ℝ-Vector-Space w) + triangular-Normed-ℝ-Vector-Space = + triangular-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))))) +``` + +### The norm of the zero vector is zero + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + abstract + is-zero-norm-zero-Normed-ℝ-Vector-Space : + map-norm-Normed-ℝ-Vector-Space V (zero-Normed-ℝ-Vector-Space V) ＝ + raise-ℝ l1 zero-ℝ + is-zero-norm-zero-Normed-ℝ-Vector-Space = + is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) +``` + +## 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..a7dcce022d --- /dev/null +++ b/src/linear-algebra/real-banach-spaces.lagda.md @@ -0,0 +1,158 @@ +# 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.identity-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 +open import real-numbers.nonnegative-real-numbers +``` + +
+ +## Idea + +A +{{#concept "real Banach space" WDID=Q194397 WD="Banach space" 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 + + nonnegative-norm-ℝ-Banach-Space : type-ℝ-Banach-Space → ℝ⁰⁺ l1 + nonnegative-norm-ℝ-Banach-Space = + nonnegative-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) + + dist-ℝ-Banach-Space : (u v : type-ℝ-Banach-Space) → ℝ l1 + dist-ℝ-Banach-Space = + dist-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space + + commutative-dist-ℝ-Banach-Space : + (u v : type-ℝ-Banach-Space) → + dist-ℝ-Banach-Space u v ＝ dist-ℝ-Banach-Space v u + commutative-dist-ℝ-Banach-Space = + commutative-dist-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space + + diff-ℝ-Banach-Space : + type-ℝ-Banach-Space → type-ℝ-Banach-Space → type-ℝ-Banach-Space + diff-ℝ-Banach-Space = + diff-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space +``` + +## Properties + +### The real numbers are a real Banach space with norm `x ↦ |x|` + +```agda +abstract + is-banach-normed-real-vector-space-ℝ : + (l : Level) → + is-banach-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l) + is-banach-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) + +real-banach-space-ℝ : (l : Level) → ℝ-Banach-Space l (lsuc l) +real-banach-space-ℝ l = + ( normed-real-vector-space-ℝ l , + is-banach-normed-real-vector-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..d413ae0c97 --- /dev/null +++ b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md @@ -0,0 +1,585 @@ +# 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 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 = + equational-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 + 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 is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space V _ _ + ＝ + ( raise-ℝ l1 (abs-ℝ zero-ℝ)) *ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V)) + by ap-mul-ℝ (abs-raise-ℝ l1 _) refl + ＝ + ( raise-zero-ℝ l1) *ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V)) + by ap-mul-ℝ (ap (raise-ℝ l1) abs-zero-ℝ) refl + ＝ raise-zero-ℝ l1 + by left-raise-zero-law-mul-ℝ _ + + 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) + + sim-zero-diagonal-dist-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space V) → + sim-ℝ (dist-Seminormed-ℝ-Vector-Space V v v) zero-ℝ + sim-zero-diagonal-dist-Seminormed-ℝ-Vector-Space v = + inv-tr + ( λ x → sim-ℝ x zero-ℝ) + ( is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space v) + ( sim-raise-ℝ' l1 zero-ℝ) +``` + +### 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 = + equational-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 + 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 is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space V _ _ + ＝ + ( abs-ℝ (raise-ℝ l1 one-ℝ)) *ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space V v) + by ap-mul-ℝ (abs-neg-ℝ _) refl + ＝ abs-ℝ one-ℝ *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by + eq-sim-ℝ + ( preserves-sim-right-mul-ℝ _ _ _ + ( preserves-sim-abs-ℝ (sim-raise-ℝ' l1 one-ℝ))) + ＝ one-ℝ *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by ap-mul-ℝ (abs-real-ℝ⁺ one-ℝ⁺) refl + ＝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by 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 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-ℕ 2 *ℝ zero-ℝ + ≤ zero-ℝ + by leq-sim-ℝ (right-zero-law-mul-ℝ _) + ≤ dist-Seminormed-ℝ-Vector-Space V v v + by + leq-sim-ℝ + ( symmetric-sim-ℝ + ( sim-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) + ( symmetric-sim-ℝ + ( sim-zero-diagonal-dist-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/linear-algebra/sums-of-finite-sequences-of-elements-normed-real-vector-spaces.lagda.md b/src/linear-algebra/sums-of-finite-sequences-of-elements-normed-real-vector-spaces.lagda.md new file mode 100644 index 0000000000..3bdbe8634c --- /dev/null +++ b/src/linear-algebra/sums-of-finite-sequences-of-elements-normed-real-vector-spaces.lagda.md @@ -0,0 +1,94 @@ +# Sums of finite sequences of elements in normed real vector spaces + +```agda +module linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.function-types +open import foundation.universe-levels + +open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups + +open import linear-algebra.normed-real-vector-spaces + +open import lists.finite-sequences + +open import order-theory.large-posets + +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.sums-of-finite-sequences-of-real-numbers + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +The +{{#concept "sum" Disambiguation="of a finite sequence of elements of a normed vector space over ℝ" Agda=sum-fin-sequence-type-Normed-ℝ-Vector-Space}} +of a [finite sequence](lists.finite-sequences.md) of elements of a +[normed vector space](linear-algebra.normed-real-vector-spaces.md) over the +[real numbers](real-numbers.dedekind-real-numbers.md) is the +[sum of the sequence](group-theory.sums-of-finite-sequences-of-elements-abelian-groups.md) +in the [abelian group](group-theory.abelian-groups.md) of the vector space under +addition. + +## Definition + +```agda +sum-fin-sequence-type-Normed-ℝ-Vector-Space : + {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) (n : ℕ) → + fin-sequence (type-Normed-ℝ-Vector-Space V) n → type-Normed-ℝ-Vector-Space V +sum-fin-sequence-type-Normed-ℝ-Vector-Space V = + sum-fin-sequence-type-Ab (ab-Normed-ℝ-Vector-Space V) +``` + +## Properties + +### The norm of the sum of a finite sequence is at most the sum of the norms of the terms of the sequence + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + abstract + triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space : + (n : ℕ) (σ : fin-sequence (type-Normed-ℝ-Vector-Space V) n) → + leq-ℝ + ( map-norm-Normed-ℝ-Vector-Space V + ( sum-fin-sequence-type-Normed-ℝ-Vector-Space V n σ)) + ( sum-fin-sequence-ℝ n (map-norm-Normed-ℝ-Vector-Space V ∘ σ)) + triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space 0 σ = + leq-eq-ℝ (is-zero-norm-zero-Normed-ℝ-Vector-Space V) + triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space + (succ-ℕ n) σ = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + chain-of-inequalities + map-norm-Normed-ℝ-Vector-Space V + ( sum-fin-sequence-type-Normed-ℝ-Vector-Space V (succ-ℕ n) σ) + ≤ ( map-norm-Normed-ℝ-Vector-Space V + ( sum-fin-sequence-type-Normed-ℝ-Vector-Space V + ( n) + ( σ ∘ inl-Fin n))) +ℝ + ( map-norm-Normed-ℝ-Vector-Space V (σ (neg-one-Fin n))) + by triangular-Normed-ℝ-Vector-Space V _ _ + ≤ sum-fin-sequence-ℝ (succ-ℕ n) (map-norm-Normed-ℝ-Vector-Space V ∘ σ) + by + preserves-leq-right-add-ℝ _ _ _ + ( triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space + ( n) + ( σ ∘ inl-Fin n)) +``` diff --git a/src/linear-algebra/sums-of-finite-sequences-of-elements-real-banach-spaces.lagda.md b/src/linear-algebra/sums-of-finite-sequences-of-elements-real-banach-spaces.lagda.md new file mode 100644 index 0000000000..ba3aa4cac9 --- /dev/null +++ b/src/linear-algebra/sums-of-finite-sequences-of-elements-real-banach-spaces.lagda.md @@ -0,0 +1,67 @@ +# Sums of finite sequences of elements in real Banach spaces + +```agda +module linear-algebra.sums-of-finite-sequences-of-elements-real-banach-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.function-types +open import foundation.universe-levels + +open import linear-algebra.real-banach-spaces +open import linear-algebra.sums-of-finite-sequences-of-elements-normed-real-vector-spaces + +open import lists.finite-sequences + +open import real-numbers.inequality-real-numbers +open import real-numbers.sums-of-finite-sequences-of-real-numbers +``` + +
+ +## Idea + +The +{{#concept "sum" Disambiguation="of a finite sequence of elements of a real Banach space" Agda=sum-fin-sequence-type-ℝ-Banach-Space}} +of a [finite sequence](lists.finite-sequences.md) of elements of a +[real Banach space](linear-algebra.real-banach-spaces.md) is the +[sum of the sequence](group-theory.sums-of-finite-sequences-of-elements-abelian-groups.md) +in the [abelian group](group-theory.abelian-groups.md) of the space under +addition. + +## Definition + +```agda +sum-fin-sequence-type-ℝ-Banach-Space : + {l1 l2 : Level} (V : ℝ-Banach-Space l1 l2) → + (n : ℕ) → fin-sequence (type-ℝ-Banach-Space V) n → type-ℝ-Banach-Space V +sum-fin-sequence-type-ℝ-Banach-Space V = + sum-fin-sequence-type-Normed-ℝ-Vector-Space + ( normed-vector-space-ℝ-Banach-Space V) +``` + +## Properties + +### The norm of the sum of a finite sequence is at most the sum of the norms of the terms of the sequence + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + where + + abstract + triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space : + (n : ℕ) (σ : fin-sequence (type-ℝ-Banach-Space V) n) → + leq-ℝ + ( map-norm-ℝ-Banach-Space V + ( sum-fin-sequence-type-ℝ-Banach-Space V n σ)) + ( sum-fin-sequence-ℝ n (map-norm-ℝ-Banach-Space V ∘ σ)) + triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space = + triangle-inequality-norm-sum-fin-sequence-type-Normed-ℝ-Vector-Space + ( normed-vector-space-ℝ-Banach-Space V) +``` diff --git a/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md b/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md index 71c916ccf9..8538d56529 100644 --- a/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md +++ b/src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md @@ -9,6 +9,7 @@ module metric-spaces.cauchy-sequences-metric-spaces where
Imports ```agda +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.archimedean-property-positive-rational-numbers @@ -85,6 +86,31 @@ module _ (m k : ℕ) → leq-ℕ N m → leq-ℕ N k → neighborhood-Metric-Space M ε (x m) (x k) + is-cauchy-modulus-sequence-Metric-Space' : ℚ⁺ → ℕ → UU l2 + is-cauchy-modulus-sequence-Metric-Space' ε N = + (m k : ℕ) → leq-ℕ N m → + neighborhood-Metric-Space M ε (x (m +ℕ k)) (x m) + + is-cauchy-modulus-is-cauchy-modulus-sequence-Metric-Space' : + (ε : ℚ⁺) (N : ℕ) → is-cauchy-modulus-sequence-Metric-Space' ε N → + is-cauchy-modulus-sequence-Metric-Space ε N + is-cauchy-modulus-is-cauchy-modulus-sequence-Metric-Space' ε N H m k N≤m N≤k = + let + case a b N≤a a≤b = + let + ( c , c+a=b) = subtraction-leq-ℕ a b a≤b + in + tr + ( λ d → neighborhood-Metric-Space M ε (x d) (x a)) + ( commutative-add-ℕ a c ∙ c+a=b) + ( H a c N≤a) + in + rec-coproduct + ( λ m≤k → + symmetric-neighborhood-Metric-Space M ε _ _ (case m k N≤m m≤k)) + ( λ k≤m → case k m N≤k k≤m) + ( linear-leq-ℕ m k) + is-cauchy-sequence-Metric-Space : UU l2 is-cauchy-sequence-Metric-Space = (ε : ℚ⁺) → Σ ℕ (is-cauchy-modulus-sequence-Metric-Space ε) diff --git a/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md b/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md index 2cfda0f25e..984330b2f5 100644 --- a/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md +++ b/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md @@ -31,6 +31,7 @@ open import foundation.universe-levels open import lists.sequences open import metric-spaces.cartesian-products-metric-spaces +open import metric-spaces.isometries-metric-spaces open import metric-spaces.metric-spaces open import metric-spaces.modulated-uniformly-continuous-functions-metric-spaces open import metric-spaces.sequences-metric-spaces @@ -383,6 +384,46 @@ module _ map-is-inhabited short-map-limit-modulus-sequence-Metric-Space ``` +### Isometries between metric spaces preserve limits + +```agda +module _ + {la la' lb lb' : Level} + (A : Metric-Space la la') + (B : Metric-Space lb lb') + (f : isometry-Metric-Space A B) + (u : sequence-type-Metric-Space A) + (lim : type-Metric-Space A) + where + + isometry-map-limit-modulus-sequence-Metric-Space : + limit-modulus-sequence-Metric-Space A u lim → + limit-modulus-sequence-Metric-Space + ( B) + ( map-sequence + ( map-isometry-Metric-Space A B f) + ( u)) + ( map-isometry-Metric-Space A B f lim) + isometry-map-limit-modulus-sequence-Metric-Space = + short-map-limit-modulus-sequence-Metric-Space + ( A) + ( B) + ( short-isometry-Metric-Space A B f) + ( u) + ( lim) + + preserves-limits-sequence-isometry-Metric-Space : + is-limit-sequence-Metric-Space A u lim → + is-limit-sequence-Metric-Space + ( B) + ( map-sequence + ( map-isometry-Metric-Space A B f) + ( u)) + ( map-isometry-Metric-Space A B f lim) + preserves-limits-sequence-isometry-Metric-Space = + map-is-inhabited isometry-map-limit-modulus-sequence-Metric-Space +``` + ### If two sequences have limits in metric spaces, their pairing has a limit in the product space The converse has yet to be proved. 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..7daa3f52a8 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 @@ -105,6 +103,7 @@ open import real-numbers.strict-inequality-nonnegative-real-numbers public open import real-numbers.strict-inequality-positive-real-numbers public open import real-numbers.strict-inequality-real-numbers public open import real-numbers.subsets-real-numbers public +open import real-numbers.sums-of-finite-sequences-of-real-numbers public open import real-numbers.suprema-families-real-numbers public open import real-numbers.totally-bounded-subsets-real-numbers public open import real-numbers.transposition-addition-subtraction-cuts-dedekind-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..5ee9b077e1 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` @@ -258,6 +298,20 @@ module _ leq-abs-leq-leq-neg-ℝ = leq-max-leq-leq-ℝ x (neg-ℝ x) y ``` +### If `x < y` and `-x < y`, `|x| < y` + +```agda +module _ + {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} + where + + abstract opaque + unfolding abs-ℝ + + le-abs-le-le-neg-ℝ : le-ℝ x y → le-ℝ (neg-ℝ x) y → le-ℝ (abs-ℝ x) y + le-abs-le-le-neg-ℝ = le-max-le-le-ℝ +``` + ### Triangle inequality ```agda 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..8a716b033f 100644 --- a/src/real-numbers/cauchy-sequences-real-numbers.lagda.md +++ b/src/real-numbers/cauchy-sequences-real-numbers.lagda.md @@ -9,8 +9,12 @@ module real-numbers.cauchy-sequences-real-numbers where
Imports ```agda +open import foundation.dependent-pair-types +open import foundation.inhabited-types 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 @@ -18,6 +22,7 @@ open import metric-spaces.cauchy-sequences-metric-spaces open import real-numbers.cauchy-completeness-dedekind-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.isometry-addition-real-numbers +open import real-numbers.limits-sequences-real-numbers open import real-numbers.metric-space-of-real-numbers ``` @@ -39,6 +44,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) ``` @@ -70,3 +78,20 @@ add-cauchy-sequence-ℝ {l1} {l2} u v = ( u) ( v)) ``` + +### If a sequence has a limit, there exists a modulus making it a Cauchy sequence + +```agda +abstract + exists-cauchy-modulus-has-limit-sequence-ℝ : + {l : Level} (σ : sequence (ℝ l)) → + has-limit-sequence-ℝ σ → + is-inhabited (is-cauchy-sequence-ℝ σ) + exists-cauchy-modulus-has-limit-sequence-ℝ {l} σ (lim , is-lim) = + map-is-inhabited + ( is-cauchy-has-limit-modulus-sequence-Metric-Space + ( metric-space-ℝ l) + ( σ) + ( lim)) + ( is-lim) +``` 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/distance-real-numbers.lagda.md b/src/real-numbers/distance-real-numbers.lagda.md index 91f5380524..bc4e128fd6 100644 --- a/src/real-numbers/distance-real-numbers.lagda.md +++ b/src/real-numbers/distance-real-numbers.lagda.md @@ -254,6 +254,16 @@ abstract ( leq-transpose-right-add-ℝ _ _ _ y≤z+x) ``` +### The difference of two real numbers is at most their distance + +```agda +abstract + leq-diff-dist-ℝ : + {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → + leq-ℝ (x -ℝ y) (dist-ℝ x y) + leq-diff-dist-ℝ _ _ = leq-abs-ℝ _ +``` + ### Addition preserves distance between real numbers ```agda diff --git a/src/real-numbers/geometric-sequences-real-numbers.lagda.md b/src/real-numbers/geometric-sequences-real-numbers.lagda.md index a868836657..dfc8de55e8 100644 --- a/src/real-numbers/geometric-sequences-real-numbers.lagda.md +++ b/src/real-numbers/geometric-sequences-real-numbers.lagda.md @@ -9,12 +9,16 @@ 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 open import foundation.action-on-identifications-functions open import foundation.binary-transport +open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.identity-types open import foundation.transport-along-identifications @@ -27,7 +31,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 +44,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 @@ -241,6 +243,13 @@ module _ ( λ n → power-ℝ n r) ( raise-ℝ l zero-ℝ) ( is-zero-lim-power-le-one-abs-ℝ r |r|<1)) + + convergent-standard-geometric-series-ℝ : + le-ℝ (abs-ℝ r) one-ℝ → convergent-series-ℝ l + convergent-standard-geometric-series-ℝ |r|<1 = + ( standard-geometric-series-ℝ , + a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1) , + compute-sum-standard-geometric-series-ℝ |r|<1) ``` ## References 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/multiplication-real-numbers.lagda.md b/src/real-numbers/multiplication-real-numbers.lagda.md index a4d70e4bbd..002c926006 100644 --- a/src/real-numbers/multiplication-real-numbers.lagda.md +++ b/src/real-numbers/multiplication-real-numbers.lagda.md @@ -1038,33 +1038,6 @@ abstract by ap-add-ℝ (commutative-mul-ℝ z x) (commutative-mul-ℝ z y) ``` -### Zero laws - -```agda -module _ - {l : Level} (x : ℝ l) - where - - abstract - left-zero-law-mul-ℝ : sim-ℝ (zero-ℝ *ℝ x) zero-ℝ - left-zero-law-mul-ℝ = - inv-tr - ( λ y → sim-ℝ y zero-ℝ) - ( is-zero-is-idempotent-Ab - ( ab-add-ℝ l) - ( equational-reasoning - zero-ℝ *ℝ x +ℝ zero-ℝ *ℝ x - ＝ (zero-ℝ +ℝ zero-ℝ) *ℝ x - by inv (right-distributive-mul-add-ℝ zero-ℝ zero-ℝ x) - ＝ zero-ℝ *ℝ x - by ap-mul-ℝ (left-unit-law-add-ℝ zero-ℝ) refl)) - ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ)) - - right-zero-law-mul-ℝ : sim-ℝ (x *ℝ zero-ℝ) zero-ℝ - right-zero-law-mul-ℝ = - tr (λ y → sim-ℝ y zero-ℝ) (commutative-mul-ℝ _ _) left-zero-law-mul-ℝ -``` - ### The inclusion of rational numbers preserves multiplication ```agda @@ -1166,6 +1139,51 @@ abstract ( preserves-sim-left-mul-ℝ a b b' b~b') ``` +### Zero laws + +```agda +module _ + {l : Level} (x : ℝ l) + where + + abstract + left-zero-law-mul-ℝ : sim-ℝ (zero-ℝ *ℝ x) zero-ℝ + left-zero-law-mul-ℝ = + inv-tr + ( λ y → sim-ℝ y zero-ℝ) + ( is-zero-is-idempotent-Ab + ( ab-add-ℝ l) + ( equational-reasoning + zero-ℝ *ℝ x +ℝ zero-ℝ *ℝ x + ＝ (zero-ℝ +ℝ zero-ℝ) *ℝ x + by inv (right-distributive-mul-add-ℝ zero-ℝ zero-ℝ x) + ＝ zero-ℝ *ℝ x + by ap-mul-ℝ (left-unit-law-add-ℝ zero-ℝ) refl)) + ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ)) + + left-raise-zero-law-mul-ℝ : + raise-zero-ℝ l *ℝ x ＝ raise-zero-ℝ l + left-raise-zero-law-mul-ℝ = + eq-sim-ℝ + ( similarity-reasoning-ℝ + raise-zero-ℝ l *ℝ x + ~ℝ zero-ℝ *ℝ x + by + preserves-sim-right-mul-ℝ + ( x) + ( raise-zero-ℝ l) + ( zero-ℝ) + ( sim-raise-ℝ' l zero-ℝ) + ~ℝ zero-ℝ + by left-zero-law-mul-ℝ + ~ℝ raise-zero-ℝ l + by sim-raise-ℝ l zero-ℝ) + + right-zero-law-mul-ℝ : sim-ℝ (x *ℝ zero-ℝ) zero-ℝ + right-zero-law-mul-ℝ = + tr (λ y → sim-ℝ y zero-ℝ) (commutative-mul-ℝ _ _) left-zero-law-mul-ℝ +``` + ### Swapping laws for multiplication on real numbers ```agda 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 -``` diff --git a/src/real-numbers/sums-of-finite-sequences-of-real-numbers.lagda.md b/src/real-numbers/sums-of-finite-sequences-of-real-numbers.lagda.md new file mode 100644 index 0000000000..8da6c6955b --- /dev/null +++ b/src/real-numbers/sums-of-finite-sequences-of-real-numbers.lagda.md @@ -0,0 +1,69 @@ +# Sums of finite sequences of real numbers + +```agda +module real-numbers.sums-of-finite-sequences-of-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.function-types +open import foundation.universe-levels + +open import group-theory.sums-of-finite-sequences-of-elements-abelian-groups + +open import lists.finite-sequences + +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.large-additive-group-of-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers + +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +The +{{#concept "sum operation" Disambiguation="of a finite sequence in ℝ" WD="sum" WDID=Q218005 Agda=sum-fin-sequence-ℝ}} +extends the operation of [addition](real-numbers.addition-real-numbers.md) on +the [real numbers](real-numbers.dedekind-real-numbers.md) to any +[finite sequence](lists.finite-sequences.md) of real numbers. + +## Definition + +```agda +sum-fin-sequence-ℝ : {l : Level} (n : ℕ) → fin-sequence (ℝ l) n → ℝ l +sum-fin-sequence-ℝ {l} = sum-fin-sequence-type-Ab (ab-add-ℝ l) +``` + +## Properties + +### If `aₙ ≤ bₙ` for all `n`, then `∑ aₙ ≤ ∑ bₙ` + +```agda +abstract + leq-sum-fin-sequence-ℝ : + {l1 l2 : Level} (n : ℕ) → + (a : fin-sequence (ℝ l1) n) (b : fin-sequence (ℝ l2) n) → + ((k : Fin n) → leq-ℝ (a k) (b k)) → + leq-ℝ (sum-fin-sequence-ℝ n a) (sum-fin-sequence-ℝ n b) + leq-sum-fin-sequence-ℝ {l1} {l2} 0 _ _ _ = + leq-sim-ℝ + ( transitive-sim-ℝ _ _ _ (sim-raise-ℝ l2 zero-ℝ) (sim-raise-ℝ' l1 zero-ℝ)) + leq-sum-fin-sequence-ℝ (succ-ℕ n) a b H = + preserves-leq-add-ℝ + ( leq-sum-fin-sequence-ℝ + ( n) + ( a ∘ inl-Fin n) + ( b ∘ inl-Fin n) + ( H ∘ inl-Fin n)) + ( H (neg-one-Fin n)) +```