:: CSSPACE3 semantic presentation

definition

func the_set_of_l1ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE3:def 1
for b₁ being set holds
( b₁ in a₁ iff ( b₁ in the_set_of_ComplexSequences & seq_id b₁ 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 b₁ being Complex
for b₂ being Complex_Sequence
for b₃ being Real_Sequence st b₂ is convergent & ( for b₄ being Nat holds b₃ . b₄ = |.((b₂ . b₄) - b₁).| ) holds
( b₃ is convergent & lim b₃ = |.((lim b₂) - b₁).| )

proof end;

registration

cluster the_set_of_l1ComplexSequences -> non empty ;
coherence

proof end;

end;

registration

cluster the_set_of_l1ComplexSequences -> non empty lineary-closed ;
coherence

proof end;

end;

Lemma3: 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 by CSSPACE:13;

end;

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

Lemma5: ex b₁ being Function of the_set_of_l1ComplexSequences , REAL st
for b₂ being set st b₂ in the_set_of_l1ComplexSequences holds
b₁ . b₂ = Sum |.(seq_id b₂).|

proof end;

definition

func cl_norm -> Function of the_set_of_l1ComplexSequences , REAL means :Def2: :: CSSPACE3:def 2
for b₁ being set st b₁ in the_set_of_l1ComplexSequences holds
a₁ . b₁ = Sum |.(seq_id b₁).|;
existence by Lemma5;
uniqueness

proof end;

end;

:: deftheorem Def2 defines cl_norm CSSPACE3:def 2 :

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be BinOp of c₁;
let c₄ be Function of [:COMPLEX ,c₁:],c₁;
let c₅ be Function of c₁, REAL ;
cluster CNORMSTR(# a₁,a₂,a₃,a₄,a₅ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

theorem Th2: :: CSSPACE3:2

canceled;

theorem Th3: :: CSSPACE3:3

canceled;

theorem Th4: :: CSSPACE3:4

for b₁ being CNORMSTR st CLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) is ComplexLinearSpace holds
b₁ is ComplexLinearSpace

proof end;

theorem Th5: :: CSSPACE3:5

for b₁ being Complex_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0c ) holds
( b₁ is absolutely_summable & Sum |.b₁.| = 0 )

proof end;

theorem Th6: :: CSSPACE3:6

for b₁ being Complex_Sequence st b₁ is absolutely_summable & Sum |.b₁.| = 0 holds
for b₂ being Nat holds b₁ . b₂ = 0c

proof end;

theorem Th7: :: CSSPACE3:7

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 Lemma4, Th4;

definition end;

:: deftheorem Def3 defines Complex_l1_Space CSSPACE3:def 3 :

theorem Th8: :: CSSPACE3:8

( the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & ( for b₁ being set holds
( b₁ is VECTOR of Complex_l1_Space iff ( b₁ is Complex_Sequence & seq_id b₁ is absolutely_summable ) ) ) & 0. Complex_l1_Space = CZeroseq & ( for b₁ being VECTOR of Complex_l1_Space holds b₁ = seq_id b₁ ) & ( for b₁, b₂ being VECTOR of Complex_l1_Space holds b₁ + b₂ = (seq_id b₁) + (seq_id b₂) ) & ( for b₁ being Complex
for b₂ being VECTOR of Complex_l1_Space holds b₁ * b₂ = b₁ (#) (seq_id b₂) ) & ( for b₁ being VECTOR of Complex_l1_Space holds
( - b₁ = - (seq_id b₁) & seq_id (- b₁) = - (seq_id b₁) ) ) & ( for b₁, b₂ being VECTOR of Complex_l1_Space holds b₁ - b₂ = (seq_id b₁) - (seq_id b₂) ) & ( for b₁ being VECTOR of Complex_l1_Space holds seq_id b₁ is absolutely_summable ) & ( for b₁ being VECTOR of Complex_l1_Space holds ||.b₁.|| = Sum |.(seq_id b₁).| ) )

proof end;

theorem Th9: :: CSSPACE3:9

for b₁, b₂ being Point of Complex_l1_Space
for b₃ being Complex holds
( ( ||.b₁.|| = 0 implies b₁ = 0. Complex_l1_Space ) & ( b₁ = 0. Complex_l1_Space implies ||.b₁.|| = 0 ) & 0 <= ||.b₁.|| & ||.(b₁ + b₂).|| <= ||.b₁.|| + ||.b₂.|| & ||.(b₃ * b₁).|| = |.b₃.| * ||.b₁.|| )

proof end;

registration end;

Lemma13: for b₁ being Complex
for b₂ being Complex_Sequence
for b₃ being Real_Sequence st b₂ is convergent & b₃ is convergent holds
for b₄ being Real_Sequence st ( for b₅ being Nat holds b₄ . b₅ = |.((b₂ . b₅) - b₁).| + (b₃ . b₅) ) holds
( b₄ is convergent & lim b₄ = |.((lim b₂) - b₁).| + (lim b₃) )

proof end;

definition

let c₁ be non empty CNORMSTR ;
let c₂, c₃ be Point of c₁;
func dist c₂,c₃ -> Real equals :: CSSPACE3:def 4
||.(a₂ - a₃).||;
coherence ;

end;

:: deftheorem Def4 defines dist CSSPACE3:def 4 :

definition

let c₁ be non empty CNORMSTR ;
let c₂ be sequence of c₁;
attr a₂ is CCauchy means :Def5: :: CSSPACE3:def 5
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃, b₄ being Nat st b₃ >= b₂ & b₄ >= b₂ holds
dist (a₂ . b₃),(a₂ . b₄) < b₁;

end;

:: deftheorem Def5 defines CCauchy CSSPACE3:def 5 :

notation

let c₁ be non empty CNORMSTR ;
let c₂ be sequence of c₁;
synonym Cauchy_sequence_by_Norm c₂ for CCauchy c₂;

end;

theorem Th10: :: CSSPACE3:10

for b₁ being non empty ComplexNormSpace
for b₂ being sequence of b₁ holds
( b₂ is CCauchy iff for b₃ being Real st b₃ > 0 holds
ex b₄ being Nat st
for b₅, b₆ being Nat st b₅ >= b₄ & b₆ >= b₄ holds
||.((b₂ . b₅) - (b₂ . b₆)).|| < b₃ )

proof end;

theorem Th11: :: CSSPACE3:11

for b₁ being sequence of Complex_l1_Space st b₁ is CCauchy holds
b₁ is convergent

proof end;