diff --git a/src/analysis.lagda.md b/src/analysis.lagda.md index 99788b360c..32ce20fbad 100644 --- a/src/analysis.lagda.md +++ b/src/analysis.lagda.md @@ -3,7 +3,18 @@ ```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.complete-metric-abelian-groups public +open import analysis.complete-metric-abelian-groups-real-banach-spaces public +open import analysis.convergent-series-complete-metric-abelian-groups public open import analysis.convergent-series-metric-abelian-groups public +open import analysis.convergent-series-real-banach-spaces public +open import analysis.convergent-series-real-numbers public open import analysis.metric-abelian-groups public +open import analysis.metric-abelian-groups-normed-real-vector-spaces public +open import analysis.series-complete-metric-abelian-groups public open import analysis.series-metric-abelian-groups public +open import analysis.series-real-banach-spaces public +open import analysis.series-real-numbers public ``` diff --git a/src/analysis/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..d36b05318e --- /dev/null +++ b/src/analysis/absolute-convergence-series-real-banach-spaces.lagda.md @@ -0,0 +1,193 @@ +# 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))) +``` 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..19a6940362 --- /dev/null +++ b/src/analysis/absolute-convergence-series-real-numbers.lagda.md @@ -0,0 +1,73 @@ +# 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)) +``` 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 6e5e9cfe3f..d78cf2b8bd 100644 --- a/src/analysis/convergent-series-metric-abelian-groups.lagda.md +++ b/src/analysis/convergent-series-metric-abelian-groups.lagda.md @@ -43,7 +43,7 @@ module _ is-sum-prop-series-Metric-Ab = is-limit-prop-sequence-Metric-Space ( metric-space-Metric-Ab G) - ( partial-sum-series-Metric-Ab G σ) + ( partial-sum-series-Metric-Ab σ) is-sum-series-Metric-Ab : type-Metric-Ab G → UU l2 is-sum-series-Metric-Ab s = type-Prop (is-sum-prop-series-Metric-Ab s) @@ -52,7 +52,7 @@ module _ is-convergent-prop-series-Metric-Ab = subtype-convergent-sequence-Metric-Space ( metric-space-Metric-Ab G) - ( partial-sum-series-Metric-Ab G σ) + ( partial-sum-series-Metric-Ab σ) is-convergent-series-Metric-Ab : UU (l1 ⊔ l2) is-convergent-series-Metric-Ab = @@ -76,7 +76,7 @@ module _ partial-sum-convergent-series-Metric-Ab : sequence (type-Metric-Ab G) partial-sum-convergent-series-Metric-Ab = - partial-sum-series-Metric-Ab G series-convergent-series-Metric-Ab + 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 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..b0c0dc877d --- /dev/null +++ b/src/analysis/convergent-series-real-numbers.lagda.md @@ -0,0 +1,74 @@ +# Convergent series in the real numbers + +```agda +module analysis.convergent-series-real-numbers where +``` + +
Imports + +```agda +open import analysis.convergent-series-complete-metric-abelian-groups +open import analysis.convergent-series-metric-abelian-groups +open import analysis.series-real-numbers + +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import real-numbers.cauchy-sequences-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-additive-group-of-real-numbers +``` + +
+ +## Idea + +A [series of real numbers](analysis.series-real-numbers.md) is +{{#concept "convergent" Disambiguation="series in 𝐑" Agda=is-convergent-series-ℝ Agda=convergent-series-ℝ WDID=Q1211057 WD="convergent series"}} +if its partial sums converge in the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md). + +## Definition + +```agda +module _ + {l : Level} + (σ : series-ℝ l) + where + + is-sum-prop-series-ℝ : ℝ l → Prop l + is-sum-prop-series-ℝ = is-sum-prop-series-Metric-Ab σ + + is-sum-series-ℝ : ℝ l → UU l + is-sum-series-ℝ = is-sum-series-Metric-Ab σ + + is-convergent-prop-series-ℝ : Prop (lsuc l) + is-convergent-prop-series-ℝ = + is-convergent-prop-series-Metric-Ab σ + + is-convergent-series-ℝ : UU (lsuc l) + is-convergent-series-ℝ = is-convergent-series-Metric-Ab σ + +convergent-series-ℝ : (l : Level) → UU (lsuc l) +convergent-series-ℝ l = type-subtype (is-convergent-prop-series-ℝ {l}) +``` + +## 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) + ( σ) +``` diff --git a/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md b/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md new file mode 100644 index 0000000000..4ee09d54d5 --- /dev/null +++ b/src/analysis/metric-abelian-groups-normed-real-vector-spaces.lagda.md @@ -0,0 +1,94 @@ +# Metric abelian groups of normed real vector spaces + +```agda +module analysis.metric-abelian-groups-normed-real-vector-spaces where +``` + +
Imports + +```agda +open import analysis.metric-abelian-groups + +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.subtypes +open import foundation.universe-levels + +open import group-theory.abelian-groups + +open import linear-algebra.normed-real-vector-spaces + +open import metric-spaces.extensionality-pseudometric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.pseudometric-spaces +open import metric-spaces.rational-neighborhood-relations + +open import real-numbers.dedekind-real-numbers +open import real-numbers.distance-real-numbers +open import real-numbers.large-additive-group-of-real-numbers +open import real-numbers.metric-additive-group-of-real-numbers +``` + +
+ +## Idea + +A [normed](linear-algebra.normed-real-vector-spaces.md) +[real vector space](linear-algebra.real-vector-spaces.md) forms a +[metric abelian group](analysis.metric-abelian-groups.md) under addition. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : Normed-ℝ-Vector-Space l1 l2) + where + + ab-metric-ab-Normed-ℝ-Vector-Space : Ab l2 + ab-metric-ab-Normed-ℝ-Vector-Space = ab-Normed-ℝ-Vector-Space V + + type-metric-ab-Normed-ℝ-Vector-Space : UU l2 + type-metric-ab-Normed-ℝ-Vector-Space = type-Normed-ℝ-Vector-Space V + + pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space : + Pseudometric-Structure l1 type-metric-ab-Normed-ℝ-Vector-Space + pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space = + pseudometric-structure-Metric-Space (metric-space-Normed-ℝ-Vector-Space V) + + pseudometric-space-metric-ab-Normed-ℝ-Vector-Space : + Pseudometric-Space l2 l1 + pseudometric-space-metric-ab-Normed-ℝ-Vector-Space = + pseudometric-Metric-Space (metric-space-Normed-ℝ-Vector-Space V) + + metric-ab-Normed-ℝ-Vector-Space : Metric-Ab l2 l1 + metric-ab-Normed-ℝ-Vector-Space = + ( ab-metric-ab-Normed-ℝ-Vector-Space , + pseudometric-structure-metric-ab-Normed-ℝ-Vector-Space , + is-extensional-pseudometric-Metric-Space + ( metric-space-Normed-ℝ-Vector-Space V) , + is-isometry-neg-Normed-ℝ-Vector-Space V , + is-isometry-left-add-Normed-ℝ-Vector-Space V) +``` + +## Properties + +### The metric abelian group associated with `ℝ` as a normed vector space over `ℝ` is equal to the metric additive group of `ℝ` + +```agda +abstract + eq-metric-ab-normed-real-vector-space-metric-ab-ℝ : + (l : Level) → + metric-ab-Normed-ℝ-Vector-Space (normed-real-vector-space-ℝ l) ＝ + metric-ab-add-ℝ l + eq-metric-ab-normed-real-vector-space-metric-ab-ℝ l = + eq-pair-eq-fiber + ( eq-type-subtype + ( λ M → is-metric-ab-prop-Ab-Pseudometric-Structure (ab-add-ℝ l) M) + ( eq-type-subtype + ( is-pseudometric-prop-Rational-Neighborhood-Relation (ℝ l)) + ( eq-Eq-Rational-Neighborhood-Relation _ _ + ( λ d x y → inv-iff (neighborhood-iff-leq-dist-ℝ d x y))))) +``` diff --git a/src/analysis/metric-abelian-groups.lagda.md b/src/analysis/metric-abelian-groups.lagda.md index 3306202936..fe8317d466 100644 --- a/src/analysis/metric-abelian-groups.lagda.md +++ b/src/analysis/metric-abelian-groups.lagda.md @@ -12,8 +12,10 @@ open import elementary-number-theory.positive-rational-numbers open import foundation.action-on-identifications-binary-functions open import foundation.binary-relations open import foundation.cartesian-product-types +open import foundation.conjunction open import foundation.dependent-pair-types open import foundation.identity-types +open import foundation.propositions open import foundation.universe-levels open import group-theory.abelian-groups @@ -39,18 +41,25 @@ and negation operation are ## Definition ```agda +is-metric-ab-prop-Ab-Pseudometric-Structure : + {l1 l2 : Level} (G : Ab l1) (M : Pseudometric-Structure l2 (type-Ab G)) → + Prop (l1 ⊔ l2) +is-metric-ab-prop-Ab-Pseudometric-Structure G M = + let + MS = (type-Ab G , M) + in + is-extensional-prop-Pseudometric-Space MS ∧ + is-isometry-prop-Pseudometric-Space MS MS (neg-Ab G) ∧ + Π-Prop + ( type-Ab G) + ( λ x → is-isometry-prop-Pseudometric-Space MS MS (add-Ab G x)) + Metric-Ab : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Metric-Ab l1 l2 = Σ ( Ab l1) ( λ G → Σ ( Pseudometric-Structure l2 (type-Ab G)) - ( λ M → - let MS = (type-Ab G , M) - in - is-extensional-Pseudometric-Space MS × - is-isometry-Pseudometric-Space MS MS (neg-Ab G) × - ( (x : type-Ab G) → - is-isometry-Pseudometric-Space MS MS (add-Ab G x)))) + ( λ M → type-Prop (is-metric-ab-prop-Ab-Pseudometric-Structure G M))) module _ {l1 l2 : Level} (MG : Metric-Ab l1 l2) diff --git a/src/analysis/series-complete-metric-abelian-groups.lagda.md b/src/analysis/series-complete-metric-abelian-groups.lagda.md new file mode 100644 index 0000000000..bb936a8eb0 --- /dev/null +++ b/src/analysis/series-complete-metric-abelian-groups.lagda.md @@ -0,0 +1,49 @@ +# Series in complete metric abelian groups + +```agda +module analysis.series-complete-metric-abelian-groups where +``` + +
Imports + +```agda +open import analysis.complete-metric-abelian-groups +open import analysis.series-metric-abelian-groups + +open import foundation.universe-levels + +open import lists.sequences +``` + +
+ +## Idea + +A [series](analysis.series-metric-abelian-groups.md) in a +[complete metric abelian group](analysis.complete-metric-abelian-groups.md) is a +series in the underlying +[metric abelian group](analysis.metric-abelian-groups.md). + +## Definition + +```agda +module _ + {l1 l2 : Level} + (G : Complete-Metric-Ab l1 l2) + where + + series-Complete-Metric-Ab : UU l1 + series-Complete-Metric-Ab = series-Metric-Ab (metric-ab-Complete-Metric-Ab G) + + series-terms-Complete-Metric-Ab : + sequence (type-Complete-Metric-Ab G) → series-Complete-Metric-Ab + series-terms-Complete-Metric-Ab = series-terms-Metric-Ab + + term-series-Complete-Metric-Ab : + series-Complete-Metric-Ab → sequence (type-Complete-Metric-Ab G) + term-series-Complete-Metric-Ab = term-series-Metric-Ab + + partial-sum-series-Complete-Metric-Ab : + series-Complete-Metric-Ab → sequence (type-Complete-Metric-Ab G) + partial-sum-series-Complete-Metric-Ab = partial-sum-series-Metric-Ab +``` diff --git a/src/analysis/series-metric-abelian-groups.lagda.md b/src/analysis/series-metric-abelian-groups.lagda.md index 1bb3d80a5e..b450b78d25 100644 --- a/src/analysis/series-metric-abelian-groups.lagda.md +++ b/src/analysis/series-metric-abelian-groups.lagda.md @@ -83,7 +83,7 @@ module _ ```agda module _ - {l1 l2 : Level} (G : Metric-Ab l1 l2) + {l1 l2 : Level} {G : Metric-Ab l1 l2} where partial-sum-series-Metric-Ab : series-Metric-Ab G → ℕ → type-Metric-Ab G @@ -95,14 +95,14 @@ module _ ```agda module _ - {l1 l2 : Level} (G : Metric-Ab l1 l2) + {l1 l2 : Level} {G : Metric-Ab l1 l2} where eq-term-diff-partial-sum-series-Metric-Ab : (f : series-Metric-Ab G) (n : ℕ) → add-Metric-Ab G - ( partial-sum-series-Metric-Ab G f (succ-ℕ n)) - ( neg-Metric-Ab G (partial-sum-series-Metric-Ab G f n)) ＝ + ( partial-sum-series-Metric-Ab f (succ-ℕ n)) + ( neg-Metric-Ab G (partial-sum-series-Metric-Ab f n)) ＝ term-series-Metric-Ab f n eq-term-diff-partial-sum-series-Metric-Ab (series-terms-Metric-Ab f) n = ap-add-Metric-Ab G @@ -118,21 +118,21 @@ module _ ```agda module _ - {l1 l2 : Level} (G : Metric-Ab l1 l2) + {l1 l2 : Level} {G : Metric-Ab l1 l2} where htpy-htpy-partial-sum-series-Metric-Ab : {σ τ : series-Metric-Ab G} → - (partial-sum-series-Metric-Ab G σ ~ partial-sum-series-Metric-Ab G τ) → + (partial-sum-series-Metric-Ab σ ~ partial-sum-series-Metric-Ab τ) → term-series-Metric-Ab σ ~ term-series-Metric-Ab τ htpy-htpy-partial-sum-series-Metric-Ab {σ} {τ} psσ~psτ n = - inv (eq-term-diff-partial-sum-series-Metric-Ab G σ n) ∙ + inv (eq-term-diff-partial-sum-series-Metric-Ab σ n) ∙ ap-right-subtraction-Ab (ab-Metric-Ab G) (psσ~psτ (succ-ℕ n)) (psσ~psτ n) ∙ - eq-term-diff-partial-sum-series-Metric-Ab G τ n + eq-term-diff-partial-sum-series-Metric-Ab τ n eq-htpy-partial-sum-series-Metric-Ab : {σ τ : series-Metric-Ab G} → - (partial-sum-series-Metric-Ab G σ ~ partial-sum-series-Metric-Ab G τ) → + (partial-sum-series-Metric-Ab σ ~ partial-sum-series-Metric-Ab τ) → σ ＝ τ eq-htpy-partial-sum-series-Metric-Ab psσ~psτ = eq-htpy-term-series-Metric-Ab G @@ -155,23 +155,22 @@ module _ ```agda module _ - {l1 l2 : Level} (G : Metric-Ab l1 l2) + {l1 l2 : Level} {G : Metric-Ab l1 l2} where abstract partial-sum-drop-series-Metric-Ab : - (n : ℕ) → (σ : series-Metric-Ab G) → (i : ℕ) → - partial-sum-series-Metric-Ab G (drop-series-Metric-Ab n σ) i ＝ + (n : ℕ) (σ : series-Metric-Ab G) (i : ℕ) → + partial-sum-series-Metric-Ab (drop-series-Metric-Ab n σ) i ＝ diff-Metric-Ab G - ( partial-sum-series-Metric-Ab G σ (n +ℕ i)) - ( partial-sum-series-Metric-Ab G σ n) - partial-sum-drop-series-Metric-Ab n (series-terms-Metric-Ab σ) i = + ( partial-sum-series-Metric-Ab σ (n +ℕ i)) + ( partial-sum-series-Metric-Ab σ n) + partial-sum-drop-series-Metric-Ab n s@(series-terms-Metric-Ab σ) i = inv ( equational-reasoning diff-Metric-Ab G - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) - ( n +ℕ i)) - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n) + ( partial-sum-series-Metric-Ab s (n +ℕ i)) + ( partial-sum-series-Metric-Ab s n) ＝ diff-Metric-Ab G ( add-Metric-Ab G @@ -179,7 +178,7 @@ module _ ( σ ∘ nat-Fin (n +ℕ i) ∘ inl-coproduct-Fin n i)) ( sum-fin-sequence-type-Ab (ab-Metric-Ab G) i ( σ ∘ nat-Fin (n +ℕ i) ∘ inr-coproduct-Fin n i))) - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n) + ( partial-sum-series-Metric-Ab s n) by ap-diff-Metric-Ab G ( split-sum-fin-sequence-type-Ab @@ -191,10 +190,11 @@ module _ ＝ diff-Metric-Ab G ( add-Metric-Ab G - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n) - ( partial-sum-series-Metric-Ab G - ( series-terms-Metric-Ab (σ ∘ add-ℕ n)) i)) - ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n) + ( partial-sum-series-Metric-Ab s n) + ( partial-sum-series-Metric-Ab + ( series-terms-Metric-Ab {G = G} (σ ∘ add-ℕ n)) + ( i))) + ( partial-sum-series-Metric-Ab s n) by ap-diff-Metric-Ab G ( ap-add-Metric-Ab G @@ -204,8 +204,8 @@ module _ ( λ j → ap σ (nat-inr-coproduct-Fin n i j)))) ( refl) ＝ - partial-sum-series-Metric-Ab G - ( series-terms-Metric-Ab (σ ∘ add-ℕ n)) + partial-sum-series-Metric-Ab + ( series-terms-Metric-Ab {G = G} (σ ∘ add-ℕ n)) ( i) by is-identity-left-conjugation-Ab (ab-Metric-Ab G) _ _) ``` 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..db12638a3e --- /dev/null +++ b/src/analysis/series-real-numbers.lagda.md @@ -0,0 +1,112 @@ +# 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.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 + +### 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) → + ((n : ℕ) → is-nonnegative-ℝ (term-series-ℝ σ n)) → + 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/commutative-algebra/local-commutative-rings.lagda.md b/src/commutative-algebra/local-commutative-rings.lagda.md index 9de71b60fc..717095eaa5 100644 --- a/src/commutative-algebra/local-commutative-rings.lagda.md +++ b/src/commutative-algebra/local-commutative-rings.lagda.md @@ -66,4 +66,24 @@ module _ is-local-commutative-ring-Local-Commutative-Ring : is-local-Commutative-Ring commutative-ring-Local-Commutative-Ring is-local-commutative-ring-Local-Commutative-Ring = pr2 A + + zero-Local-Commutative-Ring : type-Local-Commutative-Ring + zero-Local-Commutative-Ring = zero-Ring ring-Local-Commutative-Ring + + one-Local-Commutative-Ring : type-Local-Commutative-Ring + one-Local-Commutative-Ring = one-Ring ring-Local-Commutative-Ring + + add-Local-Commutative-Ring : + type-Local-Commutative-Ring → type-Local-Commutative-Ring → + type-Local-Commutative-Ring + add-Local-Commutative-Ring = add-Ring ring-Local-Commutative-Ring + + mul-Local-Commutative-Ring : + type-Local-Commutative-Ring → type-Local-Commutative-Ring → + type-Local-Commutative-Ring + mul-Local-Commutative-Ring = mul-Ring ring-Local-Commutative-Ring + + neg-Local-Commutative-Ring : + type-Local-Commutative-Ring → type-Local-Commutative-Ring + neg-Local-Commutative-Ring = neg-Ring ring-Local-Commutative-Ring ``` diff --git a/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md b/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md index b1a0ac28aa..f5113246e1 100644 --- a/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md +++ b/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md @@ -8,6 +8,7 @@ module commutative-algebra.sums-of-finite-sequences-of-elements-commutative-ring ```agda open import commutative-algebra.commutative-rings +open import commutative-algebra.multiples-of-elements-commutative-rings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers @@ -244,6 +245,19 @@ module _ preserves-sum-permutation-fin-sequence-type-Ring (ring-Commutative-Ring A) ``` +### The sum of a constant finite sequence in a commutative ring is scalar multiplication by the length of the sequence + +```agda +abstract + sum-constant-fin-sequence-type-Commutative-Ring : + {l : Level} (R : Commutative-Ring l) (n : ℕ) → + (x : type-Commutative-Ring R) → + sum-fin-sequence-type-Commutative-Ring R n (λ _ → x) ＝ + multiple-Commutative-Ring R n x + sum-constant-fin-sequence-type-Commutative-Ring R = + sum-constant-fin-sequence-type-Ring (ring-Commutative-Ring R) +``` + ## See also - [Sums of finite families of elements in commutative rings](commutative-algebra.sums-of-finite-families-of-elements-commutative-rings.md) diff --git a/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md b/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md index 5c5bfabafc..4292c3ed0e 100644 --- a/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md +++ b/src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md @@ -8,6 +8,7 @@ module commutative-algebra.sums-of-finite-sequences-of-elements-commutative-semi ```agda open import commutative-algebra.commutative-semirings +open import commutative-algebra.multiples-of-elements-commutative-semirings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.natural-numbers @@ -260,3 +261,16 @@ module _ preserves-sum-permutation-fin-sequence-type-Semiring ( semiring-Commutative-Semiring R) ``` + +### The sum of a constant finite sequence in a commutative semiring is scalar multiplication by the length of the sequence + +```agda +abstract + sum-constant-fin-sequence-type-Commutative-Semiring : + {l : Level} (R : Commutative-Semiring l) (n : ℕ) → + (x : type-Commutative-Semiring R) → + sum-fin-sequence-type-Commutative-Semiring R n (λ _ → x) ＝ + multiple-Commutative-Semiring R n x + sum-constant-fin-sequence-type-Commutative-Semiring R = + sum-constant-fin-sequence-type-Semiring (semiring-Commutative-Semiring R) +``` diff --git a/src/complex-numbers.lagda.md b/src/complex-numbers.lagda.md index 647fd88a7d..bb5ba406cb 100644 --- a/src/complex-numbers.lagda.md +++ b/src/complex-numbers.lagda.md @@ -4,12 +4,17 @@ module complex-numbers where open import complex-numbers.addition-complex-numbers public +open import complex-numbers.apartness-complex-numbers public open import complex-numbers.complex-numbers public +open import complex-numbers.conjugation-complex-numbers public open import complex-numbers.eisenstein-integers public open import complex-numbers.gaussian-integers public open import complex-numbers.large-additive-group-of-complex-numbers public open import complex-numbers.large-ring-of-complex-numbers public +open import complex-numbers.magnitude-complex-numbers public open import complex-numbers.multiplication-complex-numbers public +open import complex-numbers.multiplicative-inverses-nonzero-complex-numbers public +open import complex-numbers.nonzero-complex-numbers public open import complex-numbers.raising-universe-levels-complex-numbers public open import complex-numbers.similarity-complex-numbers public ``` diff --git a/src/complex-numbers/apartness-complex-numbers.lagda.md b/src/complex-numbers/apartness-complex-numbers.lagda.md new file mode 100644 index 0000000000..e58a5ee728 --- /dev/null +++ b/src/complex-numbers/apartness-complex-numbers.lagda.md @@ -0,0 +1,102 @@ +# Apartness of complex numbers + +```agda +module complex-numbers.apartness-complex-numbers where +``` + +
Imports + +```agda +open import complex-numbers.complex-numbers + +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.empty-types +open import foundation.function-types +open import foundation.functoriality-disjunction +open import foundation.large-apartness-relations +open import foundation.negation +open import foundation.propositions +open import foundation.universe-levels + +open import real-numbers.apartness-real-numbers +``` + +
+ +## Idea + +Two [complex numbers](complex-numbers.complex-numbers.md) are +{{#concept "apart" Agda=apart-ℂ}} if their +[real](real-numbers.dedekind-real-numbers.md) parts are +[apart](real-numbers.apartness-real-numbers.md) [or](foundation.disjunction.md) +their imaginary parts are [apart]. + +## Definition + +```agda +module _ + {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) + where + + apart-prop-ℂ : Prop (l1 ⊔ l2) + apart-prop-ℂ = + apart-prop-ℝ (re-ℂ z) (re-ℂ w) ∨ apart-prop-ℝ (im-ℂ z) (im-ℂ w) + + apart-ℂ : UU (l1 ⊔ l2) + apart-ℂ = type-Prop apart-prop-ℂ +``` + +## Properties + +### Apartness is antireflexive + +```agda +abstract + antireflexive-apart-ℂ : {l : Level} (z : ℂ l) → ¬ (apart-ℂ z z) + antireflexive-apart-ℂ (a , b) = + elim-disjunction + ( empty-Prop) + ( antireflexive-apart-ℝ a) + ( antireflexive-apart-ℝ b) +``` + +### Apartness is symmetric + +```agda +abstract + symmetric-apart-ℂ : + {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → apart-ℂ z w → apart-ℂ w z + symmetric-apart-ℂ (a , b) (c , d) = + map-disjunction symmetric-apart-ℝ symmetric-apart-ℝ +``` + +### Apartness is cotransitive + +```agda +abstract + cotransitive-apart-ℂ : + {l1 l2 l3 : Level} (x : ℂ l1) (y : ℂ l2) (z : ℂ l3) → + apart-ℂ x y → disjunction-type (apart-ℂ x z) (apart-ℂ z y) + cotransitive-apart-ℂ x@(a , b) y@(c , d) z@(e , f) = + elim-disjunction + ( (apart-prop-ℂ x z) ∨ (apart-prop-ℂ z y)) + ( map-disjunction inl-disjunction inl-disjunction ∘ + cotransitive-apart-ℝ a c e) + ( map-disjunction inr-disjunction inr-disjunction ∘ + cotransitive-apart-ℝ b d f) +``` + +### Apartness on the complex numbers is a large apartness relation + +```agda +large-apartness-relation-ℂ : Large-Apartness-Relation _⊔_ ℂ +apart-prop-Large-Apartness-Relation large-apartness-relation-ℂ = + apart-prop-ℂ +antirefl-Large-Apartness-Relation large-apartness-relation-ℂ = + antireflexive-apart-ℂ +symmetric-Large-Apartness-Relation large-apartness-relation-ℂ = + symmetric-apart-ℂ +cotransitive-Large-Apartness-Relation large-apartness-relation-ℂ = + cotransitive-apart-ℂ +``` diff --git a/src/complex-numbers/complex-numbers.lagda.md b/src/complex-numbers/complex-numbers.lagda.md index 450fdc6bc9..0b7cc5fcf8 100644 --- a/src/complex-numbers/complex-numbers.lagda.md +++ b/src/complex-numbers/complex-numbers.lagda.md @@ -38,6 +38,8 @@ are numbers of the form `a + bi`, where `a` and `b` are ℂ : (l : Level) → UU (lsuc l) ℂ l = ℝ l × ℝ l +pattern _+iℂ_ x y = (x , y) + re-ℂ : {l : Level} → ℂ l → ℝ l re-ℂ = pr1 @@ -81,13 +83,6 @@ complex-ℤ[i] : ℤ[i] → ℂ lzero complex-ℤ[i] (a , b) = (real-ℤ a , real-ℤ b) ``` -### The conjugate of a complex number - -```agda -conjugate-ℂ : {l : Level} → ℂ l → ℂ l -conjugate-ℂ (a , b) = (a , neg-ℝ b) -``` - ### Important complex numbers ```agda @@ -110,3 +105,11 @@ i-ℂ = (zero-ℝ , one-ℝ) neg-ℂ : {l : Level} → ℂ l → ℂ l neg-ℂ (a , b) = (neg-ℝ a , neg-ℝ b) ``` + +### `complex-ℝ one-ℝ` is equal to `one-ℂ` + +```agda +abstract + eq-complex-one-ℝ : complex-ℝ one-ℝ ＝ one-ℂ + eq-complex-one-ℝ = eq-ℂ refl (inv (eq-raise-ℝ zero-ℝ)) +``` diff --git a/src/complex-numbers/conjugation-complex-numbers.lagda.md b/src/complex-numbers/conjugation-complex-numbers.lagda.md new file mode 100644 index 0000000000..8f3eb54ba1 --- /dev/null +++ b/src/complex-numbers/conjugation-complex-numbers.lagda.md @@ -0,0 +1,42 @@ +# Conjugation of complex numbers + +```agda +module complex-numbers.conjugation-complex-numbers where +``` + +
Imports + +```agda +open import complex-numbers.complex-numbers + +open import foundation.identity-types +open import foundation.universe-levels + +open import real-numbers.negation-real-numbers +``` + +
+ +## Idea + +The +{{#concept "conjugate" WDID=Q381040 WD="complex conjugate" Disambiguation="of a complex number" Agda=conjugate-ℂ}} +of a [complex number](complex-numbers.complex-numbers.md) `a + bi` is `a - bi`. + +## Definition + +```agda +conjugate-ℂ : {l : Level} → ℂ l → ℂ l +conjugate-ℂ (a +iℂ b) = a +iℂ neg-ℝ b +``` + +## Properties + +### Conjugation is an involution + +```agda +abstract + is-involution-conjugate-ℂ : + {l : Level} (z : ℂ l) → conjugate-ℂ (conjugate-ℂ z) ＝ z + is-involution-conjugate-ℂ (a +iℂ b) = eq-ℂ refl (neg-neg-ℝ b) +``` diff --git a/src/complex-numbers/magnitude-complex-numbers.lagda.md b/src/complex-numbers/magnitude-complex-numbers.lagda.md new file mode 100644 index 0000000000..ee2b26b10c --- /dev/null +++ b/src/complex-numbers/magnitude-complex-numbers.lagda.md @@ -0,0 +1,233 @@ +# Magnitude of complex numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module complex-numbers.magnitude-complex-numbers where +``` + +
Imports + +```agda +open import complex-numbers.complex-numbers +open import complex-numbers.conjugation-complex-numbers +open import complex-numbers.multiplication-complex-numbers + +open import foundation.action-on-identifications-functions +open import foundation.identity-types +open import foundation.universe-levels + +open import real-numbers.addition-nonnegative-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.multiplication-nonnegative-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.square-roots-nonnegative-real-numbers +open import real-numbers.squares-real-numbers +``` + +
+ +## Idea + +The +{{#concept "magnitude" WD="magnitude of a complex number" WDID=Q3317982 Agda=magnitude-ℂ}} +of a [complex number](complex-numbers.complex-numbers.md) `a + bi` is defined as +$$\sqrt{a^2 + b^2}$$. + +## Definition + +```agda +nonnegative-squared-magnitude-ℂ : {l : Level} → ℂ l → ℝ⁰⁺ l +nonnegative-squared-magnitude-ℂ (a +iℂ b) = + nonnegative-square-ℝ a +ℝ⁰⁺ nonnegative-square-ℝ b + +squared-magnitude-ℂ : {l : Level} → ℂ l → ℝ l +squared-magnitude-ℂ z = real-ℝ⁰⁺ (nonnegative-squared-magnitude-ℂ z) + +∥_∥²ℂ : {l : Level} → ℂ l → ℝ l +∥ z ∥²ℂ = squared-magnitude-ℂ z + +nonnegative-magnitude-ℂ : {l : Level} → ℂ l → ℝ⁰⁺ l +nonnegative-magnitude-ℂ z = sqrt-ℝ⁰⁺ (nonnegative-squared-magnitude-ℂ z) + +magnitude-ℂ : {l : Level} → ℂ l → ℝ l +magnitude-ℂ z = real-ℝ⁰⁺ (nonnegative-magnitude-ℂ z) + +∥_∥ℂ : {l : Level} → ℂ l → ℝ l +∥ z ∥ℂ = magnitude-ℂ z +``` + +## Properties + +### The square of the magnitude of `z` is the product of `z` and the conjugate of `z` + +```agda +abstract + eq-squared-magnitude-mul-conjugate-ℂ : + {l : Level} (z : ℂ l) → + z *ℂ conjugate-ℂ z ＝ complex-ℝ (squared-magnitude-ℂ z) + eq-squared-magnitude-mul-conjugate-ℂ (a +iℂ b) = + eq-ℂ + ( equational-reasoning + square-ℝ a -ℝ (b *ℝ neg-ℝ b) + ＝ square-ℝ a -ℝ (neg-ℝ (square-ℝ b)) + by ap-diff-ℝ refl (right-negative-law-mul-ℝ _ _) + ＝ square-ℝ a +ℝ square-ℝ b + by ap-add-ℝ refl (neg-neg-ℝ _)) + ( eq-sim-ℝ + ( similarity-reasoning-ℝ + a *ℝ neg-ℝ b +ℝ b *ℝ a + ~ℝ neg-ℝ (a *ℝ b) +ℝ a *ℝ b + by + sim-eq-ℝ + ( ap-add-ℝ + ( right-negative-law-mul-ℝ a b) + ( commutative-mul-ℝ b a)) + ~ℝ zero-ℝ + by left-inverse-law-add-ℝ (a *ℝ b) + ~ℝ raise-ℝ _ zero-ℝ + by sim-raise-ℝ _ _)) +``` + +### The square of the magnitude of `zw` is the product of the squares of the magnitudes of `z` and `w` + +```agda +abstract + distributive-squared-magnitude-mul-ℂ : + {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → + squared-magnitude-ℂ (z *ℂ w) ＝ + squared-magnitude-ℂ z *ℝ squared-magnitude-ℂ w + distributive-squared-magnitude-mul-ℂ (a +iℂ b) (c +iℂ d) = + equational-reasoning + square-ℝ (a *ℝ c -ℝ b *ℝ d) +ℝ square-ℝ (a *ℝ d +ℝ b *ℝ c) + ＝ + ( square-ℝ (a *ℝ c) +ℝ + neg-ℝ (real-ℕ 2 *ℝ ((a *ℝ c) *ℝ (b *ℝ d))) +ℝ + square-ℝ (b *ℝ d)) +ℝ + ( square-ℝ (a *ℝ d) +ℝ + real-ℕ 2 *ℝ ((a *ℝ d) *ℝ (b *ℝ c)) +ℝ + square-ℝ (b *ℝ c)) + by + ap-add-ℝ + ( square-diff-ℝ _ _) + ( square-add-ℝ _ _) + ＝ + ( square-ℝ (a *ℝ c) +ℝ square-ℝ (b *ℝ d) +ℝ + neg-ℝ (real-ℕ 2 *ℝ (a *ℝ c *ℝ (b *ℝ d)))) +ℝ + ( square-ℝ (a *ℝ d) +ℝ square-ℝ (b *ℝ c) +ℝ + real-ℕ 2 *ℝ ((a *ℝ d) *ℝ (b *ℝ c))) + by + ap-add-ℝ + ( right-swap-add-ℝ _ _ _) + ( right-swap-add-ℝ _ _ _) + ＝ + ( ( square-ℝ (a *ℝ c) +ℝ square-ℝ (b *ℝ d)) +ℝ + ( square-ℝ (a *ℝ d) +ℝ square-ℝ (b *ℝ c))) +ℝ + ( neg-ℝ (real-ℕ 2 *ℝ ((a *ℝ c) *ℝ (b *ℝ d))) +ℝ + real-ℕ 2 *ℝ ((a *ℝ d) *ℝ (b *ℝ c))) + by interchange-law-add-add-ℝ _ _ _ _ + ＝ + ( ( square-ℝ (a *ℝ c) +ℝ square-ℝ (b *ℝ d)) +ℝ + ( square-ℝ (a *ℝ d) +ℝ square-ℝ (b *ℝ c))) +ℝ + ( neg-ℝ (real-ℕ 2 *ℝ (a *ℝ c *ℝ (b *ℝ d))) +ℝ + real-ℕ 2 *ℝ (a *ℝ d *ℝ (c *ℝ b))) + by + ap-add-ℝ + ( refl) + ( ap-add-ℝ + ( refl) + ( ap-mul-ℝ refl (ap-mul-ℝ refl (commutative-mul-ℝ b c)))) + ＝ + ( ( square-ℝ (a *ℝ c) +ℝ square-ℝ (b *ℝ d)) +ℝ + ( square-ℝ (a *ℝ d) +ℝ square-ℝ (b *ℝ c))) +ℝ + ( neg-ℝ (real-ℕ 2 *ℝ (a *ℝ c *ℝ (b *ℝ d))) +ℝ + real-ℕ 2 *ℝ (a *ℝ c *ℝ (d *ℝ b))) + by + ap-add-ℝ + ( refl) + ( ap-add-ℝ refl (ap-mul-ℝ refl (interchange-law-mul-mul-ℝ _ _ _ _))) + ＝ + ( ( square-ℝ (a *ℝ c) +ℝ square-ℝ (b *ℝ d)) +ℝ + ( square-ℝ (a *ℝ d) +ℝ square-ℝ (b *ℝ c))) +ℝ + ( neg-ℝ (real-ℕ 2 *ℝ (a *ℝ c *ℝ (b *ℝ d))) +ℝ + real-ℕ 2 *ℝ (a *ℝ c *ℝ (b *ℝ d))) + by + ap-add-ℝ + ( refl) + ( ap-add-ℝ + ( refl) + ( ap-mul-ℝ refl (ap-mul-ℝ refl (commutative-mul-ℝ d b)))) + ＝ + ( ( square-ℝ (a *ℝ c) +ℝ square-ℝ (b *ℝ d)) +ℝ + ( square-ℝ (a *ℝ d) +ℝ square-ℝ (b *ℝ c))) +ℝ + zero-ℝ + by eq-sim-ℝ (preserves-sim-left-add-ℝ _ _ _ (left-inverse-law-add-ℝ _)) + ＝ + ( square-ℝ (a *ℝ c) +ℝ square-ℝ (b *ℝ d)) +ℝ + ( square-ℝ (a *ℝ d) +ℝ square-ℝ (b *ℝ c)) + by right-unit-law-add-ℝ _ + ＝ + ( square-ℝ (a *ℝ c) +ℝ square-ℝ (a *ℝ d)) +ℝ + ( square-ℝ (b *ℝ d) +ℝ square-ℝ (b *ℝ c)) + by interchange-law-add-add-ℝ _ _ _ _ + ＝ + ( square-ℝ a *ℝ square-ℝ c +ℝ square-ℝ a *ℝ square-ℝ d) +ℝ + ( square-ℝ b *ℝ square-ℝ d +ℝ square-ℝ b *ℝ square-ℝ c) + by + ap-add-ℝ + ( ap-add-ℝ + ( distributive-square-mul-ℝ a c) + ( distributive-square-mul-ℝ a d)) + ( ap-add-ℝ + ( distributive-square-mul-ℝ b d) + ( distributive-square-mul-ℝ b c)) + ＝ + square-ℝ a *ℝ (square-ℝ c +ℝ square-ℝ d) +ℝ + square-ℝ b *ℝ (square-ℝ d +ℝ square-ℝ c) + by + inv + ( ap-add-ℝ + ( left-distributive-mul-add-ℝ _ _ _) + ( left-distributive-mul-add-ℝ _ _ _)) + ＝ + square-ℝ a *ℝ (square-ℝ c +ℝ square-ℝ d) +ℝ + square-ℝ b *ℝ (square-ℝ c +ℝ square-ℝ d) + by ap-add-ℝ refl (ap-mul-ℝ refl (commutative-add-ℝ _ _)) + ＝ + (square-ℝ a +ℝ square-ℝ b) *ℝ (square-ℝ c +ℝ square-ℝ d) + by + inv + ( right-distributive-mul-add-ℝ + ( square-ℝ a) + ( square-ℝ b) + ( square-ℝ c +ℝ square-ℝ d)) +``` + +### The magnitude of `zw` is the product of the magnitudes of `z` and `w` + +```agda +abstract + distributive-magnitude-mul-ℂ : + {l1 l2 : Level} (z : ℂ l1) (w : ℂ l2) → + magnitude-ℂ (z *ℂ w) ＝ magnitude-ℂ z *ℝ magnitude-ℂ w + distributive-magnitude-mul-ℂ z w = + equational-reasoning + real-sqrt-ℝ⁰⁺ (nonnegative-squared-magnitude-ℂ (z *ℂ w)) + ＝ + real-sqrt-ℝ⁰⁺ + ( nonnegative-squared-magnitude-ℂ z *ℝ⁰⁺ + nonnegative-squared-magnitude-ℂ w) + by + ap + ( real-sqrt-ℝ⁰⁺) + ( eq-ℝ⁰⁺ _ _ (distributive-squared-magnitude-mul-ℂ z w)) + ＝ magnitude-ℂ z *ℝ magnitude-ℂ w + by ap real-ℝ⁰⁺ (distributive-sqrt-mul-ℝ⁰⁺ _ _) +``` diff --git a/src/complex-numbers/multiplication-complex-numbers.lagda.md b/src/complex-numbers/multiplication-complex-numbers.lagda.md index fcef6b3b34..8893042eeb 100644 --- a/src/complex-numbers/multiplication-complex-numbers.lagda.md +++ b/src/complex-numbers/multiplication-complex-numbers.lagda.md @@ -13,6 +13,7 @@ open import complex-numbers.similarity-complex-numbers open import elementary-number-theory.rational-numbers +open import foundation.action-on-identifications-binary-functions open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.identity-types @@ -20,9 +21,11 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers open import real-numbers.multiplication-real-numbers open import real-numbers.negation-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 ``` @@ -45,6 +48,11 @@ mul-ℂ (a , b) (c , d) = (a *ℝ c -ℝ b *ℝ d , a *ℝ d +ℝ b *ℝ c) infixl 40 _*ℂ_ _*ℂ_ : {l1 l2 : Level} → ℂ l1 → ℂ l2 → ℂ (l1 ⊔ l2) _*ℂ_ = mul-ℂ + +ap-mul-ℂ : + {l1 l2 : Level} {z z' : ℂ l1} → z ＝ z' → {w w' : ℂ l2} → w ＝ w' → + mul-ℂ z w ＝ mul-ℂ z' w' +ap-mul-ℂ = ap-binary mul-ℂ ``` ## Properties @@ -256,6 +264,48 @@ opaque by left-unit-law-add-ℝ zero-ℝ) ``` +### The canonical embedding of real numbers in the complex numbers preserves multiplication + +```agda +abstract + mul-complex-ℝ : + {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → + complex-ℝ x *ℂ complex-ℝ y ＝ complex-ℝ (x *ℝ y) + mul-complex-ℝ {l1} {l2} x y = + eq-ℂ + ( equational-reasoning + x *ℝ y -ℝ raise-ℝ l1 zero-ℝ *ℝ raise-ℝ l2 zero-ℝ + ＝ x *ℝ y -ℝ zero-ℝ *ℝ zero-ℝ + by + eq-sim-ℝ + ( preserves-sim-diff-ℝ + ( refl-sim-ℝ (x *ℝ y)) + ( symmetric-sim-ℝ + ( preserves-sim-mul-ℝ (sim-raise-ℝ _ _) (sim-raise-ℝ _ _)))) + ＝ x *ℝ y -ℝ zero-ℝ + by ap-diff-ℝ refl (eq-sim-ℝ (right-zero-law-mul-ℝ _)) + ＝ x *ℝ y + by right-unit-law-diff-ℝ (x *ℝ y)) + ( eq-sim-ℝ + ( similarity-reasoning-ℝ + x *ℝ raise-ℝ l2 zero-ℝ +ℝ raise-ℝ l1 zero-ℝ *ℝ y + ~ℝ x *ℝ zero-ℝ +ℝ zero-ℝ *ℝ y + by + symmetric-sim-ℝ + ( preserves-sim-add-ℝ + ( preserves-sim-left-mul-ℝ _ _ _ (sim-raise-ℝ l2 zero-ℝ)) + ( preserves-sim-right-mul-ℝ _ _ _ (sim-raise-ℝ l1 zero-ℝ))) + ~ℝ zero-ℝ +ℝ zero-ℝ + by + preserves-sim-add-ℝ + ( right-zero-law-mul-ℝ x) + ( left-zero-law-mul-ℝ y) + ~ℝ zero-ℝ + by sim-eq-ℝ (left-unit-law-add-ℝ zero-ℝ) + ~ℝ raise-ℝ (l1 ⊔ l2) zero-ℝ + by sim-raise-ℝ (l1 ⊔ l2) zero-ℝ)) +``` + ### Similarity is preserved by multiplication ```agda diff --git a/src/complex-numbers/multiplicative-inverses-nonzero-complex-numbers.lagda.md b/src/complex-numbers/multiplicative-inverses-nonzero-complex-numbers.lagda.md new file mode 100644 index 0000000000..183fbec3b2 --- /dev/null +++ b/src/complex-numbers/multiplicative-inverses-nonzero-complex-numbers.lagda.md @@ -0,0 +1,88 @@ +# Multiplicative inverses of complex numbers + +```agda +module complex-numbers.multiplicative-inverses-nonzero-complex-numbers where +``` + +
Imports + +```agda +open import complex-numbers.complex-numbers +open import complex-numbers.conjugation-complex-numbers +open import complex-numbers.magnitude-complex-numbers +open import complex-numbers.multiplication-complex-numbers +open import complex-numbers.nonzero-complex-numbers +open import complex-numbers.similarity-complex-numbers + +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.multiplication-real-numbers +open import real-numbers.multiplicative-inverses-positive-real-numbers +open import real-numbers.rational-real-numbers +``` + +
+ +## Idea + +[Nonzero](complex-numbers.nonzero-complex-numbers.md) +[complex numbers](complex-numbers.complex-numbers.md) have inverses under +[multiplication](complex-numbers.multiplication-complex-numbers.md). + +## Definition + +```agda +complex-inv-nonzero-ℂ : {l : Level} (z : nonzero-ℂ l) → ℂ l +complex-inv-nonzero-ℂ (z , z≠0) = + conjugate-ℂ z *ℂ + complex-ℝ (real-inv-ℝ⁺ (positive-squared-magnitude-nonzero-ℂ (z , z≠0))) +``` + +## Properties + +### Inverse laws of multiplication + +```agda +abstract + right-inverse-law-mul-nonzero-ℂ : {l : Level} (z : nonzero-ℂ l) → + sim-ℂ (complex-nonzero-ℂ z *ℂ complex-inv-nonzero-ℂ z) one-ℂ + right-inverse-law-mul-nonzero-ℂ (z@(a +iℂ b) , z≠0) = + similarity-reasoning-ℂ + z *ℂ + ( conjugate-ℂ z *ℂ + complex-ℝ + ( real-inv-ℝ⁺ (positive-squared-magnitude-nonzero-ℂ (z , z≠0)))) + ~ℂ + ( z *ℂ conjugate-ℂ z) *ℂ + ( complex-ℝ + ( real-inv-ℝ⁺ (positive-squared-magnitude-nonzero-ℂ (z , z≠0)))) + by sim-eq-ℂ (inv (associative-mul-ℂ _ _ _)) + ~ℂ + complex-ℝ (squared-magnitude-ℂ z) *ℂ + complex-ℝ + ( real-inv-ℝ⁺ (positive-squared-magnitude-nonzero-ℂ (z , z≠0))) + by sim-eq-ℂ (ap-mul-ℂ (eq-squared-magnitude-mul-conjugate-ℂ z) refl) + ~ℂ + complex-ℝ + ( squared-magnitude-ℂ z *ℝ + real-inv-ℝ⁺ (positive-squared-magnitude-nonzero-ℂ (z , z≠0))) + by sim-eq-ℂ (mul-complex-ℝ _ _) + ~ℂ complex-ℝ one-ℝ + by + preserves-sim-complex-ℝ + ( right-inverse-law-mul-ℝ⁺ + ( positive-squared-magnitude-nonzero-ℂ (z , z≠0))) + ~ℂ one-ℂ + by sim-eq-ℂ eq-complex-one-ℝ + + left-inverse-law-mul-nonzero-ℂ : {l : Level} (z : nonzero-ℂ l) → + sim-ℂ (complex-inv-nonzero-ℂ z *ℂ complex-nonzero-ℂ z) one-ℂ + left-inverse-law-mul-nonzero-ℂ z = + tr + ( λ w → sim-ℂ w one-ℂ) + ( commutative-mul-ℂ _ _) + ( right-inverse-law-mul-nonzero-ℂ z) +``` diff --git a/src/complex-numbers/nonzero-complex-numbers.lagda.md b/src/complex-numbers/nonzero-complex-numbers.lagda.md new file mode 100644 index 0000000000..a10fec5897 --- /dev/null +++ b/src/complex-numbers/nonzero-complex-numbers.lagda.md @@ -0,0 +1,99 @@ +# Nonzero complex numbers + +```agda +module complex-numbers.nonzero-complex-numbers where +``` + +
Imports + +```agda +open import complex-numbers.apartness-complex-numbers +open import complex-numbers.complex-numbers +open import complex-numbers.magnitude-complex-numbers + +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.propositions +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.addition-nonnegative-real-numbers +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.nonzero-real-numbers +open import real-numbers.positive-and-negative-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.squares-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +A [complex number](complex-numbers.complex-numbers.md) is +{{#concept "nonzero" Agda=is-nonzero-ℂ}} if it is +[apart](complex-numbers.apartness-complex-numbers.md) from zero, that is, its +[real](real-numbers.dedekind-real-numbers.md) part +[or](foundation.disjunction.md) its imaginary part are +[nonzero](real-numbers.nonzero-real-numbers.md). + +## Definition + +```agda +is-nonzero-prop-ℂ : {l : Level} → ℂ l → Prop l +is-nonzero-prop-ℂ z = apart-prop-ℂ z zero-ℂ + +is-nonzero-ℂ : {l : Level} → ℂ l → UU l +is-nonzero-ℂ z = type-Prop (is-nonzero-prop-ℂ z) + +nonzero-ℂ : (l : Level) → UU (lsuc l) +nonzero-ℂ l = type-subtype (is-nonzero-prop-ℂ {l}) + +complex-nonzero-ℂ : {l : Level} → nonzero-ℂ l → ℂ l +complex-nonzero-ℂ = pr1 +``` + +## Properties + +### A complex number is nonzero if and only if its squared magnitude is positive + +```agda +abstract + is-positive-squared-magnitude-is-nonzero-ℂ : + {l : Level} (z : ℂ l) → is-nonzero-ℂ z → is-positive-ℝ ∥ z ∥²ℂ + is-positive-squared-magnitude-is-nonzero-ℂ (a +iℂ b) = + elim-disjunction + ( is-positive-prop-ℝ ∥ a +iℂ b ∥²ℂ) + ( λ a≠0 → + concatenate-le-leq-ℝ + ( zero-ℝ) + ( square-ℝ a) + ( square-ℝ a +ℝ square-ℝ b) + ( is-positive-square-is-nonzero-ℝ a a≠0) + ( leq-left-add-real-ℝ⁰⁺ _ (nonnegative-square-ℝ b))) + ( λ b≠0 → + concatenate-le-leq-ℝ + ( zero-ℝ) + ( square-ℝ b) + ( square-ℝ a +ℝ square-ℝ b) + ( is-positive-square-is-nonzero-ℝ b b≠0) + ( leq-right-add-real-ℝ⁰⁺ _ (nonnegative-square-ℝ a))) + + is-nonzero-is-positive-squared-magnitude-ℂ : + {l : Level} (z : ℂ l) → is-positive-ℝ ∥ z ∥²ℂ → is-nonzero-ℂ z + is-nonzero-is-positive-squared-magnitude-ℂ (a +iℂ b) 0Imports + +```agda +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.addition-nonnegative-rational-numbers +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers +open import elementary-number-theory.archimedean-property-rational-numbers +open import elementary-number-theory.exponentiation-natural-numbers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.multiplication-positive-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.positive-and-negative-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.series-rational-numbers +open import elementary-number-theory.strict-inequality-natural-numbers +open import elementary-number-theory.strict-inequality-rational-numbers +open import elementary-number-theory.sums-of-finite-sequences-of-rational-numbers +open import elementary-number-theory.unit-fractions-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.function-extensionality +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 group-theory.abelian-groups + +open import order-theory.posets + +open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.standard-finite-types +``` + + + +## Idea + +The +{{#concept "harmonic series" WDID=Q464100 WD="harmonic series" Agda=harmonic-series-ℚ}} +is the sum $$Σ_{n=0}^{∞} \frac{1}{n}$$. + +## Definition + +```agda +harmonic-series-ℚ : series-ℚ +harmonic-series-ℚ = series-terms-ℚ reciprocal-rational-succ-ℕ +``` + +## Properties + +### For any `k`, the `2ᵏ`th partial sum of the harmonic series is at least `1 + k/2` + +```agda +abstract + lower-bound-sum-harmonic-series-power-of-two-ℚ : + (k : ℕ) → + leq-ℚ + ( one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ rational-ℕ k) + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 k)) + lower-bound-sum-harmonic-series-power-of-two-ℚ 0 = + leq-eq-ℚ + ( inv + ( equational-reasoning + partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 zero-ℕ) + ＝ reciprocal-rational-succ-ℕ 0 + by compute-sum-one-element-ℚ _ + ＝ one-ℚ + by ap rational-ℚ⁺ inv-one-ℚ⁺ + ＝ one-ℚ +ℚ zero-ℚ + by inv (right-unit-law-add-ℚ one-ℚ) + ＝ one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ zero-ℚ + by ap-add-ℚ refl (inv (right-zero-law-mul-ℚ _)))) + lower-bound-sum-harmonic-series-power-of-two-ℚ (succ-ℕ n) = + let + open inequality-reasoning-Poset ℚ-Poset + in + chain-of-inequalities + one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ rational-ℕ (succ-ℕ n) + ≤ one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ succ-ℚ (rational-ℕ n) + by leq-eq-ℚ (ap-add-ℚ refl (ap-mul-ℚ refl (inv (succ-rational-ℕ n)))) + ≤ ( one-ℚ) +ℚ + ( reciprocal-rational-succ-ℕ 1 +ℚ + reciprocal-rational-succ-ℕ 1 *ℚ rational-ℕ n) + by leq-eq-ℚ (ap-add-ℚ refl (mul-right-succ-ℚ _ _)) + ≤ ( reciprocal-rational-succ-ℕ 1) +ℚ + ( one-ℚ +ℚ reciprocal-rational-succ-ℕ 1 *ℚ rational-ℕ n) + by leq-eq-ℚ (left-swap-add-ℚ _ _ _) + ≤ ( reciprocal-rational-succ-ℕ 1) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by + preserves-leq-right-add-ℚ _ _ _ + ( lower-bound-sum-harmonic-series-power-of-two-ℚ n) + ≤ ( ( rational-ℕ (exp-ℕ 2 n)) *ℚ + ( reciprocal-rational-succ-ℕ 1) *ℚ + ( reciprocal-rational-ℕ⁺ (exp-ℕ⁺ (2 , (λ ())) n))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by + leq-eq-ℚ + ( ap-add-ℚ + ( inv + ( ap + ( rational-ℚ⁺) + ( is-identity-left-conjugation-Ab + ( abelian-group-mul-ℚ⁺) + ( positive-rational-ℕ⁺ (exp-ℕ⁺ (2 , λ ()) n)) + ( positive-reciprocal-rational-succ-ℕ 1)))) + ( refl)) + ≤ ( ( rational-ℕ (exp-ℕ 2 n)) *ℚ + ( ( reciprocal-rational-succ-ℕ 1) *ℚ + ( reciprocal-rational-ℕ⁺ (exp-ℕ⁺ (2 , (λ ())) n)))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by leq-eq-ℚ (ap-add-ℚ (associative-mul-ℚ _ _ _) refl) + ≤ ( ( rational-ℕ (exp-ℕ 2 n)) *ℚ + ( ( reciprocal-rational-ℕ⁺ (exp-ℕ⁺ (2 , (λ ())) n)) *ℚ + ( reciprocal-rational-succ-ℕ 1))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by leq-eq-ℚ (ap-add-ℚ (ap-mul-ℚ refl (commutative-mul-ℚ _ _)) refl) + ≤ ( ( rational-ℕ (exp-ℕ 2 n)) *ℚ + ( reciprocal-rational-ℕ⁺ (exp-ℕ⁺ (2 , λ ()) (succ-ℕ n)))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by + leq-eq-ℚ + ( ap-add-ℚ + ( ap-mul-ℚ + ( refl) + ( ( inv + ( distributive-reciprocal-mul-ℕ⁺ + ( exp-ℕ⁺ (2 , λ ()) n) + ( 2 , λ ()))) ∙ + ( ap + ( reciprocal-rational-ℕ⁺) + ( eq-nonzero-ℕ + { exp-ℕ⁺ (2 , λ ()) n *ℕ⁺ (2 , λ ())} + { exp-ℕ⁺ (2 , (λ ())) (succ-ℕ n)} + ( refl))))) + ( refl)) + ≤ ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ _ → reciprocal-rational-ℕ⁺ (exp-ℕ⁺ (2 , (λ ())) (succ-ℕ n)))) +ℚ + ( partial-sum-series-ℚ harmonic-series-ℚ (exp-ℕ 2 n)) + by leq-eq-ℚ (ap-add-ℚ (inv (sum-constant-fin-sequence-ℚ _ _)) refl) + ≤ ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inr-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) +ℚ + ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → reciprocal-rational-succ-ℕ (nat-Fin (exp-ℕ 2 n) k))) + by + preserves-leq-left-add-ℚ _ _ _ + ( preserves-leq-sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( _) + ( _) + ( λ k → + inv-leq-ℚ⁺ _ _ + ( preserves-leq-rational-ℕ + ( leq-succ-le-ℕ + ( nat-Fin (exp-ℕ 2 n +ℕ exp-ℕ 2 n) _) + ( exp-ℕ 2 (succ-ℕ n)) + ( inv-tr + ( le-ℕ _) + ( right-two-law-mul-ℕ _) + ( strict-upper-bound-nat-Fin _ _)))))) + ≤ ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inr-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) +ℚ + ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inl-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) + by + leq-eq-ℚ + ( ap-add-ℚ + ( refl) + ( ap + ( sum-fin-sequence-ℚ (exp-ℕ 2 n)) + ( eq-htpy + ( λ k → + ap + ( reciprocal-rational-succ-ℕ) + ( inv (nat-inl-coproduct-Fin _ _ k)))))) + ≤ ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inl-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) +ℚ + ( sum-fin-sequence-ℚ + ( exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ + ( nat-Fin + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( inr-coproduct-Fin (exp-ℕ 2 n) (exp-ℕ 2 n) k)))) + by leq-eq-ℚ (commutative-add-ℚ _ _) + ≤ sum-fin-sequence-ℚ + ( exp-ℕ 2 n +ℕ exp-ℕ 2 n) + ( λ k → + reciprocal-rational-succ-ℕ (nat-Fin (exp-ℕ 2 n +ℕ exp-ℕ 2 n) k)) + by leq-eq-ℚ (inv (split-sum-fin-sequence-ℚ _ _ _)) + ≤ sum-fin-sequence-ℚ + ( exp-ℕ 2 (succ-ℕ n)) + ( reciprocal-rational-succ-ℕ ∘ nat-Fin (exp-ℕ 2 (succ-ℕ n))) + by + leq-eq-ℚ + ( ap + ( λ k → + sum-fin-sequence-ℚ k (reciprocal-rational-succ-ℕ ∘ nat-Fin k)) + ( inv (right-two-law-mul-ℕ _))) +``` + +### The harmonic series diverges + +The divergence of the harmonic series is the +[34th](literature.100-theorems.md#34) theorem on +[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of +[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. + +```agda +abstract + grows-without-bound-harmonic-series-ℚ : + grows-without-bound-series-ℚ harmonic-series-ℚ + grows-without-bound-harmonic-series-ℚ q = + let + open + do-syntax-trunc-Prop + ( ∃ ℕ (partial-sum-stays-above-prop-series-ℚ harmonic-series-ℚ q)) + open inequality-reasoning-Poset ℚ-Poset + in do + (n , 2q @@ -452,17 +455,33 @@ abstract by ap-add-ℚ (right-unit-law-mul-ℚ p) refl ``` +### Multiplication by a natural number is repeated addition + +```agda +abstract + left-mul-rational-nat-ℚ : + (n : ℕ) (q : ℚ) → rational-ℕ n *ℚ q ＝ multiple-Ab abelian-group-add-ℚ n q + left-mul-rational-nat-ℚ 0 q = left-zero-law-mul-ℚ q + left-mul-rational-nat-ℚ 1 q = left-unit-law-mul-ℚ q + left-mul-rational-nat-ℚ (succ-ℕ n@(succ-ℕ _)) q = + equational-reasoning + rational-ℕ (succ-ℕ n) *ℚ q + ＝ succ-ℚ (rational-ℕ n) *ℚ q + by ap-mul-ℚ (inv (succ-rational-ℕ n)) refl + ＝ q +ℚ rational-ℕ n *ℚ q by + mul-left-succ-ℚ _ _ + ＝ q +ℚ multiple-Ab abelian-group-add-ℚ n q + by ap-add-ℚ refl (left-mul-rational-nat-ℚ n q) + ＝ multiple-Ab abelian-group-add-ℚ (succ-ℕ n) q + by inv (multiple-succ-Ab' abelian-group-add-ℚ n q) +``` + ### `2q = q + q` ```agda abstract mul-two-ℚ : (q : ℚ) → rational-ℕ 2 *ℚ q ＝ q +ℚ q - mul-two-ℚ q = - equational-reasoning - rational-ℤ (one-ℤ +ℤ one-ℤ) *ℚ q - ＝ (one-ℚ +ℚ one-ℚ) *ℚ q by ap (_*ℚ q) (inv (add-rational-ℤ one-ℤ one-ℤ)) - ＝ (one-ℚ *ℚ q) +ℚ (one-ℚ *ℚ q) by right-distributive-mul-add-ℚ _ _ _ - ＝ q +ℚ q by ap-add-ℚ (left-unit-law-mul-ℚ q) (left-unit-law-mul-ℚ q) + mul-two-ℚ = left-mul-rational-nat-ℚ 2 ``` ### The product of a rational number and its denominator is its numerator diff --git a/src/elementary-number-theory/series-rational-numbers.lagda.md b/src/elementary-number-theory/series-rational-numbers.lagda.md new file mode 100644 index 0000000000..15f361eeda --- /dev/null +++ b/src/elementary-number-theory/series-rational-numbers.lagda.md @@ -0,0 +1,102 @@ +# Series of rational numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module elementary-number-theory.series-rational-numbers where +``` + +
Imports + +```agda +open import analysis.convergent-series-metric-abelian-groups +open import analysis.series-metric-abelian-groups + +open import elementary-number-theory.addition-nonnegative-rational-numbers +open import elementary-number-theory.inequality-natural-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.metric-additive-group-of-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.rational-numbers + +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.propositions +open import foundation.universe-levels + +open import lists.sequences + +open import order-theory.monotonic-sequences-posets +open import order-theory.order-preserving-maps-posets +``` + +
+ +## Idea + +A {{#concept "series" Disambiguation="in ℚ" Agda=series-ℚ}} of +[rational numbers](elementary-number-theory.rational-numbers.md) is a +[series](analysis.series-metric-abelian-groups.md) in the +[metric additive group of rational numbers](elementary-number-theory.metric-additive-group-of-rational-numbers.md) + +## Definition + +```agda +series-ℚ : UU lzero +series-ℚ = series-Metric-Ab metric-ab-add-ℚ + +series-terms-ℚ : sequence ℚ → series-ℚ +series-terms-ℚ = series-terms-Metric-Ab + +partial-sum-series-ℚ : series-ℚ → ℕ → ℚ +partial-sum-series-ℚ = partial-sum-series-Metric-Ab + +term-series-ℚ : series-ℚ → ℕ → ℚ +term-series-ℚ = term-series-Metric-Ab +``` + +## Properties + +### The proposition that a series converges to a sum + +```agda +is-sum-prop-series-ℚ : series-ℚ → ℚ → Prop lzero +is-sum-prop-series-ℚ = is-sum-prop-series-Metric-Ab + +is-sum-series-ℚ : series-ℚ → ℚ → UU lzero +is-sum-series-ℚ = is-sum-series-Metric-Ab +``` + +### The proposition that a series grows without bound + +```agda +partial-sum-stays-above-prop-series-ℚ : series-ℚ → ℚ → ℕ → Prop lzero +partial-sum-stays-above-prop-series-ℚ σ q n = + Π-Prop ℕ (λ k → leq-ℕ-Prop n k ⇒ leq-ℚ-Prop q (partial-sum-series-ℚ σ k)) + +grows-without-bound-prop-series-ℚ : series-ℚ → Prop lzero +grows-without-bound-prop-series-ℚ σ = + Π-Prop ℚ (λ q → ∃ ℕ (partial-sum-stays-above-prop-series-ℚ σ q)) + +grows-without-bound-series-ℚ : series-ℚ → UU lzero +grows-without-bound-series-ℚ σ = + type-Prop (grows-without-bound-prop-series-ℚ σ) +``` + +### If all elements of a series are nonnegative, its partial sums are monotonic + +```agda +abstract + is-monotonic-partial-sum-is-nonnegative-term-series-ℚ : + (σ : series-ℚ) → ((n : ℕ) → is-nonnegative-ℚ (term-series-ℚ σ n)) → + is-monotonic-sequence-Poset ℚ-Poset (partial-sum-series-ℚ σ) + is-monotonic-partial-sum-is-nonnegative-term-series-ℚ σ H = + is-monotonic-sequence-is-increasing-Poset + ( ℚ-Poset) + ( partial-sum-series-ℚ σ) + ( λ n → + is-inflationary-map-right-add-rational-ℚ⁰⁺ + ( term-series-ℚ σ n , H n) + ( partial-sum-series-ℚ σ n)) +``` diff --git a/src/elementary-number-theory/sums-of-finite-sequences-of-rational-numbers.lagda.md b/src/elementary-number-theory/sums-of-finite-sequences-of-rational-numbers.lagda.md new file mode 100644 index 0000000000..374a1d8051 --- /dev/null +++ b/src/elementary-number-theory/sums-of-finite-sequences-of-rational-numbers.lagda.md @@ -0,0 +1,109 @@ +# Sums of finite sequences of rational numbers + +```agda +module elementary-number-theory.sums-of-finite-sequences-of-rational-numbers where +``` + +
Imports + +```agda +open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings + +open import elementary-number-theory.addition-natural-numbers +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.ring-of-rational-numbers + +open import foundation.function-types +open import foundation.identity-types + +open import lists.finite-sequences + +open import univalent-combinatorics.coproduct-types +open import univalent-combinatorics.standard-finite-types +``` + +
+ +## Idea + +The +{{#concept "sum operation" Disambiguation="of a finite sequence of rational numbers" Agda=sum-fin-sequence-ℚ}} +extends [addition](elementary-number-theory.addition-rational-numbers.md) on the +[rational numbers](elementary-number-theory.rational-numbers.md) to any +[finite sequence](lists.finite-sequences.md) of rational numbers. + +## Definition + +```agda +sum-fin-sequence-ℚ : (n : ℕ) → fin-sequence ℚ n → ℚ +sum-fin-sequence-ℚ = sum-fin-sequence-type-Commutative-Ring commutative-ring-ℚ +``` + +## Properties + +### The sum of a constant sequence is multiplication by a natural number + +```agda +abstract + sum-constant-fin-sequence-ℚ : + (n : ℕ) (q : ℚ) → + sum-fin-sequence-ℚ n (λ _ → q) ＝ rational-ℕ n *ℚ q + sum-constant-fin-sequence-ℚ n q = + sum-constant-fin-sequence-type-Commutative-Ring commutative-ring-ℚ n q ∙ + inv (left-mul-rational-nat-ℚ n q) +``` + +### If `aₙ ≤ bₙ` for each `n`, then `Σ aₙ ≤ Σ bₙ` + +```agda +abstract + preserves-leq-sum-fin-sequence-ℚ : + (n : ℕ) (a b : fin-sequence ℚ n) → ((k : Fin n) → leq-ℚ (a k) (b k)) → + leq-ℚ (sum-fin-sequence-ℚ n a) (sum-fin-sequence-ℚ n b) + preserves-leq-sum-fin-sequence-ℚ 0 _ _ _ = refl-leq-ℚ zero-ℚ + preserves-leq-sum-fin-sequence-ℚ (succ-ℕ n) a b H = + preserves-leq-add-ℚ + ( preserves-leq-sum-fin-sequence-ℚ + ( n) + ( a ∘ inl-Fin n) + ( b ∘ inl-Fin n) + ( H ∘ inl-Fin n)) + ( H (neg-one-Fin n)) +``` + +### Multiplication is distributive over sums on finite sequences + +```agda +abstract + left-distributive-mul-sum-fin-sequence-ℚ : + (n : ℕ) (q : ℚ) (a : fin-sequence ℚ n) → + q *ℚ sum-fin-sequence-ℚ n a ＝ sum-fin-sequence-ℚ n (mul-ℚ q ∘ a) + left-distributive-mul-sum-fin-sequence-ℚ = + left-distributive-mul-sum-fin-sequence-type-Commutative-Ring + ( commutative-ring-ℚ) +``` + +### Splitting sums of `n + m` elements into a sum of `n` elements and a sum of `m` elements + +```agda +split-sum-fin-sequence-ℚ : + (n m : ℕ) (f : fin-sequence ℚ (n +ℕ m)) → + sum-fin-sequence-ℚ (n +ℕ m) f ＝ + sum-fin-sequence-ℚ n (f ∘ inl-coproduct-Fin n m) +ℚ + sum-fin-sequence-ℚ m (f ∘ inr-coproduct-Fin n m) +split-sum-fin-sequence-ℚ = + split-sum-fin-sequence-type-Commutative-Ring commutative-ring-ℚ +``` + +### The sum of a single element is the single element + +```agda +compute-sum-one-element-ℚ : + (a : fin-sequence ℚ 1) → sum-fin-sequence-ℚ 1 a ＝ a (zero-Fin 0) +compute-sum-one-element-ℚ = + compute-sum-one-element-Commutative-Ring commutative-ring-ℚ +``` diff --git a/src/elementary-number-theory/triangular-numbers.lagda.md b/src/elementary-number-theory/triangular-numbers.lagda.md index 0a3f74aae1..d7c5a79cef 100644 --- a/src/elementary-number-theory/triangular-numbers.lagda.md +++ b/src/elementary-number-theory/triangular-numbers.lagda.md @@ -9,15 +9,11 @@ module elementary-number-theory.triangular-numbers where
Imports ```agda -open import analysis.convergent-series-metric-abelian-groups -open import analysis.series-metric-abelian-groups - open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.divisibility-natural-numbers -open import elementary-number-theory.metric-additive-group-of-rational-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.multiplication-rational-numbers @@ -27,6 +23,7 @@ open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.semiring-of-natural-numbers +open import elementary-number-theory.series-rational-numbers open import elementary-number-theory.unit-fractions-rational-numbers open import foundation.action-on-identifications-functions @@ -203,15 +200,14 @@ abstract ( eq-nonzero-ℕ ( compute-double-triangular-number-ℕ (succ-ℕ n))))) -series-reciprocal-triangular-number-ℕ : series-Metric-Ab metric-ab-add-ℚ +series-reciprocal-triangular-number-ℕ : series-ℚ series-reciprocal-triangular-number-ℕ = - series-terms-Metric-Ab reciprocal-triangular-number-succ-ℕ + series-terms-ℚ reciprocal-triangular-number-succ-ℕ abstract compute-partial-sum-series-reciprocal-triangular-number-ℕ : (n : ℕ) → - partial-sum-series-Metric-Ab - ( metric-ab-add-ℚ) + partial-sum-series-ℚ ( series-reciprocal-triangular-number-ℕ) ( n) ＝ rational-ℕ 2 *ℚ (one-ℚ -ℚ reciprocal-rational-succ-ℕ n) @@ -227,8 +223,7 @@ abstract by right-zero-law-mul-ℚ _) compute-partial-sum-series-reciprocal-triangular-number-ℕ (succ-ℕ n) = equational-reasoning - partial-sum-series-Metric-Ab - ( metric-ab-add-ℚ) + partial-sum-series-ℚ ( series-reciprocal-triangular-number-ℕ) ( n) +ℚ reciprocal-triangular-number-succ-ℕ n @@ -271,7 +266,7 @@ This theorem is the [42nd](literature.100-theorems.md#42) theorem on ```agda abstract sum-reciprocal-triangular-number-ℕ : - is-sum-series-Metric-Ab + is-sum-series-ℚ ( series-reciprocal-triangular-number-ℕ) ( rational-ℕ 2) sum-reciprocal-triangular-number-ℕ = diff --git a/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md b/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md index 035a9a963f..8d26e1dcbc 100644 --- a/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md +++ b/src/elementary-number-theory/unit-fractions-rational-numbers.lagda.md @@ -119,6 +119,19 @@ module _ ( eq-denominator-reciprocal-rational-ℤ⁺) ``` +### Taking the reciprocal of a nonzero natural number distributes over multiplication + +```agda +abstract + distributive-reciprocal-mul-ℕ⁺ : + (m n : ℕ⁺) → + reciprocal-rational-ℕ⁺ (m *ℕ⁺ n) ＝ + reciprocal-rational-ℕ⁺ m *ℚ reciprocal-rational-ℕ⁺ n + distributive-reciprocal-mul-ℕ⁺ m⁺@(m , _) n⁺@(n , _) = + ap rational-inv-ℚ⁺ (eq-ℚ⁺ (inv (mul-rational-ℕ m n))) ∙ + ap rational-ℚ⁺ (distributive-inv-mul-ℚ⁺ _ _) +``` + ### If `m ≤ n`, the reciprocal of `n` is less than or equal to the reciprocal of `n` ```agda 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/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md index 266b0d6d45..6eb7fb632f 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-abelian-groups.lagda.md @@ -218,11 +218,11 @@ module _ ```agda abstract - constant-sum-fin-sequence-type-Ab : + sum-constant-fin-sequence-type-Ab : {l : Level} (G : Ab l) (n : ℕ) (x : type-Ab G) → sum-fin-sequence-type-Ab G n (λ _ → x) ＝ multiple-Ab G n x - constant-sum-fin-sequence-type-Ab G = - constant-sum-fin-sequence-type-Group (group-Ab G) + sum-constant-fin-sequence-type-Ab G = + sum-constant-fin-sequence-type-Group (group-Ab G) ``` ## See also diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md index 374bcb0542..2386f64fef 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-commutative-monoids.lagda.md @@ -260,13 +260,13 @@ module _ ```agda abstract - constant-sum-fin-sequence-type-Commutative-Monoid : + sum-constant-fin-sequence-type-Commutative-Monoid : {l : Level} (M : Commutative-Monoid l) (n : ℕ) → (x : type-Commutative-Monoid M) → sum-fin-sequence-type-Commutative-Monoid M n (λ _ → x) ＝ power-Commutative-Monoid M n x - constant-sum-fin-sequence-type-Commutative-Monoid M = - constant-sum-fin-sequence-type-Monoid (monoid-Commutative-Monoid M) + sum-constant-fin-sequence-type-Commutative-Monoid M = + sum-constant-fin-sequence-type-Monoid (monoid-Commutative-Monoid M) ``` ## See also diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-groups.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-groups.lagda.md index 33badd9fbc..27101833bb 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-groups.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-groups.lagda.md @@ -184,9 +184,9 @@ split-sum-fin-sequence-type-Group G = ```agda abstract - constant-sum-fin-sequence-type-Group : + sum-constant-fin-sequence-type-Group : {l : Level} (G : Group l) (n : ℕ) (x : type-Group G) → sum-fin-sequence-type-Group G n (λ _ → x) ＝ power-Group G n x - constant-sum-fin-sequence-type-Group G = - constant-sum-fin-sequence-type-Monoid (monoid-Group G) + sum-constant-fin-sequence-type-Group G = + sum-constant-fin-sequence-type-Monoid (monoid-Group G) ``` diff --git a/src/group-theory/sums-of-finite-sequences-of-elements-monoids.lagda.md b/src/group-theory/sums-of-finite-sequences-of-elements-monoids.lagda.md index 4b58cd16e5..dcf4a4ff64 100644 --- a/src/group-theory/sums-of-finite-sequences-of-elements-monoids.lagda.md +++ b/src/group-theory/sums-of-finite-sequences-of-elements-monoids.lagda.md @@ -213,14 +213,14 @@ split-sum-fin-sequence-type-Monoid M n (succ-ℕ m) f = ```agda abstract - constant-sum-fin-sequence-type-Monoid : + sum-constant-fin-sequence-type-Monoid : {l : Level} (M : Monoid l) (n : ℕ) (x : type-Monoid M) → sum-fin-sequence-type-Monoid M n (λ _ → x) ＝ power-Monoid M n x - constant-sum-fin-sequence-type-Monoid M 0 x = refl - constant-sum-fin-sequence-type-Monoid M 1 x = + sum-constant-fin-sequence-type-Monoid M 0 x = refl + sum-constant-fin-sequence-type-Monoid M 1 x = compute-sum-one-element-Monoid M (λ _ → x) - constant-sum-fin-sequence-type-Monoid M (succ-ℕ n@(succ-ℕ _)) x = + sum-constant-fin-sequence-type-Monoid M (succ-ℕ n@(succ-ℕ _)) x = ap-mul-Monoid M - ( constant-sum-fin-sequence-type-Monoid M n x) + ( sum-constant-fin-sequence-type-Monoid M n x) ( refl) ``` diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index ba50e0c42c..623205a1be 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -31,13 +31,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 @@ -46,4 +52,5 @@ open import linear-algebra.tuples-on-euclidean-domains public open import linear-algebra.tuples-on-monoids public open import linear-algebra.tuples-on-rings public open import linear-algebra.tuples-on-semirings public +open import linear-algebra.vector-spaces 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..88f59ca969 --- /dev/null +++ b/src/linear-algebra/normed-real-vector-spaces.lagda.md @@ -0,0 +1,426 @@ +# 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.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 + + metric-Normed-ℝ-Vector-Space : Metric l1 (set-Normed-ℝ-Vector-Space V) + metric-Normed-ℝ-Vector-Space = + ( nonnegative-dist-Normed-ℝ-Vector-Space V , + ( λ v → + similarity-reasoning-ℝ + zero-ℝ + ~ℝ raise-ℝ l1 zero-ℝ + by sim-raise-ℝ l1 zero-ℝ + ~ℝ dist-Normed-ℝ-Vector-Space V v v + by + sim-eq-ℝ + ( inv + ( is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space + ( seminormed-vector-space-Normed-ℝ-Vector-Space V) + ( v)))) , + ( λ 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-ℝ + ( similarity-reasoning-ℝ + dist-Normed-ℝ-Vector-Space V v w + ~ℝ zero-ℝ + by symmetric-sim-ℝ 0~dvw + ~ℝ raise-ℝ l1 zero-ℝ + by sim-raise-ℝ l1 zero-ℝ)))) + + 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-ℝ) , + λ x |x|=0 → + eq-sim-ℝ + ( similarity-reasoning-ℝ + x + ~ℝ zero-ℝ + by + sim-zero-sim-zero-abs-ℝ x + ( transitive-sim-ℝ _ _ _ + ( sim-raise-ℝ' l zero-ℝ) + ( sim-eq-ℝ |x|=0)) + ~ℝ raise-ℝ l zero-ℝ + by sim-raise-ℝ l zero-ℝ)) + +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) +``` 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..8686f1c2fb --- /dev/null +++ b/src/linear-algebra/real-banach-spaces.lagda.md @@ -0,0 +1,142 @@ +# 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 +``` + +
+ +## Idea + +A real +{{#concept "Banach space" WDID=Q194397 WD="Banach space" Disambiguation="over the real numbers" Agda=ℝ-Banach-Space}} +is a [normed](linear-algebra.normed-real-vector-spaces.md) +[real vector space](linear-algebra.real-vector-spaces.md) such that the +[metric space](metric-spaces.metric-spaces.md) induced by the norm is +[complete](metric-spaces.complete-metric-spaces.md). + +## Definition + +```agda +is-banach-prop-Normed-ℝ-Vector-Space : + {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) → Prop (l1 ⊔ l2) +is-banach-prop-Normed-ℝ-Vector-Space V = + is-complete-prop-Metric-Space (metric-space-Normed-ℝ-Vector-Space V) + +is-banach-Normed-ℝ-Vector-Space : + {l1 l2 : Level} (V : Normed-ℝ-Vector-Space l1 l2) → UU (l1 ⊔ l2) +is-banach-Normed-ℝ-Vector-Space V = + type-Prop (is-banach-prop-Normed-ℝ-Vector-Space V) + +ℝ-Banach-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +ℝ-Banach-Space l1 l2 = + type-subtype (is-banach-prop-Normed-ℝ-Vector-Space {l1} {l2}) + +module _ + {l1 l2 : Level} + (V : ℝ-Banach-Space l1 l2) + where + + normed-vector-space-ℝ-Banach-Space : Normed-ℝ-Vector-Space l1 l2 + normed-vector-space-ℝ-Banach-Space = pr1 V + + metric-space-ℝ-Banach-Space : Metric-Space l2 l1 + metric-space-ℝ-Banach-Space = + metric-space-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space + + is-complete-metric-space-ℝ-Banach-Space : + is-complete-Metric-Space metric-space-ℝ-Banach-Space + is-complete-metric-space-ℝ-Banach-Space = pr2 V + + complete-metric-space-ℝ-Banach-Space : Complete-Metric-Space l2 l1 + complete-metric-space-ℝ-Banach-Space = + ( metric-space-ℝ-Banach-Space , is-complete-metric-space-ℝ-Banach-Space) + + type-ℝ-Banach-Space : UU l2 + type-ℝ-Banach-Space = + type-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space + + map-norm-ℝ-Banach-Space : type-ℝ-Banach-Space → ℝ l1 + map-norm-ℝ-Banach-Space = + map-norm-Normed-ℝ-Vector-Space normed-vector-space-ℝ-Banach-Space + + cauchy-sequence-ℝ-Banach-Space : UU (l1 ⊔ l2) + cauchy-sequence-ℝ-Banach-Space = + cauchy-sequence-Metric-Space metric-space-ℝ-Banach-Space + + is-cauchy-sequence-ℝ-Banach-Space : + sequence type-ℝ-Banach-Space → UU l1 + is-cauchy-sequence-ℝ-Banach-Space = + is-cauchy-sequence-Metric-Space metric-space-ℝ-Banach-Space + + map-cauchy-sequence-ℝ-Banach-Space : + cauchy-sequence-ℝ-Banach-Space → sequence type-ℝ-Banach-Space + map-cauchy-sequence-ℝ-Banach-Space = pr1 + + has-limit-sequence-ℝ-Banach-Space : + sequence type-ℝ-Banach-Space → UU (l1 ⊔ l2) + has-limit-sequence-ℝ-Banach-Space = + has-limit-sequence-Metric-Space metric-space-ℝ-Banach-Space + + has-limit-cauchy-sequence-ℝ-Banach-Space : + (σ : cauchy-sequence-ℝ-Banach-Space) → + has-limit-sequence-ℝ-Banach-Space (map-cauchy-sequence-ℝ-Banach-Space σ) + has-limit-cauchy-sequence-ℝ-Banach-Space = + has-limit-cauchy-sequence-Complete-Metric-Space + ( complete-metric-space-ℝ-Banach-Space) + + 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 +real-banach-space-ℝ : (l : Level) → ℝ-Banach-Space l (lsuc l) +real-banach-space-ℝ l = + ( normed-real-vector-space-ℝ l , + inv-tr + ( is-complete-Metric-Space) + ( eq-metric-space-normed-real-vector-space-metric-space-ℝ l) + ( is-complete-metric-space-ℝ l)) +``` diff --git a/src/linear-algebra/real-vector-spaces.lagda.md b/src/linear-algebra/real-vector-spaces.lagda.md new file mode 100644 index 0000000000..79e1d71d95 --- /dev/null +++ b/src/linear-algebra/real-vector-spaces.lagda.md @@ -0,0 +1,248 @@ +# 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 + +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.local-ring-of-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-real-numbers +``` + +
+ +## Idea + +A +{{#concept "real vector space" WD="real vector space" WDID=Q46996054 Agda=ℝ-Vector-Space}} +is a [vector space](linear-algebra.vector-spaces.md) over the +[local commutative ring of real numbers](real-numbers.local-ring-of-real-numbers.md). + +## Definition + +```agda +ℝ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +ℝ-Vector-Space l1 l2 = Vector-Space l2 (local-commutative-ring-ℝ l1) +``` + +## Properties + +```agda +module _ + {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2) + where + + ab-ℝ-Vector-Space : Ab l2 + ab-ℝ-Vector-Space = ab-Vector-Space (local-commutative-ring-ℝ l1) V + + set-ℝ-Vector-Space : Set l2 + set-ℝ-Vector-Space = set-Ab ab-ℝ-Vector-Space + + type-ℝ-Vector-Space : UU l2 + type-ℝ-Vector-Space = type-Ab ab-ℝ-Vector-Space + + add-ℝ-Vector-Space : + type-ℝ-Vector-Space → type-ℝ-Vector-Space → type-ℝ-Vector-Space + add-ℝ-Vector-Space = add-Ab ab-ℝ-Vector-Space + + 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 (local-commutative-ring-ℝ 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 ＝ + add-ℝ-Vector-Space v (add-ℝ-Vector-Space w x) + associative-add-ℝ-Vector-Space = associative-add-Ab ab-ℝ-Vector-Space + + left-unit-law-add-ℝ-Vector-Space : + (v : type-ℝ-Vector-Space) → add-ℝ-Vector-Space zero-ℝ-Vector-Space v ＝ v + left-unit-law-add-ℝ-Vector-Space = left-unit-law-add-Ab ab-ℝ-Vector-Space + + right-unit-law-add-ℝ-Vector-Space : + (v : type-ℝ-Vector-Space) → add-ℝ-Vector-Space v zero-ℝ-Vector-Space ＝ v + right-unit-law-add-ℝ-Vector-Space = right-unit-law-add-Ab ab-ℝ-Vector-Space + + left-inverse-law-add-ℝ-Vector-Space : + (v : type-ℝ-Vector-Space) → + add-ℝ-Vector-Space (neg-ℝ-Vector-Space v) v ＝ zero-ℝ-Vector-Space + left-inverse-law-add-ℝ-Vector-Space = + left-inverse-law-add-Ab ab-ℝ-Vector-Space + + right-inverse-law-add-ℝ-Vector-Space : + (v : type-ℝ-Vector-Space) → + add-ℝ-Vector-Space v (neg-ℝ-Vector-Space v) ＝ zero-ℝ-Vector-Space + right-inverse-law-add-ℝ-Vector-Space = + right-inverse-law-add-Ab ab-ℝ-Vector-Space + + commutative-add-ℝ-Vector-Space : + (v w : type-ℝ-Vector-Space) → + add-ℝ-Vector-Space v w ＝ add-ℝ-Vector-Space w v + commutative-add-ℝ-Vector-Space = commutative-add-Ab ab-ℝ-Vector-Space + + 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 + left-unit-law-mul-ℝ-Vector-Space = + left-unit-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V + + left-distributive-mul-add-ℝ-Vector-Space : + (r : ℝ l1) (v w : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space r (add-ℝ-Vector-Space v w) ＝ + add-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) (mul-ℝ-Vector-Space r w) + left-distributive-mul-add-ℝ-Vector-Space = + left-distributive-mul-add-Vector-Space (local-commutative-ring-ℝ l1) V + + right-distributive-mul-add-ℝ-Vector-Space : + (r s : ℝ l1) (v : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space (r +ℝ s) v ＝ + add-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) (mul-ℝ-Vector-Space s v) + right-distributive-mul-add-ℝ-Vector-Space = + right-distributive-mul-add-Vector-Space (local-commutative-ring-ℝ l1) V + + associative-mul-ℝ-Vector-Space : + (r s : ℝ l1) (v : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space (r *ℝ s) v ＝ + mul-ℝ-Vector-Space r (mul-ℝ-Vector-Space s v) + associative-mul-ℝ-Vector-Space = + associative-mul-Vector-Space (local-commutative-ring-ℝ l1) V + + left-zero-law-mul-ℝ-Vector-Space : + (v : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space (raise-ℝ l1 zero-ℝ) v ＝ zero-ℝ-Vector-Space + left-zero-law-mul-ℝ-Vector-Space = + left-zero-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V + + right-zero-law-mul-ℝ-Vector-Space : + (r : ℝ l1) → + mul-ℝ-Vector-Space r zero-ℝ-Vector-Space ＝ zero-ℝ-Vector-Space + right-zero-law-mul-ℝ-Vector-Space = + right-zero-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V + + left-negative-law-mul-ℝ-Vector-Space : + (r : ℝ l1) (v : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space (neg-ℝ r) v ＝ + neg-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) + left-negative-law-mul-ℝ-Vector-Space = + left-negative-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V + + right-negative-law-mul-ℝ-Vector-Space : + (r : ℝ l1) (v : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space r (neg-ℝ-Vector-Space v) ＝ + neg-ℝ-Vector-Space (mul-ℝ-Vector-Space r v) + right-negative-law-mul-ℝ-Vector-Space = + right-negative-law-mul-Vector-Space (local-commutative-ring-ℝ l1) V + + mul-neg-one-ℝ-Vector-Space : + (v : type-ℝ-Vector-Space) → + mul-ℝ-Vector-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝ neg-ℝ-Vector-Space v + mul-neg-one-ℝ-Vector-Space = + mul-neg-one-Vector-Space (local-commutative-ring-ℝ 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 + +```agda +real-vector-space-ℝ : (l : Level) → ℝ-Vector-Space l (lsuc l) +real-vector-space-ℝ l = + vector-space-local-commutative-ring-Local-Commutative-Ring + ( local-commutative-ring-ℝ l) +``` 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..d6a562ec17 --- /dev/null +++ b/src/linear-algebra/seminormed-real-vector-spaces.lagda.md @@ -0,0 +1,608 @@ +# Seminormed real vector spaces + +```agda +{-# OPTIONS --lossy-unification #-} + +module linear-algebra.seminormed-real-vector-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.binary-relations +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import group-theory.abelian-groups + +open import linear-algebra.real-vector-spaces + +open import metric-spaces.pseudometric-spaces + +open import order-theory.large-posets + +open import real-numbers.absolute-value-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.multiplication-positive-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.saturation-inequality-nonnegative-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +A +{{#concept "seminorm" WDID=Q1416088 WD="seminorm" Disambiguation="on a real vector space" Agda=seminorm-ℝ-Vector-Space}} +on a [real vector space](linear-algebra.real-vector-spaces.md) `V` is a +[real](real-numbers.dedekind-real-numbers.md)-valued function `p` on the vector +space such that `p (x + y) ≤ p x + p y` for all `x` and `y` in `V`, and +`p (c * x) = |c| * p x` for all real numbers `c` and `x` in `V`. + +These conditions imply that `p 0 = 0` and that `p` is nonnegative. + +A real vector space equipped with such a seminorm is called a +{{#concept "seminormed space" WD="seminormed space" WDID=Q63793693 Agda=Seminormed-ℝ-Vector-Space}}. +A seminormed space has an induced +[pseudometric structure](metric-spaces.pseudometric-spaces.md) defined by the +neighborhood relation that `v` and `w` are in an `ε`-neighborhood of each other +if `p (v - w) ≤ ε`. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (V : ℝ-Vector-Space l1 l2) + (p : type-ℝ-Vector-Space V → ℝ l1) + where + + is-triangular-prop-seminorm-ℝ-Vector-Space : Prop (l1 ⊔ l2) + is-triangular-prop-seminorm-ℝ-Vector-Space = + Π-Prop + ( type-ℝ-Vector-Space V) + ( λ x → + Π-Prop + ( type-ℝ-Vector-Space V) + ( λ y → leq-prop-ℝ (p (add-ℝ-Vector-Space V x y)) (p x +ℝ p y))) + + is-triangular-seminorm-ℝ-Vector-Space : UU (l1 ⊔ l2) + is-triangular-seminorm-ℝ-Vector-Space = + type-Prop is-triangular-prop-seminorm-ℝ-Vector-Space + + is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2) + is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space = + Π-Prop + ( ℝ l1) + ( λ c → + Π-Prop + ( type-ℝ-Vector-Space V) + ( λ x → + Id-Prop + ( ℝ-Set l1) + ( p (mul-ℝ-Vector-Space V c x)) + ( abs-ℝ c *ℝ p x))) + + is-absolutely-homogeneous-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2) + is-absolutely-homogeneous-seminorm-ℝ-Vector-Space = + type-Prop is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space + + is-seminorm-prop-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2) + is-seminorm-prop-ℝ-Vector-Space = + is-triangular-prop-seminorm-ℝ-Vector-Space ∧ + is-absolutely-homogeneous-prop-seminorm-ℝ-Vector-Space + + is-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2) + is-seminorm-ℝ-Vector-Space = type-Prop is-seminorm-prop-ℝ-Vector-Space + +seminorm-ℝ-Vector-Space : + {l1 l2 : Level} → ℝ-Vector-Space l1 l2 → UU (lsuc l1 ⊔ l2) +seminorm-ℝ-Vector-Space V = + type-subtype (is-seminorm-prop-ℝ-Vector-Space V) + +Seminormed-ℝ-Vector-Space : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Seminormed-ℝ-Vector-Space l1 l2 = + Σ (ℝ-Vector-Space l1 l2) seminorm-ℝ-Vector-Space +``` + +## Properties + +### Vector space properties + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + vector-space-Seminormed-ℝ-Vector-Space : ℝ-Vector-Space l1 l2 + vector-space-Seminormed-ℝ-Vector-Space = pr1 V + + set-Seminormed-ℝ-Vector-Space : Set l2 + set-Seminormed-ℝ-Vector-Space = + set-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + type-Seminormed-ℝ-Vector-Space : UU l2 + type-Seminormed-ℝ-Vector-Space = + type-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + seminorm-Seminormed-ℝ-Vector-Space : + seminorm-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + seminorm-Seminormed-ℝ-Vector-Space = pr2 V + + map-seminorm-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space → ℝ l1 + map-seminorm-Seminormed-ℝ-Vector-Space = + pr1 seminorm-Seminormed-ℝ-Vector-Space + + zero-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space + zero-Seminormed-ℝ-Vector-Space = + zero-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + is-zero-prop-Seminormed-ℝ-Vector-Space : + subtype l2 type-Seminormed-ℝ-Vector-Space + is-zero-prop-Seminormed-ℝ-Vector-Space = + is-zero-prop-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + is-zero-Seminormed-ℝ-Vector-Space : type-Seminormed-ℝ-Vector-Space → UU l2 + is-zero-Seminormed-ℝ-Vector-Space = + is-zero-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + add-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space → + type-Seminormed-ℝ-Vector-Space + add-Seminormed-ℝ-Vector-Space = + add-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + mul-Seminormed-ℝ-Vector-Space : + ℝ l1 → type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space + mul-Seminormed-ℝ-Vector-Space = + mul-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + neg-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space + neg-Seminormed-ℝ-Vector-Space = + neg-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + diff-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space → + type-Seminormed-ℝ-Vector-Space + diff-Seminormed-ℝ-Vector-Space v w = + add-Seminormed-ℝ-Vector-Space v (neg-Seminormed-ℝ-Vector-Space w) + + right-inverse-law-add-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space) → + add-Seminormed-ℝ-Vector-Space v (neg-Seminormed-ℝ-Vector-Space v) ＝ + zero-Seminormed-ℝ-Vector-Space + right-inverse-law-add-Seminormed-ℝ-Vector-Space = + right-inverse-law-add-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + add-diff-Seminormed-ℝ-Vector-Space : + (v w x : type-Seminormed-ℝ-Vector-Space) → + add-Seminormed-ℝ-Vector-Space + ( diff-Seminormed-ℝ-Vector-Space v w) + ( diff-Seminormed-ℝ-Vector-Space w x) ＝ + diff-Seminormed-ℝ-Vector-Space v x + add-diff-Seminormed-ℝ-Vector-Space = + add-diff-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + neg-neg-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space) → + neg-Seminormed-ℝ-Vector-Space (neg-Seminormed-ℝ-Vector-Space v) ＝ v + neg-neg-Seminormed-ℝ-Vector-Space = + neg-neg-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + left-zero-law-mul-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space) → + mul-Seminormed-ℝ-Vector-Space (raise-ℝ l1 zero-ℝ) v ＝ + zero-Seminormed-ℝ-Vector-Space + left-zero-law-mul-Seminormed-ℝ-Vector-Space = + left-zero-law-mul-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + mul-neg-one-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space) → + mul-Seminormed-ℝ-Vector-Space (neg-ℝ (raise-ℝ l1 one-ℝ)) v ＝ + neg-Seminormed-ℝ-Vector-Space v + mul-neg-one-Seminormed-ℝ-Vector-Space = + mul-neg-one-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space + + distributive-neg-diff-Seminormed-ℝ-Vector-Space : + (v w : type-Seminormed-ℝ-Vector-Space) → + neg-Seminormed-ℝ-Vector-Space (diff-Seminormed-ℝ-Vector-Space v w) ＝ + diff-Seminormed-ℝ-Vector-Space w v + distributive-neg-diff-Seminormed-ℝ-Vector-Space = + neg-right-subtraction-Ab + ( ab-ℝ-Vector-Space vector-space-Seminormed-ℝ-Vector-Space) + + triangular-Seminormed-ℝ-Vector-Space : + (v w : type-Seminormed-ℝ-Vector-Space) → + leq-ℝ + ( map-seminorm-Seminormed-ℝ-Vector-Space + ( add-Seminormed-ℝ-Vector-Space v w)) + ( map-seminorm-Seminormed-ℝ-Vector-Space v +ℝ + map-seminorm-Seminormed-ℝ-Vector-Space w) + triangular-Seminormed-ℝ-Vector-Space = + pr1 (pr2 seminorm-Seminormed-ℝ-Vector-Space) + + is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space : + (c : ℝ l1) (v : type-Seminormed-ℝ-Vector-Space) → + map-seminorm-Seminormed-ℝ-Vector-Space + ( mul-Seminormed-ℝ-Vector-Space c v) ＝ + abs-ℝ c *ℝ map-seminorm-Seminormed-ℝ-Vector-Space v + is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space = + pr2 (pr2 seminorm-Seminormed-ℝ-Vector-Space) + + dist-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space → type-Seminormed-ℝ-Vector-Space → ℝ l1 + dist-Seminormed-ℝ-Vector-Space v w = + map-seminorm-Seminormed-ℝ-Vector-Space + ( diff-Seminormed-ℝ-Vector-Space v w) +``` + +### The seminorm of the zero vector in a seminormed real vector space is zero + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + abstract + is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space : + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) ＝ + raise-ℝ l1 zero-ℝ + is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space = + eq-sim-ℝ + ( similarity-reasoning-ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) + ~ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( mul-Seminormed-ℝ-Vector-Space + ( V) + ( raise-ℝ l1 zero-ℝ) + ( zero-Seminormed-ℝ-Vector-Space V)) + by + sim-eq-ℝ + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( inv (left-zero-law-mul-Seminormed-ℝ-Vector-Space V _))) + ~ℝ + abs-ℝ (raise-ℝ l1 zero-ℝ) *ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) + by + sim-eq-ℝ + ( is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space V _ _) + ~ℝ + abs-ℝ zero-ℝ *ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) + by + preserves-sim-right-mul-ℝ _ _ _ + ( preserves-sim-abs-ℝ (sim-raise-ℝ' l1 zero-ℝ)) + ~ℝ + zero-ℝ *ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) + by sim-eq-ℝ (ap-mul-ℝ abs-zero-ℝ refl) + ~ℝ zero-ℝ + by left-zero-law-mul-ℝ _ + ~ℝ raise-ℝ l1 zero-ℝ + by sim-raise-ℝ l1 zero-ℝ) + + is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space V) → + dist-Seminormed-ℝ-Vector-Space V v v ＝ raise-ℝ l1 zero-ℝ + is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space v = + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( right-inverse-law-add-Seminormed-ℝ-Vector-Space V v)) ∙ + ( is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space) +``` + +### The seminorm of the negation of a vector is equal to the seminorm of the vector + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + abstract + seminorm-neg-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space V) → + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( neg-Seminormed-ℝ-Vector-Space V v) ＝ + map-seminorm-Seminormed-ℝ-Vector-Space V v + seminorm-neg-Seminormed-ℝ-Vector-Space v = + eq-sim-ℝ + ( similarity-reasoning-ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( neg-Seminormed-ℝ-Vector-Space V v) + ~ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( mul-Seminormed-ℝ-Vector-Space + ( V) + ( neg-ℝ (raise-ℝ l1 one-ℝ)) + ( v)) + by + sim-eq-ℝ + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( inv (mul-neg-one-Seminormed-ℝ-Vector-Space V v))) + ~ℝ + abs-ℝ (neg-ℝ (raise-ℝ l1 one-ℝ)) *ℝ + map-seminorm-Seminormed-ℝ-Vector-Space V v + by + sim-eq-ℝ + ( is-absolutely-homogeneous-Seminormed-ℝ-Vector-Space V _ _) + ~ℝ + abs-ℝ (raise-ℝ l1 one-ℝ) *ℝ + map-seminorm-Seminormed-ℝ-Vector-Space V v + by sim-eq-ℝ (ap-mul-ℝ (abs-neg-ℝ _) refl) + ~ℝ abs-ℝ one-ℝ *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by + preserves-sim-right-mul-ℝ _ _ _ + ( preserves-sim-abs-ℝ (sim-raise-ℝ' l1 one-ℝ)) + ~ℝ one-ℝ *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by + sim-eq-ℝ (ap-mul-ℝ (abs-real-ℝ⁺ one-ℝ⁺) refl) + ~ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by sim-eq-ℝ (left-unit-law-mul-ℝ _)) + + commutative-dist-Seminormed-ℝ-Vector-Space : + (v w : type-Seminormed-ℝ-Vector-Space V) → + dist-Seminormed-ℝ-Vector-Space V v w ＝ + dist-Seminormed-ℝ-Vector-Space V w v + commutative-dist-Seminormed-ℝ-Vector-Space v w = + ( inv + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( distributive-neg-diff-Seminormed-ℝ-Vector-Space V w v))) ∙ + ( seminorm-neg-Seminormed-ℝ-Vector-Space _) +``` + +### The distance function on a seminormed vector space satisfies the triangle inequality + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + abstract + triangular-dist-Seminormed-ℝ-Vector-Space : + (v w x : type-Seminormed-ℝ-Vector-Space V) → + leq-ℝ + ( dist-Seminormed-ℝ-Vector-Space V v x) + ( dist-Seminormed-ℝ-Vector-Space V v w +ℝ + dist-Seminormed-ℝ-Vector-Space V w x) + triangular-dist-Seminormed-ℝ-Vector-Space v w x = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + chain-of-inequalities + dist-Seminormed-ℝ-Vector-Space V v x + ≤ map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( add-Seminormed-ℝ-Vector-Space + ( V) + ( diff-Seminormed-ℝ-Vector-Space V v w) + ( diff-Seminormed-ℝ-Vector-Space V w x)) + by + leq-eq-ℝ + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( inv (add-diff-Seminormed-ℝ-Vector-Space V v w x))) + ≤ dist-Seminormed-ℝ-Vector-Space V v w +ℝ + dist-Seminormed-ℝ-Vector-Space V w x + by triangular-Seminormed-ℝ-Vector-Space V _ _ +``` + +### The seminorm of a vector in a seminormed vector space is nonnegative + +```agda +module _ + {l1 l2 : Level} + (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + abstract + is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space : + (v : type-Seminormed-ℝ-Vector-Space V) → + is-nonnegative-ℝ (map-seminorm-Seminormed-ℝ-Vector-Space V v) + is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space v = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + reflects-leq-left-mul-ℝ⁺ + ( positive-real-ℕ⁺ (2 , λ ())) + ( zero-ℝ) + ( map-seminorm-Seminormed-ℝ-Vector-Space V v) + ( chain-of-inequalities + real-ℝ⁺ (positive-real-ℕ⁺ (2 , (λ ()))) *ℝ zero-ℝ + ≤ zero-ℝ + by leq-sim-ℝ (right-zero-law-mul-ℝ _) + ≤ raise-ℝ l1 zero-ℝ + by leq-sim-ℝ (sim-raise-ℝ l1 zero-ℝ) + ≤ dist-Seminormed-ℝ-Vector-Space V v v + by + leq-eq-ℝ + ( inv (is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space V v)) + ≤ map-seminorm-Seminormed-ℝ-Vector-Space V v +ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( neg-Seminormed-ℝ-Vector-Space V v) + by triangular-Seminormed-ℝ-Vector-Space V _ _ + ≤ map-seminorm-Seminormed-ℝ-Vector-Space V v +ℝ + map-seminorm-Seminormed-ℝ-Vector-Space V v + by + leq-eq-ℝ + ( ap-add-ℝ + ( refl) + ( seminorm-neg-Seminormed-ℝ-Vector-Space V v)) + ≤ real-ℕ 2 *ℝ map-seminorm-Seminormed-ℝ-Vector-Space V v + by leq-eq-ℝ (inv (left-mul-real-ℕ 2 _))) + + nonnegative-seminorm-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space V → ℝ⁰⁺ l1 + nonnegative-seminorm-Seminormed-ℝ-Vector-Space v = + ( map-seminorm-Seminormed-ℝ-Vector-Space V v , + is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space v) +``` + +### The pseudometric space induced by a seminorm + +```agda +module _ + {l1 l2 : Level} (V : Seminormed-ℝ-Vector-Space l1 l2) + where + + nonnegative-dist-Seminormed-ℝ-Vector-Space : + type-Seminormed-ℝ-Vector-Space V → type-Seminormed-ℝ-Vector-Space V → ℝ⁰⁺ l1 + nonnegative-dist-Seminormed-ℝ-Vector-Space v w = + ( dist-Seminormed-ℝ-Vector-Space V v w , + is-nonnegative-seminorm-Seminormed-ℝ-Vector-Space V _) + + neighborhood-prop-Seminormed-ℝ-Vector-Space : + ℚ⁺ → Relation-Prop l1 (type-Seminormed-ℝ-Vector-Space V) + neighborhood-prop-Seminormed-ℝ-Vector-Space ε v w = + leq-prop-ℝ + ( dist-Seminormed-ℝ-Vector-Space V v w) + ( real-ℚ⁺ ε) + + neighborhood-Seminormed-ℝ-Vector-Space : + ℚ⁺ → Relation l1 (type-Seminormed-ℝ-Vector-Space V) + neighborhood-Seminormed-ℝ-Vector-Space d = + type-Relation-Prop (neighborhood-prop-Seminormed-ℝ-Vector-Space d) + + abstract + refl-neighborhood-Seminormed-ℝ-Vector-Space : + (ε : ℚ⁺) (v : type-Seminormed-ℝ-Vector-Space V) → + neighborhood-Seminormed-ℝ-Vector-Space ε v v + refl-neighborhood-Seminormed-ℝ-Vector-Space ε v = + leq-le-ℝ + ( preserves-le-left-sim-ℝ + ( real-ℚ⁺ ε) + ( zero-ℝ) + ( dist-Seminormed-ℝ-Vector-Space V v v) + ( similarity-reasoning-ℝ + zero-ℝ + ~ℝ raise-ℝ l1 zero-ℝ + by sim-raise-ℝ l1 zero-ℝ + ~ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( zero-Seminormed-ℝ-Vector-Space V) + by + sim-eq-ℝ + ( inv (is-zero-seminorm-zero-Seminormed-ℝ-Vector-Space V)) + ~ℝ + map-seminorm-Seminormed-ℝ-Vector-Space + ( V) + ( diff-Seminormed-ℝ-Vector-Space V v v) + by + sim-eq-ℝ + ( ap + ( map-seminorm-Seminormed-ℝ-Vector-Space V) + ( inv + ( right-inverse-law-add-Seminormed-ℝ-Vector-Space V v)))) + ( preserves-is-positive-real-ℚ (is-positive-rational-ℚ⁺ ε))) + + symmetric-neighborhood-Seminormed-ℝ-Vector-Space : + (d : ℚ⁺) (v w : type-Seminormed-ℝ-Vector-Space V) → + neighborhood-Seminormed-ℝ-Vector-Space d v w → + neighborhood-Seminormed-ℝ-Vector-Space d w v + symmetric-neighborhood-Seminormed-ℝ-Vector-Space d v w = + tr + ( λ z → leq-ℝ z (real-ℚ⁺ d)) + ( commutative-dist-Seminormed-ℝ-Vector-Space V v w) + + triangular-neighborhood-Seminormed-ℝ-Vector-Space : + (v w x : type-Seminormed-ℝ-Vector-Space V) (d1 d2 : ℚ⁺) → + neighborhood-Seminormed-ℝ-Vector-Space d2 w x → + neighborhood-Seminormed-ℝ-Vector-Space d1 v w → + neighborhood-Seminormed-ℝ-Vector-Space (d1 +ℚ⁺ d2) v x + triangular-neighborhood-Seminormed-ℝ-Vector-Space + v w x d1 d2 Nd2wx Nd1vw = + let + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + chain-of-inequalities + dist-Seminormed-ℝ-Vector-Space V v x + ≤ dist-Seminormed-ℝ-Vector-Space V v w +ℝ + dist-Seminormed-ℝ-Vector-Space V w x + by triangular-dist-Seminormed-ℝ-Vector-Space V v w x + ≤ real-ℚ⁺ d1 +ℝ real-ℚ⁺ d2 + by preserves-leq-add-ℝ Nd1vw Nd2wx + ≤ real-ℚ⁺ (d1 +ℚ⁺ d2) + by leq-eq-ℝ (add-real-ℚ _ _) + + saturated-neighborhood-Seminormed-ℝ-Vector-Space : + (d : ℚ⁺) (v w : type-Seminormed-ℝ-Vector-Space V) → + ((δ : ℚ⁺) → neighborhood-Seminormed-ℝ-Vector-Space (d +ℚ⁺ δ) v w) → + neighborhood-Seminormed-ℝ-Vector-Space d v w + saturated-neighborhood-Seminormed-ℝ-Vector-Space d v w H = + saturated-leq-ℝ⁰⁺ + ( nonnegative-dist-Seminormed-ℝ-Vector-Space v w) + ( nonnegative-real-ℚ⁺ d) + ( λ δ → + inv-tr + ( leq-ℝ (dist-Seminormed-ℝ-Vector-Space V v w)) + ( add-real-ℚ _ _) + ( H δ)) + + pseudometric-structure-Seminormed-ℝ-Vector-Space : + Pseudometric-Structure l1 (type-Seminormed-ℝ-Vector-Space V) + pseudometric-structure-Seminormed-ℝ-Vector-Space = + ( neighborhood-prop-Seminormed-ℝ-Vector-Space , + refl-neighborhood-Seminormed-ℝ-Vector-Space , + symmetric-neighborhood-Seminormed-ℝ-Vector-Space , + triangular-neighborhood-Seminormed-ℝ-Vector-Space , + saturated-neighborhood-Seminormed-ℝ-Vector-Space) + + pseudometric-space-Seminormed-ℝ-Vector-Space : Pseudometric-Space l2 l1 + pseudometric-space-Seminormed-ℝ-Vector-Space = + ( type-Seminormed-ℝ-Vector-Space V , + pseudometric-structure-Seminormed-ℝ-Vector-Space) +``` + +### The real numbers are a seminormed vector space over themselves with seminorm `x ↦ |x|` + +```agda +seminormed-real-vector-space-ℝ : + (l : Level) → Seminormed-ℝ-Vector-Space l (lsuc l) +seminormed-real-vector-space-ℝ l = + ( real-vector-space-ℝ l , abs-ℝ , triangle-inequality-abs-ℝ , abs-mul-ℝ) +``` diff --git a/src/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/linear-algebra/vector-spaces.lagda.md b/src/linear-algebra/vector-spaces.lagda.md new file mode 100644 index 0000000000..55c407c4c5 --- /dev/null +++ b/src/linear-algebra/vector-spaces.lagda.md @@ -0,0 +1,190 @@ +# Vector spaces + +```agda +module linear-algebra.vector-spaces where +``` + +
Imports + +```agda +open import commutative-algebra.local-commutative-rings + +open import foundation.identity-types +open import foundation.sets +open import foundation.universe-levels + +open import group-theory.abelian-groups + +open import linear-algebra.left-modules-commutative-rings +``` + +
+ +## Idea + +A {{#concept "vector space" WD="vector space" WDID=Q125977}} is a +[left module](linear-algebra.left-modules-rings.md) over a +[local commutative ring](commutative-algebra.local-commutative-rings.md). + +## Definition + +```agda +Vector-Space : + {l1 : Level} (l2 : Level) → Local-Commutative-Ring l1 → UU (l1 ⊔ lsuc l2) +Vector-Space l2 R = + left-module-Commutative-Ring l2 (commutative-ring-Local-Commutative-Ring R) +``` + +## Properties + +```agda +module _ + {l1 l2 : Level} (R : Local-Commutative-Ring l1) (V : Vector-Space l2 R) + where + + ab-Vector-Space : Ab l2 + ab-Vector-Space = + ab-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + set-Vector-Space : Set l2 + set-Vector-Space = set-Ab ab-Vector-Space + + type-Vector-Space : UU l2 + type-Vector-Space = type-Ab ab-Vector-Space + + add-Vector-Space : type-Vector-Space → type-Vector-Space → type-Vector-Space + add-Vector-Space = add-Ab ab-Vector-Space + + zero-Vector-Space : type-Vector-Space + zero-Vector-Space = 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 : + type-Local-Commutative-Ring R → type-Vector-Space → type-Vector-Space + mul-Vector-Space = + mul-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + associative-add-Vector-Space : + (v w x : type-Vector-Space) → + add-Vector-Space (add-Vector-Space v w) x ＝ + add-Vector-Space v (add-Vector-Space w x) + associative-add-Vector-Space = associative-add-Ab ab-Vector-Space + + left-unit-law-add-Vector-Space : + (v : type-Vector-Space) → add-Vector-Space zero-Vector-Space v ＝ v + left-unit-law-add-Vector-Space = left-unit-law-add-Ab ab-Vector-Space + + right-unit-law-add-Vector-Space : + (v : type-Vector-Space) → add-Vector-Space v zero-Vector-Space ＝ v + right-unit-law-add-Vector-Space = right-unit-law-add-Ab ab-Vector-Space + + left-inverse-law-add-Vector-Space : + (v : type-Vector-Space) → + add-Vector-Space (neg-Vector-Space v) v ＝ zero-Vector-Space + left-inverse-law-add-Vector-Space = left-inverse-law-add-Ab ab-Vector-Space + + right-inverse-law-add-Vector-Space : + (v : type-Vector-Space) → + add-Vector-Space v (neg-Vector-Space v) ＝ zero-Vector-Space + right-inverse-law-add-Vector-Space = right-inverse-law-add-Ab ab-Vector-Space + + commutative-add-Vector-Space : + (v w : type-Vector-Space) → add-Vector-Space v w ＝ add-Vector-Space w v + commutative-add-Vector-Space = commutative-add-Ab ab-Vector-Space + + left-unit-law-mul-Vector-Space : + (v : type-Vector-Space) → + mul-Vector-Space (one-Local-Commutative-Ring R) v ＝ v + left-unit-law-mul-Vector-Space = + left-unit-law-mul-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + left-distributive-mul-add-Vector-Space : + (r : type-Local-Commutative-Ring R) (v w : type-Vector-Space) → + mul-Vector-Space r (add-Vector-Space v w) ＝ + add-Vector-Space (mul-Vector-Space r v) (mul-Vector-Space r w) + left-distributive-mul-add-Vector-Space = + left-distributive-mul-add-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + right-distributive-mul-add-Vector-Space : + (r s : type-Local-Commutative-Ring R) (v : type-Vector-Space) → + mul-Vector-Space (add-Local-Commutative-Ring R r s) v ＝ + add-Vector-Space (mul-Vector-Space r v) (mul-Vector-Space s v) + right-distributive-mul-add-Vector-Space = + right-distributive-mul-add-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + associative-mul-Vector-Space : + (r s : type-Local-Commutative-Ring R) (v : type-Vector-Space) → + mul-Vector-Space (mul-Local-Commutative-Ring R r s) v ＝ + mul-Vector-Space r (mul-Vector-Space s v) + associative-mul-Vector-Space = + associative-mul-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + left-zero-law-mul-Vector-Space : + (v : type-Vector-Space) → + mul-Vector-Space (zero-Local-Commutative-Ring R) v ＝ zero-Vector-Space + left-zero-law-mul-Vector-Space = + left-zero-law-mul-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + right-zero-law-mul-Vector-Space : + (r : type-Local-Commutative-Ring R) → + mul-Vector-Space r zero-Vector-Space ＝ zero-Vector-Space + right-zero-law-mul-Vector-Space = + right-zero-law-mul-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + left-negative-law-mul-Vector-Space : + (r : type-Local-Commutative-Ring R) (v : type-Vector-Space) → + mul-Vector-Space (neg-Local-Commutative-Ring R r) v ＝ + neg-Vector-Space (mul-Vector-Space r v) + left-negative-law-mul-Vector-Space = + left-negative-law-mul-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + right-negative-law-mul-Vector-Space : + (r : type-Local-Commutative-Ring R) (v : type-Vector-Space) → + mul-Vector-Space r (neg-Vector-Space v) ＝ + neg-Vector-Space (mul-Vector-Space r v) + right-negative-law-mul-Vector-Space = + right-negative-law-mul-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) + + mul-neg-one-Vector-Space : + (v : type-Vector-Space) → + mul-Vector-Space + ( neg-Local-Commutative-Ring R (one-Local-Commutative-Ring R)) + ( v) ＝ + neg-Vector-Space v + mul-neg-one-Vector-Space = + mul-neg-one-left-module-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) + ( V) +``` + +### Any local commutative ring is a vector space over itself + +```agda +vector-space-local-commutative-ring-Local-Commutative-Ring : + {l : Level} (R : Local-Commutative-Ring l) → Vector-Space l R +vector-space-local-commutative-ring-Local-Commutative-Ring R = + left-module-commutative-ring-Commutative-Ring + ( commutative-ring-Local-Commutative-Ring R) +``` diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md index 862d0a1cea..81353f5e14 100644 --- a/src/literature/100-theorems.lagda.md +++ b/src/literature/100-theorems.lagda.md @@ -46,6 +46,15 @@ open import foundation.cantor-schroder-bernstein-decidable-embeddings using ( Cantor-Schröder-Bernstein-WLPO) ``` +### 34. Divergence of the Harmonic Series {#34} + +**Author:** [Louis Wasserman](https://github.com/lowasser) + +```agda +open import elementary-number-theory.harmonic-series-rational-numbers using + ( grows-without-bound-harmonic-series-ℚ) +``` + ### 42. Sum of the Reciprocals of the Triangular Numbers {#42} **Author:** [Louis Wasserman](https://github.com/lowasser) 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 139b1a33aa..e1d9a1f129 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -9,7 +9,10 @@ open import real-numbers.absolute-value-closed-intervals-real-numbers public open import real-numbers.absolute-value-real-numbers public open import real-numbers.accumulation-points-subsets-real-numbers public open import real-numbers.addition-lower-dedekind-real-numbers public +open import real-numbers.addition-negative-real-numbers public open import real-numbers.addition-nonnegative-real-numbers public +open import real-numbers.addition-nonzero-real-numbers public +open import real-numbers.addition-positive-real-numbers public open import real-numbers.addition-real-numbers public open import real-numbers.addition-upper-dedekind-real-numbers public open import real-numbers.apartness-real-numbers public @@ -45,13 +48,14 @@ open import real-numbers.large-multiplicative-monoid-of-real-numbers public open import real-numbers.large-ring-of-real-numbers public open import real-numbers.limits-sequences-real-numbers public open import real-numbers.lipschitz-continuity-multiplication-real-numbers public +open import real-numbers.local-ring-of-real-numbers public open import real-numbers.located-metric-space-of-real-numbers public open import real-numbers.lower-dedekind-real-numbers public 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 @@ -60,6 +64,7 @@ open import real-numbers.minimum-lower-dedekind-real-numbers public open import real-numbers.minimum-upper-dedekind-real-numbers public open import real-numbers.multiplication-negative-real-numbers public open import real-numbers.multiplication-nonnegative-real-numbers public +open import real-numbers.multiplication-nonzero-real-numbers public open import real-numbers.multiplication-positive-and-negative-real-numbers public open import real-numbers.multiplication-positive-real-numbers public open import real-numbers.multiplication-real-numbers public @@ -97,6 +102,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..371e592c16 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,22 @@ 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)))) + module _ (x : ℝ lzero) (|x|=0 : abs-ℝ x ＝ zero-ℝ) where @@ -190,14 +225,7 @@ module _ abstract is-zero-is-zero-abs-ℝ : x ＝ zero-ℝ is-zero-is-zero-abs-ℝ = - antisymmetric-leq-ℝ - ( x) - ( zero-ℝ) - ( tr (leq-ℝ x) |x|=0 (leq-abs-ℝ x)) - ( tr - ( λ y → leq-ℝ y x) - ( (ap neg-ℝ |x|=0) ∙ neg-zero-ℝ) - ( leq-neg-abs-ℝ x)) + eq-sim-ℝ (sim-zero-sim-zero-abs-ℝ x (sim-eq-ℝ |x|=0)) ``` ### If `|x| ≤ 0` then `|x| ＝ 0` and `x ＝ 0` diff --git a/src/real-numbers/addition-negative-real-numbers.lagda.md b/src/real-numbers/addition-negative-real-numbers.lagda.md new file mode 100644 index 0000000000..c3e3cef113 --- /dev/null +++ b/src/real-numbers/addition-negative-real-numbers.lagda.md @@ -0,0 +1,85 @@ +# Addition of negative real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.addition-negative-real-numbers where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.functoriality-disjunction +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.negative-real-numbers +open import real-numbers.positive-and-negative-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +The [negative](real-numbers.negative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) are closed under +[addition](real-numbers.addition-real-numbers.md). + +## Definition + +```agda +abstract + is-negative-add-ℝ : + {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → is-negative-ℝ x → is-negative-ℝ y → + is-negative-ℝ (x +ℝ y) + is-negative-add-ℝ {x = x} {y = y} x<0 y<0 = + transitive-le-ℝ + ( x +ℝ y) + ( x) + ( zero-ℝ) + ( x<0) + ( tr + ( le-ℝ (x +ℝ y)) + ( right-unit-law-add-ℝ x) + ( preserves-le-left-add-ℝ x y zero-ℝ y<0)) + +add-ℝ⁻ : {l1 l2 : Level} → ℝ⁻ l1 → ℝ⁻ l2 → ℝ⁻ (l1 ⊔ l2) +add-ℝ⁻ (x , x<0) (y , y<0) = (add-ℝ x y , is-negative-add-ℝ x<0 y<0) + +infixl 35 _+ℝ⁻_ + +_+ℝ⁻_ : {l1 l2 : Level} → ℝ⁻ l1 → ℝ⁻ l2 → ℝ⁻ (l1 ⊔ l2) +_+ℝ⁻_ = add-ℝ⁻ +``` + +## Properties + +### If `x + y` is negative, `x` or `y` is negative + +```agda +abstract + is-negative-either-is-negative-add-ℝ : + {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → is-negative-ℝ (x +ℝ y) → + disjunction-type (is-negative-ℝ x) (is-negative-ℝ y) + is-negative-either-is-negative-add-ℝ x y x+y<0 = + map-disjunction + ( is-negative-is-positive-neg-ℝ x) + ( is-negative-is-positive-neg-ℝ y) + ( is-positive-either-is-positive-add-ℝ + ( neg-ℝ x) + ( neg-ℝ y) + ( tr + ( is-positive-ℝ) + ( distributive-neg-add-ℝ x y) + ( neg-is-negative-ℝ (x +ℝ y) x+y<0))) +``` diff --git a/src/real-numbers/addition-nonnegative-real-numbers.lagda.md b/src/real-numbers/addition-nonnegative-real-numbers.lagda.md index 6c29699df8..22600ad7dc 100644 --- a/src/real-numbers/addition-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/addition-nonnegative-real-numbers.lagda.md @@ -12,9 +12,12 @@ module real-numbers.addition-nonnegative-real-numbers where open import elementary-number-theory.addition-nonnegative-rational-numbers open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.positive-and-negative-rational-numbers open import elementary-number-theory.positive-rational-numbers +open import foundation.coproduct-types open import foundation.dependent-pair-types +open import foundation.disjunction open import foundation.identity-types open import foundation.transport-along-identifications open import foundation.universe-levels @@ -133,3 +136,21 @@ module _ le-ℝ⁰⁺ x y → le-ℝ⁰⁺ z w → le-ℝ⁰⁺ (x +ℝ⁰⁺ z) (y +ℝ⁰⁺ w) preserves-le-add-ℝ⁰⁺ = preserves-le-add-ℝ ``` + +### Addition with a nonnegative real number is an inflationary map + +```agda +abstract + leq-left-add-real-ℝ⁰⁺ : + {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁰⁺ l2) → leq-ℝ x (x +ℝ real-ℝ⁰⁺ d) + leq-left-add-real-ℝ⁰⁺ x d⁺@(d , pos-d) = + tr + ( λ y → leq-ℝ y (x +ℝ d)) + ( right-unit-law-add-ℝ x) + ( preserves-leq-left-add-ℝ x zero-ℝ d pos-d) + +leq-right-add-real-ℝ⁰⁺ : + {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁰⁺ l2) → leq-ℝ x (real-ℝ⁰⁺ d +ℝ x) +leq-right-add-real-ℝ⁰⁺ x d = + tr (leq-ℝ x) (commutative-add-ℝ x (real-ℝ⁰⁺ d)) (leq-left-add-real-ℝ⁰⁺ x d) +``` diff --git a/src/real-numbers/addition-nonzero-real-numbers.lagda.md b/src/real-numbers/addition-nonzero-real-numbers.lagda.md new file mode 100644 index 0000000000..e59f5b96f1 --- /dev/null +++ b/src/real-numbers/addition-nonzero-real-numbers.lagda.md @@ -0,0 +1,56 @@ +# Addition of nonzero real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.addition-nonzero-real-numbers where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.functoriality-disjunction +open import foundation.universe-levels + +open import real-numbers.addition-negative-real-numbers +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.nonzero-real-numbers +``` + +
+ +## Idea + +On this page we describe properties of +[addition](real-numbers.addition-real-numbers.md) of +[nonzero](real-numbers.nonzero-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md). + +## Properties + +### If `x + y` is nonzero, `x` is nonzero or `y` is nonzero + +```agda +abstract + is-nonzero-either-is-nonzero-add-ℝ : + {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → + is-nonzero-ℝ (x +ℝ y) → + disjunction-type (is-nonzero-ℝ x) (is-nonzero-ℝ y) + is-nonzero-either-is-nonzero-add-ℝ x y = + elim-disjunction + ( is-nonzero-prop-ℝ x ∨ is-nonzero-prop-ℝ y) + ( λ x+y<0 → + map-disjunction + ( inl-disjunction) + ( inl-disjunction) + ( is-negative-either-is-negative-add-ℝ x y x+y<0)) + ( λ 0Imports + +```agda +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.nonnegative-rational-numbers +open import elementary-number-theory.positive-and-negative-rational-numbers + +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +The [positive](real-numbers.positive-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) are closed under +[addition](real-numbers.addition-real-numbers.md). + +## Definition + +```agda +abstract + is-positive-add-ℝ : + {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → is-positive-ℝ x → is-positive-ℝ y → + is-positive-ℝ (x +ℝ y) + is-positive-add-ℝ {x = x} {y = y} 0Imports ```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/binary-maximum-real-numbers.lagda.md b/src/real-numbers/binary-maximum-real-numbers.lagda.md index b225ca7890..8ea3ab74b6 100644 --- a/src/real-numbers/binary-maximum-real-numbers.lagda.md +++ b/src/real-numbers/binary-maximum-real-numbers.lagda.md @@ -28,6 +28,7 @@ open import order-theory.join-semilattices open import order-theory.large-join-semilattices open import order-theory.least-upper-bounds-large-posets +open import real-numbers.addition-positive-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers open import real-numbers.inequality-real-numbers diff --git a/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md b/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md index 6e102ad464..ce1647b2d5 100644 --- a/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md +++ b/src/real-numbers/cauchy-completeness-dedekind-real-numbers.lagda.md @@ -38,6 +38,7 @@ open import metric-spaces.convergent-cauchy-approximations-metric-spaces open import metric-spaces.limits-of-cauchy-approximations-metric-spaces open import metric-spaces.metric-spaces +open import real-numbers.addition-positive-real-numbers open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers 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/distance-real-numbers.lagda.md b/src/real-numbers/distance-real-numbers.lagda.md index 8b9f67f22b..7527cdf664 100644 --- a/src/real-numbers/distance-real-numbers.lagda.md +++ b/src/real-numbers/distance-real-numbers.lagda.md @@ -248,6 +248,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/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 commutative-algebra.local-commutative-rings + +open import foundation.dependent-pair-types +open import foundation.functoriality-disjunction +open import foundation.universe-levels + +open import real-numbers.addition-nonzero-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.large-ring-of-real-numbers +open import real-numbers.multiplicative-inverses-nonzero-real-numbers +open import real-numbers.nonzero-real-numbers +``` + +
+ +## Idea + +The [ring of real numbers](real-numbers.large-ring-of-real-numbers.md) is a +[local](commutative-algebra.local-commutative-rings.md) +[commutative ring](commutative-algebra.commutative-rings.md). Notably, this is +one of the strongest alternatives for the concept of field that applies to the +[Dedekind real numbers](real-numbers.dedekind-real-numbers.md) constructively. + +## Definition + +```agda +is-local-commutative-ring-ℝ : + (l : Level) → is-local-Commutative-Ring (commutative-ring-ℝ l) +is-local-commutative-ring-ℝ l x y is-invertible-x+y = + map-disjunction + ( is-invertible-is-nonzero-ℝ x) + ( is-invertible-is-nonzero-ℝ y) + ( is-nonzero-either-is-nonzero-add-ℝ + ( x) + ( y) + ( is-nonzero-is-invertible-ℝ (x +ℝ y) is-invertible-x+y)) + +local-commutative-ring-ℝ : (l : Level) → Local-Commutative-Ring (lsuc l) +local-commutative-ring-ℝ l = + ( commutative-ring-ℝ l , is-local-commutative-ring-ℝ l) +``` diff --git a/src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md b/src/real-numbers/metric-additive-group-of-real-numbers.lagda.md similarity index 71% rename from src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md rename to src/real-numbers/metric-additive-group-of-real-numbers.lagda.md index 3402489495..db74d26fd0 100644 --- a/src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md +++ b/src/real-numbers/metric-additive-group-of-real-numbers.lagda.md @@ -3,12 +3,13 @@ ```agda {-# OPTIONS --lossy-unification #-} -module real-numbers.metric-abelian-group-of-real-numbers where +module real-numbers.metric-additive-group-of-real-numbers where ```
Imports ```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-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplication-nonzero-real-numbers.lagda.md new file mode 100644 index 0000000000..5f6c869630 --- /dev/null +++ b/src/real-numbers/multiplication-nonzero-real-numbers.lagda.md @@ -0,0 +1,68 @@ +# Multiplication of nonzero real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.multiplication-nonzero-real-numbers where +``` + +
Imports + +```agda +open import foundation.dependent-pair-types +open import foundation.disjunction +open import foundation.function-types +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +open import real-numbers.multiplication-negative-real-numbers +open import real-numbers.multiplication-positive-and-negative-real-numbers +open import real-numbers.multiplication-positive-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.multiplicative-inverses-nonzero-real-numbers +open import real-numbers.nonzero-real-numbers +``` + +
+ +## Idea + +The +{{#concept "product" Disambiguation="of pairs of nonzero real numbers" Agda=mul-nonzero-ℝ}} +of two [nonzero](real-numbers.nonzero-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) is their +[product](real-numbers.multiplication-real-numbers.md) as real numbers, and is +itself nonzero. + +## Definition + +```agda +abstract + is-nonzero-mul-ℝ : + {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → is-nonzero-ℝ x → is-nonzero-ℝ y → + is-nonzero-ℝ (x *ℝ y) + is-nonzero-mul-ℝ {x = x} {y = y} x#0 y#0 = + let + motive = is-nonzero-prop-ℝ (x *ℝ y) + in + elim-disjunction + ( motive) + ( λ x<0 → + elim-disjunction + ( motive) + ( inr-disjunction ∘ is-positive-mul-is-negative-ℝ x<0) + ( inl-disjunction ∘ is-negative-mul-negative-positive-ℝ x<0) + ( y#0)) + ( λ 0Imports ```agda +open import foundation.action-on-identifications-functions open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.disjunction @@ -25,10 +26,13 @@ open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers open import real-numbers.negation-real-numbers 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.rational-real-numbers open import real-numbers.similarity-real-numbers +open import real-numbers.square-roots-nonnegative-real-numbers +open import real-numbers.squares-real-numbers open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers open import real-numbers.strict-inequality-real-numbers ``` @@ -162,3 +166,40 @@ module _ ( neg-le-ℝ |x|-ε<-x)))) ( approximate-below-abs-ℝ x ε) ``` + +### `x` is nonzero if and only if `x²` is positive + +```agda +module _ + {l : Level} (x : ℝ l) + where + + abstract + is-positive-square-is-nonzero-ℝ : + is-nonzero-ℝ x → is-positive-ℝ (square-ℝ x) + is-positive-square-is-nonzero-ℝ = + elim-disjunction + ( is-positive-prop-ℝ (square-ℝ x)) + ( λ is-neg-x → is-positive-square-ℝ⁻ (x , is-neg-x)) + ( λ is-pos-x → is-positive-square-ℝ⁺ (x , is-pos-x)) + + is-nonzero-square-is-positive-ℝ : + is-positive-ℝ (square-ℝ x) → is-nonzero-ℝ x + is-nonzero-square-is-positive-ℝ 0Imports ```agda +open import foundation.cartesian-product-types open import foundation.dependent-pair-types +open import foundation.logical-equivalences +open import foundation.negation open import foundation.transport-along-identifications open import foundation.universe-levels @@ -78,6 +81,38 @@ neg-ℝ⁻ : {l : Level} → ℝ⁻ l → ℝ⁺ l neg-ℝ⁻ (x , is-neg-x) = (neg-ℝ x , neg-is-negative-ℝ x is-neg-x) ``` +### A real number is negative if and only if its negation is positive + +```agda +abstract + is-negative-is-positive-neg-ℝ : + {l : Level} (x : ℝ l) → is-positive-ℝ (neg-ℝ x) → is-negative-ℝ x + is-negative-is-positive-neg-ℝ x 0<-x = + tr is-negative-ℝ (neg-neg-ℝ x) (neg-is-positive-ℝ (neg-ℝ x) 0<-x) + +is-negative-iff-neg-is-positive-ℝ : + {l : Level} (x : ℝ l) → is-negative-ℝ x ↔ is-positive-ℝ (neg-ℝ x) +is-negative-iff-neg-is-positive-ℝ x = + ( neg-is-negative-ℝ x , + is-negative-is-positive-neg-ℝ x) +``` + +### A real number is positive if and only if its negation is negative + +```agda +abstract + is-positive-is-negative-neg-ℝ : + {l : Level} (x : ℝ l) → is-negative-ℝ (neg-ℝ x) → is-positive-ℝ x + is-positive-is-negative-neg-ℝ x -x<0 = + tr is-positive-ℝ (neg-neg-ℝ x) (neg-is-negative-ℝ (neg-ℝ x) -x<0) + +is-positive-iff-neg-is-negative-ℝ : + {l : Level} (x : ℝ l) → is-positive-ℝ x ↔ is-negative-ℝ (neg-ℝ x) +is-positive-iff-neg-is-negative-ℝ x = + ( neg-is-positive-ℝ x , + is-positive-is-negative-neg-ℝ x) +``` + ### If a nonnegative real number `x` is less than a real number `y`, `y` is positive ```agda @@ -87,3 +122,13 @@ abstract is-positive-ℝ y is-positive-le-ℝ⁰⁺ (x , 0≤x) y = concatenate-leq-le-ℝ zero-ℝ x y 0≤x ``` + +### Real numbers are not both negative and nonnegative + +```agda +abstract + is-not-negative-and-nonnegative-ℝ : + {l : Level} {x : ℝ l} → ¬ (is-negative-ℝ x × is-nonnegative-ℝ x) + is-not-negative-and-nonnegative-ℝ {x = x} (x<0 , 0≤x) = + not-leq-le-ℝ x zero-ℝ x<0 0≤x +``` diff --git a/src/real-numbers/positive-real-numbers.lagda.md b/src/real-numbers/positive-real-numbers.lagda.md index ab55377d25..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 @@ -202,44 +206,6 @@ exists-ℚ⁺-in-lower-cut-ℝ⁺ : exists-ℚ⁺-in-lower-cut-ℝ⁺ = ind-Σ exists-ℚ⁺-in-lower-cut-is-positive-ℝ ``` -### Addition with a positive real number is a strictly inflationary map - -```agda -abstract opaque - unfolding add-ℝ le-ℝ - - le-left-add-real-ℝ⁺ : - {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → le-ℝ x (x +ℝ real-ℝ⁺ d) - le-left-add-real-ℝ⁺ x d⁺@(d , pos-d) = - tr - ( λ y → le-ℝ y (x +ℝ d)) - ( right-unit-law-add-ℝ x) - ( preserves-le-left-add-ℝ x zero-ℝ d pos-d) - -le-right-add-real-ℝ⁺ : - {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → le-ℝ x (real-ℝ⁺ d +ℝ x) -le-right-add-real-ℝ⁺ x d = - tr (le-ℝ x) (commutative-add-ℝ x (real-ℝ⁺ d)) (le-left-add-real-ℝ⁺ x d) -``` - -### Subtraction by a positive real number is a strictly deflationary map - -```agda -abstract - le-diff-real-ℝ⁺ : - {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → le-ℝ (x -ℝ real-ℝ⁺ d) x - le-diff-real-ℝ⁺ x d⁺@(d , _) = - preserves-le-right-sim-ℝ - ( x -ℝ d) - ( (x -ℝ d) +ℝ d) - ( x) - ( tr - ( λ y → sim-ℝ y x) - ( right-swap-add-ℝ x d (neg-ℝ d)) - ( cancel-right-add-diff-ℝ x d)) - ( le-left-add-real-ℝ⁺ (x -ℝ d) d⁺) -``` - ### `x < y` if and only if `y - x` is positive ```agda @@ -291,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/raising-universe-levels-real-numbers.lagda.md b/src/real-numbers/raising-universe-levels-real-numbers.lagda.md index c3f1b1d417..8a8d783ae8 100644 --- a/src/real-numbers/raising-universe-levels-real-numbers.lagda.md +++ b/src/real-numbers/raising-universe-levels-real-numbers.lagda.md @@ -170,9 +170,13 @@ module _ opaque unfolding sim-ℝ - sim-raise-ℝ : {l0 : Level} → (l : Level) → (x : ℝ l0) → sim-ℝ x (raise-ℝ l x) + sim-raise-ℝ : {l0 : Level} (l : Level) (x : ℝ l0) → sim-ℝ x (raise-ℝ l x) pr1 (sim-raise-ℝ l x) _ = map-raise pr2 (sim-raise-ℝ l x) _ = map-inv-raise + +abstract + sim-raise-ℝ' : {l0 : Level} (l : Level) (x : ℝ l0) → sim-ℝ (raise-ℝ l x) x + sim-raise-ℝ' l x = symmetric-sim-ℝ (sim-raise-ℝ l x) ``` ### Raising a real to its own level is the identity diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index 285729c4a4..4e48764ed5 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -10,6 +10,7 @@ module real-numbers.rational-real-numbers where ```agda open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers @@ -83,6 +84,13 @@ real-ℤ : ℤ → ℝ lzero real-ℤ x = real-ℚ (rational-ℤ x) ``` +### The canonical map from `ℕ` to `ℝ lzero` + +```agda +real-ℕ : ℕ → ℝ lzero +real-ℕ n = real-ℤ (int-ℕ n) +``` + ### Zero as a real number ```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 index f3d0ecf21e..e85b062a00 100644 --- a/src/real-numbers/series-real-numbers.lagda.md +++ b/src/real-numbers/series-real-numbers.lagda.md @@ -16,7 +16,7 @@ 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 +open import real-numbers.metric-additive-group-of-real-numbers ```
@@ -26,13 +26,13 @@ open import real-numbers.metric-abelian-group-of-real-numbers 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). +[metric abelian group of real numbers](real-numbers.metric-additive-group-of-real-numbers.md). ## Definition ```agda series-ℝ : (l : Level) → UU (lsuc l) -series-ℝ l = series-Metric-Ab (metric-ab-ℝ l) +series-ℝ l = series-Metric-Ab (metric-ab-add-ℝ l) series-terms-ℝ : {l : Level} → sequence (ℝ l) → series-ℝ l series-terms-ℝ = series-terms-Metric-Ab diff --git a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md index d73dc98a0f..d7c62f6516 100644 --- a/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md +++ b/src/real-numbers/square-roots-nonnegative-real-numbers.lagda.md @@ -53,10 +53,14 @@ 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.positive-and-negative-real-numbers +open import real-numbers.positive-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.similarity-nonnegative-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.squares-real-numbers +open import real-numbers.strict-inequality-nonnegative-real-numbers +open import real-numbers.strict-inequality-real-numbers ```
@@ -646,3 +650,21 @@ abstract ( is-section-square-ℝ⁰⁺ x) ( is-section-square-ℝ⁰⁺ y))))))) ``` + +### The square root of a positive real number is positive + +```agda +abstract opaque + unfolding real-sqrt-ℝ⁰⁺ + + is-positive-sqrt-ℝ⁺ : + {l : Level} (x : ℝ⁺ l) → is-positive-ℝ (real-sqrt-ℝ⁰⁺ (nonnegative-ℝ⁺ x)) + is-positive-sqrt-ℝ⁺ x⁺@(x , _) = + is-positive-zero-in-lower-cut-ℝ + ( real-sqrt-ℝ⁰⁺ (nonnegative-ℝ⁺ x⁺)) + ( λ _ → + inv-tr + ( is-in-lower-cut-ℝ x) + ( left-zero-law-mul-ℚ zero-ℚ) + ( zero-in-lower-cut-ℝ⁺ x⁺)) +``` diff --git a/src/real-numbers/squares-real-numbers.lagda.md b/src/real-numbers/squares-real-numbers.lagda.md index 86d106d8c6..d64d870327 100644 --- a/src/real-numbers/squares-real-numbers.lagda.md +++ b/src/real-numbers/squares-real-numbers.lagda.md @@ -20,6 +20,7 @@ open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers +open import elementary-number-theory.square-roots-positive-rational-numbers open import elementary-number-theory.squares-rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers @@ -31,8 +32,11 @@ open import foundation.propositional-truncations open import foundation.transport-along-identifications open import foundation.universe-levels +open import real-numbers.addition-real-numbers open import real-numbers.dedekind-real-numbers +open import real-numbers.difference-real-numbers open import real-numbers.enclosing-closed-rational-intervals-real-numbers +open import real-numbers.inequality-nonnegative-real-numbers open import real-numbers.multiplication-nonnegative-real-numbers open import real-numbers.multiplication-positive-real-numbers open import real-numbers.multiplication-real-numbers @@ -218,6 +222,25 @@ abstract ( preserves-le-right-mul-ℝ⁺ (y , is-positive-le-ℝ⁰⁺ x⁰⁺ y xImports + +```agda +open import elementary-number-theory.natural-numbers + +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.large-additive-group-of-real-numbers +``` + + + +## 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) +``` diff --git a/src/ring-theory/arithmetic-series-semirings.lagda.md b/src/ring-theory/arithmetic-series-semirings.lagda.md index af626c0a4d..653e708c38 100644 --- a/src/ring-theory/arithmetic-series-semirings.lagda.md +++ b/src/ring-theory/arithmetic-series-semirings.lagda.md @@ -180,7 +180,7 @@ module _ compute-sum-add-mul-nat-Semiring n = ap-binary ( add-Semiring R) - ( inv (constant-sum-fin-sequence-type-Semiring R (succ-ℕ n) a)) + ( inv (sum-constant-fin-sequence-type-Semiring R (succ-ℕ n) a)) ( ( ap ( λ i → multiple-Semiring R i d) ( htpy-sum-leq-triangular-ℕ n)) ∙ diff --git a/src/ring-theory/sums-of-finite-sequences-of-elements-rings.lagda.md b/src/ring-theory/sums-of-finite-sequences-of-elements-rings.lagda.md index c65dd2c1a7..17eec95acf 100644 --- a/src/ring-theory/sums-of-finite-sequences-of-elements-rings.lagda.md +++ b/src/ring-theory/sums-of-finite-sequences-of-elements-rings.lagda.md @@ -26,6 +26,7 @@ open import linear-algebra.linear-maps-left-modules-rings open import lists.finite-sequences +open import ring-theory.multiples-of-elements-rings open import ring-theory.rings open import ring-theory.sums-of-finite-sequences-of-elements-semirings @@ -254,6 +255,18 @@ module _ ( λ c x → inv (left-distributive-mul-sum-fin-sequence-type-Ring R n c x)) ``` +### The sum of a constant finite sequence in a ring is scalar multiplication by the length of the sequence + +```agda +abstract + sum-constant-fin-sequence-type-Ring : + {l : Level} (R : Ring l) (n : ℕ) (x : type-Ring R) → + sum-fin-sequence-type-Ring R n (λ _ → x) ＝ + multiple-Ring R n x + sum-constant-fin-sequence-type-Ring R = + sum-constant-fin-sequence-type-Semiring ( semiring-Ring R) +``` + ## See also - [Sums of finite families of elements in rings](ring-theory.sums-of-finite-families-of-elements-rings.md) diff --git a/src/ring-theory/sums-of-finite-sequences-of-elements-semirings.lagda.md b/src/ring-theory/sums-of-finite-sequences-of-elements-semirings.lagda.md index fc420c7089..be44be3ed9 100644 --- a/src/ring-theory/sums-of-finite-sequences-of-elements-semirings.lagda.md +++ b/src/ring-theory/sums-of-finite-sequences-of-elements-semirings.lagda.md @@ -286,12 +286,12 @@ module _ ```agda abstract - constant-sum-fin-sequence-type-Semiring : + sum-constant-fin-sequence-type-Semiring : {l : Level} (R : Semiring l) (n : ℕ) (x : type-Semiring R) → sum-fin-sequence-type-Semiring R n (λ _ → x) ＝ multiple-Semiring R n x - constant-sum-fin-sequence-type-Semiring R = - constant-sum-fin-sequence-type-Commutative-Monoid + sum-constant-fin-sequence-type-Semiring R = + sum-constant-fin-sequence-type-Commutative-Monoid ( additive-commutative-monoid-Semiring R) ```