:: by Noboru Endou

::

:: Received March 18, 2004

:: Copyright (c) 2004-2016 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

ex b_{1} being Subset of Linear_Space_of_ComplexSequences st

for x being object holds

( x in b_{1} iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) )

for b_{1}, b_{2} being Subset of Linear_Space_of_ComplexSequences st ( for x being object holds

( x in b_{1} iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) & ( for x being object holds

( x in b_{2} iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) ) holds

b_{1} = b_{2}
end;

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 for x being object holds

( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines the_set_of_BoundedComplexSequences CSSPACE4:def 1 :

for b_{1} being Subset of Linear_Space_of_ComplexSequences holds

( b_{1} = the_set_of_BoundedComplexSequences iff for x being object holds

( x in b_{1} iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) ) );

for b

( b

( x in b

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

coherence

not the_set_of_BoundedComplexSequences is empty

the_set_of_BoundedComplexSequences is linearly-closed

end;
not the_set_of_BoundedComplexSequences is empty

proof end;

coherence the_set_of_BoundedComplexSequences is linearly-closed

proof 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

( 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;

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;

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

ex b_{1} being Function of the_set_of_BoundedComplexSequences,REAL st

for x being object st x in the_set_of_BoundedComplexSequences holds

b_{1} . x = upper_bound (rng |.(seq_id x).|)

for b_{1}, b_{2} being Function of the_set_of_BoundedComplexSequences,REAL st ( for x being object st x in the_set_of_BoundedComplexSequences holds

b_{1} . x = upper_bound (rng |.(seq_id x).|) ) & ( for x being object st x in the_set_of_BoundedComplexSequences holds

b_{2} . x = upper_bound (rng |.(seq_id x).|) ) holds

b_{1} = b_{2}
end;

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 |.(seq_id x).|);

existence for x being object st x in the_set_of_BoundedComplexSequences holds

it . x = upper_bound (rng |.(seq_id x).|);

ex b

for x being object st x in the_set_of_BoundedComplexSequences holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines Complex_linfty_norm CSSPACE4:def 2 :

for b_{1} being Function of the_set_of_BoundedComplexSequences,REAL holds

( b_{1} = Complex_linfty_norm iff for x being object st x in the_set_of_BoundedComplexSequences holds

b_{1} . x = upper_bound (rng |.(seq_id x).|) );

for b

( b

b

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

registration

( 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;

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;

definition

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;

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 #);

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 ;

:: 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 #);

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).|) ) )

( 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 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.|| )

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

registration

( 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 ) by Th3, CLVECT_1:def 13;

end;

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 ) by Th3, CLVECT_1:def 13;

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

vseq is convergent

proof end;

definition
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 ) ) );

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

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;

ex b_{1} being Function of X, the carrier of Y st b_{1} is bounded

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

proof end;

definition

let X be non empty set ;

let Y be ComplexNormSpace;

ex b_{1} being Subset of (ComplexVectSpace (X,Y)) st

for x being set holds

( x in b_{1} iff x is bounded Function of X, the carrier of Y )

for b_{1}, b_{2} being Subset of (ComplexVectSpace (X,Y)) st ( for x being set holds

( x in b_{1} iff x is bounded Function of X, the carrier of Y ) ) & ( for x being set holds

( x in b_{2} iff x is bounded Function of X, the carrier of Y ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is bounded Function of X, the carrier of Y );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def5 defines ComplexBoundedFunctions CSSPACE4:def 5 :

for X being non empty set

for Y being ComplexNormSpace

for b_{3} being Subset of (ComplexVectSpace (X,Y)) holds

( b_{3} = ComplexBoundedFunctions (X,Y) iff for x being set holds

( x in b_{3} iff x is bounded Function of X, the carrier of Y ) );

for X being non empty set

for Y being ComplexNormSpace

for b

( b

( x in b

registration

let X be non empty set ;

let Y be ComplexNormSpace;

coherence

not ComplexBoundedFunctions (X,Y) is empty

end;
let Y be ComplexNormSpace;

coherence

not ComplexBoundedFunctions (X,Y) is empty

proof end;

theorem Th7: :: CSSPACE4:7

for X being non empty set

for Y being ComplexNormSpace holds ComplexBoundedFunctions (X,Y) is linearly-closed

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(# (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;

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;

( 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;
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;

definition

let X be non empty set ;

let Y be 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 ;

end;
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)))) #);

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 ;

:: 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)))) #);

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;

