Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Introduction to Banach and Hilbert Spaces --- Part III

by
Jan Popiolek

MML identifier: BHSP_3
[ Mizar article, MML identifier index ]

```environ

vocabulary BHSP_1, PRE_TOPC, NORMSP_1, ORDINAL2, SEQM_3, SEQ_1, RLVECT_1,
METRIC_1, FUNCT_1, ARYTM_1, ARYTM_3, ABSVALUE, RELAT_1, SEQ_2, LATTICES,
BHSP_3, ARYTM;
notation TARSKI, ORDINAL1, NUMBERS, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1,
FUNCT_2, SEQ_1, SEQM_3, ABSVALUE, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_1,
BHSP_1, BHSP_2;
constructors REAL_1, NAT_1, SEQ_1, ABSVALUE, BHSP_2, MEMBERED, XBOOLE_0;
clusters FUNCT_1, SEQM_3, STRUCT_0, XREAL_0, RELSET_1, ARYTM_3, MEMBERED,
ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve X for RealUnitarySpace,
x, g, g1, h for Point of X,
a, p, r, M, M1, M2 for Real,
seq, seq1, seq2, seq3 for sequence of X,
Nseq,Nseq1,Nseq2 for increasing Seq_of_Nat,
Rseq for Real_Sequence,
k, l, l1, l2, l3, n, m, m1, m2 for Nat;

definition
let X;
let seq;
attr seq is Cauchy means
:: BHSP_3:def 1
for r st r > 0 ex k st for n, m st ( n >= k & m >= k )
holds dist((seq.n), (seq.m)) < r;
synonym seq is_Cauchy_sequence;
end;

theorem :: BHSP_3:1
seq is constant implies seq is_Cauchy_sequence;

theorem :: BHSP_3:2
seq is_Cauchy_sequence iff for r st r > 0 ex k st for n, m st
( n >= k & m >= k ) holds ||.(seq.n) - (seq.m).|| < r;

theorem :: BHSP_3:3
seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence implies
seq1 + seq2 is_Cauchy_sequence;

theorem :: BHSP_3:4
seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence implies
seq1 - seq2 is_Cauchy_sequence;

theorem :: BHSP_3:5
seq is_Cauchy_sequence implies a * seq is_Cauchy_sequence;

theorem :: BHSP_3:6
seq is_Cauchy_sequence implies - seq is_Cauchy_sequence;

theorem :: BHSP_3:7
seq is_Cauchy_sequence implies seq + x is_Cauchy_sequence;

theorem :: BHSP_3:8
seq is_Cauchy_sequence implies seq - x is_Cauchy_sequence;

theorem :: BHSP_3:9
seq is convergent implies seq is_Cauchy_sequence;

definition
let X;
let seq1, seq2;
pred seq1 is_compared_to seq2 means
:: BHSP_3:def 2
for r st r > 0 ex m st for n st n >= m holds
dist(seq1.n, seq2.n) < r;
end;

theorem :: BHSP_3:10
seq is_compared_to seq;

theorem :: BHSP_3:11
seq1 is_compared_to seq2 implies seq2 is_compared_to seq1;

definition let X; let seq1, seq2;
redefine pred seq1 is_compared_to seq2;
reflexivity;
symmetry;
end;

theorem :: BHSP_3:12
seq1 is_compared_to seq2 & seq2 is_compared_to seq3
implies seq1 is_compared_to seq3;

theorem :: BHSP_3:13
seq1 is_compared_to seq2 iff for r st r > 0 ex m st
for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r;

theorem :: BHSP_3:14
( ex k st for n st n >= k holds seq1.n = seq2.n )
implies seq1 is_compared_to seq2;

theorem :: BHSP_3:15
seq1 is_Cauchy_sequence & seq1 is_compared_to seq2
implies seq2 is_Cauchy_sequence;

theorem :: BHSP_3:16
seq1 is convergent & seq1 is_compared_to seq2
implies seq2 is convergent;

theorem :: BHSP_3:17
seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2
implies seq2 is convergent & lim seq2 = g;

definition
let X;
let seq;
attr seq is bounded means
:: BHSP_3:def 3
ex M st M > 0 & for n holds ||.seq.n.|| <= M;
end;

theorem :: BHSP_3:18
seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded;

theorem :: BHSP_3:19
seq is bounded implies -seq is bounded;

theorem :: BHSP_3:20
seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded;

theorem :: BHSP_3:21
seq is bounded implies a * seq is bounded;

theorem :: BHSP_3:22
seq is constant implies seq is bounded;

theorem :: BHSP_3:23
for m ex M st ( M > 0 & for n st n <= m holds ||.seq.n.|| < M );

theorem :: BHSP_3:24
seq is convergent implies seq is bounded;

theorem :: BHSP_3:25
seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded;

definition let X, Nseq, seq;
redefine func seq * Nseq -> sequence of X;
end;

definition let X be non empty 1-sorted,
s1, s be sequence of X;
pred s1 is_subsequence_of s means
:: BHSP_3:def 4
ex N being increasing Seq_of_Nat st s1 = s * N;
end;

theorem :: BHSP_3:26
for X being RealUnitarySpace,
s being sequence of X,
N being increasing Seq_of_Nat
for n being Nat holds (s * N).n=s.(N.n);

theorem :: BHSP_3:27
seq is_subsequence_of seq;

theorem :: BHSP_3:28
seq1 is_subsequence_of seq2 & seq2 is_subsequence_of seq3
implies seq1 is_subsequence_of seq3;

theorem :: BHSP_3:29
seq is constant & seq1 is_subsequence_of seq implies seq1 is constant;

theorem :: BHSP_3:30
seq is constant & seq1 is_subsequence_of seq implies seq = seq1;

theorem :: BHSP_3:31
seq is bounded & seq1 is_subsequence_of seq implies seq1 is bounded;

theorem :: BHSP_3:32
seq is convergent & seq1 is_subsequence_of seq implies seq1 is convergent;

theorem :: BHSP_3:33
seq1 is_subsequence_of seq & seq is convergent implies lim seq1=lim seq;

theorem :: BHSP_3:34
seq is_Cauchy_sequence & seq1 is_subsequence_of seq
implies seq1 is_Cauchy_sequence;

definition
let X;
let seq;
let k;
func seq ^\k -> sequence of X means
:: BHSP_3:def 5
for n holds it.n=seq.(n + k);
end;

theorem :: BHSP_3:35
seq ^\0 = seq;

theorem :: BHSP_3:36
(seq ^\k)^\m = (seq ^\m)^\k;

theorem :: BHSP_3:37
(seq ^\k)^\m=seq ^\(k + m);

theorem :: BHSP_3:38
(seq1 + seq2) ^\k = (seq1 ^\k) + (seq2 ^\k);

theorem :: BHSP_3:39
(-seq) ^\k = -(seq ^\k);

theorem :: BHSP_3:40
(seq1 - seq2) ^\k = (seq1 ^\k) - (seq2 ^\k);

theorem :: BHSP_3:41
(a * seq) ^\k = a * (seq ^\k);

theorem :: BHSP_3:42
(seq * Nseq) ^\k = seq * (Nseq ^\k);

theorem :: BHSP_3:43
seq ^\k is_subsequence_of seq;

theorem :: BHSP_3:44
seq is convergent implies ((seq ^\k) is convergent &
lim (seq ^\k)=lim seq);

canceled;

theorem :: BHSP_3:46
seq is convergent & (ex k st seq = seq1 ^\k) implies seq1 is convergent;

theorem :: BHSP_3:47
seq is_Cauchy_sequence & (ex k st seq = seq1 ^\k)
implies seq1 is_Cauchy_sequence;

theorem :: BHSP_3:48
seq is_Cauchy_sequence implies (seq ^\k) is_Cauchy_sequence;

theorem :: BHSP_3:49
seq1 is_compared_to seq2 implies (seq1 ^\k) is_compared_to (seq2 ^\k);

theorem :: BHSP_3:50
seq is bounded implies (seq ^\k) is bounded;

theorem :: BHSP_3:51
seq is constant implies (seq ^\k) is constant;

definition
let X;
attr X is complete means
:: BHSP_3:def 6
for seq holds
seq is_Cauchy_sequence implies seq is convergent;
synonym X is_complete_space;
end;

canceled;

theorem :: BHSP_3:53
X is_complete_space & seq is_Cauchy_sequence implies seq is bounded;

definition
let X;
attr X is Hilbert means
:: BHSP_3:def 7
X is RealUnitarySpace & X is_complete_space;
synonym X is_Hilbert_space;
end;
```