RSSPACE4: Banach Space of Bounded Real Sequences

:: Banach Space of Bounded Real Sequences
:: by Yasumasa Suzuki
::
:: Received January 6, 2004
:: Copyright (c) 2004 Association of Mizar Users

Lm1: for rseq being Real_Sequence
for K being real number st ( for n being Element of NAT holds rseq . n <= K ) holds
sup (rng rseq) <= K

proof end;

Lm2: for rseq being Real_Sequence st rseq is bounded holds
for n being Element of NAT holds rseq . n <= sup (rng rseq)

proof end;

definition

func the_set_of_BoundedRealSequences -> Subset of Linear_Space_of_RealSequences means :Def1: :: RSSPACE4:def 1
for x being set holds
( x in it iff ( x in the_set_of_RealSequences & seq_id x 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 -> linearly-closed ;
coherence

proof end;

end;

Lm3: 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 ) #) -> right_complementable Abelian add-associative right_zeroed 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 x being set st x in the_set_of_BoundedRealSequences holds
it . x = sup (rng (abs (seq_id x)));
existence by Lm5;
uniqueness

proof end;

end;

:: deftheorem Def2 defines linfty_norm RSSPACE4:def 2 :

Lm6: for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
( rseq is bounded & sup (rng (abs rseq)) = 0 )

proof end;

Lm7: for rseq being Real_Sequence st rseq is bounded & sup (rng (abs rseq)) = 0 holds
for n being Nat holds rseq . n = 0

proof end;

theorem :: RSSPACE4:1

canceled;

theorem :: RSSPACE4:2

for rseq being Real_Sequence holds
( ( rseq is bounded & sup (rng (abs rseq)) = 0 ) iff for n being Nat holds rseq . n = 0 ) by Lm6, Lm7;

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 #) -> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like ;
coherence by Lm4, RSSPACE3:4;

end;

definition end;

:: deftheorem defines linfty_Space RSSPACE4:def 3 :

theorem Th3: :: RSSPACE4:3

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

proof end;

theorem Th4: :: RSSPACE4:4

for x, y being Point of linfty_Space
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. linfty_Space ) & ( x = 0. linfty_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )

proof end;

registration end;

theorem :: RSSPACE4:5

for vseq being sequence of linfty_Space st vseq is CCauchy holds
vseq is convergent

proof end;

definition

let X be non empty set ;
let Y be RealNormSpace;
let IT be Function of X,the carrier of Y;
attr IT is bounded means :Def4: :: RSSPACE4:def 4
ex K being Real st
( 0 <= K & ( for x being Element of X holds ||.(IT . x).|| <= K ) );

end;

:: deftheorem Def4 defines bounded RSSPACE4:def 4 :

theorem Th6: :: RSSPACE4:6

for X being non empty set
for Y being RealNormSpace
for f being Function of X,the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded

proof end;

registration

let X be non empty set ;
let Y be RealNormSpace;
cluster bounded Relation of X,the carrier of Y;
existence

proof end;

end;

definition

let X be non empty set ;
let Y be RealNormSpace;
func BoundedFunctions X,Y -> Subset of (RealVectSpace X,Y) means :Def5: :: RSSPACE4:def 5
for x being set holds
( x in it iff x is bounded Function of X,the carrier of Y );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines BoundedFunctions RSSPACE4:def 5 :

registration

let X be non empty set ;
let Y be RealNormSpace;
cluster BoundedFunctions X,Y -> non empty ;
coherence

proof end;

end;

theorem Th7: :: RSSPACE4:7

for X being non empty set
for Y being RealNormSpace holds BoundedFunctions X,Y is linearly-closed

proof end;

theorem :: RSSPACE4:8

for X being non empty set
for Y being RealNormSpace holds RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is Subspace of RealVectSpace X,Y by Th7, RSSPACE:13;

registration

let X be non empty set ;
let Y be RealNormSpace;
cluster RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) -> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like ;
coherence by Th7, RSSPACE:13;

end;

definition

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

end;

:: deftheorem defines R_VectorSpace_of_BoundedFunctions RSSPACE4:def 6 :

registration

let X be non empty set ;
let Y be RealNormSpace;
cluster R_VectorSpace_of_BoundedFunctions X,Y -> strict ;
coherence ;

end;

theorem :: RSSPACE4:9

canceled;

theorem Th10: :: RSSPACE4:10

for X being non empty set
for Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_BoundedFunctions X,Y)
for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) )

proof end;

theorem Th11: :: RSSPACE4:11

for X being non empty set
for Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_BoundedFunctions X,Y)
for f', h' being bounded Function of X,the carrier of Y st f' = f & h' = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) )

proof end;

theorem Th12: :: RSSPACE4:12

for X being non empty set
for Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedFunctions X,Y) = X --> (0. Y)

proof end;

definition

let X be non empty set ;
let Y be RealNormSpace;
let f be set ;
assume A1: f in BoundedFunctions X,Y ;
func modetrans f,X,Y -> bounded Function of X,the carrier of Y equals :Def7: :: RSSPACE4:def 7
f;
coherence by A1, Def5;

