:: Bilinear Operators on Normed Linear Spaces
:: by Kazuhisa Nakasho
::
:: Received February 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

definition

let X, Y, Z be RealLinearSpace;

func BilinearOperators (X,Y,Z) -> Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) means :Def6: :: LOPBAN_9:def 1
for x being set holds
( x in it iff x is BilinearOperator of X,Y,Z );

existence
ex b₁ being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) st
for x being set holds
( x in b₁ iff x is BilinearOperator of X,Y,Z )

proof end;

uniqueness
for b₁, b₂ being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) st ( for x being set holds
( x in b₁ iff x is BilinearOperator of X,Y,Z ) ) & ( for x being set holds
( x in b₂ iff x is BilinearOperator of X,Y,Z ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines BilinearOperators LOPBAN_9:def 1 :
for X, Y, Z being RealLinearSpace
for b₄ being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) holds
( b₄ = BilinearOperators (X,Y,Z) iff for x being set holds
( x in b₄ iff x is BilinearOperator of X,Y,Z ) );

registration

let X, Y, Z be RealLinearSpace;

cluster BilinearOperators (X,Y,Z) -> non empty functional ;

coherence
( not BilinearOperators (X,Y,Z) is empty & BilinearOperators (X,Y,Z) is functional )

proof end;

end;

LM14: for X being RealLinearSpace
for x1, x2, x3, x4 being Point of X holds (x1 + x2) + (x3 + x4) = (x1 + x3) + (x2 + x4)

proof end;

Th14: for X, Y, Z being RealLinearSpace holds BilinearOperators (X,Y,Z) is linearly-closed

proof end;

registration

let X, Y, Z be RealLinearSpace;

cluster BilinearOperators (X,Y,Z) -> linearly-closed ;

coherence
BilinearOperators (X,Y,Z) is linearly-closed by Th14;

end;

definition

let X, Y, Z be RealLinearSpace;

func R_VectorSpace_of_BilinearOperators (X,Y,Z) -> strict RLSStruct equals :: LOPBAN_9:def 2
RLSStruct(# (BilinearOperators (X,Y,Z)),(Zero_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))),(Add_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))),(Mult_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))) #);

coherence
RLSStruct(# (BilinearOperators (X,Y,Z)),(Zero_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))),(Add_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))),(Mult_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))) #) is strict RLSStruct ;

end;

:: deftheorem defines R_VectorSpace_of_BilinearOperators LOPBAN_9:def 2 :
for X, Y, Z being RealLinearSpace holds R_VectorSpace_of_BilinearOperators (X,Y,Z) = RLSStruct(# (BilinearOperators (X,Y,Z)),(Zero_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))),(Add_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))),(Mult_ ((BilinearOperators (X,Y,Z)),(RealVectSpace ( the carrier of [:X,Y:],Z)))) #);

registration

let X, Y, Z be RealLinearSpace;

cluster R_VectorSpace_of_BilinearOperators (X,Y,Z) -> non empty strict ;

coherence
not R_VectorSpace_of_BilinearOperators (X,Y,Z) is empty ;

end;

registration

let X, Y, Z be RealLinearSpace;

cluster R_VectorSpace_of_BilinearOperators (X,Y,Z) -> right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( R_VectorSpace_of_BilinearOperators (X,Y,Z) is Abelian & R_VectorSpace_of_BilinearOperators (X,Y,Z) is add-associative & R_VectorSpace_of_BilinearOperators (X,Y,Z) is right_zeroed & R_VectorSpace_of_BilinearOperators (X,Y,Z) is right_complementable & R_VectorSpace_of_BilinearOperators (X,Y,Z) is vector-distributive & R_VectorSpace_of_BilinearOperators (X,Y,Z) is scalar-distributive & R_VectorSpace_of_BilinearOperators (X,Y,Z) is scalar-associative & R_VectorSpace_of_BilinearOperators (X,Y,Z) is scalar-unital ) by RSSPACE:11;

end;

registration

let X, Y, Z be RealLinearSpace;

cluster R_VectorSpace_of_BilinearOperators (X,Y,Z) -> strict constituted-Functions ;

coherence
R_VectorSpace_of_BilinearOperators (X,Y,Z) is constituted-Functions by MONOID_0:80;

end;

theorem :: LOPBAN_9:1

for X, Y, Z being RealLinearSpace holds R_VectorSpace_of_BilinearOperators (X,Y,Z) is Subspace of RealVectSpace ( the carrier of [:X,Y:],Z) by RSSPACE:11;

definition

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

proof end;

end;

theorem Th16: :: LOPBAN_9:2

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

proof end;

theorem Th17: :: LOPBAN_9:3

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

proof end;

theorem Th18: :: LOPBAN_9:4

for X, Y, Z being RealLinearSpace holds 0. (R_VectorSpace_of_BilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z)

proof end;

theorem :: LOPBAN_9:5

for X, Y, Z being RealLinearSpace holds the carrier of [:X,Y:] --> (0. Z) is BilinearOperator of X,Y,Z by LOPBAN_8:9, LOPBAN_8:def 2;

definition

let X, Y, Z be RealNormSpace;
let IT be BilinearOperator of X,Y,Z;

attr IT is Lipschitzian means :Def8: :: LOPBAN_9:def 3
ex K being Real st
( 0 <= K & ( for x being VECTOR of X
for y being VECTOR of Y holds ||.(IT . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) );

end;

:: deftheorem Def8 defines Lipschitzian LOPBAN_9:def 3 :
for X, Y, Z being RealNormSpace
for IT being BilinearOperator of X,Y,Z holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K & ( for x being VECTOR of X
for y being VECTOR of Y holds ||.(IT . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) );

theorem Th21: :: LOPBAN_9:6

for X, Y, Z being RealNormSpace
for f being BilinearOperator of X,Y,Z st ( for x being VECTOR of X
for y being VECTOR of Y holds f . (x,y) = 0. Z ) holds
f is Lipschitzian

proof end;

theorem :: LOPBAN_9:7

for X, Y, Z being RealNormSpace holds the carrier of [:X,Y:] --> (0. Z) is BilinearOperator of X,Y,Z by LOPBAN_8:9, LOPBAN_8:def 3;

registration

let X, Y, Z be RealNormSpace;

cluster Relation-like the carrier of [:X,Y:] -defined the carrier of Z -valued non empty Function-like V28( the carrier of [:X,Y:]) quasi_total Bilinear Lipschitzian for Element of bool [: the carrier of [:X,Y:], the carrier of Z:];

existence
ex b₁ being BilinearOperator of X,Y,Z st b₁ is Lipschitzian

proof end;

end;

theorem EQSET: :: LOPBAN_9:8

for X, Y, Z being RealNormSpace
for z being object holds
( z in BilinearOperators (X,Y,Z) iff z is BilinearOperator of X,Y,Z )

proof end;

definition

let X, Y, Z be RealNormSpace;

func BoundedBilinearOperators (X,Y,Z) -> Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) means :Def9: :: LOPBAN_9:def 4
for x being set holds
( x in it iff x is Lipschitzian BilinearOperator of X,Y,Z );

existence
ex b₁ being Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) st
for x being set holds
( x in b₁ iff x is Lipschitzian BilinearOperator of X,Y,Z )

proof end;

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

proof end;

end;

:: deftheorem Def9 defines BoundedBilinearOperators LOPBAN_9:def 4 :
for X, Y, Z being RealNormSpace
for b₄ being Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds
( b₄ = BoundedBilinearOperators (X,Y,Z) iff for x being set holds
( x in b₄ iff x is Lipschitzian BilinearOperator of X,Y,Z ) );

registration

let X, Y, Z be RealNormSpace;

cluster BoundedBilinearOperators (X,Y,Z) -> non empty ;

coherence
not BoundedBilinearOperators (X,Y,Z) is empty

proof end;

end;

registration

let X, Y, Z be RealNormSpace;

cluster BoundedBilinearOperators (X,Y,Z) -> linearly-closed ;

coherence
BoundedBilinearOperators (X,Y,Z) is linearly-closed

proof end;

end;

definition

let X, Y, Z be RealNormSpace;

func R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) -> strict RLSStruct equals :: LOPBAN_9:def 5
RLSStruct(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Add_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))) #);

