:: CSSPACE4 semantic presentation
begin
Lm1: for rseq being Real_Sequence
for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K
proof
let rseq be Real_Sequence; ::_thesis: for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K
let K be real number ; ::_thesis: ( ( for n being Element of NAT holds rseq . n <= K ) implies upper_bound (rng rseq) <= K )
assume A1: for n being Element of NAT holds rseq . n <= K ; ::_thesis: upper_bound (rng rseq) <= K
now__::_thesis:_for_s_being_real_number_st_s_in_rng_rseq_holds_
s_<=_K
let s be real number ; ::_thesis: ( s in rng rseq implies s <= K )
assume s in rng rseq ; ::_thesis: s <= K
then ex n being set st
( n in NAT & rseq . n = s ) by FUNCT_2:11;
hence s <= K by A1; ::_thesis: verum
end;
hence upper_bound (rng rseq) <= K by SEQ_4:45; ::_thesis: verum
end;
Lm2: for rseq being Real_Sequence st rseq is bounded holds
for n being Element of NAT holds rseq . n <= upper_bound (rng rseq)
proof
let rseq be Real_Sequence; ::_thesis: ( rseq is bounded implies for n being Element of NAT holds rseq . n <= upper_bound (rng rseq) )
assume rseq is bounded ; ::_thesis: for n being Element of NAT holds rseq . n <= upper_bound (rng rseq)
then rng rseq is real-bounded by MEASURE6:39;
then A1: rng rseq is bounded_above by XXREAL_2:def_11;
let n be Element of NAT ; ::_thesis: rseq . n <= upper_bound (rng rseq)
NAT = dom rseq by FUNCT_2:def_1;
then rseq . n in rng rseq by FUNCT_1:3;
hence rseq . n <= upper_bound (rng rseq) by A1, SEQ_4:def_1; ::_thesis: verum
end;
definition
func the_set_of_BoundedComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE4:def 1
for x being set holds
( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) );
existence
ex b1 being Subset of Linear_Space_of_ComplexSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) )
proof
defpred S1[ set ] means seq_id $1 is bounded ;
consider IT being set such that
A1: for x being set holds
( x in IT iff ( x in the_set_of_ComplexSequences & S1[x] ) ) from XBOOLE_0:sch_1();
for x being set st x in IT holds
x in the_set_of_ComplexSequences by A1;
then IT is Subset of the_set_of_ComplexSequences by TARSKI:def_3;
hence ex b1 being Subset of Linear_Space_of_ComplexSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) by A1, CSSPACE:def_7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_ComplexSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) holds
b1 = b2
proof
let X1, X2 be Subset of Linear_Space_of_ComplexSequences; ::_thesis: ( ( for x being set holds
( x in X1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) & ( for x being set holds
( x in X2 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) implies X1 = X2 )
assume that
A2: for x being set holds
( x in X1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) and
A3: for x being set holds
( x in X2 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ; ::_thesis: X1 = X2
thus X1 c= X2 :: according to XBOOLE_0:def_10 ::_thesis: X2 c= X1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X1 or x in X2 )
assume x in X1 ; ::_thesis: x in X2
then ( x in the_set_of_ComplexSequences & seq_id x is bounded ) by A2;
hence x in X2 by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X2 or x in X1 )
assume x in X2 ; ::_thesis: x in X1
then ( x in the_set_of_ComplexSequences & seq_id x is bounded ) by A3;
hence x in X1 by A2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines the_set_of_BoundedComplexSequences CSSPACE4:def_1_:_
for b1 being Subset of Linear_Space_of_ComplexSequences holds
( b1 = the_set_of_BoundedComplexSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) );
Lm3: for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
proof
let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded )
assume that
A1: seq1 is bounded and
A2: seq2 is bounded ; ::_thesis: seq1 + seq2 is bounded
consider r2 being Real such that
0 < r2 and
A3: for n being Element of NAT holds |.(seq2 . n).| < r2 by A2, COMSEQ_2:8;
consider r1 being Real such that
0 < r1 and
A4: for n being Element of NAT holds |.(seq1 . n).| < r1 by A1, COMSEQ_2:8;
for n being Element of NAT holds |.((seq1 + seq2) . n).| < r1 + r2
proof
let n be Element of NAT ; ::_thesis: |.((seq1 + seq2) . n).| < r1 + r2
|.((seq1 + seq2) . n).| = |.((seq1 . n) + (seq2 . n)).| by VALUED_1:1;
then A5: |.((seq1 + seq2) . n).| <= |.(seq1 . n).| + |.(seq2 . n).| by COMPLEX1:56;
|.(seq1 . n).| < r1 by A4;
then |.(seq1 . n).| + |.(seq2 . n).| < r1 + r2 by A3, XREAL_1:8;
hence |.((seq1 + seq2) . n).| < r1 + r2 by A5, XXREAL_0:2; ::_thesis: verum
end;
hence seq1 + seq2 is bounded by COMSEQ_2:def_4; ::_thesis: verum
end;
Lm4: for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded
proof
let c be Complex; ::_thesis: for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded
let seq be Complex_Sequence; ::_thesis: ( seq is bounded implies c (#) seq is bounded )
assume seq is bounded ; ::_thesis: c (#) seq is bounded
then consider r being Real such that
0 < r and
A1: for n being Element of NAT holds |.(seq . n).| < r by COMSEQ_2:8;
ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1
proof
now__::_thesis:_(_(_c_=_0c_&_ex_r1_being_Element_of_NAT_ex_r1_being_Real_st_
for_n_being_Element_of_NAT_holds_|.((c_(#)_seq)_._n).|_<_r1_)_or_(_c_<>_0c_&_ex_r1_being_Element_of_REAL_ex_r1_being_Real_st_
for_n_being_Element_of_NAT_holds_|.((c_(#)_seq)_._n).|_<_r1_)_)
percases ( c = 0c or c <> 0c ) ;
caseA2: c = 0c ; ::_thesis: ex r1 being Element of NAT ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1
take r1 = 1; ::_thesis: ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1
for n being Element of NAT holds |.((c (#) seq) . n).| < 1
proof
let n be Element of NAT ; ::_thesis: |.((c (#) seq) . n).| < 1
(c (#) seq) . n = c * (seq . n) by VALUED_1:6
.= 0 by A2 ;
hence |.((c (#) seq) . n).| < 1 by COMPLEX1:44; ::_thesis: verum
end;
hence ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1 ; ::_thesis: verum
end;
caseA3: c <> 0c ; ::_thesis: ex r1 being Element of REAL ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1
take r1 = |.c.| * r; ::_thesis: ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1
for n being Element of NAT holds |.((c (#) seq) . n).| < |.c.| * r
proof
let n be Element of NAT ; ::_thesis: |.((c (#) seq) . n).| < |.c.| * r
A4: |.((c (#) seq) . n).| = |.(c * (seq . n)).| by VALUED_1:6
.= |.c.| * |.(seq . n).| by COMPLEX1:65 ;
|.c.| > 0 by A3, COMPLEX1:47;
hence |.((c (#) seq) . n).| < |.c.| * r by A1, A4, XREAL_1:68; ::_thesis: verum
end;
hence ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1 ; ::_thesis: verum
end;
end;
end;
hence ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1 ; ::_thesis: verum
end;
hence c (#) seq is bounded by COMSEQ_2:def_4; ::_thesis: verum
end;
registration
cluster the_set_of_BoundedComplexSequences -> non empty ;
coherence
not the_set_of_BoundedComplexSequences is empty
proof
seq_id CZeroseq is bounded
proof
reconsider seq = seq_id CZeroseq as Complex_Sequence ;
for n being Element of NAT holds |.(seq . n).| < 1 by COMPLEX1:44, CSSPACE:def_6;
hence seq_id CZeroseq is bounded by COMSEQ_2:8; ::_thesis: verum
end;
hence not the_set_of_BoundedComplexSequences is empty by Def1; ::_thesis: verum
end;
cluster the_set_of_BoundedComplexSequences -> linearly-closed ;
coherence
the_set_of_BoundedComplexSequences is linearly-closed
proof
set W = the_set_of_BoundedComplexSequences ;
A1: for c being Complex
for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences holds
c * v in the_set_of_BoundedComplexSequences
proof
let c be Complex; ::_thesis: for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences holds
c * v in the_set_of_BoundedComplexSequences
let v be VECTOR of Linear_Space_of_ComplexSequences; ::_thesis: ( v in the_set_of_BoundedComplexSequences implies c * v in the_set_of_BoundedComplexSequences )
assume v in the_set_of_BoundedComplexSequences ; ::_thesis: c * v in the_set_of_BoundedComplexSequences
then A2: seq_id v is bounded by Def1;
seq_id (c * v) = seq_id (c (#) (seq_id v)) by CSSPACE:3, CSSPACE:def_7
.= c (#) (seq_id v) by CSSPACE:1 ;
then seq_id (c * v) is bounded by A2, Lm4;
hence c * v in the_set_of_BoundedComplexSequences by Def1, CSSPACE:def_7; ::_thesis: verum
end;
for v, u being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences holds
v + u in the_set_of_BoundedComplexSequences
proof
let v, u be VECTOR of Linear_Space_of_ComplexSequences; ::_thesis: ( v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences implies v + u in the_set_of_BoundedComplexSequences )
assume ( v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences ) ; ::_thesis: v + u in the_set_of_BoundedComplexSequences
then A3: ( seq_id v is bounded & seq_id u is bounded ) by Def1;
seq_id (v + u) = seq_id ((seq_id v) + (seq_id u)) by CSSPACE:2, CSSPACE:def_7
.= (seq_id v) + (seq_id u) by CSSPACE:1 ;
then seq_id (v + u) is bounded by A3, Lm3;
hence v + u in the_set_of_BoundedComplexSequences by Def1, CSSPACE:def_7; ::_thesis: verum
end;
hence the_set_of_BoundedComplexSequences is linearly-closed by A1, CLVECT_1:def_7; ::_thesis: verum
end;
end;
Lm5: CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Subspace of Linear_Space_of_ComplexSequences
by CSSPACE:11;
registration
cluster CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is vector-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-unital ) by CSSPACE:11;
end;
Lm6: ( CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is Abelian & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is add-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_zeroed & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_complementable & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is vector-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-distributive & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-associative & CLSStruct(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-unital )
;
definition
func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences,REAL means :Def2: :: CSSPACE4:def 2
for x being set st x in the_set_of_BoundedComplexSequences holds
it . x = upper_bound (rng |.(seq_id x).|);
existence
ex b1 being Function of the_set_of_BoundedComplexSequences,REAL st
for x being set st x in the_set_of_BoundedComplexSequences holds
b1 . x = upper_bound (rng |.(seq_id x).|)
proof
deffunc H1( set ) -> Element of REAL = upper_bound (rng |.(seq_id $1).|);
A1: for z being set st z in the_set_of_BoundedComplexSequences holds
H1(z) in REAL ;
ex f being Function of the_set_of_BoundedComplexSequences,REAL st
for x being set st x in the_set_of_BoundedComplexSequences holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence ex b1 being Function of the_set_of_BoundedComplexSequences,REAL st
for x being set st x in the_set_of_BoundedComplexSequences holds
b1 . x = upper_bound (rng |.(seq_id x).|) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of the_set_of_BoundedComplexSequences,REAL st ( for x being set st x in the_set_of_BoundedComplexSequences holds
b1 . x = upper_bound (rng |.(seq_id x).|) ) & ( for x being set st x in the_set_of_BoundedComplexSequences holds
b2 . x = upper_bound (rng |.(seq_id x).|) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of the_set_of_BoundedComplexSequences,REAL; ::_thesis: ( ( for x being set st x in the_set_of_BoundedComplexSequences holds
NORM1 . x = upper_bound (rng |.(seq_id x).|) ) & ( for x being set st x in the_set_of_BoundedComplexSequences holds
NORM2 . x = upper_bound (rng |.(seq_id x).|) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in the_set_of_BoundedComplexSequences holds
NORM1 . x = upper_bound (rng |.(seq_id x).|) and
A3: for x being set st x in the_set_of_BoundedComplexSequences holds
NORM2 . x = upper_bound (rng |.(seq_id x).|) ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in the_set_of_BoundedComplexSequences holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in the_set_of_BoundedComplexSequences implies NORM1 . z = NORM2 . z )
assume A5: z in the_set_of_BoundedComplexSequences ; ::_thesis: NORM1 . z = NORM2 . z
NORM1 . z = upper_bound (rng |.(seq_id z).|) by A2, A5;
hence NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
( dom NORM1 = the_set_of_BoundedComplexSequences & dom NORM2 = the_set_of_BoundedComplexSequences ) by FUNCT_2:def_1;
hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Complex_linfty_norm CSSPACE4:def_2_:_
for b1 being Function of the_set_of_BoundedComplexSequences,REAL holds
( b1 = Complex_linfty_norm iff for x being set st x in the_set_of_BoundedComplexSequences holds
b1 . x = upper_bound (rng |.(seq_id x).|) );
Lm7: for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds
( seq is bounded & upper_bound (rng |.seq.|) = 0 )
proof
let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) )
assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: ( seq is bounded & upper_bound (rng |.seq.|) = 0 )
for n being Element of NAT holds |.(seq . n).| < 1 by A1, COMPLEX1:44;
hence seq is bounded by COMSEQ_2:def_4; ::_thesis: upper_bound (rng |.seq.|) = 0
rng |.seq.| c= {0}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng |.seq.| or y in {0} )
assume y in rng |.seq.| ; ::_thesis: y in {0}
then consider n being set such that
A2: n in NAT and
A3: |.seq.| . n = y by FUNCT_2:11;
reconsider n = n as Element of NAT by A2;
|.seq.| . n = |.(seq . n).| by VALUED_1:18
.= |.0c.| by A1 ;
hence y in {0} by A3, COMPLEX1:44, TARSKI:def_1; ::_thesis: verum
end;
then rng |.seq.| = {0} by ZFMISC_1:33;
hence upper_bound (rng |.seq.|) = 0 by SEQ_4:9; ::_thesis: verum
end;
Lm8: for seq being Complex_Sequence st seq is bounded holds
|.seq.| is bounded
proof
let seq be Complex_Sequence; ::_thesis: ( seq is bounded implies |.seq.| is bounded )
A1: 0 <= |.(seq . 0).| by COMPLEX1:46;
assume seq is bounded ; ::_thesis: |.seq.| is bounded
then consider r being Real such that
A2: for n being Element of NAT holds |.(seq . n).| < r by COMSEQ_2:def_4;
A3: for n being Element of NAT holds abs (|.seq.| . n) < r
proof
let n be Element of NAT ; ::_thesis: abs (|.seq.| . n) < r
|.seq.| . n = |.(seq . n).| by VALUED_1:18;
hence abs (|.seq.| . n) < r by A2; ::_thesis: verum
end;
|.(seq . 0).| < r by A2;
hence |.seq.| is bounded by A1, A3, SEQ_2:3; ::_thesis: verum
end;
Lm9: for seq being Complex_Sequence st |.seq.| is bounded holds
seq is bounded
proof
let seq be Complex_Sequence; ::_thesis: ( |.seq.| is bounded implies seq is bounded )
assume |.seq.| is bounded ; ::_thesis: seq is bounded
then consider r being real number such that
0 < r and
A1: for n being Element of NAT holds abs (|.seq.| . n) < r by SEQ_2:3;
reconsider r = r as Real by XREAL_0:def_1;
for n being Element of NAT holds |.(seq . n).| < r
proof
let n be Element of NAT ; ::_thesis: |.(seq . n).| < r
|.seq.| . n = |.(seq . n).| by VALUED_1:18;
then abs (|.seq.| . n) = |.(seq . n).| ;
hence |.(seq . n).| < r by A1; ::_thesis: verum
end;
hence seq is bounded by COMSEQ_2:def_4; ::_thesis: verum
end;
Lm10: for seq being Complex_Sequence st seq is bounded & upper_bound (rng |.seq.|) = 0 holds
for n being Element of NAT holds seq . n = 0c
proof
let seq be Complex_Sequence; ::_thesis: ( seq is bounded & upper_bound (rng |.seq.|) = 0 implies for n being Element of NAT holds seq . n = 0c )
assume that
A1: seq is bounded and
A2: upper_bound (rng |.seq.|) = 0 ; ::_thesis: for n being Element of NAT holds seq . n = 0c
let n be Element of NAT ; ::_thesis: seq . n = 0c
0 <= |.(seq . n).| by COMPLEX1:46;
then A3: 0 <= |.seq.| . n by VALUED_1:18;
|.seq.| is bounded by A1, Lm8;
then |.seq.| . n = 0 by A2, A3, Lm2;
then |.(seq . n).| = 0 by VALUED_1:18;
hence seq . n = 0c by COMPLEX1:45; ::_thesis: verum
end;
theorem :: CSSPACE4:1
for seq being Complex_Sequence holds
( ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) iff for n being Element of NAT holds seq . n = 0c ) by Lm7, Lm10;
registration
cluster CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is Abelian & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is add-associative & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is right_zeroed & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is right_complementable & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is vector-distributive & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-distributive & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-associative & CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is scalar-unital ) by Lm6, CSSPACE3:2;
end;
definition
func Complex_linfty_Space -> non empty CNORMSTR equals :: CSSPACE4:def 3
CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #);
coherence
CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #) is non empty CNORMSTR ;
end;
:: deftheorem defines Complex_linfty_Space CSSPACE4:def_3_:_
Complex_linfty_Space = CNORMSTR(# the_set_of_BoundedComplexSequences,(Zero_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences)),Complex_linfty_norm #);
theorem Th2: :: CSSPACE4:2
( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for x being set holds
( x is VECTOR of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for u being VECTOR of Complex_linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) ) & ( for u being VECTOR of Complex_linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) ) )
proof
set l1 = Complex_linfty_Space ;
A1: for x being set holds
( x is Element of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) )
proof
let x be set ; ::_thesis: ( x is Element of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) )
( x in the_set_of_ComplexSequences iff x is Complex_Sequence ) by CSSPACE:def_1;
hence ( x is Element of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) by Def1; ::_thesis: verum
end;
A2: for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v)
proof
let u, v be VECTOR of Complex_linfty_Space; ::_thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_BoundedComplexSequences ;
dom the addF of Linear_Space_of_ComplexSequences = [: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def_1;
then A3: dom ( the addF of Linear_Space_of_ComplexSequences || the_set_of_BoundedComplexSequences) = [:the_set_of_BoundedComplexSequences,the_set_of_BoundedComplexSequences:] by RELAT_1:62;
u + v = ( the addF of Linear_Space_of_ComplexSequences || the_set_of_BoundedComplexSequences) . [u,v] by CSSPACE:def_8
.= u1 + v1 by A3, FUNCT_1:47 ;
hence u + v = (seq_id u) + (seq_id v) by CSSPACE:2, CSSPACE:def_7; ::_thesis: verum
end;
A4: for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u)
proof
let c be Complex; ::_thesis: for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u)
let u be VECTOR of Complex_linfty_Space; ::_thesis: c * u = c (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_BoundedComplexSequences ;
reconsider c = c as Element of COMPLEX by XCMPLX_0:def_2;
dom the Mult of Linear_Space_of_ComplexSequences = [:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def_1;
then A5: dom ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_BoundedComplexSequences:]) = [:COMPLEX,the_set_of_BoundedComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
c * u = the Mult of Complex_linfty_Space . [c,u] by CLVECT_1:def_1
.= ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_BoundedComplexSequences:]) . [c,u] by CSSPACE:def_9
.= the Mult of Linear_Space_of_ComplexSequences . [c,u] by A5, FUNCT_1:47
.= c * u1 by CLVECT_1:def_1 ;
hence c * u = c (#) (seq_id u) by CSSPACE:3, CSSPACE:def_7; ::_thesis: verum
end;
A6: for u being VECTOR of Complex_linfty_Space holds u = seq_id u
proof
let u be VECTOR of Complex_linfty_Space; ::_thesis: u = seq_id u
u is VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29;
hence u = seq_id u by CSSPACE:def_2, CSSPACE:def_7; ::_thesis: verum
end;
A7: for u being VECTOR of Complex_linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
proof
let u be VECTOR of Complex_linfty_Space; ::_thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1r) * u by CLVECT_1:3
.= (- 1r) (#) (seq_id u) by A4
.= - (seq_id u) by COMSEQ_1:11 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by A6; ::_thesis: verum
end;
A8: for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v)
proof
let u, v be VECTOR of Complex_linfty_Space; ::_thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by A2
.= (seq_id u) - (seq_id v) by A7 ; ::_thesis: verum
end;
A9: for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) by Def2;
0. Complex_linfty_Space = 0. Linear_Space_of_ComplexSequences by CSSPACE:def_10
.= CZeroseq by CSSPACE:def_7 ;
hence ( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for x being set holds
( x is VECTOR of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for u being VECTOR of Complex_linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) ) & ( for u being VECTOR of Complex_linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) ) ) by A1, A6, A2, A4, A7, A8, A9; ::_thesis: verum
end;
theorem Th3: :: CSSPACE4:3
for x, y being Point of Complex_linfty_Space
for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| )
proof
let x, y be Point of Complex_linfty_Space; ::_thesis: for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| )
let c be Complex; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| )
A1: for n being Element of NAT holds |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n)
proof
let n be Element of NAT ; ::_thesis: |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n)
|.(c (#) (seq_id x)).| . n = |.((c (#) (seq_id x)) . n).| by VALUED_1:18
.= |.(c * ((seq_id x) . n)).| by VALUED_1:6
.= |.c.| * |.((seq_id x) . n).| by COMPLEX1:65
.= |.c.| * (|.(seq_id x).| . n) by VALUED_1:18 ;
hence |.(c (#) (seq_id x)).| . n = |.c.| * (|.(seq_id x).| . n) ; ::_thesis: verum
end;
|.(seq_id x).| . 1 = |.((seq_id x) . 1).| by VALUED_1:18;
then A2: 0 <= |.(seq_id x).| . 1 by COMPLEX1:46;
A3: for n being Element of NAT holds |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|
proof
let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|
|.(seq_id (x + y)).| . n = |.(seq_id ((seq_id x) + (seq_id y))).| . n by Th2
.= |.((seq_id x) + (seq_id y)).| . n by CSSPACE:1
.= |.(((seq_id x) + (seq_id y)) . n).| by VALUED_1:18
.= |.(((seq_id x) . n) + ((seq_id y) . n)).| by VALUED_1:1 ;
hence |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).| ; ::_thesis: verum
end;
A4: for n being Element of NAT holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n)
proof
let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n)
|.(((seq_id x) . n) + ((seq_id y) . n)).| <= |.((seq_id x) . n).| + |.((seq_id y) . n).| by COMPLEX1:56;
then |.(seq_id (x + y)).| . n <= |.((seq_id x) . n).| + |.((seq_id y) . n).| by A3;
then |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + |.((seq_id y) . n).| by VALUED_1:18;
hence |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n) by VALUED_1:18; ::_thesis: verum
end;
A5: for n being Element of NAT holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n
proof
let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n
(|.(seq_id x).| . n) + (|.(seq_id y).| . n) = (|.(seq_id x).| + |.(seq_id y).|) . n by SEQ_1:7;
hence |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n by A4; ::_thesis: verum
end;
A6: now__::_thesis:_(_||.x.||_=_0_implies_x_=_0._Complex_linfty_Space_)
A7: x in the_set_of_ComplexSequences by Def1;
assume A8: ||.x.|| = 0 ; ::_thesis: x = 0. Complex_linfty_Space
( ||.x.|| = upper_bound (rng |.(seq_id x).|) & seq_id x is bounded ) by Th2;
then for n being Element of NAT holds 0c = (seq_id x) . n by A8, Lm10;
hence x = 0. Complex_linfty_Space by A7, Th2, CSSPACE:def_6; ::_thesis: verum
end;
seq_id x is bounded by Def1;
then |.(seq_id x).| is bounded by Lm8;
then A9: 0 <= upper_bound (rng |.(seq_id x).|) by A2, Lm2;
seq_id y is bounded by Def1;
then A10: |.(seq_id y).| is bounded by Lm8;
seq_id x is bounded by Def1;
then |.(seq_id x).| is bounded by Lm8;
then rng |.(seq_id x).| is real-bounded by MEASURE6:39;
then A11: rng |.(seq_id x).| is bounded_above by XXREAL_2:def_11;
A12: now__::_thesis:_(_x_=_0._Complex_linfty_Space_implies_||.x.||_=_0_)
assume x = 0. Complex_linfty_Space ; ::_thesis: ||.x.|| = 0
then A13: for n being Element of NAT holds (seq_id x) . n = 0c by Th2, CSSPACE:def_6;
thus ||.x.|| = upper_bound (rng |.(seq_id x).|) by Th2
.= 0 by A13, Lm7 ; ::_thesis: verum
end;
seq_id x is bounded by Def1;
then A14: |.(seq_id x).| is bounded by Lm8;
now__::_thesis:_for_n_being_Element_of_NAT_holds_|.(seq_id_(x_+_y)).|_._n_<=_(upper_bound_(rng_|.(seq_id_x).|))_+_(upper_bound_(rng_|.(seq_id_y).|))
let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|))
A15: |.(seq_id y).| . n <= upper_bound (rng |.(seq_id y).|) by A10, Lm2;
( (|.(seq_id x).| + |.(seq_id y).|) . n = (|.(seq_id x).| . n) + (|.(seq_id y).| . n) & |.(seq_id x).| . n <= upper_bound (rng |.(seq_id x).|) ) by A14, Lm2, SEQ_1:7;
then A16: (|.(seq_id x).| + |.(seq_id y).|) . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) by A15, XREAL_1:7;
|.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n by A5;
hence |.(seq_id (x + y)).| . n <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) by A16, XXREAL_0:2; ::_thesis: verum
end;
then A17: upper_bound (rng |.(seq_id (x + y)).|) <= (upper_bound (rng |.(seq_id x).|)) + (upper_bound (rng |.(seq_id y).|)) by Lm1;
A18: ( ||.y.|| = upper_bound (rng |.(seq_id y).|) & upper_bound (rng |.(seq_id (x + y)).|) = ||.(x + y).|| ) by Th2;
||.(c * x).|| = upper_bound (rng |.(seq_id (c * x)).|) by Th2
.= upper_bound (rng |.(seq_id (c (#) (seq_id x))).|) by Th2
.= upper_bound (rng |.(c (#) (seq_id x)).|) by CSSPACE:1
.= upper_bound (rng (|.c.| (#) |.(seq_id x).|)) by A1, SEQ_1:9
.= upper_bound (|.c.| ** (rng |.(seq_id x).|)) by INTEGRA2:17
.= |.c.| * (upper_bound (rng |.(seq_id x).|)) by A11, COMPLEX1:46, INTEGRA2:13
.= |.c.| * ||.x.|| by Th2 ;
hence ( ( ||.x.|| = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(c * x).|| = |.c.| * ||.x.|| ) by A6, A12, A9, A18, A17, Th2; ::_thesis: verum
end;
registration
cluster Complex_linfty_Space -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence
( Complex_linfty_Space is reflexive & Complex_linfty_Space is discerning & Complex_linfty_Space is ComplexNormSpace-like & Complex_linfty_Space is vector-distributive & Complex_linfty_Space is scalar-distributive & Complex_linfty_Space is scalar-associative & Complex_linfty_Space is scalar-unital & Complex_linfty_Space is Abelian & Complex_linfty_Space is add-associative & Complex_linfty_Space is right_zeroed & Complex_linfty_Space is right_complementable )
proof
thus Complex_linfty_Space is reflexive ::_thesis: ( Complex_linfty_Space is discerning & Complex_linfty_Space is ComplexNormSpace-like & Complex_linfty_Space is vector-distributive & Complex_linfty_Space is scalar-distributive & Complex_linfty_Space is scalar-associative & Complex_linfty_Space is scalar-unital & Complex_linfty_Space is Abelian & Complex_linfty_Space is add-associative & Complex_linfty_Space is right_zeroed & Complex_linfty_Space is right_complementable )
proof
thus ||.(0. Complex_linfty_Space).|| = 0 by Th3; :: according to NORMSP_0:def_6 ::_thesis: verum
end;
thus ( Complex_linfty_Space is discerning & Complex_linfty_Space is ComplexNormSpace-like & Complex_linfty_Space is vector-distributive & Complex_linfty_Space is scalar-distributive & Complex_linfty_Space is scalar-associative & Complex_linfty_Space is scalar-unital & Complex_linfty_Space is Abelian & Complex_linfty_Space is add-associative & Complex_linfty_Space is right_zeroed & Complex_linfty_Space is right_complementable ) by Th3, CLVECT_1:def_13, NORMSP_0:def_5; ::_thesis: verum
end;
end;
Lm11: for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
proof
let seq1, seq2, seq3 be Complex_Sequence; ::_thesis: ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
A1: ( ( for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 )
proof
assume A2: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: seq1 = seq2 - seq3
for x being set st x in NAT holds
seq1 . x = (seq2 - seq3) . x
proof
let x be set ; ::_thesis: ( x in NAT implies seq1 . x = (seq2 - seq3) . x )
assume x in NAT ; ::_thesis: seq1 . x = (seq2 - seq3) . x
then reconsider x = x as Element of NAT ;
seq1 . x = (seq2 . x) - (seq3 . x) by A2
.= (seq2 . x) + (- (seq3 . x))
.= (seq2 . x) + ((- seq3) . x) by VALUED_1:8
.= (seq2 + (- seq3)) . x by VALUED_1:1 ;
hence seq1 . x = (seq2 - seq3) . x ; ::_thesis: verum
end;
hence seq1 = seq2 - seq3 by FUNCT_2:12; ::_thesis: verum
end;
( seq1 = seq2 - seq3 implies for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) )
proof
assume A3: seq1 = seq2 - seq3 ; ::_thesis: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n)
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_._n)_-_(seq3_._n)
let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 . n) - (seq3 . n)
seq1 . n = (seq2 . n) + ((- seq3) . n) by A3, VALUED_1:1
.= (seq2 . n) + (- (seq3 . n)) by VALUED_1:8 ;
hence seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum
end;
hence for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum
end;
hence ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) by A1; ::_thesis: verum
end;
theorem Th4: :: CSSPACE4:4
for vseq being sequence of Complex_linfty_Space st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent
proof
let vseq be sequence of Complex_linfty_Space; ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
defpred S1[ set , set ] means ex i being Element of NAT st
( $1 = i & ex cseqi being Complex_Sequence st
( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & $2 = lim cseqi ) );
A2: for x being set st x in NAT holds
ex y being set st
( y in COMPLEX & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in COMPLEX & S1[x,y] ) )
assume x in NAT ; ::_thesis: ex y being set st
( y in COMPLEX & S1[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H1( Element of NAT ) -> Element of COMPLEX = (seq_id (vseq . $1)) . i;
consider cseqi being Complex_Sequence such that
A3: for n being Element of NAT holds cseqi . n = H1(n) from COMSEQ_1:sch_1();
take lim cseqi ; ::_thesis: ( lim cseqi in COMPLEX & S1[x, lim cseqi] )
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.((cseqi_._m)_-_(cseqi_._k)).|_<_e
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e )
assume A4: e > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e
thus ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e ::_thesis: verum
proof
consider k being Element of NAT such that
A5: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A4, CSSPACE3:8;
take k ; ::_thesis: for m being Element of NAT st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e
let m be Element of NAT ; ::_thesis: ( k <= m implies |.((cseqi . m) - (cseqi . k)).| < e )
assume A6: k <= m ; ::_thesis: |.((cseqi . m) - (cseqi . k)).| < e
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by CSSPACE:1 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by VALUED_1:1
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by VALUED_1:8
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (cseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (cseqi . m) - (cseqi . k) by A3 ;
then A7: |.((cseqi . m) - (cseqi . k)).| = |.(seq_id ((vseq . m) - (vseq . k))).| . i by VALUED_1:18;
seq_id ((vseq . m) - (vseq . k)) is bounded by Def1;
then |.(seq_id ((vseq . m) - (vseq . k))).| is bounded by Lm8;
then A8: |.(seq_id ((vseq . m) - (vseq . k))).| . i <= upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Lm2;
||.((vseq . m) - (vseq . k)).|| = upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Th2;
then upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) < e by A5, A6;
hence |.((cseqi . m) - (cseqi . k)).| < e by A8, A7, XXREAL_0:2; ::_thesis: verum
end;
end;
then cseqi is convergent by COMSEQ_3:46;
hence ( lim cseqi in COMPLEX & S1[x, lim cseqi] ) by A3; ::_thesis: verum
end;
consider f being Function of NAT,COMPLEX such that
A9: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
reconsider tseq = f as Complex_Sequence ;
A10: now__::_thesis:_for_i_being_Element_of_NAT_ex_cseqi_being_Complex_Sequence_st_
(_(_for_n_being_Element_of_NAT_holds_cseqi_._n_=_(seq_id_(vseq_._n))_._i_)_&_cseqi_is_convergent_&_tseq_._i_=_lim_cseqi_)
let i be Element of NAT ; ::_thesis: ex cseqi being Complex_Sequence st
( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & tseq . i = lim cseqi )
reconsider x = i as set ;
ex i0 being Element of NAT st
( x = i0 & ex cseqi being Complex_Sequence st
( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i0 ) & cseqi is convergent & f . x = lim cseqi ) ) by A9;
hence ex cseqi being Complex_Sequence st
( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & tseq . i = lim cseqi ) ; ::_thesis: verum
end;
A11: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) )
assume A12: e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
consider k being Element of NAT such that
A13: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A12, CSSPACE3:8;
A14: for m, n being Element of NAT st n >= k & m >= k holds
( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e )
proof
let m, n be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) )
assume ( n >= k & m >= k ) ; ::_thesis: ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e )
then ||.((vseq . n) - (vseq . m)).|| < e by A13;
then A15: the normF of Complex_linfty_Space . ((vseq . n) - (vseq . m)) < e ;
seq_id ((vseq . n) - (vseq . m)) is bounded by Def1;
hence ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) by A15, Def2, Lm8; ::_thesis: verum
end;
A16: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i )
proof
let n be Element of NAT ; ::_thesis: for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i )
A17: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
proof
let m, k be Element of NAT ; ::_thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by CSSPACE:1; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_
for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|_._i_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|_._i_)
let i be Element of NAT ; ::_thesis: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i )
consider cseqi being Complex_Sequence such that
A18: for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i and
A19: ( cseqi is convergent & tseq . i = lim cseqi ) by A10;
now__::_thesis:_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|_._i_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|_._i_)
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) implies ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) )
assume A20: for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ; ::_thesis: ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i )
A21: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_|.((cseqi_._m)_-_((seq_id_(vseq_._n))_._i)).|
let m be Element of NAT ; ::_thesis: rseq . m = |.((cseqi . m) - ((seq_id (vseq . n)) . i)).|
A22: seq_id ((vseq . m) - (vseq . n)) = (seq_id (vseq . m)) - (seq_id (vseq . n)) by A17;
thus rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i by A20
.= |.((seq_id ((vseq . m) - (vseq . n))) . i).| by VALUED_1:18
.= |.(((seq_id (vseq . m)) . i) - ((seq_id (vseq . n)) . i)).| by A22, Lm11
.= |.((cseqi . m) - ((seq_id (vseq . n)) . i)).| by A18 ; ::_thesis: verum
end;
|.((tseq . i) - ((seq_id (vseq . n)) . i)).| = |.((tseq - (seq_id (vseq . n))) . i).| by Lm11
.= |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| by CSSPACE:1
.= |.((seq_id tseq) - (seq_id (vseq . n))).| . i by VALUED_1:18 ;
hence ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) by A19, A21, CSSPACE3:1; ::_thesis: verum
end;
hence for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) ; ::_thesis: verum
end;
hence for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) ; ::_thesis: verum
end;
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
proof
let n be Element of NAT ; ::_thesis: ( n >= k implies ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) )
assume A23: n >= k ; ::_thesis: ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
A24: for i being Element of NAT holds |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e
proof
let i be Element of NAT ; ::_thesis: |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e
deffunc H1( Element of NAT ) -> Element of REAL = |.(seq_id ((vseq . $1) - (vseq . n))).| . i;
consider rseq being Real_Sequence such that
A25: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A26: for m being Element of NAT st m >= k holds
rseq . m <= e
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e )
A27: rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i by A25;
assume A28: m >= k ; ::_thesis: rseq . m <= e
then |.(seq_id ((vseq . m) - (vseq . n))).| is bounded by A14, A23;
then A29: |.(seq_id ((vseq . m) - (vseq . n))).| . i <= upper_bound (rng |.(seq_id ((vseq . m) - (vseq . n))).|) by Lm2;
upper_bound (rng |.(seq_id ((vseq . m) - (vseq . n))).|) <= e by A14, A23, A28;
hence rseq . m <= e by A29, A27, XXREAL_0:2; ::_thesis: verum
end;
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) by A16, A25;
hence |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e by A26, RSSPACE2:5; ::_thesis: verum
end;
A30: 0 + e < 1 + e by XREAL_1:8;
now__::_thesis:_for_i_being_Element_of_NAT_holds_|.(((seq_id_tseq)_-_(seq_id_(vseq_._n)))_._i).|_<_e_+_1
let i be Element of NAT ; ::_thesis: |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| < e + 1
|.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e by A24;
then |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| <= e by VALUED_1:18;
hence |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| < e + 1 by A30, XXREAL_0:2; ::_thesis: verum
end;
then (seq_id tseq) - (seq_id (vseq . n)) is bounded by A12, COMSEQ_2:8;
hence ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) by A24, Lm1, Lm8; ::_thesis: verum
end;
hence ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) ; ::_thesis: verum
end;
A31: seq_id tseq is bounded
proof
consider m being Element of NAT such that
A32: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= 1 ) by A11;
A33: |.((seq_id tseq) - (seq_id (vseq . m))).| is bounded by A32;
set d = |.(seq_id tseq).|;
set b = |.(seq_id (vseq . m)).|;
set a = |.((seq_id tseq) - (seq_id (vseq . m))).|;
seq_id (vseq . m) is bounded by Def1;
then A34: |.(seq_id (vseq . m)).| is bounded by Lm8;
A35: for i being Element of NAT holds |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i
proof
let i be Element of NAT ; ::_thesis: |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i
A36: ( |.(seq_id (vseq . m)).| . i = |.((seq_id (vseq . m)) . i).| & |.(seq_id tseq).| . i = |.((seq_id tseq) . i).| ) by VALUED_1:18;
|.((seq_id tseq) - (seq_id (vseq . m))).| . i = |.(((seq_id tseq) + (- (seq_id (vseq . m)))) . i).| by VALUED_1:18
.= |.(((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)).| by VALUED_1:1
.= |.(((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))).| by VALUED_1:8
.= |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ;
then (|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i) <= |.((seq_id tseq) - (seq_id (vseq . m))).| . i by A36, COMPLEX1:59;
then ((|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i)) + (|.(seq_id (vseq . m)).| . i) <= (|.((seq_id tseq) - (seq_id (vseq . m))).| . i) + (|.(seq_id (vseq . m)).| . i) by XREAL_1:6;
hence |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i by SEQ_1:7; ::_thesis: verum
end;
|.(seq_id tseq).| is bounded
proof
reconsider r = (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 as real number ;
|.(seq_id (vseq . m)).| . 1 = |.((seq_id (vseq . m)) . 1).| by VALUED_1:18;
then A37: 0 <= |.(seq_id (vseq . m)).| . 1 by COMPLEX1:46;
A38: (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 0 < (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 by XREAL_1:8;
A39: now__::_thesis:_for_i_being_Element_of_NAT_holds_|.((seq_id_tseq)_._i).|_<_r
let i be Element of NAT ; ::_thesis: |.((seq_id tseq) . i).| < r
( |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i & (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) ) by A33, A34, A35, Lm2;
then A40: |.(seq_id tseq).| . i <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by XXREAL_0:2;
|.(seq_id tseq).| . i = |.((seq_id tseq) . i).| by VALUED_1:18;
hence |.((seq_id tseq) . i).| < r by A38, A40, XXREAL_0:2; ::_thesis: verum
end;
|.((seq_id tseq) - (seq_id (vseq . m))).| . 1 = |.(((seq_id tseq) - (seq_id (vseq . m))) . 1).| by VALUED_1:18;
then ( (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . 1 = (|.((seq_id tseq) - (seq_id (vseq . m))).| . 1) + (|.(seq_id (vseq . m)).| . 1) & 0 <= |.((seq_id tseq) - (seq_id (vseq . m))).| . 1 ) by COMPLEX1:46, SEQ_1:7;
then 0 <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by A33, A34, A37, Lm2;
then seq_id tseq is bounded by A39, COMSEQ_2:8;
hence |.(seq_id tseq).| is bounded by Lm8; ::_thesis: verum
end;
hence seq_id tseq is bounded by Lm9; ::_thesis: verum
end;
A41: tseq in the_set_of_ComplexSequences by CSSPACE:def_1;
then reconsider tv = tseq as Point of Complex_linfty_Space by A31, Def1;
ex tv being Point of Complex_linfty_Space st
for e1 being Real st e1 > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1
proof
take tv ; ::_thesis: for e1 being Real st e1 > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1
let e1 be Real; ::_thesis: ( e1 > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1 )
assume A42: e1 > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1
set e = e1 / 2;
consider m being Element of NAT such that
A43: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 ) by A11, A42;
A44: e1 / 2 < e1 by A42, XREAL_1:216;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e1
reconsider u = tseq as VECTOR of Complex_linfty_Space by A31, A41, Def1;
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e1 )
assume n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e1
then A45: upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 by A43;
reconsider v = vseq . n as VECTOR of Complex_linfty_Space ;
seq_id (u - v) = u - v by Th2;
then upper_bound (rng |.(seq_id (u - v)).|) = upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) by Th2;
then A46: the normF of Complex_linfty_Space . (u - v) <= e1 / 2 by A45, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by CLVECT_1:103 ;
then ||.((vseq . n) - tv).|| <= e1 / 2 by A46;
hence ||.((vseq . n) - tv).|| < e1 by A44, XXREAL_0:2; ::_thesis: verum
end;
hence ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1 ; ::_thesis: verum
end;
hence vseq is convergent by CLVECT_1:def_15; ::_thesis: verum
end;
theorem :: CSSPACE4:5
Complex_linfty_Space is ComplexBanachSpace by Th4, CLOPBAN1:def_13;
begin
definition
let X be non empty set ;
let Y be ComplexNormSpace;
let IT be Function of X, the carrier of Y;
attrIT is bounded means :Def4: :: CSSPACE4:def 4
ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) );
end;
:: deftheorem Def4 defines bounded CSSPACE4:def_4_:_
for X being non empty set
for Y being ComplexNormSpace
for IT being Function of X, the carrier of Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) ) );
theorem Th6: :: CSSPACE4:6
for X being non empty set
for Y being ComplexNormSpace
for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
let Y be ComplexNormSpace; ::_thesis: for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
let f be Function of X, the carrier of Y; ::_thesis: ( ( for x being Element of X holds f . x = 0. Y ) implies f is bounded )
assume A1: for x being Element of X holds f . x = 0. Y ; ::_thesis: f is bounded
A2: now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_=_0
let x be Element of X; ::_thesis: ||.(f . x).|| = 0
thus ||.(f . x).|| = ||.(0. Y).|| by A1
.= 0 ; ::_thesis: verum
end;
take 0 ; :: according to CSSPACE4:def_4 ::_thesis: ( 0 <= 0 & ( for x being Element of X holds ||.(f . x).|| <= 0 ) )
thus ( 0 <= 0 & ( for x being Element of X holds ||.(f . x).|| <= 0 ) ) by A2; ::_thesis: verum
end;
registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster non empty Relation-like X -defined the carrier of Y -valued Function-like V23(X) quasi_total bounded for Element of bool [:X, the carrier of Y:];
existence
ex b1 being Function of X, the carrier of Y st b1 is bounded
proof
set f = X --> (0. Y);
reconsider f = X --> (0. Y) as Function of X, the carrier of Y ;
take f ; ::_thesis: f is bounded
for x being Element of X holds f . x = 0. Y by FUNCOP_1:7;
hence f is bounded by Th6; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let Y be ComplexNormSpace;
func ComplexBoundedFunctions (X,Y) -> Subset of (ComplexVectSpace (X,Y)) means :Def5: :: CSSPACE4:def 5
for x being set holds
( x in it iff x is bounded Function of X, the carrier of Y );
existence
ex b1 being Subset of (ComplexVectSpace (X,Y)) st
for x being set holds
( x in b1 iff x is bounded Function of X, the carrier of Y )
proof
defpred S1[ set ] means $1 is bounded Function of X, the carrier of Y;
consider IT being set such that
A1: for x being set holds
( x in IT iff ( x in Funcs (X, the carrier of Y) & S1[x] ) ) from XBOOLE_0:sch_1();
take IT ; ::_thesis: ( IT is Subset of (ComplexVectSpace (X,Y)) & ( for x being set holds
( x in IT iff x is bounded Function of X, the carrier of Y ) ) )
for x being set st x in IT holds
x in Funcs (X, the carrier of Y) by A1;
hence IT is Subset of (ComplexVectSpace (X,Y)) by TARSKI:def_3; ::_thesis: for x being set holds
( x in IT iff x is bounded Function of X, the carrier of Y )
let x be set ; ::_thesis: ( x in IT iff x is bounded Function of X, the carrier of Y )
thus ( x in IT implies x is bounded Function of X, the carrier of Y ) by A1; ::_thesis: ( x is bounded Function of X, the carrier of Y implies x in IT )
assume A2: x is bounded Function of X, the carrier of Y ; ::_thesis: x in IT
then x in Funcs (X, the carrier of Y) by FUNCT_2:8;
hence x in IT by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (ComplexVectSpace (X,Y)) st ( for x being set holds
( x in b1 iff x is bounded Function of X, the carrier of Y ) ) & ( for x being set holds
( x in b2 iff x is bounded Function of X, the carrier of Y ) ) holds
b1 = b2
proof
let X1, X2 be Subset of (ComplexVectSpace (X,Y)); ::_thesis: ( ( for x being set holds
( x in X1 iff x is bounded Function of X, the carrier of Y ) ) & ( for x being set holds
( x in X2 iff x is bounded Function of X, the carrier of Y ) ) implies X1 = X2 )
assume that
A3: for x being set holds
( x in X1 iff x is bounded Function of X, the carrier of Y ) and
A4: for x being set holds
( x in X2 iff x is bounded Function of X, the carrier of Y ) ; ::_thesis: X1 = X2
for x being set st x in X2 holds
x in X1
proof
let x be set ; ::_thesis: ( x in X2 implies x in X1 )
assume x in X2 ; ::_thesis: x in X1
then x is bounded Function of X, the carrier of Y by A4;
hence x in X1 by A3; ::_thesis: verum
end;
then A5: X2 c= X1 by TARSKI:def_3;
for x being set st x in X1 holds
x in X2
proof
let x be set ; ::_thesis: ( x in X1 implies x in X2 )
assume x in X1 ; ::_thesis: x in X2
then x is bounded Function of X, the carrier of Y by A3;
hence x in X2 by A4; ::_thesis: verum
end;
then X1 c= X2 by TARSKI:def_3;
hence X1 = X2 by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines ComplexBoundedFunctions CSSPACE4:def_5_:_
for X being non empty set
for Y being ComplexNormSpace
for b3 being Subset of (ComplexVectSpace (X,Y)) holds
( b3 = ComplexBoundedFunctions (X,Y) iff for x being set holds
( x in b3 iff x is bounded Function of X, the carrier of Y ) );
registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster ComplexBoundedFunctions (X,Y) -> non empty ;
coherence
not ComplexBoundedFunctions (X,Y) is empty
proof
set f = X --> (0. Y);
reconsider f = X --> (0. Y) as Function of X, the carrier of Y ;
for x being Element of X holds f . x = 0. Y by FUNCOP_1:7;
then f is bounded by Th6;
hence not ComplexBoundedFunctions (X,Y) is empty by Def5; ::_thesis: verum
end;
end;
theorem Th7: :: CSSPACE4:7
for X being non empty set
for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed
let Y be ComplexNormSpace; ::_thesis: ComplexBoundedFunctions (X,Y) is linearly-closed
set W = ComplexBoundedFunctions (X,Y);
A1: for v, u being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) & u in ComplexBoundedFunctions (X,Y) holds
v + u in ComplexBoundedFunctions (X,Y)
proof
let v, u be VECTOR of (ComplexVectSpace (X,Y)); ::_thesis: ( v in ComplexBoundedFunctions (X,Y) & u in ComplexBoundedFunctions (X,Y) implies v + u in ComplexBoundedFunctions (X,Y) )
assume that
A2: v in ComplexBoundedFunctions (X,Y) and
A3: u in ComplexBoundedFunctions (X,Y) ; ::_thesis: v + u in ComplexBoundedFunctions (X,Y)
reconsider f = v + u as Function of X, the carrier of Y by FUNCT_2:66;
f is bounded
proof
reconsider v1 = v as bounded Function of X, the carrier of Y by A2, Def5;
consider K2 being Real such that
A4: 0 <= K2 and
A5: for x being Element of X holds ||.(v1 . x).|| <= K2 by Def4;
reconsider u1 = u as bounded Function of X, the carrier of Y by A3, Def5;
consider K1 being Real such that
A6: 0 <= K1 and
A7: for x being Element of X holds ||.(u1 . x).|| <= K1 by Def4;
take K3 = K1 + K2; :: according to CSSPACE4:def_4 ::_thesis: ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) )
now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_<=_K3
let x be Element of X; ::_thesis: ||.(f . x).|| <= K3
( ||.(u1 . x).|| <= K1 & ||.(v1 . x).|| <= K2 ) by A7, A5;
then A8: ||.(u1 . x).|| + ||.(v1 . x).|| <= K1 + K2 by XREAL_1:7;
( ||.(f . x).|| = ||.((v1 . x) + (u1 . x)).|| & ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| ) by CLOPBAN1:11, CLVECT_1:def_13;
hence ||.(f . x).|| <= K3 by A8, XXREAL_0:2; ::_thesis: verum
end;
hence ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) by A6, A4; ::_thesis: verum
end;
hence v + u in ComplexBoundedFunctions (X,Y) by Def5; ::_thesis: verum
end;
for c being Complex
for v being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) holds
c * v in ComplexBoundedFunctions (X,Y)
proof
let c be Complex; ::_thesis: for v being VECTOR of (ComplexVectSpace (X,Y)) st v in ComplexBoundedFunctions (X,Y) holds
c * v in ComplexBoundedFunctions (X,Y)
let v be VECTOR of (ComplexVectSpace (X,Y)); ::_thesis: ( v in ComplexBoundedFunctions (X,Y) implies c * v in ComplexBoundedFunctions (X,Y) )
assume A9: v in ComplexBoundedFunctions (X,Y) ; ::_thesis: c * v in ComplexBoundedFunctions (X,Y)
reconsider f = c * v as Function of X, the carrier of Y by FUNCT_2:66;
f is bounded
proof
reconsider v1 = v as bounded Function of X, the carrier of Y by A9, Def5;
consider K being Real such that
A10: 0 <= K and
A11: for x being Element of X holds ||.(v1 . x).|| <= K by Def4;
take |.c.| * K ; :: according to CSSPACE4:def_4 ::_thesis: ( 0 <= |.c.| * K & ( for x being Element of X holds ||.(f . x).|| <= |.c.| * K ) )
A12: now__::_thesis:_for_x_being_Element_of_X_holds_||.(f_._x).||_<=_|.c.|_*_K
let x be Element of X; ::_thesis: ||.(f . x).|| <= |.c.| * K
A13: 0 <= |.c.| by COMPLEX1:46;
( ||.(f . x).|| = ||.(c * (v1 . x)).|| & ||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| ) by CLOPBAN1:12, CLVECT_1:def_13;
hence ||.(f . x).|| <= |.c.| * K by A11, A13, XREAL_1:64; ::_thesis: verum
end;
0 <= |.c.| by COMPLEX1:46;
hence ( 0 <= |.c.| * K & ( for x being Element of X holds ||.(f . x).|| <= |.c.| * K ) ) by A10, A12; ::_thesis: verum
end;
hence c * v in ComplexBoundedFunctions (X,Y) by Def5; ::_thesis: verum
end;
hence ComplexBoundedFunctions (X,Y) is linearly-closed by A1, CLVECT_1:def_7; ::_thesis: verum
end;
theorem :: CSSPACE4:8
for X being non empty set
for Y being ComplexNormSpace holds CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is Subspace of ComplexVectSpace (X,Y) by Th7, CSSPACE:11;
registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is Abelian & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is add-associative & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is right_zeroed & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is right_complementable & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is vector-distributive & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-distributive & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-associative & CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is scalar-unital ) by Th7, CSSPACE:11;
end;
definition
let X be non empty set ;
let Y be ComplexNormSpace;
func C_VectorSpace_of_BoundedFunctions (X,Y) -> ComplexLinearSpace equals :: CSSPACE4:def 6
CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #);
coherence
CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is ComplexLinearSpace ;
end;
:: deftheorem defines C_VectorSpace_of_BoundedFunctions CSSPACE4:def_6_:_
for X being non empty set
for Y being ComplexNormSpace holds C_VectorSpace_of_BoundedFunctions (X,Y) = CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #);
registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster C_VectorSpace_of_BoundedFunctions (X,Y) -> strict ;
coherence
C_VectorSpace_of_BoundedFunctions (X,Y) is strict ;
end;
theorem Th9: :: CSSPACE4:9
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f, g, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
let Y be ComplexNormSpace; ::_thesis: for f, g, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
let f, g, h be VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
A1: C_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of ComplexVectSpace (X,Y) by Th7, CSSPACE:11;
then reconsider f1 = f as VECTOR of (ComplexVectSpace (X,Y)) by CLVECT_1:29;
reconsider h1 = h as VECTOR of (ComplexVectSpace (X,Y)) by A1, CLVECT_1:29;
reconsider g1 = g as VECTOR of (ComplexVectSpace (X,Y)) by A1, CLVECT_1:29;
let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) )
assume A2: ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
A3: now__::_thesis:_(_h_=_f_+_g_implies_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_+_(g9_._x)_)
assume A4: h = f + g ; ::_thesis: for x being Element of X holds h9 . x = (f9 . x) + (g9 . x)
let x be Element of X; ::_thesis: h9 . x = (f9 . x) + (g9 . x)
h1 = f1 + g1 by A1, A4, CLVECT_1:32;
hence h9 . x = (f9 . x) + (g9 . x) by A2, CLOPBAN1:11; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_+_(g9_._x)_)_implies_h_=_f_+_g_)
assume for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ; ::_thesis: h = f + g
then h1 = f1 + g1 by A2, CLOPBAN1:11;
hence h = f + g by A1, CLVECT_1:32; ::_thesis: verum
end;
hence ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) by A3; ::_thesis: verum
end;
theorem Th10: :: CSSPACE4:10
for X being non empty set
for Y being ComplexNormSpace
for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
let Y be ComplexNormSpace; ::_thesis: for f, h being VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
let f, h be VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
let f9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & h9 = h implies for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) )
assume A1: ( f9 = f & h9 = h ) ; ::_thesis: for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
let c be Complex; ::_thesis: ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
A2: C_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of ComplexVectSpace (X,Y) by Th7, CSSPACE:11;
then reconsider f1 = f, h1 = h as VECTOR of (ComplexVectSpace (X,Y)) by CLVECT_1:29;
A3: now__::_thesis:_(_h_=_c_*_f_implies_for_x_being_Element_of_X_holds_h9_._x_=_c_*_(f9_._x)_)
assume A4: h = c * f ; ::_thesis: for x being Element of X holds h9 . x = c * (f9 . x)
let x be Element of X; ::_thesis: h9 . x = c * (f9 . x)
h1 = c * f1 by A2, A4, CLVECT_1:33;
hence h9 . x = c * (f9 . x) by A1, CLOPBAN1:12; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_c_*_(f9_._x)_)_implies_h_=_c_*_f_)
assume for x being Element of X holds h9 . x = c * (f9 . x) ; ::_thesis: h = c * f
then h1 = c * f1 by A1, CLOPBAN1:12;
hence h = c * f by A2, CLVECT_1:33; ::_thesis: verum
end;
hence ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) by A3; ::_thesis: verum
end;
theorem Th11: :: CSSPACE4:11
for X being non empty set
for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
let Y be ComplexNormSpace; ::_thesis: 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y)
( C_VectorSpace_of_BoundedFunctions (X,Y) is Subspace of ComplexVectSpace (X,Y) & 0. (ComplexVectSpace (X,Y)) = X --> (0. Y) ) by Th7, CSSPACE:11, LOPBAN_1:def_3;
hence 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = X --> (0. Y) by CLVECT_1:30; ::_thesis: verum
end;
definition
let X be non empty set ;
let Y be ComplexNormSpace;
let f be set ;
assume A1: f in ComplexBoundedFunctions (X,Y) ;
func modetrans (f,X,Y) -> bounded Function of X, the carrier of Y equals :Def7: :: CSSPACE4:def 7
f;
coherence
f is bounded Function of X, the carrier of Y by A1, Def5;
end;
:: deftheorem Def7 defines modetrans CSSPACE4:def_7_:_
for X being non empty set
for Y being ComplexNormSpace
for f being set st f in ComplexBoundedFunctions (X,Y) holds
modetrans (f,X,Y) = f;
definition
let X be non empty set ;
let Y be ComplexNormSpace;
let u be Function of X, the carrier of Y;
func PreNorms u -> non empty Subset of REAL equals :: CSSPACE4:def 8
{ ||.(u . t).|| where t is Element of X : verum } ;
coherence
{ ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL
proof
set x = the Element of X;
A1: now__::_thesis:_for_x_being_set_st_x_in__{__||.(u_._t).||_where_t_is_Element_of_X_:_verum__}__holds_
x_in_REAL
let x be set ; ::_thesis: ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL )
now__::_thesis:_(_x_in__{__||.(u_._t).||_where_t_is_Element_of_X_:_verum__}__implies_x_in_REAL_)
assume x in { ||.(u . t).|| where t is Element of X : verum } ; ::_thesis: x in REAL
then ex t being Element of X st x = ||.(u . t).|| ;
hence x in REAL ; ::_thesis: verum
end;
hence ( x in { ||.(u . t).|| where t is Element of X : verum } implies x in REAL ) ; ::_thesis: verum
end;
||.(u . the Element of X).|| in { ||.(u . t).|| where t is Element of X : verum } ;
hence { ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL by A1, TARSKI:def_3; ::_thesis: verum
end;
end;
:: deftheorem defines PreNorms CSSPACE4:def_8_:_
for X being non empty set
for Y being ComplexNormSpace
for u being Function of X, the carrier of Y holds PreNorms u = { ||.(u . t).|| where t is Element of X : verum } ;
theorem Th12: :: CSSPACE4:12
for X being non empty set
for Y being ComplexNormSpace
for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
let Y be ComplexNormSpace; ::_thesis: for g being bounded Function of X, the carrier of Y holds PreNorms g is bounded_above
let g be bounded Function of X, the carrier of Y; ::_thesis: PreNorms g is bounded_above
consider K being Real such that
0 <= K and
A1: for x being Element of X holds ||.(g . x).|| <= K by Def4;
take K ; :: according to XXREAL_2:def_10 ::_thesis: K is UpperBound of PreNorms g
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in PreNorms g or r <= K )
assume r in PreNorms g ; ::_thesis: r <= K
then ex t being Element of X st r = ||.(g . t).|| ;
hence r <= K by A1; ::_thesis: verum
end;
theorem :: CSSPACE4:13
for X being non empty set
for Y being ComplexNormSpace
for g being Function of X, the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for g being Function of X, the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
let Y be ComplexNormSpace; ::_thesis: for g being Function of X, the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )
let g be Function of X, the carrier of Y; ::_thesis: ( g is bounded iff PreNorms g is bounded_above )
now__::_thesis:_(_PreNorms_g_is_bounded_above_implies_ex_K_being_Real_st_g_is_bounded_)
reconsider K = upper_bound (PreNorms g) as Real ;
assume A1: PreNorms g is bounded_above ; ::_thesis: ex K being Real st g is bounded
A2: 0 <= K
proof
consider r0 being set such that
A3: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A3;
now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
0_<=_r
let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r )
assume r in PreNorms g ; ::_thesis: 0 <= r
then ex t being Element of X st r = ||.(g . t).|| ;
hence 0 <= r by CLVECT_1:105; ::_thesis: verum
end;
then 0 <= r0 by A3;
hence 0 <= K by A1, A3, SEQ_4:def_1; ::_thesis: verum
end;
take K = K; ::_thesis: g is bounded
now__::_thesis:_for_t_being_Element_of_X_holds_||.(g_._t).||_<=_K
let t be Element of X; ::_thesis: ||.(g . t).|| <= K
||.(g . t).|| in PreNorms g ;
hence ||.(g . t).|| <= K by A1, SEQ_4:def_1; ::_thesis: verum
end;
hence g is bounded by A2, Def4; ::_thesis: verum
end;
hence ( g is bounded iff PreNorms g is bounded_above ) by Th12; ::_thesis: verum
end;
definition
let X be non empty set ;
let Y be ComplexNormSpace;
func ComplexBoundedFunctionsNorm (X,Y) -> Function of (ComplexBoundedFunctions (X,Y)),REAL means :Def9: :: CSSPACE4:def 9
for x being set st x in ComplexBoundedFunctions (X,Y) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y)));
existence
ex b1 being Function of (ComplexBoundedFunctions (X,Y)),REAL st
for x being set st x in ComplexBoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
proof
deffunc H1( set ) -> Element of REAL = upper_bound (PreNorms (modetrans ($1,X,Y)));
A1: for z being set st z in ComplexBoundedFunctions (X,Y) holds
H1(z) in REAL ;
ex f being Function of (ComplexBoundedFunctions (X,Y)),REAL st
for x being set st x in ComplexBoundedFunctions (X,Y) holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence ex b1 being Function of (ComplexBoundedFunctions (X,Y)),REAL st
for x being set st x in ComplexBoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (ComplexBoundedFunctions (X,Y)),REAL st ( for x being set st x in ComplexBoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in ComplexBoundedFunctions (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of (ComplexBoundedFunctions (X,Y)),REAL; ::_thesis: ( ( for x being set st x in ComplexBoundedFunctions (X,Y) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in ComplexBoundedFunctions (X,Y) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in ComplexBoundedFunctions (X,Y) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) and
A3: for x being set st x in ComplexBoundedFunctions (X,Y) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in ComplexBoundedFunctions (X,Y) holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in ComplexBoundedFunctions (X,Y) implies NORM1 . z = NORM2 . z )
assume A5: z in ComplexBoundedFunctions (X,Y) ; ::_thesis: NORM1 . z = NORM2 . z
NORM1 . z = upper_bound (PreNorms (modetrans (z,X,Y))) by A2, A5;
hence NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
( dom NORM1 = ComplexBoundedFunctions (X,Y) & dom NORM2 = ComplexBoundedFunctions (X,Y) ) by FUNCT_2:def_1;
hence NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CSSPACE4:def_9_:_
for X being non empty set
for Y being ComplexNormSpace
for b3 being Function of (ComplexBoundedFunctions (X,Y)),REAL holds
( b3 = ComplexBoundedFunctionsNorm (X,Y) iff for x being set st x in ComplexBoundedFunctions (X,Y) holds
b3 . x = upper_bound (PreNorms (modetrans (x,X,Y))) );
theorem Th14: :: CSSPACE4:14
for X being non empty set
for Y being ComplexNormSpace
for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
let Y be ComplexNormSpace; ::_thesis: for f being bounded Function of X, the carrier of Y holds modetrans (f,X,Y) = f
let f be bounded Function of X, the carrier of Y; ::_thesis: modetrans (f,X,Y) = f
f in ComplexBoundedFunctions (X,Y) by Def5;
hence modetrans (f,X,Y) = f by Def7; ::_thesis: verum
end;
theorem Th15: :: CSSPACE4:15
for X being non empty set
for Y being ComplexNormSpace
for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
let Y be ComplexNormSpace; ::_thesis: for f being bounded Function of X, the carrier of Y holds (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
let f be bounded Function of X, the carrier of Y; ::_thesis: (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)
reconsider f9 = f as set ;
f in ComplexBoundedFunctions (X,Y) by Def5;
hence (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def9
.= upper_bound (PreNorms f) by Th14 ;
::_thesis: verum
end;
definition
let X be non empty set ;
let Y be ComplexNormSpace;
func C_NormSpace_of_BoundedFunctions (X,Y) -> non empty CNORMSTR equals :: CSSPACE4:def 10
CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #);
coherence
CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #) is non empty CNORMSTR ;
end;
:: deftheorem defines C_NormSpace_of_BoundedFunctions CSSPACE4:def_10_:_
for X being non empty set
for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) = CNORMSTR(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(ComplexBoundedFunctionsNorm (X,Y)) #);
theorem Th16: :: CSSPACE4:16
for X being non empty set
for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y))
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y))
let Y be ComplexNormSpace; ::_thesis: X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y))
X --> (0. Y) = 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) by Th11
.= 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ;
hence X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: verum
end;
theorem Th17: :: CSSPACE4:17
for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let Y be ComplexNormSpace; ::_thesis: for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let f be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let g be bounded Function of X, the carrier of Y; ::_thesis: ( g = f implies for t being Element of X holds ||.(g . t).|| <= ||.f.|| )
assume A1: g = f ; ::_thesis: for t being Element of X holds ||.(g . t).|| <= ||.f.||
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th12;
now__::_thesis:_for_t_being_Element_of_X_holds_||.(g_._t).||_<=_||.f.||
let t be Element of X; ::_thesis: ||.(g . t).|| <= ||.f.||
||.(g . t).|| in PreNorms g ;
then ||.(g . t).|| <= upper_bound (PreNorms g) by A2, SEQ_4:def_1;
then ||.(g . t).|| <= (ComplexBoundedFunctionsNorm (X,Y)) . g by Th15;
hence ||.(g . t).|| <= ||.f.|| by A1; ::_thesis: verum
end;
hence for t being Element of X holds ||.(g . t).|| <= ||.f.|| ; ::_thesis: verum
end;
theorem :: CSSPACE4:18
for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||
let Y be ComplexNormSpace; ::_thesis: for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||
let f be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: 0 <= ||.f.||
reconsider g = f as bounded Function of X, the carrier of Y by Def5;
consider r0 being set such that
A1: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A1;
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th12;
A3: (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms g) by Th15;
now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
0_<=_r
let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r )
assume r in PreNorms g ; ::_thesis: 0 <= r
then ex t being Element of X st r = ||.(g . t).|| ;
hence 0 <= r by CLVECT_1:105; ::_thesis: verum
end;
then 0 <= r0 by A1;
then 0 <= upper_bound (PreNorms g) by A2, A1, SEQ_4:def_1;
hence 0 <= ||.f.|| by A3; ::_thesis: verum
end;
theorem Th19: :: CSSPACE4:19
for X being non empty set
for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) holds
0 = ||.f.||
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) holds
0 = ||.f.||
let Y be ComplexNormSpace; ::_thesis: for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) st f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) holds
0 = ||.f.||
let f be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies 0 = ||.f.|| )
assume A1: f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: 0 = ||.f.||
thus ||.f.|| = 0 ::_thesis: verum
proof
reconsider g = f as bounded Function of X, the carrier of Y by Def5;
set z = X --> (0. Y);
reconsider z = X --> (0. Y) as Function of X, the carrier of Y ;
consider r0 being set such that
A2: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A2;
A3: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th12;
A5: z = g by A1, Th16;
A6: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A7: r = ||.(g . t).|| ;
||.(g . t).|| = ||.(0. Y).|| by A5, FUNCOP_1:7
.= 0 ;
hence ( 0 <= r & r <= 0 ) by A7; ::_thesis: verum
end;
then 0 <= r0 by A2;
then upper_bound (PreNorms g) = 0 by A6, A4, A2, A3, SEQ_4:def_1;
then (ComplexBoundedFunctionsNorm (X,Y)) . f = 0 by Th15;
hence ||.f.|| = 0 ; ::_thesis: verum
end;
end;
theorem Th20: :: CSSPACE4:20
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
let Y be ComplexNormSpace; ::_thesis: for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
let f, g, h be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
reconsider f1 = f, g1 = g, h1 = h as VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) ;
A1: ( h = f + g iff h1 = f1 + g1 ) ;
let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) )
assume ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) )
hence ( h = f + g iff for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ) by A1, Th9; ::_thesis: verum
end;
theorem Th21: :: CSSPACE4:21
for X being non empty set
for Y being ComplexNormSpace
for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
let Y be ComplexNormSpace; ::_thesis: for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
let f, h be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
let f9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & h9 = h implies for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) )
assume A1: ( f9 = f & h9 = h ) ; ::_thesis: for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
reconsider h1 = h as VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) ;
reconsider f1 = f as VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) ;
let c be Complex; ::_thesis: ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )
A2: now__::_thesis:_(_h1_=_c_*_f1_implies_h_=_c_*_f_)
assume h1 = c * f1 ; ::_thesis: h = c * f
hence h = (Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) . [c,f1] by CLVECT_1:def_1
.= c * f by CLVECT_1:def_1 ;
::_thesis: verum
end;
now__::_thesis:_(_h_=_c_*_f_implies_h1_=_c_*_f1_)
assume h = c * f ; ::_thesis: h1 = c * f1
hence h1 = (Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) . [c,f] by CLVECT_1:def_1
.= c * f1 by CLVECT_1:def_1 ;
::_thesis: verum
end;
hence ( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) ) by A1, A2, Th10; ::_thesis: verum
end;
theorem Th22: :: CSSPACE4:22
for X being non empty set
for Y being ComplexNormSpace
for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let Y be ComplexNormSpace; ::_thesis: for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let f, g be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let c be Complex; ::_thesis: ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
A1: now__::_thesis:_(_f_=_0._(C_NormSpace_of_BoundedFunctions_(X,Y))_implies_||.f.||_=_0_)
assume A2: f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ; ::_thesis: ||.f.|| = 0
thus ||.f.|| = 0 ::_thesis: verum
proof
reconsider g = f as bounded Function of X, the carrier of Y by Def5;
set z = X --> (0. Y);
reconsider z = X --> (0. Y) as Function of X, the carrier of Y ;
consider r0 being set such that
A3: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A3;
A4: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
A5: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th12;
A6: z = g by A2, Th16;
A7: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being Element of X such that
A8: r = ||.(g . t).|| ;
||.(g . t).|| = ||.(0. Y).|| by A6, FUNCOP_1:7
.= 0 ;
hence ( 0 <= r & r <= 0 ) by A8; ::_thesis: verum
end;
then 0 <= r0 by A3;
then upper_bound (PreNorms g) = 0 by A7, A5, A3, A4, SEQ_4:def_1;
then (ComplexBoundedFunctionsNorm (X,Y)) . f = 0 by Th15;
hence ||.f.|| = 0 ; ::_thesis: verum
end;
end;
A9: ||.(f + g).|| <= ||.f.|| + ||.g.||
proof
reconsider f1 = f, g1 = g, h1 = f + g as bounded Function of X, the carrier of Y by Def5;
A10: ( ( for s being real number st s in PreNorms h1 holds
s <= ||.f.|| + ||.g.|| ) implies upper_bound (PreNorms h1) <= ||.f.|| + ||.g.|| ) by SEQ_4:45;
A11: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_||.f.||_+_||.g.||
let t be Element of X; ::_thesis: ||.(h1 . t).|| <= ||.f.|| + ||.g.||
( ||.(f1 . t).|| <= ||.f.|| & ||.(g1 . t).|| <= ||.g.|| ) by Th17;
then A12: ||.(f1 . t).|| + ||.(g1 . t).|| <= ||.f.|| + ||.g.|| by XREAL_1:7;
( ||.(h1 . t).|| = ||.((f1 . t) + (g1 . t)).|| & ||.((f1 . t) + (g1 . t)).|| <= ||.(f1 . t).|| + ||.(g1 . t).|| ) by Th20, CLVECT_1:def_13;
hence ||.(h1 . t).|| <= ||.f.|| + ||.g.|| by A12, XXREAL_0:2; ::_thesis: verum
end;
A13: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_||.f.||_+_||.g.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= ||.f.|| + ||.g.|| )
assume r in PreNorms h1 ; ::_thesis: r <= ||.f.|| + ||.g.||
then ex t being Element of X st r = ||.(h1 . t).|| ;
hence r <= ||.f.|| + ||.g.|| by A11; ::_thesis: verum
end;
(ComplexBoundedFunctionsNorm (X,Y)) . (f + g) = upper_bound (PreNorms h1) by Th15;
hence ||.(f + g).|| <= ||.f.|| + ||.g.|| by A13, A10; ::_thesis: verum
end;
A14: ||.(c * f).|| = |.c.| * ||.f.||
proof
reconsider f1 = f, h1 = c * f as bounded Function of X, the carrier of Y by Def5;
A15: ( ( for s being real number st s in PreNorms h1 holds
s <= |.c.| * ||.f.|| ) implies upper_bound (PreNorms h1) <= |.c.| * ||.f.|| ) by SEQ_4:45;
A16: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_|.c.|_*_||.f.||
let t be Element of X; ::_thesis: ||.(h1 . t).|| <= |.c.| * ||.f.||
A17: 0 <= |.c.| by COMPLEX1:46;
( ||.(h1 . t).|| = ||.(c * (f1 . t)).|| & ||.(c * (f1 . t)).|| = |.c.| * ||.(f1 . t).|| ) by Th21, CLVECT_1:def_13;
hence ||.(h1 . t).|| <= |.c.| * ||.f.|| by A17, Th17, XREAL_1:64; ::_thesis: verum
end;
A18: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_|.c.|_*_||.f.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= |.c.| * ||.f.|| )
assume r in PreNorms h1 ; ::_thesis: r <= |.c.| * ||.f.||
then ex t being Element of X st r = ||.(h1 . t).|| ;
hence r <= |.c.| * ||.f.|| by A16; ::_thesis: verum
end;
A19: now__::_thesis:_(_(_c_<>_0c_&_|.c.|_*_||.f.||_<=_||.(c_*_f).||_)_or_(_c_=_0c_&_||.(c_*_f).||_=_|.c.|_*_||.f.||_)_)
percases ( c <> 0c or c = 0c ) ;
caseA20: c <> 0c ; ::_thesis: |.c.| * ||.f.|| <= ||.(c * f).||
A21: now__::_thesis:_for_t_being_Element_of_X_holds_||.(f1_._t).||_<=_(|.c.|_")_*_||.(c_*_f).||
let t be Element of X; ::_thesis: ||.(f1 . t).|| <= (|.c.| ") * ||.(c * f).||
A22: |.(c ").| = |.(1r / c).| by COMPLEX1:def_4, XCMPLX_1:215
.= 1 / |.c.| by COMPLEX1:48, COMPLEX1:67
.= 1 * (|.c.| ") by XCMPLX_0:def_9
.= |.c.| " ;
h1 . t = c * (f1 . t) by Th21;
then A23: (c ") * (h1 . t) = ((c ") * c) * (f1 . t) by CLVECT_1:def_4
.= 1r * (f1 . t) by A20, COMPLEX1:def_4, XCMPLX_0:def_7
.= f1 . t by CLVECT_1:def_5 ;
( ||.((c ") * (h1 . t)).|| = |.(c ").| * ||.(h1 . t).|| & 0 <= |.(c ").| ) by CLVECT_1:def_13, COMPLEX1:46;
hence ||.(f1 . t).|| <= (|.c.| ") * ||.(c * f).|| by A23, A22, Th17, XREAL_1:64; ::_thesis: verum
end;
A24: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_f1_holds_
r_<=_(|.c.|_")_*_||.(c_*_f).||
let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= (|.c.| ") * ||.(c * f).|| )
assume r in PreNorms f1 ; ::_thesis: r <= (|.c.| ") * ||.(c * f).||
then ex t being Element of X st r = ||.(f1 . t).|| ;
hence r <= (|.c.| ") * ||.(c * f).|| by A21; ::_thesis: verum
end;
A25: ( ( for s being real number st s in PreNorms f1 holds
s <= (|.c.| ") * ||.(c * f).|| ) implies upper_bound (PreNorms f1) <= (|.c.| ") * ||.(c * f).|| ) by SEQ_4:45;
A26: 0 <= |.c.| by COMPLEX1:46;
(ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f1) by Th15;
then ||.f.|| <= (|.c.| ") * ||.(c * f).|| by A24, A25;
then |.c.| * ||.f.|| <= |.c.| * ((|.c.| ") * ||.(c * f).||) by A26, XREAL_1:64;
then A27: |.c.| * ||.f.|| <= (|.c.| * (|.c.| ")) * ||.(c * f).|| ;
|.c.| <> 0 by A20, COMPLEX1:47;
then |.c.| * ||.f.|| <= 1 * ||.(c * f).|| by A27, XCMPLX_0:def_7;
hence |.c.| * ||.f.|| <= ||.(c * f).|| ; ::_thesis: verum
end;
caseA28: c = 0c ; ::_thesis: ||.(c * f).|| = |.c.| * ||.f.||
reconsider fz = f as VECTOR of (C_VectorSpace_of_BoundedFunctions (X,Y)) ;
c * f = (Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) . [c,f] by CLVECT_1:def_1
.= c * fz by CLVECT_1:def_1
.= 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) by A28, CLVECT_1:1
.= 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ;
hence ||.(c * f).|| = |.c.| * ||.f.|| by A28, Th19, COMPLEX1:44; ::_thesis: verum
end;
end;
end;
(ComplexBoundedFunctionsNorm (X,Y)) . (c * f) = upper_bound (PreNorms h1) by Th15;
then ||.(c * f).|| <= |.c.| * ||.f.|| by A18, A15;
hence ||.(c * f).|| = |.c.| * ||.f.|| by A19, XXREAL_0:1; ::_thesis: verum
end;
now__::_thesis:_(_||.f.||_=_0_implies_f_=_0._(C_NormSpace_of_BoundedFunctions_(X,Y))_)
reconsider g = f as bounded Function of X, the carrier of Y by Def5;
set z = X --> (0. Y);
reconsider z = X --> (0. Y) as Function of X, the carrier of Y ;
assume A29: ||.f.|| = 0 ; ::_thesis: f = 0. (C_NormSpace_of_BoundedFunctions (X,Y))
now__::_thesis:_for_t_being_Element_of_X_holds_g_._t_=_z_._t
let t be Element of X; ::_thesis: g . t = z . t
||.(g . t).|| <= ||.f.|| by Th17;
then ||.(g . t).|| = 0 by A29, CLVECT_1:105;
hence g . t = 0. Y by NORMSP_0:def_5
.= z . t by FUNCOP_1:7 ;
::_thesis: verum
end;
then g = z by FUNCT_2:63;
hence f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) by Th16; ::_thesis: verum
end;
hence ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by A1, A14, A9; ::_thesis: verum
end;
theorem Th23: :: CSSPACE4:23
for X being non empty set
for Y being ComplexNormSpace holds
( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds
( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )
let Y be ComplexNormSpace; ::_thesis: ( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )
thus ||.(0. (C_NormSpace_of_BoundedFunctions (X,Y))).|| = 0 by Th22; :: according to NORMSP_0:def_6 ::_thesis: ( C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like )
for x, y being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( x = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.x.|| = 0 ) & ||.(c * x).|| = |.c.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th22;
hence ( C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like ) by CLVECT_1:def_13, NORMSP_0:def_5; ::_thesis: verum
end;
theorem Th24: :: CSSPACE4:24
for X being non empty set
for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace
let Y be ComplexNormSpace; ::_thesis: C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace
CLSStruct(# (ComplexBoundedFunctions (X,Y)),(Zero_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Add_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))),(Mult_ ((ComplexBoundedFunctions (X,Y)),(ComplexVectSpace (X,Y)))) #) is ComplexLinearSpace ;
hence C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace by Th23, CSSPACE3:2; ::_thesis: verum
end;
registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster C_NormSpace_of_BoundedFunctions (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence
( C_NormSpace_of_BoundedFunctions (X,Y) is reflexive & C_NormSpace_of_BoundedFunctions (X,Y) is discerning & C_NormSpace_of_BoundedFunctions (X,Y) is ComplexNormSpace-like & C_NormSpace_of_BoundedFunctions (X,Y) is vector-distributive & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-distributive & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-associative & C_NormSpace_of_BoundedFunctions (X,Y) is scalar-unital & C_NormSpace_of_BoundedFunctions (X,Y) is Abelian & C_NormSpace_of_BoundedFunctions (X,Y) is add-associative & C_NormSpace_of_BoundedFunctions (X,Y) is right_zeroed & C_NormSpace_of_BoundedFunctions (X,Y) is right_complementable ) by Th24;
end;
theorem Th25: :: CSSPACE4:25
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace
for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
let Y be ComplexNormSpace; ::_thesis: for f, g, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
let f, g, h be Point of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: for f9, g9, h9 being bounded Function of X, the carrier of Y st f9 = f & g9 = g & h9 = h holds
( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
let f9, g9, h9 be bounded Function of X, the carrier of Y; ::_thesis: ( f9 = f & g9 = g & h9 = h implies ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ) )
assume A1: ( f9 = f & g9 = g & h9 = h ) ; ::_thesis: ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) )
A2: now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_-_(g9_._x)_)_implies_f_-_g_=_h_)
assume A3: for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ; ::_thesis: f - g = h
now__::_thesis:_for_x_being_Element_of_X_holds_(h9_._x)_+_(g9_._x)_=_f9_._x
let x be Element of X; ::_thesis: (h9 . x) + (g9 . x) = f9 . x
h9 . x = (f9 . x) - (g9 . x) by A3;
then (h9 . x) + (g9 . x) = (f9 . x) - ((g9 . x) - (g9 . x)) by RLVECT_1:29;
then (h9 . x) + (g9 . x) = (f9 . x) - (0. Y) by RLVECT_1:15;
hence (h9 . x) + (g9 . x) = f9 . x by RLVECT_1:13; ::_thesis: verum
end;
then f = h + g by A1, Th20;
then f - g = h + (g - g) by RLVECT_1:def_3;
then f - g = h + (0. (C_NormSpace_of_BoundedFunctions (X,Y))) by RLVECT_1:15;
hence f - g = h by RLVECT_1:4; ::_thesis: verum
end;
now__::_thesis:_(_h_=_f_-_g_implies_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_-_(g9_._x)_)
assume h = f - g ; ::_thesis: for x being Element of X holds h9 . x = (f9 . x) - (g9 . x)
then h + g = f - (g - g) by RLVECT_1:29;
then h + g = f - (0. (C_NormSpace_of_BoundedFunctions (X,Y))) by RLVECT_1:15;
then A4: h + g = f by RLVECT_1:13;
now__::_thesis:_for_x_being_Element_of_X_holds_(f9_._x)_-_(g9_._x)_=_h9_._x
let x be Element of X; ::_thesis: (f9 . x) - (g9 . x) = h9 . x
f9 . x = (h9 . x) + (g9 . x) by A1, A4, Th20;
then (f9 . x) - (g9 . x) = (h9 . x) + ((g9 . x) - (g9 . x)) by RLVECT_1:def_3;
then (f9 . x) - (g9 . x) = (h9 . x) + (0. Y) by RLVECT_1:15;
hence (f9 . x) - (g9 . x) = h9 . x by RLVECT_1:4; ::_thesis: verum
end;
hence for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ; ::_thesis: verum
end;
hence ( h = f - g iff for x being Element of X holds h9 . x = (f9 . x) - (g9 . x) ) by A2; ::_thesis: verum
end;
Lm12: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
proof
let e be Real; ::_thesis: for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
let seq be Real_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e implies lim seq <= e )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e ; ::_thesis: lim seq <= e
consider k being Element of NAT such that
A3: for i being Element of NAT st k <= i holds
seq . i <= e by A2;
reconsider cseq = NAT --> e as Real_Sequence ;
A4: lim cseq = cseq . 0 by SEQ_4:26
.= e by FUNCOP_1:7 ;
A5: now__::_thesis:_for_i_being_Element_of_NAT_holds_(seq_^\_k)_._i_<=_cseq_._i
let i be Element of NAT ; ::_thesis: (seq ^\ k) . i <= cseq . i
( (seq ^\ k) . i = seq . (k + i) & seq . (k + i) <= e ) by A3, NAT_1:11, NAT_1:def_3;
hence (seq ^\ k) . i <= cseq . i by FUNCOP_1:7; ::_thesis: verum
end;
lim (seq ^\ k) = lim seq by A1, SEQ_4:20;
hence lim seq <= e by A1, A5, A4, SEQ_2:18; ::_thesis: verum
end;
theorem Th26: :: CSSPACE4:26
for X being non empty set
for Y being ComplexNormSpace st Y is complete holds
for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let X be non empty set ; ::_thesis: for Y being ComplexNormSpace st Y is complete holds
for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let Y be ComplexNormSpace; ::_thesis: ( Y is complete implies for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent )
assume A1: Y is complete ; ::_thesis: for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (C_NormSpace_of_BoundedFunctions (X,Y)); ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A2: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
defpred S1[ set , set ] means ex xseq being sequence of Y st
( ( for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . $1 ) & xseq is convergent & $2 = lim xseq );
A3: for x being Element of X ex y being Element of Y st S1[x,y]
proof
let x be Element of X; ::_thesis: ex y being Element of Y st S1[x,y]
deffunc H1( Element of NAT ) -> Element of the carrier of Y = (modetrans ((vseq . $1),X,Y)) . x;
consider xseq being sequence of Y such that
A4: for n being Element of NAT holds xseq . n = H1(n) from FUNCT_2:sch_4();
take lim xseq ; ::_thesis: S1[x, lim xseq]
A5: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
vseq . k is bounded Function of X, the carrier of Y by Def5;
then A6: modetrans ((vseq . k),X,Y) = vseq . k by Th14;
reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5;
vseq . m is bounded Function of X, the carrier of Y by Def5;
then A7: modetrans ((vseq . m),X,Y) = vseq . m by Th14;
( xseq . m = (modetrans ((vseq . m),X,Y)) . x & xseq . k = (modetrans ((vseq . k),X,Y)) . x ) by A4;
then (xseq . m) - (xseq . k) = h1 . x by A7, A6, Th25;
hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th17; ::_thesis: verum
end;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((xseq_._n)_-_(xseq_._m)).||_<_e
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e )
assume A8: e > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
thus ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ::_thesis: verum
proof
consider k being Element of NAT such that
A9: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A8, CSSPACE3:8;
take k ; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
thus for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ::_thesis: verum
proof
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume ( n >= k & m >= k ) ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| < e
then A10: ||.((vseq . n) - (vseq . m)).|| < e by A9;
||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A5;
hence ||.((xseq . n) - (xseq . m)).|| < e by A10, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
then xseq is Cauchy_sequence_by_Norm by CSSPACE3:8;
then xseq is convergent by A1, CLOPBAN1:def_13;
hence S1[x, lim xseq] by A4; ::_thesis: verum
end;
consider f being Function of X, the carrier of Y such that
A11: for x being Element of X holds S1[x,f . x] from FUNCT_2:sch_3(A3);
reconsider tseq = f as Function of X, the carrier of Y ;
now__::_thesis:_for_e1_being_real_number_st_e1_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let e1 be real number ; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume A12: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
reconsider e = e1 as Real by XREAL_0:def_1;
consider k being Element of NAT such that
A13: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A12, CSSPACE3:8;
take k = k; ::_thesis: for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let m be Element of NAT ; ::_thesis: ( m >= k implies abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume m >= k ; ::_thesis: abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
then A14: ( ||.(vseq . m).|| = ||.vseq.|| . m & ||.((vseq . m) - (vseq . k)).|| < e ) by A13, NORMSP_0:def_4;
( abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| & ||.(vseq . k).|| = ||.vseq.|| . k ) by CLVECT_1:110, NORMSP_0:def_4;
hence abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A14, XXREAL_0:2; ::_thesis: verum
end;
hence for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 ; ::_thesis: verum
end;
then A15: ||.vseq.|| is convergent by SEQ_4:41;
A16: tseq is bounded
proof
take lim ||.vseq.|| ; :: according to CSSPACE4:def_4 ::_thesis: ( 0 <= lim ||.vseq.|| & ( for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) )
A17: now__::_thesis:_for_x_being_Element_of_X_holds_||.(tseq_._x).||_<=_lim_||.vseq.||
let x be Element of X; ::_thesis: ||.(tseq . x).|| <= lim ||.vseq.||
consider xseq being sequence of Y such that
A18: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A19: ( xseq is convergent & tseq . x = lim xseq ) by A11;
A20: for m being Element of NAT holds ||.(xseq . m).|| <= ||.(vseq . m).||
proof
let m be Element of NAT ; ::_thesis: ||.(xseq . m).|| <= ||.(vseq . m).||
( vseq . m is bounded Function of X, the carrier of Y & xseq . m = (modetrans ((vseq . m),X,Y)) . x ) by A18, Def5;
hence ||.(xseq . m).|| <= ||.(vseq . m).|| by Th14, Th17; ::_thesis: verum
end;
A21: for n being Element of NAT holds ||.xseq.|| . n <= ||.vseq.|| . n
proof
let n be Element of NAT ; ::_thesis: ||.xseq.|| . n <= ||.vseq.|| . n
( ||.xseq.|| . n = ||.(xseq . n).|| & ||.(xseq . n).|| <= ||.(vseq . n).|| ) by A20, NORMSP_0:def_4;
hence ||.xseq.|| . n <= ||.vseq.|| . n by NORMSP_0:def_4; ::_thesis: verum
end;
( ||.xseq.|| is convergent & ||.(tseq . x).|| = lim ||.xseq.|| ) by A19, CLOPBAN1:40;
hence ||.(tseq . x).|| <= lim ||.vseq.|| by A15, A21, SEQ_2:18; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.vseq.||_._n_>=_0
let n be Element of NAT ; ::_thesis: ||.vseq.|| . n >= 0
||.(vseq . n).|| >= 0 by CLVECT_1:105;
hence ||.vseq.|| . n >= 0 by NORMSP_0:def_4; ::_thesis: verum
end;
hence ( 0 <= lim ||.vseq.|| & ( for x being Element of X holds ||.(tseq . x).|| <= lim ||.vseq.|| ) ) by A15, A17, SEQ_2:17; ::_thesis: verum
end;
A22: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e )
assume e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
then consider k being Element of NAT such that
A23: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, CSSPACE3:8;
take k ; ::_thesis: for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
for_x_being_Element_of_X_holds_||.(((modetrans_((vseq_._n),X,Y))_._x)_-_(tseq_._x)).||_<=_e
let n be Element of NAT ; ::_thesis: ( n >= k implies for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e )
assume A24: n >= k ; ::_thesis: for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
now__::_thesis:_for_x_being_Element_of_X_holds_||.(((modetrans_((vseq_._n),X,Y))_._x)_-_(tseq_._x)).||_<=_e
let x be Element of X; ::_thesis: ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e
consider xseq being sequence of Y such that
A25: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A26: ( xseq is convergent & tseq . x = lim xseq ) by A11;
A27: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
proof
let m, k be Element of NAT ; ::_thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
vseq . k is bounded Function of X, the carrier of Y by Def5;
then A28: modetrans ((vseq . k),X,Y) = vseq . k by Th14;
reconsider h1 = (vseq . m) - (vseq . k) as bounded Function of X, the carrier of Y by Def5;
vseq . m is bounded Function of X, the carrier of Y by Def5;
then A29: modetrans ((vseq . m),X,Y) = vseq . m by Th14;
( xseq . m = (modetrans ((vseq . m),X,Y)) . x & xseq . k = (modetrans ((vseq . k),X,Y)) . x ) by A25;
then (xseq . m) - (xseq . k) = h1 . x by A29, A28, Th25;
hence ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| by Th17; ::_thesis: verum
end;
A30: for m being Element of NAT st m >= k holds
||.((xseq . n) - (xseq . m)).|| <= e
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies ||.((xseq . n) - (xseq . m)).|| <= e )
assume m >= k ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| <= e
then A31: ||.((vseq . n) - (vseq . m)).|| < e by A23, A24;
||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| by A27;
hence ||.((xseq . n) - (xseq . m)).|| <= e by A31, XXREAL_0:2; ::_thesis: verum
end;
||.((xseq . n) - (tseq . x)).|| <= e
proof
deffunc H1( Element of NAT ) -> Element of REAL = ||.((xseq . $1) - (xseq . n)).||;
consider rseq being Real_Sequence such that
A32: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
rseq_._x_=_||.(xseq_-_(xseq_._n)).||_._x
let x be set ; ::_thesis: ( x in NAT implies rseq . x = ||.(xseq - (xseq . n)).|| . x )
assume x in NAT ; ::_thesis: rseq . x = ||.(xseq - (xseq . n)).|| . x
then reconsider k = x as Element of NAT ;
thus rseq . x = ||.((xseq . k) - (xseq . n)).|| by A32
.= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def_4
.= ||.(xseq - (xseq . n)).|| . x by NORMSP_0:def_4 ; ::_thesis: verum
end;
then A33: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2:12;
A34: ( xseq - (xseq . n) is convergent & lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) ) by A26, CLVECT_1:115, CLVECT_1:121;
then A35: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A33, CLOPBAN1:19;
for m being Element of NAT st m >= k holds
rseq . m <= e
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e )
assume A36: m >= k ; ::_thesis: rseq . m <= e
rseq . m = ||.((xseq . m) - (xseq . n)).|| by A32
.= ||.((xseq . n) - (xseq . m)).|| by CLVECT_1:108 ;
hence rseq . m <= e by A30, A36; ::_thesis: verum
end;
then lim rseq <= e by A34, A33, Lm12, CLOPBAN1:19;
hence ||.((xseq . n) - (tseq . x)).|| <= e by A35, CLVECT_1:108; ::_thesis: verum
end;
hence ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e by A25; ::_thesis: verum
end;
hence for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e ; ::_thesis: verum
end;
hence for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e ; ::_thesis: verum
end;
reconsider tseq = tseq as bounded Function of X, the carrier of Y by A16;
reconsider tv = tseq as Point of (C_NormSpace_of_BoundedFunctions (X,Y)) by Def5;
A37: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e )
assume e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
then consider k being Element of NAT such that
A38: for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e by A22;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
||.((vseq_._n)_-_tv).||_<=_e
set g1 = tseq;
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )
assume A39: n >= k ; ::_thesis: ||.((vseq . n) - tv).|| <= e
reconsider h1 = (vseq . n) - tv as bounded Function of X, the carrier of Y by Def5;
set f1 = modetrans ((vseq . n),X,Y);
A40: now__::_thesis:_for_t_being_Element_of_X_holds_||.(h1_._t).||_<=_e
let t be Element of X; ::_thesis: ||.(h1 . t).|| <= e
vseq . n is bounded Function of X, the carrier of Y by Def5;
then modetrans ((vseq . n),X,Y) = vseq . n by Th14;
then ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by Th25;
hence ||.(h1 . t).|| <= e by A38, A39; ::_thesis: verum
end;
A41: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_e
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= e )
assume r in PreNorms h1 ; ::_thesis: r <= e
then ex t being Element of X st r = ||.(h1 . t).|| ;
hence r <= e by A40; ::_thesis: verum
end;
A42: ( ( for s being real number st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;
(ComplexBoundedFunctionsNorm (X,Y)) . ((vseq . n) - tv) = upper_bound (PreNorms h1) by Th15;
hence ||.((vseq . n) - tv).|| <= e by A41, A42; ::_thesis: verum
end;
hence ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e ; ::_thesis: verum
end;
for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A43: e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Element of NAT such that
A44: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A37, A43;
A45: e / 2 < e by A43, XREAL_1:216;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq . n) - tv).|| <= e / 2 by A44;
hence ||.((vseq . n) - tv).|| < e by A45, XXREAL_0:2; ::_thesis: verum
end;
hence ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e ; ::_thesis: verum
end;
hence vseq is convergent by CLVECT_1:def_15; ::_thesis: verum
end;
theorem Th27: :: CSSPACE4:27
for X being non empty set
for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace
proof
let X be non empty set ; ::_thesis: for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace
let Y be ComplexBanachSpace; ::_thesis: C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace
for seq being sequence of (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th26;
hence C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace by CLOPBAN1:def_13; ::_thesis: verum
end;
registration
let X be non empty set ;
let Y be ComplexBanachSpace;
cluster C_NormSpace_of_BoundedFunctions (X,Y) -> non empty complete ;
coherence
C_NormSpace_of_BoundedFunctions (X,Y) is complete by Th27;
end;
begin
theorem :: CSSPACE4:28
for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded by Lm3;
theorem :: CSSPACE4:29
for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded by Lm4;
theorem :: CSSPACE4:30
for seq being Complex_Sequence holds
( seq is bounded iff |.seq.| is bounded ) by Lm8, Lm9;
theorem :: CSSPACE4:31
for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) by Lm11;