:: Banach Space of Absolute Summable Complex Sequences
:: by Noboru Endou
::
:: Received February 24, 2004
:: Copyright (c) 2004 Association of Mizar Users
:: deftheorem Def1 defines the_set_of_l1ComplexSequences CSSPACE3:def 1 :
theorem Th1: :: CSSPACE3:1
Lm1:
CLSStruct(# the_set_of_l1ComplexSequences ,(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Subspace of Linear_Space_of_ComplexSequences
by CSSPACE:13;
registration
cluster CLSStruct(#
the_set_of_l1ComplexSequences ,
(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),
(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),
(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ) #)
-> right_complementable Abelian add-associative right_zeroed ComplexLinearSpace-like ;
coherence
( CLSStruct(# the_set_of_l1ComplexSequences ,(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Abelian & CLSStruct(# the_set_of_l1ComplexSequences ,(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is add-associative & CLSStruct(# the_set_of_l1ComplexSequences ,(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_zeroed & CLSStruct(# the_set_of_l1ComplexSequences ,(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is right_complementable & CLSStruct(# the_set_of_l1ComplexSequences ,(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is ComplexLinearSpace-like )
by CSSPACE:13;
end;
Lm2:
ex NORM being Function of the_set_of_l1ComplexSequences , REAL st
for x being set st x in the_set_of_l1ComplexSequences holds
NORM . x = Sum |.(seq_id x).|
:: deftheorem Def2 defines cl_norm CSSPACE3:def 2 :
registration
let X be non
empty set ;
let Z be
Element of
X;
let A be
BinOp of
X;
let M be
Function of
[:COMPLEX ,X:],
X;
let N be
Function of
X,
REAL ;
cluster CNORMSTR(#
X,
Z,
A,
M,
N #)
-> non
empty ;
coherence
not CNORMSTR(# X,Z,A,M,N #) is empty
;
end;
theorem :: CSSPACE3:2
canceled;
theorem :: CSSPACE3:3
canceled;
theorem :: CSSPACE3:4
theorem Th5: :: CSSPACE3:5
theorem Th6: :: CSSPACE3:6
Lm3:
CLSStruct(# the_set_of_l1ComplexSequences ,(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is ComplexLinearSpace
;
theorem Th7: :: CSSPACE3:7
definition
func Complex_l1_Space -> non
empty CNORMSTR equals :: CSSPACE3:def 3
CNORMSTR(#
the_set_of_l1ComplexSequences ,
(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),
(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),
(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),
cl_norm #);
coherence
CNORMSTR(# the_set_of_l1ComplexSequences ,(Zero_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l1ComplexSequences ,Linear_Space_of_ComplexSequences ),cl_norm #) is non empty CNORMSTR
;
end;
:: deftheorem defines Complex_l1_Space CSSPACE3:def 3 :
theorem Th8: :: CSSPACE3:8
theorem Th9: :: CSSPACE3:9
Lm4:
for c being Complex
for seq being Complex_Sequence
for seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
:: deftheorem defines dist CSSPACE3:def 4 :
:: deftheorem Def5 defines CCauchy CSSPACE3:def 5 :
theorem Th10: :: CSSPACE3:10
theorem :: CSSPACE3:11