Skip to content

Commit 619b7af

Browse files
lowasserlowasser
committed
Simplification
1 parent 651dca2 commit 619b7af

File tree

2 files changed

+91
-58
lines changed

2 files changed

+91
-58
lines changed

‎src/analysis/absolute-convergence-series-real-banach-spaces.lagda.md‎

Lines changed: 27 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ module _
7272

7373
## Properties
7474

75-
### A Cauchy modulus for the sequence of partial sums of norms of terms in a series is a Cauchy modulus for the series
75+
### Given a Cauchy modulus for the sequence of partial sums of norms of terms in a series, there is a Cauchy modulus of the series
7676

7777
```agda
7878
module _
@@ -86,69 +86,68 @@ module _
8686
8787
abstract
8888
neighborhood-add-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space :
89-
(ε : ℚ⁺) (n k : ℕ) → leq-ℕ (pr1 (M ε)) n →
89+
(ε : ℚ⁺) (k : ℕ) →
9090
neighborhood-ℝ-Banach-Space
9191
( V)
9292
( ε)
93-
( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ k))
94-
( partial-sum-series-ℝ-Banach-Space V σ n)
93+
( partial-sum-series-ℝ-Banach-Space V σ (pr1 (M ε)))
94+
( partial-sum-series-ℝ-Banach-Space V σ (pr1 (M ε) +ℕ k))
9595
neighborhood-add-cauchy-modulus-partial-sum-norm-series-ℝ-Banach-Space
96-
ε n k με≤n =
96+
ε k =
9797
let
9898
open inequality-reasoning-Large-Poset ℝ-Large-Poset
99+
με = pr1 (M ε)
99100
in
100101
chain-of-inequalities
101102
dist-ℝ-Banach-Space V
102-
( partial-sum-series-ℝ-Banach-Space V σ (n +ℕ k))
103-
( partial-sum-series-ℝ-Banach-Space V σ n)
103+
( partial-sum-series-ℝ-Banach-Space V σ με)
104+
( partial-sum-series-ℝ-Banach-Space V σ (με +ℕ k))
105+
≤ dist-ℝ-Banach-Space V
106+
( partial-sum-series-ℝ-Banach-Space V σ (με +ℕ k))
107+
( partial-sum-series-ℝ-Banach-Space V σ με)
108+
by leq-eq-ℝ (commutative-dist-ℝ-Banach-Space V _ _)
104109
≤ map-norm-ℝ-Banach-Space V
105110
( partial-sum-series-ℝ-Banach-Space V
106-
( drop-series-ℝ-Banach-Space V n σ)
107-
( k))
111+
( drop-series-ℝ-Banach-Space V με σ) k)
108112
by
109113
leq-eq-ℝ
110114
( ap
111115
( map-norm-ℝ-Banach-Space V)
112-
( inv (partial-sum-drop-series-ℝ-Banach-Space V n σ k)))
116+
( inv
117+
( partial-sum-drop-series-ℝ-Banach-Space V με σ k)))
113118
≤ partial-sum-series-ℝ
114-
( map-norm-series-ℝ-Banach-Space V
115-
( drop-series-ℝ-Banach-Space V n σ))
116-
( k)
117-
by
118-
triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space
119+
( map-norm-series-ℝ-Banach-Space
119120
( V)
120-
( k)
121-
( _)
121+
( drop-series-ℝ-Banach-Space V με σ))
122+
( k)
123+
by triangle-inequality-norm-sum-fin-sequence-type-ℝ-Banach-Space V k _
122124
≤ ( partial-sum-series-ℝ
123125
( map-norm-series-ℝ-Banach-Space V σ)
124-
( n +ℕ k)) -ℝ
125-
( partial-sum-series-ℝ (map-norm-series-ℝ-Banach-Space V σ) n)
126+
( με +ℕ k)) -ℝ
127+
( partial-sum-series-ℝ
128+
( map-norm-series-ℝ-Banach-Space V σ)
129+
( με))
126130
by
127131
leq-eq-ℝ
128132
( partial-sum-drop-series-ℝ
129-
( n)
133+
( με)
130134
( map-norm-series-ℝ-Banach-Space V σ)
131135
( k))
132136
≤ dist-ℝ
133137
( partial-sum-series-ℝ
134138
( map-norm-series-ℝ-Banach-Space V σ)
135-
( n +ℕ k))
139+
( με +ℕ k))
136140
( partial-sum-series-ℝ
137141
( map-norm-series-ℝ-Banach-Space V σ)
138-
( n))
142+
( με))
139143
by leq-diff-dist-ℝ _ _
140144
≤ real-ℚ⁺ ε
141145
by
142146
leq-dist-neighborhood-ℝ
143147
( ε)
144148
( _)
145149
( _)
146-
( pr2
147-
( M ε)
148-
( n +ℕ k)
149-
( n)
150-
( transitive-leq-ℕ (pr1 (M ε)) n (n +ℕ k) (leq-add-ℕ n k) με≤n)
151-
( με≤n))
150+
( pr2 (M ε) _ _ (leq-add-ℕ με k) (refl-leq-ℕ με))
152151
153152
is-cauchy-partial-sum-is-cauchy-partial-sum-norm-series-ℝ-Banach-Space :
154153
is-cauchy-sequence-Metric-Space

‎src/metric-spaces/cauchy-sequences-metric-spaces.lagda.md‎

Lines changed: 64 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,31 @@ module _
8686
(m k : ℕ) → leq-ℕ N m → leq-ℕ N k →
8787
neighborhood-Metric-Space M ε (x m) (x k)
8888
89+
is-cauchy-modulus-sequence-Metric-Space' : ℚ⁺ → ℕ → UU l2
90+
is-cauchy-modulus-sequence-Metric-Space' ε N =
91+
(m k : ℕ) → leq-ℕ N m →
92+
neighborhood-Metric-Space M ε (x (m +ℕ k)) (x m)
93+
94+
is-cauchy-modulus-is-cauchy-modulus-sequence-Metric-Space' :
95+
(ε : ℚ⁺) (N : ℕ) → is-cauchy-modulus-sequence-Metric-Space' ε N →
96+
is-cauchy-modulus-sequence-Metric-Space ε N
97+
is-cauchy-modulus-is-cauchy-modulus-sequence-Metric-Space' ε N H m k N≤m N≤k =
98+
let
99+
case a b N≤a a≤b =
100+
let
101+
( c , c+a=b) = subtraction-leq-ℕ a b a≤b
102+
in
103+
tr
104+
( λ d → neighborhood-Metric-Space M ε (x d) (x a))
105+
( commutative-add-ℕ a c ∙ c+a=b)
106+
( H a c N≤a)
107+
in
108+
rec-coproduct
109+
( λ m≤k →
110+
symmetric-neighborhood-Metric-Space M ε _ _ (case m k N≤m m≤k))
111+
( λ k≤m → case k m N≤k k≤m)
112+
( linear-leq-ℕ m k)
113+
89114
is-cauchy-sequence-Metric-Space : UU l2
90115
is-cauchy-sequence-Metric-Space =
91116
(ε : ℚ⁺) → Σ ℕ (is-cauchy-modulus-sequence-Metric-Space ε)
@@ -773,7 +798,7 @@ module _
773798
is-cauchy-sequence-pair-cauchy-sequence-Metric-Space)
774799
```
775800