coherence

C_VectorSpace_of_BoundedFunctions (X,Y) is strict ;

end;
let Y be ComplexNormSpace;

coherence

C_VectorSpace_of_BoundedFunctions (X,Y) is strict ;

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) )

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 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) )

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 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)

for Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions (X,Y)) = 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) ;

coherence

f is bounded Function of X, the carrier of Y by A1, Def5;

end;
let Y be ComplexNormSpace;

let f be object ;

assume A1: f in ComplexBoundedFunctions (X,Y) ;

coherence

f is bounded Function of X, the carrier of Y by A1, Def5;

:: 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;

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;

{ ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL

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

{ ||.(u . t).|| where t is Element of X : verum } is non empty Subset of REAL

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

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

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 )

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;

ex b_{1} being Function of (ComplexBoundedFunctions (X,Y)),REAL st

for x being object st x in ComplexBoundedFunctions (X,Y) holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X,Y)))

for b_{1}, b_{2} being Function of (ComplexBoundedFunctions (X,Y)),REAL st ( for x being object st x in ComplexBoundedFunctions (X,Y) holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in ComplexBoundedFunctions (X,Y) holds

b_{2} . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds

b_{1} = b_{2}

end;
let Y be ComplexNormSpace;

func ComplexBoundedFunctionsNorm (X,Y) -> Function of (ComplexBoundedFunctions (X,Y)),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 for x being object st x in ComplexBoundedFunctions (X,Y) holds

it . x = upper_bound (PreNorms (modetrans (x,X,Y)));

ex b

for x being object st x in ComplexBoundedFunctions (X,Y) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CSSPACE4:def 9 :

for X being non empty set

for Y being ComplexNormSpace

for b_{3} being Function of (ComplexBoundedFunctions (X,Y)),REAL holds

( b_{3} = ComplexBoundedFunctionsNorm (X,Y) iff for x being object st x in ComplexBoundedFunctions (X,Y) holds

b_{3} . x = upper_bound (PreNorms (modetrans (x,X,Y))) );

for X being non empty set

for Y being ComplexNormSpace

for b

( b

b

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

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 (ComplexBoundedFunctionsNorm (X,Y)) . f = upper_bound (PreNorms f)

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

definition

let X be non empty set ;

let Y be ComplexNormSpace;

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;
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)) #);

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 ;

:: 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)) #);

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))

for Y being ComplexNormSpace holds X --> (0. Y) = 0. (C_NormSpace_of_BoundedFunctions (X,Y))

proof 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.||

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 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.||

for Y being ComplexNormSpace

for f being Point of (C_NormSpace_of_BoundedFunctions (X,Y)) holds 0 <= ||.f.||

proof 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.||

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 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) )

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 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) )

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 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.|| )

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 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 )

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

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;

( 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;
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;

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) )

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 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 (C_NormSpace_of_BoundedFunctions (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

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

theorem Th27: :: CSSPACE4:27

for X being non empty set

for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions (X,Y) is ComplexBanachSpace

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

C_NormSpace_of_BoundedFunctions (X,Y) is complete by Th27;

end;
let Y be ComplexBanachSpace;

coherence

C_NormSpace_of_BoundedFunctions (X,Y) is complete by Th27;

theorem :: CSSPACE4:28

theorem :: CSSPACE4:29

theorem :: CSSPACE4:30

theorem :: CSSPACE4:31