:: RSSPACE4 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_BoundedRealSequences -> Subset of Linear_Space_of_RealSequences means :Def1: :: RSSPACE4:def 1
for b₁ being set holds
( b₁ in a₁ iff ( b₁ in the_set_of_RealSequences & seq_id b₁ is bounded ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines the_set_of_BoundedRealSequences RSSPACE4:def 1 :

registration

cluster the_set_of_BoundedRealSequences -> non empty ;
coherence

proof end;

cluster the_set_of_BoundedRealSequences -> lineary-closed ;
coherence

proof end;

end;

Lemma4: RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:13;

registration

cluster RLSStruct(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ) #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence by RSSPACE:13;

end;

proof end;

definition

func linfty_norm -> Function of the_set_of_BoundedRealSequences , REAL means :Def2: :: RSSPACE4:def 2
for b₁ being set st b₁ in the_set_of_BoundedRealSequences holds
a₁ . b₁ = sup (rng (abs (seq_id b₁)));
existence by Lemma6;
uniqueness

proof end;

end;

:: deftheorem Def2 defines linfty_norm RSSPACE4:def 2 :

Lemma8: for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0 ) holds
( b₁ is bounded & sup (rng (abs b₁)) = 0 )

proof end;

Lemma9: for b₁ being Real_Sequence st b₁ is bounded & sup (rng (abs b₁)) = 0 holds
for b₂ being Nat holds b₁ . b₂ = 0

proof end;

theorem Th1: :: RSSPACE4:1

canceled;

theorem Th2: :: RSSPACE4:2

for b₁ being Real_Sequence holds
( ( b₁ is bounded & sup (rng (abs b₁)) = 0 ) iff for b₂ being Nat holds b₁ . b₂ = 0 ) by Lemma8, Lemma9;

registration

cluster NORMSTR(# the_set_of_BoundedRealSequences ,(Zero_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_BoundedRealSequences ,Linear_Space_of_RealSequences ),linfty_norm #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence by Lemma5, RSSPACE3:4;

end;

definition end;

:: deftheorem Def3 defines linfty_Space RSSPACE4:def 3 :

theorem Th3: :: RSSPACE4:3

( the carrier of linfty_Space = the_set_of_BoundedRealSequences & ( for b₁ being set holds
( b₁ is VECTOR of linfty_Space iff ( b₁ is Real_Sequence & seq_id b₁ is bounded ) ) ) & 0. linfty_Space = Zeroseq & ( for b₁ being VECTOR of linfty_Space holds b₁ = seq_id b₁ ) & ( for b₁, b₂ being VECTOR of linfty_Space holds b₁ + b₂ = (seq_id b₁) + (seq_id b₂) ) & ( for b₁ being Real
for b₂ being VECTOR of linfty_Space holds b₁ * b₂ = b₁ (#) (seq_id b₂) ) & ( for b₁ being VECTOR of linfty_Space holds
( - b₁ = - (seq_id b₁) & seq_id (- b₁) = - (seq_id b₁) ) ) & ( for b₁, b₂ being VECTOR of linfty_Space holds b₁ - b₂ = (seq_id b₁) - (seq_id b₂) ) & ( for b₁ being VECTOR of linfty_Space holds seq_id b₁ is bounded ) & ( for b₁ being VECTOR of linfty_Space holds ||.b₁.|| = sup (rng (abs (seq_id b₁))) ) )

proof end;

theorem Th4: :: RSSPACE4:4

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

proof end;

registration end;

theorem Th5: :: RSSPACE4:5

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

proof end;

definition

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

end;

:: deftheorem Def4 defines bounded RSSPACE4:def 4 :

theorem Th6: :: RSSPACE4:6

for b₁ being non empty set
for b₂ being RealNormSpace
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 RealNormSpace;
cluster bounded M5(a₁,the carrier of a₂);
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
func BoundedFunctions c₁,c₂ -> Subset of (RealVectSpace a₁,a₂) means :Def5: :: RSSPACE4: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 BoundedFunctions RSSPACE4:def 5 :

registration

let c₁ be non empty set ;
let c₂ be RealNormSpace;
cluster BoundedFunctions a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th7: :: RSSPACE4:7

for b₁ being non empty set
for b₂ being RealNormSpace holds BoundedFunctions b₁,b₂ is lineary-closed

proof end;

theorem Th8: :: RSSPACE4:8

for b₁ being non empty set
for b₂ being RealNormSpace holds RLSStruct(# (BoundedFunctions b₁,b₂),(Zero_ (BoundedFunctions b₁,b₂),(RealVectSpace b₁,b₂)),(Add_ (BoundedFunctions b₁,b₂),(RealVectSpace b₁,b₂)),(Mult_ (BoundedFunctions b₁,b₂),(RealVectSpace b₁,b₂)) #) is Subspace of RealVectSpace b₁,b₂

proof end;

registration

let c₁ be non empty set ;
let c₂ be RealNormSpace;
cluster RLSStruct(# (BoundedFunctions a₁,a₂),(Zero_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)),(Add_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)),(Mult_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)) #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence by Th8;

end;

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
func R_VectorSpace_of_BoundedFunctions c₁,c₂ -> RealLinearSpace equals :: RSSPACE4:def 6
RLSStruct(# (BoundedFunctions a₁,a₂),(Zero_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)),(Add_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)),(Mult_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)) #);
coherence ;

end;

:: deftheorem Def6 defines R_VectorSpace_of_BoundedFunctions RSSPACE4:def 6 :

registration

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

end;

theorem Th9: :: RSSPACE4:9

canceled;

theorem Th10: :: RSSPACE4:10

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄, b₅ being VECTOR of (R_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 Th11: :: RSSPACE4:11

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being VECTOR of (R_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 Real holds
( b₄ = b₇ * b₃ iff for b₈ being Element of b₁ holds b₆ . b₈ = b₇ * (b₅ . b₈) )

proof end;

theorem Th12: :: RSSPACE4:12

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
let c₃ be set ;
assume E20: c₃ in BoundedFunctions c₁,c₂ ;
func modetrans c₃,c₁,c₂ -> bounded Function of a₁,the carrier of a₂ equals :Def7: :: RSSPACE4:def 7
a₃;
coherence by E20, Def5;

end;

:: deftheorem Def7 defines modetrans RSSPACE4:def 7 :

definition

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

proof end;

end;

:: deftheorem Def8 defines PreNorms RSSPACE4:def 8 :

theorem Th13: :: RSSPACE4:13

for b₁ being non empty set
for b₂ being RealNormSpace
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 Th14: :: RSSPACE4:14

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

proof end;

theorem Th15: :: RSSPACE4:15

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
func BoundedFunctionsNorm c₁,c₂ -> Function of BoundedFunctions a₁,a₂, REAL means :Def9: :: RSSPACE4:def 9
for b₁ being set st b₁ in BoundedFunctions a₁,a₂ holds
a₃ . b₁ = sup (PreNorms (modetrans b₁,a₁,a₂));
existence by Th15;
uniqueness

proof end;

end;

:: deftheorem Def9 defines BoundedFunctionsNorm RSSPACE4:def 9 :

theorem Th16: :: RSSPACE4:16

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

proof end;

theorem Th17: :: RSSPACE4:17

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be RealNormSpace;
func R_NormSpace_of_BoundedFunctions c₁,c₂ -> non empty NORMSTR equals :: RSSPACE4:def 10
NORMSTR(# (BoundedFunctions a₁,a₂),(Zero_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)),(Add_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)),(Mult_ (BoundedFunctions a₁,a₂),(RealVectSpace a₁,a₂)),(BoundedFunctionsNorm a₁,a₂) #);
coherence ;

end;

:: deftheorem Def10 defines R_NormSpace_of_BoundedFunctions RSSPACE4:def 10 :

theorem Th18: :: RSSPACE4:18

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

proof end;

theorem Th19: :: RSSPACE4:19

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃ being Point of (R_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 Th20: :: RSSPACE4:20

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

proof end;

theorem Th21: :: RSSPACE4:21

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

proof end;

theorem Th22: :: RSSPACE4:22

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄, b₅ being Point of (R_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 Th23: :: RSSPACE4:23

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being Point of (R_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 Real holds
( b₄ = b₇ * b₃ iff for b₈ being Element of b₁ holds b₆ . b₈ = b₇ * (b₅ . b₈) )

proof end;

theorem Th24: :: RSSPACE4:24

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄ being Point of (R_NormSpace_of_BoundedFunctions b₁,b₂)
for b₅ being Real holds
( ( ||.b₃.|| = 0 implies b₃ = 0. (R_NormSpace_of_BoundedFunctions b₁,b₂) ) & ( b₃ = 0. (R_NormSpace_of_BoundedFunctions b₁,b₂) implies ||.b₃.|| = 0 ) & ||.(b₅ * b₃).|| = (abs b₅) * ||.b₃.|| & ||.(b₃ + b₄).|| <= ||.b₃.|| + ||.b₄.|| )

proof end;

theorem Th25: :: RSSPACE4:25

for b₁ being non empty set
for b₂ being RealNormSpace holds R_NormSpace_of_BoundedFunctions b₁,b₂ is RealNormSpace-like

proof end;

theorem Th26: :: RSSPACE4:26

for b₁ being non empty set
for b₂ being RealNormSpace holds R_NormSpace_of_BoundedFunctions b₁,b₂ is RealNormSpace

proof end;

registration

let c₁ be non empty set ;
let c₂ be RealNormSpace;
cluster R_NormSpace_of_BoundedFunctions a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealNormSpace-like ;
coherence by Th26;

end;

theorem Th27: :: RSSPACE4:27

for b₁ being non empty set
for b₂ being RealNormSpace
for b₃, b₄, b₅ being Point of (R_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;

Lemma35: 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 Th28: :: RSSPACE4:28

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

proof end;

theorem Th29: :: RSSPACE4:29

for b₁ being non empty set
for b₂ being RealBanachSpace holds R_NormSpace_of_BoundedFunctions b₁,b₂ is RealBanachSpace

proof end;

registration

let c₁ be non empty set ;
let c₂ be RealBanachSpace;
cluster R_NormSpace_of_BoundedFunctions a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealNormSpace-like complete ;
coherence by Th29;

end;