coherence
RLSStruct(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Add_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))) #) is strict RLSStruct ;

end;

:: deftheorem defines R_VectorSpace_of_BoundedBilinearOperators LOPBAN_9:def 5 :
for X, Y, Z being RealNormSpace holds R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) = RLSStruct(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Add_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))) #);

theorem :: LOPBAN_9:9

for X, Y, Z being RealNormSpace holds R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is Subspace of R_VectorSpace_of_BilinearOperators (X,Y,Z) by RSSPACE:11;

registration

let X, Y, Z be RealNormSpace;

cluster R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) -> non empty strict ;

coherence
not R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is empty ;

end;

registration

let X, Y, Z be RealNormSpace;

cluster R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) -> right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is Abelian & R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is add-associative & R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is right_zeroed & R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is right_complementable & R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is vector-distributive & R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is scalar-distributive & R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is scalar-associative & R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is scalar-unital ) by RSSPACE:11;

end;

registration

let X, Y, Z be RealNormSpace;

cluster R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) -> strict constituted-Functions ;

coherence
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is constituted-Functions by MONOID_0:80;

end;

definition

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

proof end;

end;

theorem Th24: :: LOPBAN_9:10

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

proof end;

theorem Th25: :: LOPBAN_9:11

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

proof end;

theorem Th26: :: LOPBAN_9:12

