:: Bilinear Operators on Normed Linear Spaces
:: by Kazuhisa Nakasho
::
:: Copyright (c) 2019 Association of Mizar Users

LMELM1: for X, Y being RealLinearSpace
for x being Point of X
for y being Point of Y holds [x,y] is Point of [:X,Y:]

proof end;

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 b1 being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) st
for x being set holds
( x in b1 iff x is BilinearOperator of X,Y,Z )
proof end;
uniqueness
for b1, b2 being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) st ( for x being set holds
( x in b1 iff x is BilinearOperator of X,Y,Z ) ) & ( for x being set holds
( x in b2 iff x is BilinearOperator of X,Y,Z ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines BilinearOperators LOPBAN_9:def 1 :
for X, Y, Z being RealLinearSpace
for b4 being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) holds
( b4 = BilinearOperators (X,Y,Z) iff for x being set holds
( x in b4 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;
end;

registration
let X, Y, Z be RealLinearSpace;
coherence 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 ();
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 () 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 ()
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. () = 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 ;

LMELM2: for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y holds [x,y] is Point of [:X,Y:]

proof end;

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 * ) * ) );
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 * ) * ) ) );

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 ;

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 b1 being BilinearOperator of X,Y,Z st b1 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 () 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 b1 being Subset of () st
for x being set holds
( x in b1 iff x is Lipschitzian BilinearOperator of X,Y,Z )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for x being set holds
( x in b1 iff x is Lipschitzian BilinearOperator of X,Y,Z ) ) & ( for x being set holds
( x in b2 iff x is Lipschitzian BilinearOperator of X,Y,Z ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines BoundedBilinearOperators LOPBAN_9:def 4 :
for X, Y, Z being RealNormSpace
for b4 being Subset of () holds
( b4 = BoundedBilinearOperators (X,Y,Z) iff for x being set holds
( x in b4 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;
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)),())),(Add_ ((BoundedBilinearOperators (X,Y,Z)),())),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),())) #);
coherence
RLSStruct(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),())),(Add_ ((BoundedBilinearOperators (X,Y,Z)),())),(Mult_ ((BoundedBilinearOperators (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)),())),(Add_ ((BoundedBilinearOperators (X,Y,Z)),())),(Mult_ ((BoundedBilinearOperators (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;
coherence
not R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is empty
;
end;

registration
let X, Y, Z be RealNormSpace;
end;

registration
let X, Y, Z be RealNormSpace;
coherence by MONOID_0:80;
end;

definition
let X, Y, Z be RealNormSpace;
let f be Element of ;
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 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
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. = 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 ;
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 : ( <= 1 & <= 1 ) } ;
coherence
{ ||.(u . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( <= 1 & <= 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 : ( <= 1 & <= 1 ) } ;

registration
let X, Y, Z be RealNormSpace;
let g be Lipschitzian BilinearOperator of X,Y,Z;
coherence
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 b1 being Function of (BoundedBilinearOperators (X,Y,Z)),REAL st
for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y,Z)))
proof end;
uniqueness
for b1, b2 being Function of (BoundedBilinearOperators (X,Y,Z)),REAL st ( for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ) & ( for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines BoundedBilinearOperatorsNorm LOPBAN_9:def 8 :
for X, Y, Z being RealNormSpace
for b4 being Function of (BoundedBilinearOperators (X,Y,Z)),REAL holds
( b4 = BoundedBilinearOperatorsNorm (X,Y,Z) iff for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
b4 . 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 ()
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)),())),(Add_ ((BoundedBilinearOperators (X,Y,Z)),())),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),())),(BoundedBilinearOperatorsNorm (X,Y,Z)) #);
coherence
NORMSTR(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),())),(Add_ ((BoundedBilinearOperators (X,Y,Z)),())),(Mult_ ((BoundedBilinearOperators (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)),())),(Add_ ((BoundedBilinearOperators (X,Y,Z)),())),(Mult_ ((BoundedBilinearOperators (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. ()
proof end;

theorem Th32: :: LOPBAN_9:16
for X, Y, Z being RealNormSpace
for f being Point of ()
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)).|| <= () *
proof end;

theorem Th33: :: LOPBAN_9:17
for X, Y, Z being RealNormSpace
for f being Point of () holds 0 <=
proof end;

theorem Th34: :: LOPBAN_9:18
for X, Y, Z being RealNormSpace
for f being Point of () st f = 0. () holds
0 =
proof end;

registration
let X, Y, Z be RealNormSpace;
cluster -> Relation-like Function-like for Element of the carrier of ();
coherence
for b1 being Element of () holds
( b1 is Function-like & b1 is Relation-like )
;
end;

definition
let X, Y, Z be RealNormSpace;
let f be Element of ();
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 () 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 ()
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 ()
for a being Real holds
( ( = 0 implies f = 0. () ) & ( f = 0. () implies = 0 ) & ||.(a * f).|| = |.a.| * & ||.(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;
coherence 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;
coherence by Th39;
end;

theorem Th40: :: LOPBAN_9:23
for X, Y, Z being RealNormSpace
for f, g, h being Point of () 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 () 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;
coherence by Th43;
end;

theorem :: LOPBAN_9:26
for X, Y, Z being RealLinearSpace ex I being LinearOperator of ,() st
( I is bijective & ( for u being Point of
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 ,() st
( I is bijective & ( for u being Point of holds
( = ||.(I . u).|| & ( for x being Point of X
for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) )
proof end;