:: by Kazuhisa Nakasho

::

:: Received February 27, 2019

:: 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;

ex b_{1} being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) st

for x being set holds

( x in b_{1} iff x is BilinearOperator of X,Y,Z )

for b_{1}, b_{2} being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) st ( for x being set holds

( x in b_{1} iff x is BilinearOperator of X,Y,Z ) ) & ( for x being set holds

( x in b_{2} iff x is BilinearOperator of X,Y,Z ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is BilinearOperator of X,Y,Z );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def6 defines BilinearOperators LOPBAN_9:def 1 :

for X, Y, Z being RealLinearSpace

for b_{4} being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) holds

( b_{4} = BilinearOperators (X,Y,Z) iff for x being set holds

( x in b_{4} iff x is BilinearOperator of X,Y,Z ) );

for X, Y, Z being RealLinearSpace

for b

( b

( x in b

registration

let X, Y, Z be RealLinearSpace;

coherence

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

end;
coherence

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

proof 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
end;

definition

let X, Y, Z be RealLinearSpace;

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

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 ;

:: 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)))) #);

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
end;

registration

let X, Y, Z be RealLinearSpace;

( 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;
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;

registration

let X, Y, Z be RealLinearSpace;

coherence

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

end;
coherence

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

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

end;
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;

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

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

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;

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;

:: 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.|| ) ) );

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

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;

ex b_{1} being BilinearOperator of X,Y,Z st b_{1} is Lipschitzian

end;
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

proof 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 )

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;

ex b_{1} being Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) st

for x being set holds

( x in b_{1} iff x is Lipschitzian BilinearOperator of X,Y,Z )

for b_{1}, b_{2} being Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) st ( for x being set holds

( x in b_{1} iff x is Lipschitzian BilinearOperator of X,Y,Z ) ) & ( for x being set holds

( x in b_{2} iff x is Lipschitzian BilinearOperator of X,Y,Z ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is Lipschitzian BilinearOperator of X,Y,Z );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def9 defines BoundedBilinearOperators LOPBAN_9:def 4 :

for X, Y, Z being RealNormSpace

for b_{4} being Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds

( b_{4} = BoundedBilinearOperators (X,Y,Z) iff for x being set holds

( x in b_{4} iff x is Lipschitzian BilinearOperator of X,Y,Z ) );

for X, Y, Z being RealNormSpace

for b

( b

( x in b

registration
end;

registration

let X, Y, Z be RealNormSpace;

coherence

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

end;
coherence

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

proof end;

definition

let X, Y, Z be RealNormSpace;

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

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 ;

:: 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)))) #);

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;

coherence

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

end;
coherence

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

registration

let X, Y, Z be RealNormSpace;

( 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;
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;

registration

let X, Y, Z be RealNormSpace;

coherence

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

end;
coherence

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

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

end;
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;

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

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

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

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

end;
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;

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

:: 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;

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;

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

end;
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 ) } ;

{ ||.(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;

:: 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 ) } ;

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;

coherence

PreNorms g is bounded_above

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

coherence

PreNorms g is bounded_above

proof 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 )

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;

ex b_{1} being Function of (BoundedBilinearOperators (X,Y,Z)),REAL st

for x being object st x in BoundedBilinearOperators (X,Y,Z) holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X,Y,Z)))

for b_{1}, b_{2} being Function of (BoundedBilinearOperators (X,Y,Z)),REAL st ( for x being object st x in BoundedBilinearOperators (X,Y,Z) holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ) & ( for x being object st x in BoundedBilinearOperators (X,Y,Z) holds

b_{2} . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ) holds

b_{1} = b_{2}

end;
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 for x being object st x in BoundedBilinearOperators (X,Y,Z) holds

it . x = upper_bound (PreNorms (modetrans (x,X,Y,Z)));

ex b

for x being object st x in BoundedBilinearOperators (X,Y,Z) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines BoundedBilinearOperatorsNorm LOPBAN_9:def 8 :

for X, Y, Z being RealNormSpace

for b_{4} being Function of (BoundedBilinearOperators (X,Y,Z)),REAL holds

( b_{4} = BoundedBilinearOperatorsNorm (X,Y,Z) iff for x being object st x in BoundedBilinearOperators (X,Y,Z) holds

b_{4} . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) );

for X, Y, Z being RealNormSpace

for b

( b

b

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;

reducibility

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

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

reducibility

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

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)

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;

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

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 ;

:: 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)) #);

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.||

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.||

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.||

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;

for b_{1} being Element of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds

( b_{1} is Function-like & b_{1} is Relation-like )
;

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

coherence for b

( b

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

end;
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;

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

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

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.|| )

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;

coherence

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

end;
coherence

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

registration

let X, Y, Z be RealNormSpace;

( 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;
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;

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;

( 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;
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;

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

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

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

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

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

end;
let Z be RealBanachSpace;

coherence

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

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

( 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 ) ) ) )

( 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;