CSSPACE3: Banach Space of Absolute Summable Complex Sequences

:: Banach Space of Absolute Summable Complex Sequences
:: by Noboru Endou
::
:: Received February 24, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

definition

func the_set_of_l1ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE3:def 1
for x being object holds
( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines the_set_of_l1ComplexSequences CSSPACE3:def 1 :

theorem Th1: :: CSSPACE3:1

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

proof end;

end;

registration

cluster the_set_of_l1ComplexSequences -> linearly-closed ;

coherence

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

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 vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence by CSSPACE:11;

end;

definition

func cl_norm -> Function of the_set_of_l1ComplexSequences,REAL means :Def2: :: CSSPACE3:def 2
for x being object st x in the_set_of_l1ComplexSequences holds
it . x = Sum |.(seq_id x).|;

existence

proof end;

uniqueness

proof end;

end;

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

end;

theorem :: CSSPACE3:2

for l being CNORMSTR st CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace holds
l is ComplexLinearSpace by CSSPACE:79;

theorem Th3: :: CSSPACE3:3

for cseq being Complex_Sequence st ( for n being Nat holds cseq . n = 0c ) holds
( cseq is absolutely_summable & Sum |.cseq.| = 0 )

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

definition end;

:: deftheorem defines Complex_l1_Space CSSPACE3:def 3 :

theorem :: CSSPACE3:4

canceled;

::$CT

theorem Th4: :: CSSPACE3:5

Complex_l1_Space is ComplexLinearSpace by Lm2, CSSPACE:79;

theorem Th5: :: CSSPACE3:6

( 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 Th6: :: CSSPACE3:7

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

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

end;

:: deftheorem defines dist CSSPACE3:def 4 :

definition

let CNRM be non empty CNORMSTR ;
let seqt be sequence of CNRM;

attr seqt is CCauchy means :: 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 defines CCauchy CSSPACE3:def 5 :

notation

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

end;

theorem Th7: :: CSSPACE3:8

for NRM being ComplexNormSpace
for seq being sequence of NRM holds
( seq is Cauchy_sequence_by_Norm 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:9

for vseq being sequence of Complex_l1_Space st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent

proof end;