:: CSSPACE3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
func the_set_of_l1ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE3:def 1
for x being set holds
( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) );
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 absolutely_summable ) )
proof 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 absolutely_summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines the_set_of_l1ComplexSequences CSSPACE3:def 1 :
for b1 being Subset of Linear_Space_of_ComplexSequences holds
( b1 = the_set_of_l1ComplexSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) );

theorem Th1: :: CSSPACE3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Complex
for seq being Complex_Sequence
for rseq being Real_Sequence st seq is convergent & ( for i being Nat holds rseq . i = |.((seq . i) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| )
proof end;

registration
cluster the_set_of_l1ComplexSequences -> non empty ;
coherence
not the_set_of_l1ComplexSequences is empty
proof end;
end;

registration
cluster the_set_of_l1ComplexSequences -> non empty lineary-closed ;
coherence
the_set_of_l1ComplexSequences is lineary-closed
proof end;
end;

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 ) #) -> Abelian add-associative right_zeroed right_complementable 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: 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
;

Lm3: 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).|
proof end;

definition
func cl_norm -> Function of the_set_of_l1ComplexSequences , REAL means :Def2: :: CSSPACE3:def 2
for x being set st x in the_set_of_l1ComplexSequences holds
it . x = Sum |.(seq_id x).|;
existence
ex b1 being Function of the_set_of_l1ComplexSequences , REAL st
for x being set st x in the_set_of_l1ComplexSequences holds
b1 . x = Sum |.(seq_id x).|
by Lm3;
uniqueness
for b1, b2 being Function of the_set_of_l1ComplexSequences , REAL st ( for x being set st x in the_set_of_l1ComplexSequences holds
b1 . x = Sum |.(seq_id x).| ) & ( for x being set st x in the_set_of_l1ComplexSequences holds
b2 . x = Sum |.(seq_id x).| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines cl_norm CSSPACE3:def 2 :
for b1 being Function of the_set_of_l1ComplexSequences , REAL holds
( b1 = cl_norm iff for x being set st x in the_set_of_l1ComplexSequences holds
b1 . x = Sum |.(seq_id x).| );

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
by STRUCT_0:def 1;
end;

theorem :: CSSPACE3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CSSPACE3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: CSSPACE3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l being CNORMSTR st CLSStruct(# the carrier of l,the Zero of l,the add of l,the Mult of l #) is ComplexLinearSpace holds
l is ComplexLinearSpace
proof end;

theorem Th5: :: CSSPACE3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for cseq being Complex_Sequence st ( for n being Nat holds cseq . n = 0c ) holds
( cseq is absolutely_summable & Sum |.cseq.| = 0 )
proof end;

theorem Th6: :: CSSPACE3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for cseq being Complex_Sequence st cseq is absolutely_summable & Sum |.cseq.| = 0 holds
for n being Nat holds cseq . n = 0c
proof end;

theorem Th7: :: CSSPACE3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ComplexLinearSpace by Lm2, Th4;

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

theorem Th8: :: CSSPACE3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & ( for x being set holds
( x is VECTOR of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) ) ) & 0. Complex_l1_Space = CZeroseq & ( for u being VECTOR of Complex_l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for p being Complex
for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u) ) & ( for u being VECTOR of Complex_l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.(seq_id v).| ) )
proof end;

theorem Th9: :: CSSPACE3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Point of Complex_l1_Space
for p being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| )
proof end;

registration
cluster Complex_l1_Space -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like ;
coherence
( Complex_l1_Space is ComplexNormSpace-like & Complex_l1_Space is ComplexLinearSpace-like & Complex_l1_Space is Abelian & Complex_l1_Space is add-associative & Complex_l1_Space is right_zeroed & Complex_l1_Space is right_complementable )
by Lm2, Th4, Th9, CLVECT_1:def 10;
end;

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 Nat holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
proof end;

definition
let X be non empty CNORMSTR ;
let x, y be Point of X;
func dist x,y -> Real equals :: CSSPACE3:def 4
||.(x - y).||;
coherence
||.(x - y).|| is Real
;
end;

:: deftheorem defines dist CSSPACE3:def 4 :
for X being non empty CNORMSTR
for x, y being Point of X holds dist x,y = ||.(x - y).||;

definition
let CNRM be non empty CNORMSTR ;
let seqt be sequence of CNRM;
attr seqt is CCauchy means :Def5: :: CSSPACE3:def 5
for r1 being Real st r1 > 0 holds
ex k1 being Nat st
for n1, m1 being Nat st n1 >= k1 & m1 >= k1 holds
dist (seqt . n1),(seqt . m1) < r1;
end;

:: deftheorem Def5 defines CCauchy CSSPACE3:def 5 :
for CNRM being non empty CNORMSTR
for seqt being sequence of CNRM holds
( seqt is CCauchy iff for r1 being Real st r1 > 0 holds
ex k1 being Nat st
for n1, m1 being Nat st n1 >= k1 & m1 >= k1 holds
dist (seqt . n1),(seqt . m1) < r1 );

notation
let CNRM be non empty CNORMSTR ;
let seq be sequence of CNRM;
synonym Cauchy_sequence_by_Norm seq for CCauchy seq;
end;

theorem Th10: :: CSSPACE3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for NRM being non empty ComplexNormSpace
for seq being sequence of NRM holds
( seq is CCauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
proof end;

theorem :: CSSPACE3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for vseq being sequence of Complex_l1_Space st vseq is CCauchy holds
vseq is convergent
proof end;