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

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

registration
let X be RealUnitarySpace;
cluster V1() V4( NAT ) V5( the U1 of X) V6() constant V11() V14( NAT ) V18( NAT , the U1 of X) for sequence of ;
existence
ex b1 being sequence of X st b1 is constant
proof end;
end;

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 Nat st
for n, m being 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 Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r );

registration
let X be RealUnitarySpace;
cluster V6() constant V18( NAT , the U1 of X) -> Cauchy for sequence of ;
coherence
for b1 being sequence of X st b1 is constant holds
b1 is Cauchy
proof end;
end;

theorem :: BHSP_3:1
canceled;

::$CT 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 Nat st for n, m being Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r ) proof end; registration let X be RealUnitarySpace; let seq1, seq2 be Cauchy sequence of X; cluster K196(X,seq1,seq2) -> Cauchy ; coherence seq1 + seq2 is Cauchy proof end; end; registration let X be RealUnitarySpace; let seq1, seq2 be Cauchy sequence of X; cluster seq1 - seq2 -> Cauchy ; coherence seq1 - seq2 is Cauchy proof end; end; registration let X be RealUnitarySpace; let a be Real; let seq be Cauchy sequence of X; cluster a * seq -> Cauchy ; coherence a * seq is Cauchy proof end; end; registration let X be RealUnitarySpace; let seq be Cauchy sequence of X; cluster - seq -> Cauchy ; coherence - seq is Cauchy proof end; end; registration let X be RealUnitarySpace; let x be Point of X; let seq be Cauchy sequence of X; cluster seq + x -> Cauchy ; coherence seq + x is Cauchy proof end; end; registration let X be RealUnitarySpace; let x be Point of X; let seq be Cauchy sequence of X; cluster seq - x -> Cauchy ; coherence seq - x is Cauchy proof end; end; registration let X be RealUnitarySpace; cluster V6() V18( NAT , the U1 of X) convergent -> Cauchy for sequence of ; coherence for b1 being sequence of X st b1 is convergent holds b1 is Cauchy proof end; end; definition let X be RealUnitarySpace; let seq1, seq2 be sequence of X; pred seq1 is_compared_to seq2 means :: BHSP_3:def 2 for r being Real st r > 0 holds ex m being Nat st for n being Nat st n >= m holds dist ((seq1 . n),(seq2 . n)) < r; reflexivity for seq1 being sequence of X for r being Real st r > 0 holds ex m being Nat st for n being Nat st n >= m holds dist ((seq1 . n),(seq1 . n)) < r proof end; symmetry for seq1, seq2 being sequence of X st ( for r being Real st r > 0 holds ex m being Nat st for n being Nat st n >= m holds dist ((seq1 . n),(seq2 . n)) < r ) holds for r being Real st r > 0 holds ex m being Nat st for n being Nat st n >= m holds dist ((seq2 . n),(seq1 . n)) < r proof end; end; :: deftheorem 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 Nat st for n being Nat st n >= m holds dist ((seq1 . n),(seq2 . n)) < r ); theorem :: BHSP_3:3 canceled; theorem :: BHSP_3:4 canceled; theorem :: BHSP_3:5 canceled; theorem :: BHSP_3:6 canceled; theorem :: BHSP_3:7 canceled; theorem :: BHSP_3:8 canceled; theorem :: BHSP_3:9 canceled; theorem :: BHSP_3:10 canceled; theorem :: BHSP_3:11 canceled; ::$CT 9
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 Nat st
for n being 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 Nat st
for n being 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 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 Nat holds ||.(seq . n).|| <= M ) ) );

registration
let X be RealUnitarySpace;
cluster V6() constant V18( NAT , the U1 of X) -> bounded for sequence of ;
coherence
for b1 being sequence of X st b1 is constant holds
b1 is bounded
proof end;
end;

registration
let X be RealUnitarySpace;
let seq1, seq2 be bounded sequence of X;
cluster K196(X,seq1,seq2) -> bounded ;
coherence
seq1 + seq2 is bounded
proof end;
end;

registration
let X be RealUnitarySpace;
let seq be bounded sequence of X;
cluster - seq -> bounded ;
coherence
- seq is bounded
proof end;
end;

registration
let X be RealUnitarySpace;
let seq1, seq2 be bounded sequence of X;
cluster seq1 - seq2 -> bounded ;
coherence
seq1 - seq2 is bounded
proof end;
end;

registration
let X be RealUnitarySpace;
let a be Real;
let seq be bounded sequence of X;
cluster a * seq -> bounded ;
coherence
a * seq is bounded
proof end;
end;

theorem :: BHSP_3:18
canceled;

theorem :: BHSP_3:19
canceled;

theorem :: BHSP_3:20
canceled;

theorem :: BHSP_3:21
canceled;

theorem :: BHSP_3:22
canceled;

::$CT 5 theorem Th8: :: BHSP_3:23 for X being RealUnitarySpace for seq being sequence of X for m being Nat ex M being Real st ( M > 0 & ( for n being Nat st n <= m holds ||.(seq . n).|| < M ) ) proof end; registration let X be RealUnitarySpace; cluster V6() V18( NAT , the U1 of X) convergent -> bounded for sequence of ; coherence for b1 being sequence of X st b1 is convergent holds b1 is bounded proof end; end; theorem :: BHSP_3:24 canceled; ::$CT
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;

registration
let X be RealUnitarySpace;
let seq be bounded sequence of X;
cluster -> bounded for of ;
coherence
for b1 being subsequence of seq holds b1 is bounded
proof end;
end;

registration
let X be RealUnitarySpace;
let seq be convergent sequence of X;
cluster -> convergent for of ;
coherence
for b1 being subsequence of seq holds b1 is convergent
proof end;
end;

theorem :: BHSP_3:26
canceled;

theorem :: BHSP_3:27
canceled;

::$CT 2 theorem Th10: :: BHSP_3:28 for X being RealUnitarySpace for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds lim seq1 = lim seq proof end; registration let X be RealUnitarySpace; let seq be Cauchy sequence of X; cluster -> Cauchy for of ; coherence for b1 being subsequence of seq holds b1 is Cauchy proof end; end; theorem :: BHSP_3:29 canceled; ::$CT
theorem :: BHSP_3:30
for X being RealUnitarySpace
for seq being sequence of X
for k, m being 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 Nat holds (seq ^\ k) ^\ m = seq ^\ (k + m)
proof end;

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

theorem Th14: :: BHSP_3:33
for X being RealUnitarySpace
for seq being sequence of X
for k being 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 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 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 Nat st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th10;

theorem :: BHSP_3:37
for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & ex k being 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 Nat st seq = seq1 ^\ k holds
seq1 is Cauchy
proof end;

theorem :: BHSP_3:39
canceled;

::$CT theorem :: BHSP_3:40 for X being RealUnitarySpace for seq1, seq2 being sequence of X for k being Nat st seq1 is_compared_to seq2 holds seq1 ^\ k is_compared_to seq2 ^\ k proof end; definition let X be RealUnitarySpace; attr X is complete means :: BHSP_3:def 4 for seq being sequence of X st seq is Cauchy holds seq is convergent ; end; :: deftheorem 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:41 canceled; theorem :: BHSP_3:42 canceled; ::$CT 2
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;