:: Complex Banach Space of Bounded Complex Sequences
:: by Noboru Endou
::
:: Copyright (c) 2004-2021 Association of Mizar Users

Lm1: for rseq being Real_Sequence
for K being Real st ( for n being Nat holds rseq . n <= K ) holds
upper_bound (rng rseq) <= K

proof end;

Lm2: for rseq being Real_Sequence st rseq is bounded holds
for n being Nat holds rseq . n <= upper_bound (rng rseq)

proof end;

definition
func the_set_of_BoundedComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE4:def 1
for x being object 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 object holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_ComplexSequences st ( for x being object holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) & ( for x being object holds
( x in b2 iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) holds
b1 = b2
proof 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 object 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 end;

reconsider jj = 1 as Real ;

Lm4: for c being Complex
for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded

proof end;

registration end;

Lm5:
by CSSPACE:11;

Lm6:
;

definition
func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences,REAL means :Def2: :: CSSPACE4:def 2
for x being object st x in the_set_of_BoundedComplexSequences holds
it . x = upper_bound (rng |.().|);
existence
ex b1 being Function of the_set_of_BoundedComplexSequences,REAL st
for x being object st x in the_set_of_BoundedComplexSequences holds
b1 . x = upper_bound (rng |.().|)
proof end;
uniqueness
for b1, b2 being Function of the_set_of_BoundedComplexSequences,REAL st ( for x being object st x in the_set_of_BoundedComplexSequences holds
b1 . x = upper_bound (rng |.().|) ) & ( for x being object st x in the_set_of_BoundedComplexSequences holds
b2 . x = upper_bound (rng |.().|) ) holds
b1 = b2
proof 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 object st x in the_set_of_BoundedComplexSequences holds
b1 . x = upper_bound (rng |.().|) );

Lm7: for seq being Complex_Sequence st ( for n being Nat holds seq . n = 0c ) holds
( seq is bounded & upper_bound (rng |.seq.|) = 0 )

proof end;

Lm8: for seq being Complex_Sequence st seq is bounded holds
|.seq.| is bounded

proof end;

Lm9: for seq being Complex_Sequence st |.seq.| is bounded holds
seq is bounded

proof end;

Lm10: for seq being Complex_Sequence st seq is bounded & upper_bound (rng |.seq.|) = 0 holds
for n being Nat holds seq . n = 0c

proof end;

theorem :: CSSPACE4:1
for seq being Complex_Sequence holds
( ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) iff for n being Nat holds seq . n = 0c ) by ;

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 = () + () ) & ( for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) () ) & ( 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 = () - () ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds = upper_bound (rng |.().|) ) )
proof end;

theorem Th3: :: CSSPACE4:3
for x, y being Point of Complex_linfty_Space
for c being Complex holds
( ( = 0 implies x = 0. Complex_linfty_Space ) & ( x = 0. Complex_linfty_Space implies = 0 ) & 0 <= & ||.(x + y).|| <= + & ||.(c * x).|| = |.c.| * )
proof end;

registration
coherence by ;
end;

Lm11: for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )

proof 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 end;

theorem :: CSSPACE4:5

definition
let X be non empty set ;
let Y be ComplexNormSpace;
let IT be Function of X, the carrier of Y;
attr IT 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 end;

registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster Relation-like X -defined the carrier of Y -valued non empty Function-like V26(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 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 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 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 end;
end;

theorem Th7: :: CSSPACE4:7
for X being non empty set
for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed
proof end;

theorem :: CSSPACE4:8
for X being non empty set
for Y being ComplexNormSpace holds CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is Subspace of ComplexVectSpace (X,Y) by ;

registration
let X be non empty set ;
let Y be ComplexNormSpace;
cluster CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is Abelian & CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is add-associative & CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is right_zeroed & CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is right_complementable & CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is vector-distributive & CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is scalar-distributive & CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is scalar-associative & CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #) is scalar-unital )
by ;
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(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #);
coherence
CLSStruct(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(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(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))) #);

registration
let X be non empty set ;
let Y be ComplexNormSpace;
coherence ;
end;

theorem Th9: :: CSSPACE4:9
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being VECTOR of
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 end;

theorem Th10: :: CSSPACE4:10
for X being non empty set
for Y being ComplexNormSpace
for f, h being VECTOR of
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 end;

theorem Th11: :: CSSPACE4:11
for X being non empty set
for Y being ComplexNormSpace holds 0. = X --> (0. Y)
proof end;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
let f be object ;
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 ;
end;

:: deftheorem Def7 defines modetrans CSSPACE4:def 7 :
for X being non empty set
for Y being ComplexNormSpace
for f being object 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 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 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 end;

definition
let X be non empty set ;
let Y be ComplexNormSpace;
func ComplexBoundedFunctionsNorm (X,Y) -> Function of (),REAL means :Def9: :: CSSPACE4:def 9
for x being object st x in ComplexBoundedFunctions (X,Y) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y)));
existence
ex b1 being Function of (),REAL st
for x being object st x in ComplexBoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
proof end;
uniqueness
for b1, b2 being Function of (),REAL st ( for x being object st x in ComplexBoundedFunctions (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in ComplexBoundedFunctions (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CSSPACE4:def 9 :
for X being non empty set
for Y being ComplexNormSpace
for b3 being Function of (),REAL holds
( b3 = ComplexBoundedFunctionsNorm (X,Y) iff for x being object 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 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 () . f = upper_bound ()
proof 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(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))),() #);
coherence
CNORMSTR(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (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(# (),(Zero_ ((),(ComplexVectSpace (X,Y)))),(Add_ ((),(ComplexVectSpace (X,Y)))),(Mult_ ((),(ComplexVectSpace (X,Y)))),() #);

theorem Th16: :: CSSPACE4:16
for X being non empty set
for Y being ComplexNormSpace holds X --> (0. Y) = 0. ()
proof end;

theorem Th17: :: CSSPACE4:17
for X being non empty set
for Y being ComplexNormSpace
for f being Point of ()
for g being bounded Function of X, the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <=
proof end;

theorem :: CSSPACE4:18
for X being non empty set
for Y being ComplexNormSpace
for f being Point of () holds 0 <=
proof end;

theorem Th19: :: CSSPACE4:19
for X being non empty set
for Y being ComplexNormSpace
for f being Point of () st f = 0. () holds
0 =
proof end;

theorem Th20: :: CSSPACE4:20
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being Point of ()
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 end;

theorem Th21: :: CSSPACE4:21
for X being non empty set
for Y being ComplexNormSpace
for f, h being Point of ()
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 end;

theorem Th22: :: CSSPACE4:22
for X being non empty set
for Y being ComplexNormSpace
for f, g being Point of ()
for c being Complex holds
( ( = 0 implies f = 0. () ) & ( f = 0. () implies = 0 ) & ||.(c * f).|| = |.c.| * & ||.(f + g).|| <= + )
proof 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 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 end;

registration
let X be non empty set ;
let Y be ComplexNormSpace;
coherence by Th24;
end;

theorem Th25: :: CSSPACE4:25
for X being non empty set
for Y being ComplexNormSpace
for f, g, h being Point of ()
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 end;

Lm12: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e

proof 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 () st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof 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 end;

registration
let X be non empty set ;
let Y be ComplexBanachSpace;
coherence by Th27;
end;

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 ;

theorem :: CSSPACE4:31
for seq1, seq2, seq3 being Complex_Sequence holds
( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ) by Lm11;