end;

:: deftheorem Def7 defines modetrans RSSPACE4:def 7 :

definition

let X be non empty set ;
let Y be RealNormSpace;
let u be Function of X,the carrier of Y;
func PreNorms u -> non empty Subset of REAL equals :: RSSPACE4:def 8
{ ||.(u . t).|| where t is Element of X : verum } ;
coherence

proof end;

end;

:: deftheorem defines PreNorms RSSPACE4:def 8 :

theorem Th13: :: RSSPACE4:13

for X being non empty set
for Y being RealNormSpace
for g being bounded Function of X,the carrier of Y holds
( not PreNorms g is empty & PreNorms g is bounded_above )

proof end;

theorem :: RSSPACE4:14

for X being non empty set
for Y being RealNormSpace
for g being Function of X,the carrier of Y holds
( g is bounded iff PreNorms g is bounded_above )

proof end;

theorem Th15: :: RSSPACE4:15

for X being non empty set
for Y being RealNormSpace ex NORM being Function of BoundedFunctions X,Y, REAL st
for f being set st f in BoundedFunctions X,Y holds
NORM . f = sup (PreNorms (modetrans f,X,Y))

proof end;

definition

let X be non empty set ;
let Y be RealNormSpace;
func BoundedFunctionsNorm X,Y -> Function of BoundedFunctions X,Y, REAL means :Def9: :: RSSPACE4:def 9
for x being set st x in BoundedFunctions X,Y holds
it . x = sup (PreNorms (modetrans x,X,Y));
existence by Th15;
uniqueness

proof end;

end;

:: deftheorem Def9 defines BoundedFunctionsNorm RSSPACE4:def 9 :

theorem Th16: :: RSSPACE4:16

for X being non empty set
for Y being RealNormSpace
for f being bounded Function of X,the carrier of Y holds modetrans f,X,Y = f

proof end;

theorem Th17: :: RSSPACE4:17

for X being non empty set
for Y being RealNormSpace
for f being bounded Function of X,the carrier of Y holds (BoundedFunctionsNorm X,Y) . f = sup (PreNorms f)

proof end;

definition

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

end;

:: deftheorem defines R_NormSpace_of_BoundedFunctions RSSPACE4:def 10 :

theorem Th18: :: RSSPACE4:18

for X being non empty set
for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_BoundedFunctions X,Y)

proof end;

theorem Th19: :: RSSPACE4:19

for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions X,Y)
for g being bounded Function of X,the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||

proof end;

theorem :: RSSPACE4:20

for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions X,Y) holds 0 <= ||.f.||

proof end;

theorem Th21: :: RSSPACE4:21

for X being non empty set
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions X,Y) st f = 0. (R_NormSpace_of_BoundedFunctions X,Y) holds
0 = ||.f.||

proof end;

theorem Th22: :: RSSPACE4:22

for X being non empty set
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedFunctions X,Y)
for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f + g iff for x being Element of X holds h' . x = (f' . x) + (g' . x) )

proof end;

theorem Th23: :: RSSPACE4:23

for X being non empty set
for Y being RealNormSpace
for f, h being Point of (R_NormSpace_of_BoundedFunctions X,Y)
for f', h' being bounded Function of X,the carrier of Y st f' = f & h' = h holds
for a being Real holds
( h = a * f iff for x being Element of X holds h' . x = a * (f' . x) )

proof end;

theorem Th24: :: RSSPACE4:24

for X being non empty set
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_BoundedFunctions X,Y)
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedFunctions X,Y) ) & ( f = 0. (R_NormSpace_of_BoundedFunctions X,Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

proof end;

theorem Th25: :: RSSPACE4:25

for X being non empty set
for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions X,Y is RealNormSpace-like

proof end;

theorem Th26: :: RSSPACE4:26

for X being non empty set
for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions X,Y is RealNormSpace

proof end;

registration

let X be non empty set ;
let Y be RealNormSpace;
cluster R_NormSpace_of_BoundedFunctions X,Y -> non empty right_complementable Abelian add-associative right_zeroed RealLinearSpace-like RealNormSpace-like ;
coherence by Th26;

end;

theorem Th27: :: RSSPACE4:27

for X being non empty set
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedFunctions X,Y)
for f', g', h' being bounded Function of X,the carrier of Y st f' = f & g' = g & h' = h holds
( h = f - g iff for x being Element of X holds h' . x = (f' . x) - (g' . x) )

proof end;

Lm8: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e

proof end;

theorem Th28: :: RSSPACE4:28

for X being non empty set
for Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedFunctions X,Y) st seq is CCauchy holds
seq is convergent

proof end;

theorem Th29: :: RSSPACE4:29

for X being non empty set
for Y being RealBanachSpace holds R_NormSpace_of_BoundedFunctions X,Y is RealBanachSpace

proof end;

registration

let X be non empty set ;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedFunctions X,Y -> non empty complete ;
coherence by Th29;

end;