for X, Y, Z being RealNormSpace holds 0. (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) = the carrier of [:X,Y:] --> (0. Z)

proof end;

definition

let X, Y, Z be RealNormSpace;
let f be object ;
assume A1: f in BoundedBilinearOperators (X,Y,Z) ;

func modetrans (f,X,Y,Z) -> Lipschitzian BilinearOperator of X,Y,Z equals :Def11: :: LOPBAN_9:def 6
f;

coherence
f is Lipschitzian BilinearOperator of X,Y,Z by A1, Def9;

end;

:: deftheorem Def11 defines modetrans LOPBAN_9:def 6 :
for X, Y, Z being RealNormSpace
for f being object st f in BoundedBilinearOperators (X,Y,Z) holds
modetrans (f,X,Y,Z) = f;

definition

let X, Y, Z be RealNormSpace;
let u be BilinearOperator of X,Y,Z;

func PreNorms u -> non empty Subset of REAL equals :: LOPBAN_9:def 7
{ ||.(u . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( ||.t.|| <= 1 & ||.s.|| <= 1 ) } ;

coherence
{ ||.(u . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( ||.t.|| <= 1 & ||.s.|| <= 1 ) } is non empty Subset of REAL

proof end;

end;

:: deftheorem defines PreNorms LOPBAN_9:def 7 :
for X, Y, Z being RealNormSpace
for u being BilinearOperator of X,Y,Z holds PreNorms u = { ||.(u . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( ||.t.|| <= 1 & ||.s.|| <= 1 ) } ;

registration

let X, Y, Z be RealNormSpace;
let g be Lipschitzian BilinearOperator of X,Y,Z;

cluster PreNorms g -> non empty bounded_above ;

coherence
PreNorms g is bounded_above

proof end;

end;

theorem :: LOPBAN_9:13

for X, Y, Z being RealNormSpace
for g being BilinearOperator of X,Y,Z holds
( g is Lipschitzian iff PreNorms g is bounded_above )

proof end;

definition

let X, Y, Z be RealNormSpace;

func BoundedBilinearOperatorsNorm (X,Y,Z) -> Function of (BoundedBilinearOperators (X,Y,Z)),REAL means :Def13: :: LOPBAN_9:def 8
for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y,Z)));

existence
ex b₁ being Function of (BoundedBilinearOperators (X,Y,Z)),REAL st
for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b₁ . x = upper_bound (PreNorms (modetrans (x,X,Y,Z)))

proof end;

uniqueness
for b₁, b₂ being Function of (BoundedBilinearOperators (X,Y,Z)),REAL st ( for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b₁ . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ) & ( for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b₂ . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines BoundedBilinearOperatorsNorm LOPBAN_9:def 8 :
for X, Y, Z being RealNormSpace
for b₄ being Function of (BoundedBilinearOperators (X,Y,Z)),REAL holds
( b₄ = BoundedBilinearOperatorsNorm (X,Y,Z) iff for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b₄ . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) );

