:: CSSPACE4 semantic presentation

Lemma1: for b₁ being Real_Sequence
for b₂ being real number st ( for b₃ being Nat holds b₁ . b₃ <= b₂ ) holds
sup (rng b₁) <= b₂

proof end;

Lemma2: for b₁ being Real_Sequence st b₁ is bounded holds
for b₂ being Nat holds b₁ . b₂ <= sup (rng b₁)

proof end;

definition

func the_set_of_BoundedComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE4:def 1
for b₁ being set holds
( b₁ in a₁ iff ( b₁ in the_set_of_ComplexSequences & seq_id b₁ is bounded ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines the_set_of_BoundedComplexSequences CSSPACE4:def 1 :

Lemma4: for b₁, b₂ being Complex_Sequence st b₁ is bounded & b₂ is bounded holds
b₁ + b₂ is bounded

proof end;

Lemma5: for b₁ being Complex
for b₂ being Complex_Sequence st b₂ is bounded holds
b₁ (#) b₂ is bounded

proof end;

registration

cluster the_set_of_BoundedComplexSequences -> non empty ;
coherence

proof end;

cluster the_set_of_BoundedComplexSequences -> lineary-closed ;
coherence

proof end;

end;

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

registration

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 ) #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence by CSSPACE:13;

end;

proof end;

definition

func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences , REAL means :Def2: :: CSSPACE4:def 2
for b₁ being set st b₁ in the_set_of_BoundedComplexSequences holds
a₁ . b₁ = sup (rng |.(seq_id b₁).|);
existence by Lemma8;
uniqueness

proof end;

end;

:: deftheorem Def2 defines Complex_linfty_norm CSSPACE4:def 2 :

Lemma10: for b₁ being Complex_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0c ) holds
( b₁ is bounded & sup (rng |.b₁.|) = 0 )

proof end;

Lemma11: for b₁ being Complex_Sequence st b₁ is bounded holds
|.b₁.| is bounded

proof end;

Lemma12: for b₁ being Complex_Sequence st |.b₁.| is bounded holds
b₁ is bounded

proof end;

Lemma13: for b₁ being Complex_Sequence st b₁ is bounded & sup (rng |.b₁.|) = 0 holds
for b₂ being Nat holds b₁ . b₂ = 0c

proof end;

theorem Th1: :: CSSPACE4:1

canceled;

theorem Th2: :: CSSPACE4:2

for b₁ being Complex_Sequence holds
( ( b₁ is bounded & sup (rng |.b₁.|) = 0 ) iff for b₂ being Nat holds b₁ . b₂ = 0c ) by Lemma10, Lemma13;

registration

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 #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence by Lemma7, CSSPACE3:4;

end;

definition end;

:: deftheorem Def3 defines Complex_linfty_Space CSSPACE4:def 3 :

theorem Th3: :: CSSPACE4:3

( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for b₁ being set holds
( b₁ is VECTOR of Complex_linfty_Space iff ( b₁ is Complex_Sequence & seq_id b₁ is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for b₁ being VECTOR of Complex_linfty_Space holds b₁ = seq_id b₁ ) & ( for b₁, b₂ being VECTOR of Complex_linfty_Space holds b₁ + b₂ = (seq_id b₁) + (seq_id b₂) ) & ( for b₁ being Complex
for b₂ being VECTOR of Complex_linfty_Space holds b₁ * b₂ = b₁ (#) (seq_id b₂) ) & ( for b₁ being VECTOR of Complex_linfty_Space holds
( - b₁ = - (seq_id b₁) & seq_id (- b₁) = - (seq_id b₁) ) ) & ( for b₁, b₂ being VECTOR of Complex_linfty_Space holds b₁ - b₂ = (seq_id b₁) - (seq_id b₂) ) & ( for b₁ being VECTOR of Complex_linfty_Space holds seq_id b₁ is bounded ) & ( for b₁ being VECTOR of Complex_linfty_Space holds ||.b₁.|| = sup (rng |.(seq_id b₁).|) ) )

proof end;

theorem Th4: :: CSSPACE4:4

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

proof end;

registration end;

Lemma16: for b₁, b₂, b₃ being Complex_Sequence holds
( b₁ = b₂ - b₃ iff for b₄ being Nat holds b₁ . b₄ = (b₂ . b₄) - (b₃ . b₄) )

proof end;

theorem Th5: :: CSSPACE4:5

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

proof end;

theorem Th6: :: CSSPACE4:6

Complex_linfty_Space is ComplexBanachSpace by Th5, CLOPBAN1:def 14;

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
let c₃ be Function of c₁,the carrier of c₂;
attr a₃ is bounded means :Def4: :: CSSPACE4:def 4
ex b₁ being Real st
( 0 <= b₁ & ( for b₂ being Element of a₁ holds ||.(a₃ . b₂).|| <= b₁ ) );

end;

:: deftheorem Def4 defines bounded CSSPACE4:def 4 :

theorem Th7: :: CSSPACE4:7

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being Function of b₁,the carrier of b₂ st ( for b₄ being Element of b₁ holds b₃ . b₄ = 0. b₂ ) holds
b₃ is bounded

proof end;

registration

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
cluster bounded Relation of a₁,the carrier of a₂;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
func ComplexBoundedFunctions c₁,c₂ -> Subset of (ComplexVectSpace a₁,a₂) means :Def5: :: CSSPACE4:def 5
for b₁ being set holds
( b₁ in a₃ iff b₁ is bounded Function of a₁,the carrier of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines ComplexBoundedFunctions CSSPACE4:def 5 :

registration

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
cluster ComplexBoundedFunctions a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th8: :: CSSPACE4:8

for b₁ being non empty set
for b₂ being ComplexNormSpace holds ComplexBoundedFunctions b₁,b₂ is lineary-closed

proof end;

theorem Th9: :: CSSPACE4:9

for b₁ being non empty set
for b₂ being ComplexNormSpace holds CLSStruct(# (ComplexBoundedFunctions b₁,b₂),(Zero_ (ComplexBoundedFunctions b₁,b₂),(ComplexVectSpace b₁,b₂)),(Add_ (ComplexBoundedFunctions b₁,b₂),(ComplexVectSpace b₁,b₂)),(Mult_ (ComplexBoundedFunctions b₁,b₂),(ComplexVectSpace b₁,b₂)) #) is Subspace of ComplexVectSpace b₁,b₂

proof end;

registration

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
cluster CLSStruct(# (ComplexBoundedFunctions a₁,a₂),(Zero_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)),(Add_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)),(Mult_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)) #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence by Th9;

end;

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
func C_VectorSpace_of_BoundedFunctions c₁,c₂ -> ComplexLinearSpace equals :: CSSPACE4:def 6
CLSStruct(# (ComplexBoundedFunctions a₁,a₂),(Zero_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)),(Add_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)),(Mult_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)) #);
coherence ;

end;

:: deftheorem Def6 defines C_VectorSpace_of_BoundedFunctions CSSPACE4:def 6 :

registration

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
cluster C_VectorSpace_of_BoundedFunctions a₁,a₂ -> strict ;
coherence ;

end;

theorem Th10: :: CSSPACE4:10

canceled;

theorem Th11: :: CSSPACE4:11

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄, b₅ being VECTOR of (C_VectorSpace_of_BoundedFunctions b₁,b₂)
for b₆, b₇, b₈ being bounded Function of b₁,the carrier of b₂ st b₆ = b₃ & b₇ = b₄ & b₈ = b₅ holds
( b₅ = b₃ + b₄ iff for b₉ being Element of b₁ holds b₈ . b₉ = (b₆ . b₉) + (b₇ . b₉) )

proof end;

theorem Th12: :: CSSPACE4:12

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being VECTOR of (C_VectorSpace_of_BoundedFunctions b₁,b₂)
for b₅, b₆ being bounded Function of b₁,the carrier of b₂ st b₅ = b₃ & b₆ = b₄ holds
for b₇ being Complex holds
( b₄ = b₇ * b₃ iff for b₈ being Element of b₁ holds b₆ . b₈ = b₇ * (b₅ . b₈) )

proof end;

theorem Th13: :: CSSPACE4:13

for b₁ being non empty set
for b₂ being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedFunctions b₁,b₂) = b₁ --> (0. b₂)

proof end;

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
let c₃ be set ;
assume E26: c₃ in ComplexBoundedFunctions c₁,c₂ ;
func modetrans c₃,c₁,c₂ -> bounded Function of a₁,the carrier of a₂ equals :Def7: :: CSSPACE4:def 7
a₃;
coherence by E26, Def5;

end;

:: deftheorem Def7 defines modetrans CSSPACE4:def 7 :

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
let c₃ be Function of c₁,the carrier of c₂;
func PreNorms c₃ -> non empty Subset of REAL equals :: CSSPACE4:def 8
{ ||.(a₃ . b₁).|| where B is Element of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def8 defines PreNorms CSSPACE4:def 8 :

theorem Th14: :: CSSPACE4:14

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being bounded Function of b₁,the carrier of b₂ holds
( not PreNorms b₃ is empty & PreNorms b₃ is bounded_above )

proof end;

theorem Th15: :: CSSPACE4:15

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being Function of b₁,the carrier of b₂ holds
( b₃ is bounded iff PreNorms b₃ is bounded_above )

proof end;

theorem Th16: :: CSSPACE4:16

for b₁ being non empty set
for b₂ being ComplexNormSpace ex b₃ being Function of ComplexBoundedFunctions b₁,b₂, REAL st
for b₄ being set st b₄ in ComplexBoundedFunctions b₁,b₂ holds
b₃ . b₄ = sup (PreNorms (modetrans b₄,b₁,b₂))

proof end;

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
func ComplexBoundedFunctionsNorm c₁,c₂ -> Function of ComplexBoundedFunctions a₁,a₂, REAL means :Def9: :: CSSPACE4:def 9
for b₁ being set st b₁ in ComplexBoundedFunctions a₁,a₂ holds
a₃ . b₁ = sup (PreNorms (modetrans b₁,a₁,a₂));
existence by Th16;
uniqueness

proof end;

end;

:: deftheorem Def9 defines ComplexBoundedFunctionsNorm CSSPACE4:def 9 :

theorem Th17: :: CSSPACE4:17

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being bounded Function of b₁,the carrier of b₂ holds modetrans b₃,b₁,b₂ = b₃

proof end;

theorem Th18: :: CSSPACE4:18

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being bounded Function of b₁,the carrier of b₂ holds (ComplexBoundedFunctionsNorm b₁,b₂) . b₃ = sup (PreNorms b₃)

proof end;

definition

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
func C_NormSpace_of_BoundedFunctions c₁,c₂ -> non empty CNORMSTR equals :: CSSPACE4:def 10
CNORMSTR(# (ComplexBoundedFunctions a₁,a₂),(Zero_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)),(Add_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)),(Mult_ (ComplexBoundedFunctions a₁,a₂),(ComplexVectSpace a₁,a₂)),(ComplexBoundedFunctionsNorm a₁,a₂) #);
coherence ;

end;

:: deftheorem Def10 defines C_NormSpace_of_BoundedFunctions CSSPACE4:def 10 :

theorem Th19: :: CSSPACE4:19

for b₁ being non empty set
for b₂ being ComplexNormSpace holds b₁ --> (0. b₂) = 0. (C_NormSpace_of_BoundedFunctions b₁,b₂)

proof end;

theorem Th20: :: CSSPACE4:20

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being Point of (C_NormSpace_of_BoundedFunctions b₁,b₂)
for b₄ being bounded Function of b₁,the carrier of b₂ st b₄ = b₃ holds
for b₅ being Element of b₁ holds ||.(b₄ . b₅).|| <= ||.b₃.||

proof end;

theorem Th21: :: CSSPACE4:21

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being Point of (C_NormSpace_of_BoundedFunctions b₁,b₂) holds 0 <= ||.b₃.||

proof end;

theorem Th22: :: CSSPACE4:22

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃ being Point of (C_NormSpace_of_BoundedFunctions b₁,b₂) st b₃ = 0. (C_NormSpace_of_BoundedFunctions b₁,b₂) holds
0 = ||.b₃.||

proof end;

theorem Th23: :: CSSPACE4:23

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄, b₅ being Point of (C_NormSpace_of_BoundedFunctions b₁,b₂)
for b₆, b₇, b₈ being bounded Function of b₁,the carrier of b₂ st b₆ = b₃ & b₇ = b₄ & b₈ = b₅ holds
( b₅ = b₃ + b₄ iff for b₉ being Element of b₁ holds b₈ . b₉ = (b₆ . b₉) + (b₇ . b₉) )

proof end;

theorem Th24: :: CSSPACE4:24

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being Point of (C_NormSpace_of_BoundedFunctions b₁,b₂)
for b₅, b₆ being bounded Function of b₁,the carrier of b₂ st b₅ = b₃ & b₆ = b₄ holds
for b₇ being Complex holds
( b₄ = b₇ * b₃ iff for b₈ being Element of b₁ holds b₆ . b₈ = b₇ * (b₅ . b₈) )

proof end;

theorem Th25: :: CSSPACE4:25

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄ being Point of (C_NormSpace_of_BoundedFunctions b₁,b₂)
for b₅ being Complex holds
( ( ||.b₃.|| = 0 implies b₃ = 0. (C_NormSpace_of_BoundedFunctions b₁,b₂) ) & ( b₃ = 0. (C_NormSpace_of_BoundedFunctions b₁,b₂) implies ||.b₃.|| = 0 ) & ||.(b₅ * b₃).|| = |.b₅.| * ||.b₃.|| & ||.(b₃ + b₄).|| <= ||.b₃.|| + ||.b₄.|| )

proof end;

theorem Th26: :: CSSPACE4:26

for b₁ being non empty set
for b₂ being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions b₁,b₂ is ComplexNormSpace-like

proof end;

theorem Th27: :: CSSPACE4:27

for b₁ being non empty set
for b₂ being ComplexNormSpace holds C_NormSpace_of_BoundedFunctions b₁,b₂ is ComplexNormSpace

proof end;

registration

let c₁ be non empty set ;
let c₂ be ComplexNormSpace;
cluster C_NormSpace_of_BoundedFunctions a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like ;
coherence by Th27;

end;

theorem Th28: :: CSSPACE4:28

for b₁ being non empty set
for b₂ being ComplexNormSpace
for b₃, b₄, b₅ being Point of (C_NormSpace_of_BoundedFunctions b₁,b₂)
for b₆, b₇, b₈ being bounded Function of b₁,the carrier of b₂ st b₆ = b₃ & b₇ = b₄ & b₈ = b₅ holds
( b₅ = b₃ - b₄ iff for b₉ being Element of b₁ holds b₈ . b₉ = (b₆ . b₉) - (b₇ . b₉) )

proof end;

Lemma41: for b₁ being Real
for b₂ being Real_Sequence st b₂ is convergent & ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₂ . b₄ <= b₁ holds
lim b₂ <= b₁

proof end;

theorem Th29: :: CSSPACE4:29

for b₁ being non empty set
for b₂ being ComplexNormSpace st b₂ is complete holds
for b₃ being sequence of (C_NormSpace_of_BoundedFunctions b₁,b₂) st b₃ is CCauchy holds
b₃ is convergent

proof end;

theorem Th30: :: CSSPACE4:30

for b₁ being non empty set
for b₂ being ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions b₁,b₂ is ComplexBanachSpace

proof end;

registration

let c₁ be non empty set ;
let c₂ be ComplexBanachSpace;
cluster C_NormSpace_of_BoundedFunctions a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like complete ;
coherence by Th30;

end;

theorem Th31: :: CSSPACE4:31

for b₁, b₂ being Complex_Sequence st b₁ is bounded & b₂ is bounded holds
b₁ + b₂ is bounded by Lemma4;

theorem Th32: :: CSSPACE4:32

for b₁ being Complex
for b₂ being Complex_Sequence st b₂ is bounded holds
b₁ (#) b₂ is bounded by Lemma5;

theorem Th33: :: CSSPACE4:33

for b₁ being Complex_Sequence holds
( b₁ is bounded iff |.b₁.| is bounded ) by Lemma11, Lemma12;

theorem Th34: :: CSSPACE4:34

for b₁, b₂, b₃ being Complex_Sequence holds
( b₁ = b₂ - b₃ iff for b₄ being Nat holds b₁ . b₄ = (b₂ . b₄) - (b₃ . b₄) ) by Lemma16;