:: Banach Space of Bounded Linear Operators
:: by Yasunari Shidama
::
:: Received December 22, 2003
:: Copyright (c) 2003 Association of Mizar Users

begin

definition

let X be set ;
let Y be non empty set ;
let F be Function of [:REAL ,Y:],Y;
let a be real number ;
let f be Function of X,Y;
:: original: [;]
redefine func F [;] a,f -> Element of Funcs X,Y;
coherence
F [;] a,f is Element of Funcs X,Y

proof end;

end;

theorem Th1: :: LOPBAN_1:1

for X being non empty set
for Y being non empty addLoopStr ex ADD being BinOp of Funcs X,the carrier of Y st
for f, g being Element of Funcs X,the carrier of Y holds ADD . f,g = the addF of Y .: f,g

proof end;

theorem Th2: :: LOPBAN_1:2

for X being non empty set
for Y being RealLinearSpace ex MULT being Function of [:REAL ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y st
for r being Real
for f being Element of Funcs X,the carrier of Y
for s being Element of X holds (MULT . [r,f]) . s = r * (f . s)

proof end;

definition

let X be non empty set ;
let Y be non empty addLoopStr ;
func FuncAdd X,Y -> BinOp of Funcs X,the carrier of Y means :Def1: :: LOPBAN_1:def 1
for f, g being Element of Funcs X,the carrier of Y holds it . f,g = the addF of Y .: f,g;
existence
ex b₁ being BinOp of Funcs X,the carrier of Y st
for f, g being Element of Funcs X,the carrier of Y holds b₁ . f,g = the addF of Y .: f,g by Th1;
uniqueness
for b₁, b₂ being BinOp of Funcs X,the carrier of Y st ( for f, g being Element of Funcs X,the carrier of Y holds b₁ . f,g = the addF of Y .: f,g ) & ( for f, g being Element of Funcs X,the carrier of Y holds b₂ . f,g = the addF of Y .: f,g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines FuncAdd LOPBAN_1:def 1 :

for X being non empty set
for Y being non empty addLoopStr
for b₃ being BinOp of Funcs X,the carrier of Y holds
( b₃ = FuncAdd X,Y iff for f, g being Element of Funcs X,the carrier of Y holds b₃ . f,g = the addF of Y .: f,g );

definition

let X be non empty set ;
let Y be RealLinearSpace;
func FuncExtMult X,Y -> Function of [:REAL ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y means :Def2: :: LOPBAN_1:def 2
for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (it . [a,f]) . x = a * (f . x);
existence
ex b₁ being Function of [:REAL ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y st
for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b₁ . [a,f]) . x = a * (f . x) by Th2;
uniqueness
for b₁, b₂ being Function of [:REAL ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y st ( for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b₁ . [a,f]) . x = a * (f . x) ) & ( for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b₂ . [a,f]) . x = a * (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines FuncExtMult LOPBAN_1:def 2 :

for X being non empty set
for Y being RealLinearSpace
for b₃ being Function of [:REAL ,(Funcs X,the carrier of Y):], Funcs X,the carrier of Y holds
( b₃ = FuncExtMult X,Y iff for a being Real
for f being Element of Funcs X,the carrier of Y
for x being Element of X holds (b₃ . [a,f]) . x = a * (f . x) );

definition

let X be set ;
let Y be non empty ZeroStr ;
func FuncZero X,Y -> Element of Funcs X,the carrier of Y equals :: LOPBAN_1:def 3
X --> (0. Y);
coherence
X --> (0. Y) is Element of Funcs X,the carrier of Y by FUNCT_2:11;

end;

:: deftheorem defines FuncZero LOPBAN_1:def 3 :

for X being set
for Y being non empty ZeroStr holds FuncZero X,Y = X --> (0. Y);

Lm1: for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f

proof end;

theorem Th3: :: LOPBAN_1:3

for X being non empty set
for Y being non empty addLoopStr
for f, g, h being Element of Funcs X,the carrier of Y holds
( h = (FuncAdd X,Y) . f,g iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem :: LOPBAN_1:4

canceled;

theorem Th5: :: LOPBAN_1:5

for X being non empty set
for Y being RealLinearSpace
for h, f being Element of Funcs X,the carrier of Y
for a being Real holds
( h = (FuncExtMult X,Y) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )

proof end;

theorem Th6: :: LOPBAN_1:6

for X being non empty set
for Y being RealLinearSpace
for f, g being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . f,g = (FuncAdd X,Y) . g,f

proof end;

theorem Th7: :: LOPBAN_1:7

for X being non empty set
for Y being RealLinearSpace
for f, g, h being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . f,((FuncAdd X,Y) . g,h) = (FuncAdd X,Y) . ((FuncAdd X,Y) . f,g),h

proof end;

theorem Th8: :: LOPBAN_1:8

for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . (FuncZero X,Y),f = f

proof end;

theorem Th9: :: LOPBAN_1:9

for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs X,the carrier of Y holds (FuncAdd X,Y) . f,((FuncExtMult X,Y) . [(- 1),f]) = FuncZero X,Y

proof end;

theorem Th10: :: LOPBAN_1:10

for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs X,the carrier of Y holds (FuncExtMult X,Y) . [1,f] = f

proof end;

theorem Th11: :: LOPBAN_1:11

for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs X,the carrier of Y
for a, b being Real holds (FuncExtMult X,Y) . [a,((FuncExtMult X,Y) . [b,f])] = (FuncExtMult X,Y) . [(a * b),f]

proof end;

theorem Th12: :: LOPBAN_1:12

for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs X,the carrier of Y
for a, b being Real holds (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [b,f]) = (FuncExtMult X,Y) . [(a + b),f]

proof end;

Lm2: for X being non empty set
for Y being RealLinearSpace
for f, g being Element of Funcs X,the carrier of Y
for a being Real holds (FuncAdd X,Y) . ((FuncExtMult X,Y) . [a,f]),((FuncExtMult X,Y) . [a,g]) = (FuncExtMult X,Y) . [a,((FuncAdd X,Y) . f,g)]

proof end;

theorem Th13: :: LOPBAN_1:13

for X being non empty set
for Y being RealLinearSpace holds RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace

proof end;

definition

let X be non empty set ;
let Y be RealLinearSpace;
func RealVectSpace X,Y -> RealLinearSpace equals :: LOPBAN_1:def 4
RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #);
coherence
RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #) is RealLinearSpace by Th13;

end;

:: deftheorem defines RealVectSpace LOPBAN_1:def 4 :

for X being non empty set
for Y being RealLinearSpace holds RealVectSpace X,Y = RLSStruct(# (Funcs X,the carrier of Y),(FuncZero X,Y),(FuncAdd X,Y),(FuncExtMult X,Y) #);

registration

let X be non empty set ;
let Y be RealLinearSpace;
cluster RealVectSpace X,Y -> strict ;
coherence
RealVectSpace X,Y is strict ;

end;

registration

let X be non empty set ;
let Y be RealLinearSpace;
cluster RealVectSpace X,Y -> constituted-Functions ;
coherence
RealVectSpace X,Y is constituted-Functions by MONOID_0:89;

end;

definition

let X be non empty set ;
let Y be RealLinearSpace;
let f be VECTOR of ;
let x be Element of X;
:: original: .
redefine func f . x -> VECTOR of ;
coherence
f . x is VECTOR of

proof end;

end;

theorem :: LOPBAN_1:14

for X being non empty set
for Y being RealLinearSpace
for f, g, h being VECTOR of holds
( h = f + g iff for x being Element of X holds h . x = (f . x) + (g . x) ) by Th3;

theorem :: LOPBAN_1:15

for X being non empty set
for Y being RealLinearSpace
for f, h being VECTOR of
for a being Real holds
( h = a * f iff for x being Element of X holds h . x = a * (f . x) ) by Th5;

theorem :: LOPBAN_1:16

for X being non empty set
for Y being RealLinearSpace holds 0. (RealVectSpace X,Y) = X --> (0. Y) ;

begin

definition

let X be non empty RLSStruct ;
let Y be non empty addLoopStr ;
let IT be Function of X,Y;
attr IT is additive means :Def5: :: LOPBAN_1:def 5
for x, y being VECTOR of holds IT . (x + y) = (IT . x) + (IT . y);

end;

:: deftheorem Def5 defines additive LOPBAN_1:def 5 :

for X being non empty RLSStruct
for Y being non empty addLoopStr
for IT being Function of X,Y holds
( IT is additive iff for x, y being VECTOR of holds IT . (x + y) = (IT . x) + (IT . y) );

definition

let X, Y be non empty RLSStruct ;
let IT be Function of X,Y;
attr IT is homogeneous means :Def6: :: LOPBAN_1:def 6
for x being VECTOR of
for r being Real holds IT . (r * x) = r * (IT . x);

end;

:: deftheorem Def6 defines homogeneous LOPBAN_1:def 6 :

for X, Y being non empty RLSStruct
for IT being Function of X,Y holds
( IT is homogeneous iff for x being VECTOR of
for r being Real holds IT . (r * x) = r * (IT . x) );

registration

let X be non empty RLSStruct ;
let Y be RealLinearSpace;
cluster additive homogeneous Element of bool [:the carrier of X,the carrier of Y:];
existence
ex b₁ being Function of X,Y st
( b₁ is additive & b₁ is homogeneous )

proof end;

end;

definition

let X, Y be RealLinearSpace;
mode LinearOperator of X,Y is additive homogeneous Function of X,Y;

end;

definition

let X, Y be RealLinearSpace;
func LinearOperators X,Y -> Subset of means :Def7: :: LOPBAN_1:def 7
for x being set holds
( x in it iff x is LinearOperator of X,Y );
existence
ex b₁ being Subset of st
for x being set holds
( x in b₁ iff x is LinearOperator of X,Y )

proof end;

uniqueness
for b₁, b₂ being Subset of st ( for x being set holds
( x in b₁ iff x is LinearOperator of X,Y ) ) & ( for x being set holds
( x in b₂ iff x is LinearOperator of X,Y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines LinearOperators LOPBAN_1:def 7 :

for X, Y being RealLinearSpace
for b₃ being Subset of holds
( b₃ = LinearOperators X,Y iff for x being set holds
( x in b₃ iff x is LinearOperator of X,Y ) );

registration

let X, Y be RealLinearSpace;
cluster LinearOperators X,Y -> non empty functional ;
coherence
( not LinearOperators X,Y is empty & LinearOperators X,Y is functional )

proof end;

end;

theorem Th17: :: LOPBAN_1:17

for X, Y being RealLinearSpace holds LinearOperators X,Y is linearly-closed

proof end;

theorem :: LOPBAN_1:18

for X, Y being RealLinearSpace holds RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is Subspace of RealVectSpace the carrier of X,Y by Th17, RSSPACE:13;

registration

let X, Y be RealLinearSpace;
cluster RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) -> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like ;
coherence
( RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is Abelian & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is add-associative & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is right_zeroed & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is right_complementable & RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is RealLinearSpace-like ) by Th17, RSSPACE:13;

end;

definition

let X, Y be RealLinearSpace;
func R_VectorSpace_of_LinearOperators X,Y -> RealLinearSpace equals :: LOPBAN_1:def 8
RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #);
coherence
RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #) is RealLinearSpace ;

end;

:: deftheorem defines R_VectorSpace_of_LinearOperators LOPBAN_1:def 8 :

for X, Y being RealLinearSpace holds R_VectorSpace_of_LinearOperators X,Y = RLSStruct(# (LinearOperators X,Y),(Zero_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Add_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)),(Mult_ (LinearOperators X,Y),(RealVectSpace the carrier of X,Y)) #);

registration

let X, Y be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators X,Y -> strict ;
coherence
R_VectorSpace_of_LinearOperators X,Y is strict ;

end;

registration

let X, Y be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators X,Y -> constituted-Functions ;
coherence
R_VectorSpace_of_LinearOperators X,Y is constituted-Functions by MONOID_0:89;

end;

definition

let X, Y be RealLinearSpace;
let f be Element of ;
let v be VECTOR of ;
:: original: .
redefine func f . v -> VECTOR of ;
coherence
f . v is VECTOR of

proof end;

end;

theorem :: LOPBAN_1:19

canceled;

theorem Th20: :: LOPBAN_1:20

for X, Y being RealLinearSpace
for f, g, h being VECTOR of holds
( h = f + g iff for x being VECTOR of holds h . x = (f . x) + (g . x) )

proof end;

theorem Th21: :: LOPBAN_1:21

for X, Y being RealLinearSpace
for f, h being VECTOR of
for a being Real holds
( h = a * f iff for x being VECTOR of holds h . x = a * (f . x) )

proof end;

theorem Th22: :: LOPBAN_1:22

for X, Y being RealLinearSpace holds 0. (R_VectorSpace_of_LinearOperators X,Y) = the carrier of X --> (0. Y)

proof end;

theorem Th23: :: LOPBAN_1:23

for X, Y being RealLinearSpace holds the carrier of X --> (0. Y) is LinearOperator of X,Y

proof end;

begin

theorem Th24: :: LOPBAN_1:24

for X being RealNormSpace
for seq being sequence of X
for g being Point of st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )

proof end;

definition

let X, Y be RealNormSpace;
let IT be LinearOperator of X,Y;
attr IT is bounded means :Def9: :: LOPBAN_1:def 9
ex K being Real st
( 0 <= K & ( for x being VECTOR of holds ||.(IT . x).|| <= K * ||.x.|| ) );

end;

:: deftheorem Def9 defines bounded LOPBAN_1:def 9 :

for X, Y being RealNormSpace
for IT being LinearOperator of X,Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being VECTOR of holds ||.(IT . x).|| <= K * ||.x.|| ) ) );

theorem Th25: :: LOPBAN_1:25

for X, Y being RealNormSpace
for f being LinearOperator of X,Y st ( for x being VECTOR of holds f . x = 0. Y ) holds
f is bounded

proof end;

registration

let X, Y be RealNormSpace;
cluster bounded Element of bool [:the carrier of X,the carrier of Y:];
existence
ex b₁ being LinearOperator of X,Y st b₁ is bounded

proof end;

end;

definition

let X, Y be RealNormSpace;
func BoundedLinearOperators X,Y -> Subset of means :Def10: :: LOPBAN_1:def 10
for x being set holds
( x in it iff x is bounded LinearOperator of X,Y );
existence
ex b₁ being Subset of st
for x being set holds
( x in b₁ iff x is bounded LinearOperator of X,Y )

proof end;

uniqueness
for b₁, b₂ being Subset of st ( for x being set holds
( x in b₁ iff x is bounded LinearOperator of X,Y ) ) & ( for x being set holds
( x in b₂ iff x is bounded LinearOperator of X,Y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines BoundedLinearOperators LOPBAN_1:def 10 :

for X, Y being RealNormSpace
for b₃ being Subset of holds
( b₃ = BoundedLinearOperators X,Y iff for x being set holds
( x in b₃ iff x is bounded LinearOperator of X,Y ) );

registration

let X, Y be RealNormSpace;
cluster BoundedLinearOperators X,Y -> non empty ;
coherence
not BoundedLinearOperators X,Y is empty

proof end;

end;

theorem Th26: :: LOPBAN_1:26

for X, Y being RealNormSpace holds BoundedLinearOperators X,Y is linearly-closed

proof end;

theorem :: LOPBAN_1:27

for X, Y being RealNormSpace holds RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is Subspace of R_VectorSpace_of_LinearOperators X,Y by Th26, RSSPACE:13;

registration

let X, Y be RealNormSpace;
cluster RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) -> right_complementable Abelian add-associative right_zeroed RealLinearSpace-like ;
coherence
( RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is Abelian & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is add-associative & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is right_zeroed & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is right_complementable & RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is RealLinearSpace-like ) by Th26, RSSPACE:13;

end;

definition

let X, Y be RealNormSpace;
func R_VectorSpace_of_BoundedLinearOperators X,Y -> RealLinearSpace equals :: LOPBAN_1:def 11
RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #);
coherence
RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is RealLinearSpace ;

end;

:: deftheorem defines R_VectorSpace_of_BoundedLinearOperators LOPBAN_1:def 11 :

for X, Y being RealNormSpace holds R_VectorSpace_of_BoundedLinearOperators X,Y = RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #);

registration

let X, Y be RealNormSpace;
cluster R_VectorSpace_of_BoundedLinearOperators X,Y -> strict ;
coherence
R_VectorSpace_of_BoundedLinearOperators X,Y is strict ;

end;

registration

let X, Y be RealNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (R_VectorSpace_of_BoundedLinearOperators X,Y);
coherence
for b₁ being Element of holds
( b₁ is Function-like & b₁ is Relation-like ) ;

end;

definition

let X, Y be RealNormSpace;
let f be Element of ;
let v be VECTOR of ;
:: original: .
redefine func f . v -> VECTOR of ;
coherence
f . v is VECTOR of

proof end;

end;

theorem :: LOPBAN_1:28

canceled;

theorem Th29: :: LOPBAN_1:29

for X, Y being RealNormSpace
for f, g, h being VECTOR of holds
( h = f + g iff for x being VECTOR of holds h . x = (f . x) + (g . x) )

proof end;

theorem Th30: :: LOPBAN_1:30

for X, Y being RealNormSpace
for f, h being VECTOR of
for a being Real holds
( h = a * f iff for x being VECTOR of holds h . x = a * (f . x) )

proof end;

theorem Th31: :: LOPBAN_1:31

for X, Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedLinearOperators X,Y) = the carrier of X --> (0. Y)

proof end;

definition

let X, Y be RealNormSpace;
let f be set ;
assume A1: f in BoundedLinearOperators X,Y ;
func modetrans f,X,Y -> bounded LinearOperator of X,Y equals :Def12: :: LOPBAN_1:def 12
f;
coherence
f is bounded LinearOperator of X,Y by A1, Def10;

end;

:: deftheorem Def12 defines modetrans LOPBAN_1:def 12 :

for X, Y being RealNormSpace
for f being set st f in BoundedLinearOperators X,Y holds
modetrans f,X,Y = f;

definition

let X, Y be RealNormSpace;
let u be LinearOperator of X,Y;
func PreNorms u -> non empty Subset of equals :: LOPBAN_1:def 13
{ ||.(u . t).|| where t is VECTOR of : ||.t.|| <= 1 } ;
coherence
{ ||.(u . t).|| where t is VECTOR of : ||.t.|| <= 1 } is non empty Subset of

proof end;

end;

:: deftheorem defines PreNorms LOPBAN_1:def 13 :

for X, Y being RealNormSpace
for u being LinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of : ||.t.|| <= 1 } ;

theorem Th32: :: LOPBAN_1:32

for X, Y being RealNormSpace
for g being bounded LinearOperator of X,Y holds
( not PreNorms g is empty & PreNorms g is bounded_above )

proof end;

theorem :: LOPBAN_1:33

for X, Y being RealNormSpace
for g being LinearOperator of X,Y holds
( g is bounded iff PreNorms g is bounded_above )

proof end;

theorem Th34: :: LOPBAN_1:34

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

proof end;

definition

let X, Y be RealNormSpace;
func BoundedLinearOperatorsNorm X,Y -> Function of BoundedLinearOperators X,Y, REAL means :Def14: :: LOPBAN_1:def 14
for x being set st x in BoundedLinearOperators X,Y holds
it . x = sup (PreNorms (modetrans x,X,Y));
existence
ex b₁ being Function of BoundedLinearOperators X,Y, REAL st
for x being set st x in BoundedLinearOperators X,Y holds
b₁ . x = sup (PreNorms (modetrans x,X,Y)) by Th34;
uniqueness
for b₁, b₂ being Function of BoundedLinearOperators X,Y, REAL st ( for x being set st x in BoundedLinearOperators X,Y holds
b₁ . x = sup (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in BoundedLinearOperators X,Y holds
b₂ . x = sup (PreNorms (modetrans x,X,Y)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines BoundedLinearOperatorsNorm LOPBAN_1:def 14 :

for X, Y being RealNormSpace
for b₃ being Function of BoundedLinearOperators X,Y, REAL holds
( b₃ = BoundedLinearOperatorsNorm X,Y iff for x being set st x in BoundedLinearOperators X,Y holds
b₃ . x = sup (PreNorms (modetrans x,X,Y)) );

theorem Th35: :: LOPBAN_1:35

for X, Y being RealNormSpace
for f being bounded LinearOperator of X,Y holds modetrans f,X,Y = f

proof end;

theorem Th36: :: LOPBAN_1:36

for X, Y being RealNormSpace
for f being bounded LinearOperator of X,Y holds (BoundedLinearOperatorsNorm X,Y) . f = sup (PreNorms f)

proof end;

definition

let X, Y be RealNormSpace;
func R_NormSpace_of_BoundedLinearOperators X,Y -> non empty NORMSTR equals :: LOPBAN_1:def 15
NORMSTR(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(BoundedLinearOperatorsNorm X,Y) #);
coherence
NORMSTR(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(BoundedLinearOperatorsNorm X,Y) #) is non empty NORMSTR ;

end;

:: deftheorem defines R_NormSpace_of_BoundedLinearOperators LOPBAN_1:def 15 :

for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators X,Y = NORMSTR(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(BoundedLinearOperatorsNorm X,Y) #);

theorem Th37: :: LOPBAN_1:37

for X, Y being RealNormSpace holds the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators X,Y)

proof end;

theorem Th38: :: LOPBAN_1:38

for X, Y being RealNormSpace
for f being Point of
for g being bounded LinearOperator of X,Y st g = f holds
for t being VECTOR of holds ||.(g . t).|| <= ||.f.|| * ||.t.||

proof end;

theorem Th39: :: LOPBAN_1:39

for X, Y being RealNormSpace
for f being Point of holds 0 <= ||.f.||

proof end;

theorem Th40: :: LOPBAN_1:40

for X, Y being RealNormSpace
for f being Point of st f = 0. (R_NormSpace_of_BoundedLinearOperators X,Y) holds
0 = ||.f.||

proof end;

registration

let X, Y be RealNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators X,Y);
coherence
for b₁ being Element of holds
( b₁ is Function-like & b₁ is Relation-like ) ;

end;

definition

let X, Y be RealNormSpace;
let f be Element of ;
let v be VECTOR of ;
:: original: .
redefine func f . v -> VECTOR of ;
coherence
f . v is VECTOR of

proof end;

end;

theorem Th41: :: LOPBAN_1:41

for X, Y being RealNormSpace
for f, g, h being Point of holds
( h = f + g iff for x being VECTOR of holds h . x = (f . x) + (g . x) )

proof end;

theorem Th42: :: LOPBAN_1:42

for X, Y being RealNormSpace
for f, h being Point of
for a being Real holds
( h = a * f iff for x being VECTOR of holds h . x = a * (f . x) )

proof end;

theorem Th43: :: LOPBAN_1:43

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

proof end;

theorem Th44: :: LOPBAN_1:44

for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators X,Y is RealNormSpace-like

proof end;

theorem Th45: :: LOPBAN_1:45

for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators X,Y is RealNormSpace

proof end;

registration

let X, Y be RealNormSpace;
cluster R_NormSpace_of_BoundedLinearOperators X,Y -> non empty right_complementable Abelian add-associative right_zeroed RealLinearSpace-like RealNormSpace-like ;
coherence
( R_NormSpace_of_BoundedLinearOperators X,Y is RealNormSpace-like & R_NormSpace_of_BoundedLinearOperators X,Y is RealLinearSpace-like & R_NormSpace_of_BoundedLinearOperators X,Y is Abelian & R_NormSpace_of_BoundedLinearOperators X,Y is add-associative & R_NormSpace_of_BoundedLinearOperators X,Y is right_zeroed & R_NormSpace_of_BoundedLinearOperators X,Y is right_complementable ) by Th45;

end;

theorem Th46: :: LOPBAN_1:46

for X, Y being RealNormSpace
for f, g, h being Point of holds
( h = f - g iff for x being VECTOR of holds h . x = (f . x) - (g . x) )

proof end;

begin

definition

let X be RealNormSpace;
attr X is complete means :Def16: :: LOPBAN_1:def 16
for seq being sequence of X st seq is CCauchy holds
seq is convergent ;

end;

:: deftheorem Def16 defines complete LOPBAN_1:def 16 :

for X being RealNormSpace holds
( X is complete iff for seq being sequence of X st seq is CCauchy holds
seq is convergent );

registration

cluster complete NORMSTR ;
existence
ex b₁ being RealNormSpace st b₁ is complete

proof end;

end;

definition

mode RealBanachSpace is complete RealNormSpace;

end;

Lm3: 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 Th47: :: LOPBAN_1:47

for X being RealNormSpace
for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )

proof end;

theorem Th48: :: LOPBAN_1:48

for X, Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedLinearOperators X,Y) st seq is CCauchy holds
seq is convergent

proof end;

theorem Th49: :: LOPBAN_1:49

for X being RealNormSpace
for Y being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators X,Y is RealBanachSpace

proof end;

registration

let X be RealNormSpace;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedLinearOperators X,Y -> non empty complete ;
coherence
R_NormSpace_of_BoundedLinearOperators X,Y is complete by Th49;

end;