Th29: for X, Y, Z being RealNormSpace
for f being Lipschitzian BilinearOperator of X,Y,Z holds modetrans (f,X,Y,Z) = f

proof end;

registration

let X, Y, Z be RealNormSpace;
let f be Lipschitzian BilinearOperator of X,Y,Z;

reduce modetrans (f,X,Y,Z) to f;

reducibility
modetrans (f,X,Y,Z) = f by Th29;

end;

theorem Th30: :: LOPBAN_9:14

for X, Y, Z being RealNormSpace
for f being Lipschitzian BilinearOperator of X,Y,Z holds (BoundedBilinearOperatorsNorm (X,Y,Z)) . f = upper_bound (PreNorms f)

proof end;

definition

let X, Y, Z be RealNormSpace;

func R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) -> non empty NORMSTR equals :: LOPBAN_9:def 9
NORMSTR(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Add_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(BoundedBilinearOperatorsNorm (X,Y,Z)) #);

coherence
NORMSTR(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Add_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(BoundedBilinearOperatorsNorm (X,Y,Z)) #) is non empty NORMSTR ;

end;

:: deftheorem defines R_NormSpace_of_BoundedBilinearOperators LOPBAN_9:def 9 :
for X, Y, Z being RealNormSpace holds R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) = NORMSTR(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Add_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(BoundedBilinearOperatorsNorm (X,Y,Z)) #);

theorem Th31: :: LOPBAN_9:15

for X, Y, Z being RealNormSpace holds the carrier of [:X,Y:] --> (0. Z) = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))

proof end;

theorem Th32: :: LOPBAN_9:16

for X, Y, Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
for g being Lipschitzian BilinearOperator of X,Y,Z st g = f holds
for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.||

proof end;

theorem Th33: :: LOPBAN_9:17

for X, Y, Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds 0 <= ||.f.||

proof end;

theorem Th34: :: LOPBAN_9:18

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

proof end;

registration

let X, Y, Z be RealNormSpace;

cluster -> Relation-like Function-like for Element of the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));

coherence
for b₁ being Element of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds
( b₁ is Function-like & b₁ is Relation-like ) ;

end;

definition

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

proof end;

end;

theorem Th35: :: LOPBAN_9:19

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

proof end;

theorem Th36: :: LOPBAN_9:20

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

proof end;

theorem Th37: :: LOPBAN_9:21

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

proof end;

Th38: for X, Y, Z being RealNormSpace holds
( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is reflexive & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is discerning & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace-like )

proof end;

registration

let X, Y, Z be RealNormSpace;

cluster R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) -> non empty ;

coherence
not R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is empty ;

end;

registration

let X, Y, Z be RealNormSpace;

cluster R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) -> non empty discerning reflexive RealNormSpace-like ;

coherence
( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is reflexive & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is discerning & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace-like ) by Th38;

end;

theorem Th39: :: LOPBAN_9:22

for X, Y, Z being RealNormSpace holds R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace

proof end;

registration

let X, Y, Z be RealNormSpace;

cluster R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is vector-distributive & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is scalar-distributive & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is scalar-associative & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is scalar-unital & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is Abelian & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is add-associative & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is right_zeroed & R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is right_complementable ) by Th39;

end;

theorem Th40: :: LOPBAN_9:23

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

proof end;

Lm3: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e

proof end;

theorem Th42: :: LOPBAN_9:24

for X, Y, Z being RealNormSpace st Z is complete holds
for seq being sequence of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent

proof end;

theorem Th43: :: LOPBAN_9:25

for X, Y being RealNormSpace
for Z being RealBanachSpace holds R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealBanachSpace

proof end;

registration

let X, Y be RealNormSpace;
let Z be RealBanachSpace;

cluster R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) -> non empty complete ;

coherence
R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is complete by Th43;

end;

theorem :: LOPBAN_9:26

for X, Y, Z being RealLinearSpace ex I being LinearOperator of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))),(R_VectorSpace_of_BilinearOperators (X,Y,Z)) st
( I is bijective & ( for u being Point of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z))))
for x being Point of X
for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) )

proof end;

theorem :: LOPBAN_9:27

for X, Y, Z being RealNormSpace ex I being LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st
( I is bijective & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for x being Point of X
for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) )

proof end;