776-
### To show a sequence `aₙ` is Cauchy, it suffices to have a modulus function such that for any `ε`, `aₙ` and `aₙ₊ₖ` are in an `ε`-neighborhood for sufficiently large `n`
801+
### To show a sequence `a` is Cauchy, it suffices to have a modulus function `μ` such that for any `ε`, `a (μ ε)` and `a (μ ε + k)` are in an `ε`-neighborhood
777802

778803
```agda
779804
module
@@ -785,42 +810,51 @@ module
785810
where
786811
787812
abstract
788-
is-cauchy-modulus-neighborhood-add-sequence-Metric-Space :
789-
( (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (μ ε) n →
790-
neighborhood-Metric-Space X ε (a (n +ℕ k)) (a n)) →
813+
cauchy-modulus-neighborhood-add-sequence-Metric-Space :
814+
( (ε : ℚ⁺) (k : ℕ) →
815+
neighborhood-Metric-Space X ε (a (μ ε)) (a (μ ε +ℕ k))) →
791816
(ε : ℚ⁺) →
792-
is-cauchy-modulus-sequence-Metric-Space X a ε (μ ε)
793-
is-cauchy-modulus-neighborhood-add-sequence-Metric-Space H ε p q με≤p με≤q =
817+
is-cauchy-modulus-sequence-Metric-Space
818+
( X)
819+
( a)
820+
( ε)
821+
( μ (pr1 (bound-double-le-ℚ⁺ ε)))
822+
cauchy-modulus-neighborhood-add-sequence-Metric-Space H ε p q με'≤p με'≤q =
794823
let
795-
lemma :
796-
(m n : ℕ) → leq-ℕ (μ ε) m → leq-ℕ m n →
797-
neighborhood-Metric-Space X ε (a n) (a m)
798-
lemma m n με≤m m≤n =
799-
let
800-
( k , k+m=n) = subtraction-leq-ℕ m n m≤n
801-
in
802-
tr
803-
( λ p → neighborhood-Metric-Space X ε (a p) (a m))
804-
( commutative-add-ℕ m k ∙ k+m=n)
805-
( H ε m k με≤m)
824+
(ε' , ε'+ε'<ε) = bound-double-le-ℚ⁺ ε
825+
(k , k+με'=p) = subtraction-leq-ℕ (μ ε') p με'≤p
826+
(l , l+με'=q) = subtraction-leq-ℕ (μ ε') q με'≤q
806827
in
807-
rec-coproduct
808-
( λ p≤q →
809-
symmetric-neighborhood-Metric-Space
810-
( X)
811-
( ε)
812-
( a q)
813-
( a p)
814-
( lemma p q με≤p p≤q))
815-
( lemma q p με≤q)
816-
( linear-leq-ℕ p q)
828+
monotonic-neighborhood-Metric-Space
829+
( X)
830+
( a p)
831+
( a q)
832+
( ε' +ℚ⁺ ε')
833+
( ε)
834+
( ε'+ε'<ε)
835+
( triangular-neighborhood-Metric-Space
836+
( X)
837+
( a p)
838+
( a (μ ε'))
839+
( a q)
840+
( ε')
841+
( ε')
842+
( tr
843+
( λ n → neighborhood-Metric-Space X ε' (a (μ ε')) (a n))
844+
( commutative-add-ℕ (μ ε') l ∙ l+με'=q)
845+
( H ε' l))
846+
( tr
847+
( λ n → neighborhood-Metric-Space X ε' (a n) (a (μ ε')))
848+
( commutative-add-ℕ (μ ε') k ∙ k+με'=p)
849+
( symmetric-neighborhood-Metric-Space X ε' _ _ (H ε' k))))
817850
818851
is-cauchy-sequence-modulus-neighborhood-add-sequence-Metric-Space :
819-
( (ε : ℚ⁺) (n k : ℕ) → leq-ℕ (μ ε) n →
820-
neighborhood-Metric-Space X ε (a (n +ℕ k)) (a n)) →
852+
( (ε : ℚ⁺) (k : ℕ) →
853+
neighborhood-Metric-Space X ε (a (μ ε)) (a (μ ε +ℕ k))) →
821854
is-cauchy-sequence-Metric-Space X a
822855
is-cauchy-sequence-modulus-neighborhood-add-sequence-Metric-Space H ε =
823-
( μ ε , is-cauchy-modulus-neighborhood-add-sequence-Metric-Space H ε)
856+
( _ ,
857+
cauchy-modulus-neighborhood-add-sequence-Metric-Space H ε)
824858
```
825859

826860
## See also

0 commit comments

Comments
 (0)