:: Introduction to Banach and Hilbert spaces - Part III
:: by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

deffunc H1( RealUnitarySpace) -> Element of the U1 of $1 = 0. $1;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
attr seq is Cauchy means :Def1: :: BHSP_3:def 1
 for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r;
end;

:: deftheorem Def1 defines Cauchy BHSP_3:def 1 :
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r );

theorem :: BHSP_3:1
for X being RealUnitarySpace
for seq being sequence of X st seq is constant holds
seq is Cauchy
proof end;

theorem :: BHSP_3:2
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
proof end;

theorem :: BHSP_3:3
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 + seq2 is Cauchy
proof end;

theorem :: BHSP_3:4
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 - seq2 is Cauchy
proof end;

theorem Th5: :: BHSP_3:5
for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is Cauchy holds
a * seq is Cauchy
proof end;

theorem :: BHSP_3:6
for X being RealUnitarySpace
for seq being sequence of X st seq is Cauchy holds
- seq is Cauchy
proof end;

theorem Th7: :: BHSP_3:7
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq + x is Cauchy
proof end;

theorem :: BHSP_3:8
for X being RealUnitarySpace
for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq - x is Cauchy
proof end;

theorem :: BHSP_3:9
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is Cauchy
proof end;

definition
let X be RealUnitarySpace;
let seq1, seq2 be sequence of X;
pred seq1 is_compared_to seq2 means :Def2: :: BHSP_3:def 2
 for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r;
end;

:: deftheorem Def2 defines is_compared_to BHSP_3:def 2 :
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r );

theorem Th10: :: BHSP_3:10
for X being RealUnitarySpace
for seq being sequence of X holds seq is_compared_to seq
proof end;

theorem Th11: :: BHSP_3:11
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds
seq2 is_compared_to seq1
proof end;

definition
let X be RealUnitarySpace;
let seq1, seq2 be sequence of X;
:: original: is_compared_to
redefine pred seq1 is_compared_to seq2;
reflexivity
for seq1 being sequence of X holds (X,b1,b1) by Th10;
symmetry
for seq1, seq2 being sequence of X st (X,b1,b2) holds
(X,b2,b1) by Th11;
end;

theorem :: BHSP_3:12
for X being RealUnitarySpace
for seq1, seq2, seq3 being sequence of X st seq1 is_compared_to seq2 & seq2 is_compared_to seq3 holds
seq1 is_compared_to seq3
proof end;

theorem :: BHSP_3:13
for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r )
proof end;

theorem :: BHSP_3:14
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq1 . n = seq2 . n holds
seq1 is_compared_to seq2
proof end;

theorem :: BHSP_3:15
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds
seq2 is Cauchy
proof end;

theorem :: BHSP_3:16
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds
seq2 is convergent
proof end;

theorem :: BHSP_3:17
for X being RealUnitarySpace
for g being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds
( seq2 is convergent & lim seq2 = g )
proof end;

definition
let X be RealUnitarySpace;
let seq be sequence of X;
attr seq is bounded means :Def3: :: BHSP_3:def 3
 ex M being Real st
( M > 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) );
end;

:: deftheorem Def3 defines bounded BHSP_3:def 3 :
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is bounded iff ex M being Real st
( M > 0 & ( for n being Element of NAT holds ||.(seq . n).|| <= M ) ) );

theorem Th18: :: BHSP_3:18
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
proof end;

theorem Th19: :: BHSP_3:19
for X being RealUnitarySpace
for seq being sequence of X st seq is bounded holds
- seq is bounded
proof end;

theorem :: BHSP_3:20
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 - seq2 is bounded
proof end;

theorem :: BHSP_3:21
for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is bounded holds
a * seq is bounded
proof end;

theorem :: BHSP_3:22
for X being RealUnitarySpace
for seq being sequence of X st seq is constant holds
seq is bounded
proof end;

theorem Th23: :: BHSP_3:23
for X being RealUnitarySpace
for seq being sequence of X
for m being Element of NAT ex M being Real st
( M > 0 & ( for n being Element of NAT st n <= m holds
||.(seq . n).|| < M ) )
proof end;

theorem Th24: :: BHSP_3:24
for X being RealUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is bounded
proof end;

theorem :: BHSP_3:25
for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds
seq2 is bounded
proof end;

theorem Th26: :: BHSP_3:26
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded
proof end;

theorem Th27: :: BHSP_3:27
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds
seq1 is convergent
proof end;

theorem Th28: :: BHSP_3:28
for X being RealUnitarySpace
for seq1, seq being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof end;

theorem Th29: :: BHSP_3:29
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds
seq1 is Cauchy
proof end;

theorem :: BHSP_3:30
for X being RealUnitarySpace
for seq being sequence of X
for k, m being Element of NAT holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
proof end;

theorem :: BHSP_3:31
for X being RealUnitarySpace
for seq being sequence of X
for k, m being Element of NAT holds (seq ^\ k) ^\ m = seq ^\ (k + m)
proof end;

theorem Th32: :: BHSP_3:32
for X being RealUnitarySpace
for seq1, seq2 being sequence of X
for k being Element of NAT holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)
proof end;

theorem Th33: :: BHSP_3:33
for X being RealUnitarySpace
for seq being sequence of X
for k being Element of NAT holds (- seq) ^\ k = - (seq ^\ k)
proof end;

theorem :: BHSP_3:34
for X being RealUnitarySpace
for seq1, seq2 being sequence of X
for k being Element of NAT holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
proof end;

theorem :: BHSP_3:35
for X being RealUnitarySpace
for a being Real
for seq being sequence of X
for k being Element of NAT holds (a * seq) ^\ k = a * (seq ^\ k)
proof end;

theorem :: BHSP_3:36
for X being RealUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th27, Th28;

theorem :: BHSP_3:37
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent
proof end;

theorem :: BHSP_3:38
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is Cauchy
proof end;

theorem :: BHSP_3:39
for X being RealUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is Cauchy holds
seq ^\ k is Cauchy by Th29;

theorem :: BHSP_3:40
for X being RealUnitarySpace
for seq1, seq2 being sequence of X
for k being Element of NAT st seq1 is_compared_to seq2 holds
seq1 ^\ k is_compared_to seq2 ^\ k
proof end;

theorem :: BHSP_3:41
for X being RealUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is bounded holds
seq ^\ k is bounded by Th26;

theorem :: BHSP_3:42
for X being RealUnitarySpace
for seq being sequence of X
for k being Element of NAT st seq is constant holds
seq ^\ k is constant ;

definition
let X be RealUnitarySpace;
attr X is complete means :Def4: :: BHSP_3:def 4
 for seq being sequence of X st seq is Cauchy holds
seq is convergent ;
end;

:: deftheorem Def4 defines complete BHSP_3:def 4 :
for X being RealUnitarySpace holds
( X is complete iff for seq being sequence of X st seq is Cauchy holds
seq is convergent );

theorem :: BHSP_3:43
for X being RealUnitarySpace
for seq being sequence of X st X is complete & seq is Cauchy holds
seq is bounded
proof end;