:: Bilinear Operators on Normed Linear Spaces
:: by Kazuhisa Nakasho
::
:: Received February 27, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, FUNCT_1, NAT_1,
SUBSET_1, SEQ_1, RSSPACE3, RELAT_1, LOPBAN_1, TARSKI, ARYTM_3, VALUED_1,
FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1,
FUNCOP_1, SEQ_4, ASYMPT_1, XXREAL_2, FUNCSDOM, RLSUB_1, RSSPACE, RELAT_2,
METRIC_1, ALGSTR_0, MONOID_0, XXREAL_0, XBOOLE_0, RLVECT_1, REWRITE1,
COMPLEX1, LOPBAN_8, LOPBAN_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
FUNCT_2,
BINOP_1, FUNCOP_1, NUMBERS, MONOID_0, XCMPLX_0, XXREAL_0, XXREAL_2,
XREAL_0, NAT_1, COMPLEX1, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0,
ALGSTR_0, PRE_TOPC, RLVECT_1, RLSUB_1, RSSPACE3, NORMSP_0, NORMSP_1,
RSSPACE, LOPBAN_1, PRVECT_3, LOPBAN_8;
constructors SEQ_2, SEQ_4, RLSUB_1, COMSEQ_2, RELSET_1, DUALSP01, NAT_D,
RSSPACE3, NDIFF_5, DOMAIN_1, MONOID_0, SEQ_1, LOPBAN_8, REAL_1;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_1,
FUNCT_2, NUMBERS, XBOOLE_0, ORDINAL1, NORMSP_0, NAT_1, SEQ_4, NORMSP_1,
RLVECT_1, MONOID_0, SEQ_1, SEQ_2, LOPBAN_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XXREAL_2, NORMSP_0, FUNCT_1;
equalities RLVECT_1, LOPBAN_1, NORMSP_0, BINOP_1, PRVECT_3, STRUCT_0,
ALGSTR_0;
expansions LOPBAN_1, FUNCT_1;
theorems TARSKI, XBOOLE_0, RLVECT_1, FUNCT_2, ORDINAL1, LOPBAN_1, SEQ_2,
COMPLEX1, XXREAL_0, NAT_1, XCMPLX_1, ABSVALUE, NORMSP_0, PRVECT_3, SEQ_1,
RSSPACE3, FUNCOP_1, RSSPACE, MONOID_0, BINOP_1, XCMPLX_0, XREAL_0, SEQ_4,
NORMSP_1, RLSUB_1, XREAL_1, LOPBAN_8, NDIFF_6, XBOOLE_1, FUNCT_1,
VECTSP_1;
schemes XBOOLE_0, FUNCT_2, SEQ_1;
begin :: Real Vector Space of Bilinear Operators
definition
let X, Y, Z be RealLinearSpace;
func BilinearOperators(X,Y,Z)
-> Subset of RealVectSpace(the carrier of [:X,Y:],Z) means :Def6:
for x being set holds x in it
iff x is BilinearOperator of X,Y,Z;
existence
proof
defpred P[object] means $1 is BilinearOperator of X,Y,Z;
consider IT being set such that
A1: for x being object holds x in IT
iff x in Funcs(the carrier of [:X,Y:], the
carrier of Z) & P[x] from XBOOLE_0:sch 1;
take IT;
for x be object st x in IT holds x in Funcs(the carrier of [:X,Y:],
the carrier of Z) by A1;
hence IT is Subset of RealVectSpace(the carrier of [:X,Y:],
Z) by TARSKI:def 3;
let x be set;
thus x in IT implies x is BilinearOperator of X,Y,Z by A1;
assume
A2: x is BilinearOperator of X,Y,Z;
then x in Funcs(the carrier of [:X,Y:],the carrier of Z) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of RealVectSpace(the carrier of [:X,Y:], Z);
assume that
A3: for x being set holds x in X1 iff x is BilinearOperator of X,Y,Z and
A4: for x being set holds x in X2 iff x is BilinearOperator of X,Y,Z;
A5: X2 c= X1
proof
let x be object;
assume x in X2;
then x is BilinearOperator of X,Y,Z by A4;
hence thesis by A3;
end;
X1 c= X2
proof
let x be object;
assume x in X1;
then x is BilinearOperator of X,Y,Z by A3;
hence thesis by A4;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
end;
registration
let X, Y, Z be RealLinearSpace;
cluster BilinearOperators(X,Y,Z) -> non empty functional;
coherence
proof
set f = the BilinearOperator of X,Y,Z;
f in BilinearOperators(X,Y,Z) by Def6;
hence BilinearOperators(X,Y,Z) is non empty;
let x be object;
assume x in BilinearOperators(X,Y,Z);
hence thesis;
end;
end;
LM14:
for X be RealLinearSpace,
x1,x2,x3,x4 be Point of X
holds (x1+x2) + (x3+x4) = (x1+x3) + (x2+x4)
proof
let X be RealLinearSpace,
x1,x2,x3,x4 be Point of X;
thus (x1+x2) + (x3+x4) = (x1+x2+x3)+x4 by RLVECT_1:def 3
.= (x1+x3+x2)+x4 by RLVECT_1:def 3
.= (x1+x3)+(x2+x4) by RLVECT_1:def 3;
end;
Th14:
for X, Y, Z be RealLinearSpace holds BilinearOperators(X,Y,Z)
is linearly-closed
proof
let X, Y, Z be RealLinearSpace;
set W = BilinearOperators(X,Y,Z);
A1: for v,u be VECTOR of RealVectSpace(the carrier of [:X,Y:],Z)
st v in BilinearOperators(X,Y,Z)
& u in BilinearOperators(X,Y,Z)
holds v + u in BilinearOperators(X,Y,Z)
proof
let v,u be VECTOR of RealVectSpace(the carrier of [:X,Y:],Z) such that
A2: v in W and
A3: u in W;
reconsider u1=u as BilinearOperator of X,Y,Z by A3,Def6;
reconsider v1=v as BilinearOperator of X,Y,Z by A2,Def6;
v+u is BilinearOperator of X,Y,Z
proof
reconsider L=v+u as Function of [:X,Y:],Z by FUNCT_2:66;
A4: for x1,x2 be Point of X, y be Point of Y
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y)
proof
let x1,x2 be Point of X, y be Point of Y;
A5: [x1,y] is Element of [:X,Y:]
& [x2,y] is Element of [:X,Y:]
& [x1+x2,y] is Element of [:X,Y:];
hence L. (x1+x2,y) = v1.(x1+x2,y)+u1.(x1+x2,y) by LOPBAN_1:1
.= (v1.(x1,y)+v1.(x2,y)) + u1.(x1+x2,y) by LOPBAN_8:11
.= (v1.(x1,y)+v1.(x2,y)) + (u1.(x1,y)+u1.(x2,y)) by LOPBAN_8:11
.= (v1.(x1,y)+u1.(x1,y)) + (v1.(x2,y)+u1.(x2,y)) by LM14
.= L.(x1,y) + (v1.(x2,y)+u1.(x2,y)) by A5,LOPBAN_1:1
.= L.(x1,y) + L.(x2,y) by A5,LOPBAN_1:1;
end;
A6: for x be Point of X, y be Point of Y, a be Real
holds L.(a*x,y) = a * L.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
A7: [x,y] is Element of [:X,Y:] & [a*x,y] is Element of [:X,Y:];
hence L.(a*x,y) = v1.(a*x,y)+u1.(a*x,y) by LOPBAN_1:1
.= a * v1.(x,y) + u1.(a*x,y) by LOPBAN_8:11
.= a * v1.(x,y) + a * u1.(x,y) by LOPBAN_8:11
.= a * ( v1.(x,y) + u1.(x,y) ) by RLVECT_1:def 5
.= a * L.(x,y) by A7,LOPBAN_1:1;
end;
A8: for x be Point of X, y1,y2 be Point of Y
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2)
proof
let x be Point of X, y1,y2 be Point of Y;
A9: [x,y1] is Element of [:X,Y:]
& [x,y2] is Element of [:X,Y:]
& [x,y1+y2] is Element of [:X,Y:];
hence L.(x,y1+y2) = v1.(x,y1+y2)+u1.(x,y1+y2) by LOPBAN_1:1
.= (v1.(x,y1)+v1.(x,y2)) + u1.(x,y1+y2) by LOPBAN_8:11
.= (v1.(x,y1)+v1.(x,y2)) + (u1.(x,y1)+u1.(x,y2)) by LOPBAN_8:11
.= (v1.(x,y1)+u1.(x,y1)) + (v1.(x,y2)+u1.(x,y2)) by LM14
.= L.(x,y1) + (v1.(x,y2)+u1.(x,y2)) by A9,LOPBAN_1:1
.= L.(x,y1) + L.(x,y2) by A9,LOPBAN_1:1;
end;
for x be Point of X, y be Point of Y, a be Real
holds L.(x,a*y) = a * L.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
A10: [x,y] is Element of [:X,Y:] & [x,a*y] is Element of [:X,Y:];
hence L.(x,a*y) = v1.(x,a*y) + u1.(x,a*y) by LOPBAN_1:1
.= a * v1.(x,y) + u1.(x,a*y) by LOPBAN_8:11
.= a * v1.(x,y) + a*u1.(x,y) by LOPBAN_8:11
.= a * ( v1.(x,y) + u1.(x,y) ) by RLVECT_1:def 5
.= a * L.(x,y) by A10,LOPBAN_1:1;
end;
hence thesis by A4,A6,A8,LOPBAN_8:11;
end;
hence thesis by Def6;
end;
for b be Real
for v be VECTOR of RealVectSpace(the carrier of [:X,Y:],Z)
st v in W holds b * v in W
proof
let b be Real;
let v be VECTOR of RealVectSpace(the carrier of [:X,Y:],Z) such that
A11: v in W;
reconsider v1=v as BilinearOperator of X,Y,Z by A11,Def6;
b*v is BilinearOperator of X,Y,Z
proof
reconsider L=b*v as Function of [:X,Y:],Z by FUNCT_2:66;
A12: for x1,x2 be Point of X, y be Point of Y
holds L.(x1+x2,y) = L.(x1,y) + L.(x2,y)
proof
let x1,x2 be Point of X, y be Point of Y;
A13: [x1,y] is Element of [:X,Y:]
& [x2,y] is Element of [:X,Y:]
& [x1+x2,y] is Element of [:X,Y:];
hence L. (x1+x2,y) = b*v1.(x1+x2,y) by LOPBAN_1:2
.= b*(v1.(x1,y)+v1.(x2,y)) by LOPBAN_8:11
.= b*v1.(x1,y)+b*v1.(x2,y) by RLVECT_1:def 5
.= L.(x1,y) +b*v1.(x2,y) by A13,LOPBAN_1:2
.= L.(x1,y) + L.(x2,y) by A13,LOPBAN_1:2;
end;
A14: for x be Point of X, y be Point of Y, a be Real
holds L.(a*x,y) = a * L.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
A15: [x,y] is Element of [:X,Y:] & [a*x,y] is Element of [:X,Y:];
hence L.(a*x,y) = b*v1.(a*x,y) by LOPBAN_1:2
.= b*(a*v1.(x,y)) by LOPBAN_8:11
.= (b*a)*v1.(x,y) by RLVECT_1:def 7
.= a*(b*v1.(x,y)) by RLVECT_1:def 7
.= a* L.(x,y) by A15,LOPBAN_1:2;
end;
A16: for x be Point of X, y1,y2 be Point of Y
holds L.(x,y1+y2) = L.(x,y1) + L.(x,y2)
proof
let x be Point of X, y1,y2 be Point of Y;
A17: [x,y1] is Element of [:X,Y:]
& [x,y2] is Element of [:X,Y:]
& [x,y1+y2] is Element of [:X,Y:];
hence L.(x,y1+y2) = b*v1.(x,y1+y2) by LOPBAN_1:2
.= b*(v1.(x,y1)+v1.(x,y2)) by LOPBAN_8:11
.= b*v1.(x,y1)+b*v1.(x,y2) by RLVECT_1:def 5
.= L.(x,y1) + b*v1.(x,y2) by A17,LOPBAN_1:2
.= L.(x,y1) + L.(x,y2) by A17,LOPBAN_1:2;
end;
for x be Point of X, y be Point of Y, a be Real
holds L.(x,a*y) = a * L.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
A18: [x,y] is Element of [:X,Y:] & [x,a*y] is Element of [:X,Y:];
hence L.(x,a*y) = b*v1.(x,a*y) by LOPBAN_1:2
.= b*(a*v1.(x,y)) by LOPBAN_8:11
.= (b*a)*v1.(x,y) by RLVECT_1:def 7
.= a*(b*v1.(x,y)) by RLVECT_1:def 7
.= a * L.(x,y) by A18,LOPBAN_1:2;
end;
hence thesis by A12,A14,A16,LOPBAN_8:11;
end;
hence thesis by Def6;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
registration
let X, Y, Z be RealLinearSpace;
cluster BilinearOperators(X,Y,Z) -> linearly-closed;
coherence by Th14;
end;
definition
let X, Y, Z be RealLinearSpace;
func R_VectorSpace_of_BilinearOperators(X,Y,Z) -> strict RLSStruct equals
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;
end;
registration
let X, Y, Z be RealLinearSpace;
cluster R_VectorSpace_of_BilinearOperators(X,Y,Z) -> non empty;
coherence;
end;
registration
let X, Y, Z be RealLinearSpace;
cluster R_VectorSpace_of_BilinearOperators(X,Y,Z) ->
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence by RSSPACE:11;
end;
registration
let X,Y, Z be RealLinearSpace;
cluster R_VectorSpace_of_BilinearOperators(X,Y,Z) -> constituted-Functions;
coherence by MONOID_0:80;
end;
theorem
for X, Y, Z be 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, w be VECTOR of Y;
redefine func f. (v,w) -> VECTOR of Z; :: redefines . (BINOP_1, definition)
coherence
proof
reconsider f as BilinearOperator of X,Y,Z by Def6;
f.(v,w) is VECTOR of Z;
hence thesis;
end;
end;
theorem Th16:
for X, Y, Z be RealLinearSpace
for f,g,h be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
holds
h = f+g
iff
for x be VECTOR of X,y be VECTOR of Y
holds h.(x,y) = f.(x,y) + g.(x,y)
proof
let X, Y, Z be RealLinearSpace;
let f,g,h be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z);
reconsider f9=f,g9=g,h9=h as BilinearOperator of X,Y,Z by Def6;
A1: R_VectorSpace_of_BilinearOperators(X,Y,Z)
is Subspace of RealVectSpace(the carrier of [:X,Y:],Z)
by RSSPACE:11; then
reconsider f1=f as VECTOR
of RealVectSpace(the carrier of [:X,Y:],Z ) by RLSUB_1:10;
reconsider h1=h
as VECTOR of RealVectSpace(the carrier of [:X,Y:],Z) by A1,RLSUB_1:10;
reconsider g1=g as VECTOR of RealVectSpace(the carrier of [:X,Y:],Z)
by A1,RLSUB_1:10;
A2: now
assume
A3: h = f+g;
let x be Element of X,y be Element of Y;
A4: h1=f1+g1 by A1,A3,RLSUB_1:13;
[x,y] is Element of [:X,Y:];
hence h9.(x,y)=f9.(x,y)+g9.(x,y) by A4,LOPBAN_1:1;
end;
now
assume
A5: for x be Element of X,y be Element of Y
holds h9.(x,y)=f9.(x,y)+g9.(x,y);
for z be Element of [:X,Y:] holds h9.z=f9.z+g9.z
proof
let z be Element of [:X,Y:];
consider x be Point of X,y be Point of Y such that
A6: z=[x,y] by PRVECT_3:9;
thus h9.z = h9.(x,y) by A6
.= f9.(x,y)+g9.(x,y) by A5
.= f9.z+g9.z by A6;
end; then
h1=f1+g1 by LOPBAN_1:1;
hence h =f+g by A1,RLSUB_1:13;
end;
hence thesis by A2;
end;
theorem Th17:
for X, Y, Z be RealLinearSpace
for f,h be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
for a be Real
holds
h = a*f
iff
for x be VECTOR of X, y be VECTOR of Y
holds h.(x,y) = a * f.(x,y)
proof
let X, Y, Z be RealLinearSpace;
let f,h be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z);
reconsider f9=f,h9=h as BilinearOperator of X,Y,Z by Def6;
let a be Real;
A1: R_VectorSpace_of_BilinearOperators(X,Y,Z) is Subspace of
RealVectSpace(the carrier of [:X,Y:],Z) by RSSPACE:11; then
reconsider f1=f as VECTOR of
RealVectSpace(the carrier of [:X,Y:],Z) by RLSUB_1:10;
reconsider h1=h as VECTOR of
RealVectSpace(the carrier of [:X,Y:],Z) by A1,RLSUB_1:10;
A2: now
assume
A3: h = a*f;
let x be Element of X,y be Element of Y;
A4: h1=a*f1 by A1,A3,RLSUB_1:14;
[x,y] is Element of [:X,Y:];
hence h9.(x,y)=a*f9.(x,y) by A4,LOPBAN_1:2;
end;
now
assume
A5: for x be Element of X,y be Element of Y
holds h9.(x,y) = a * f9.(x,y);
for z be Element of [:X,Y:] holds h9.z=a*f9.z
proof
let z be Element of [:X,Y:];
consider x be Point of X,y be Point of Y such that
A6: z=[x,y] by PRVECT_3:9;
thus h9.z = h9.(x,y) by A6
.= a*f9.(x,y) by A5
.= a*f9.z by A6;
end; then
h1 = a*f1 by LOPBAN_1:2;
hence h = a*f by A1,RLSUB_1:14;
end;
hence thesis by A2;
end;
theorem Th18:
for X, Y, Z be RealLinearSpace holds
0.R_VectorSpace_of_BilinearOperators(X,Y,Z)
= (the carrier of [:X,Y:] ) -->0.Z
proof
let X, Y, Z be RealLinearSpace;
A1: 0.RealVectSpace(the carrier of [:X,Y:],Z)
= ((the carrier of [:X,Y:] ) -->0.Z);
R_VectorSpace_of_BilinearOperators(X,Y,Z)
is Subspace of RealVectSpace(the carrier of [:X,Y:],Z) by RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
theorem
for X,Y, Z be RealLinearSpace holds
(the carrier of [:X,Y:] ) --> 0.Z is BilinearOperator of X,Y,Z
by LOPBAN_8:9,def 2;
begin :: Real Normed Linear Space of Bounded Bilinear Operators
definition
let X, Y, Z be RealNormSpace;
let IT be BilinearOperator of X,Y,Z;
attr IT is Lipschitzian means :Def8:
ex K being Real st 0 <= K &
for x being VECTOR of X, y being VECTOR of Y
holds ||. IT.(x,y) .|| <= K * ||. x .|| * ||. y .||;
end;
theorem Th21:
for X, Y, Z be RealNormSpace holds
for f be BilinearOperator of X,Y,Z
st (for x be VECTOR of X,y be VECTOR of Y holds f.(x,y) = 0.Z)
holds f is Lipschitzian
proof
let X,Y,Z be RealNormSpace;
let f be BilinearOperator of X,Y,Z such that
A1: for x be VECTOR of X,y be VECTOR of Y holds f.(x,y) = 0.Z;
A2: now
let x be VECTOR of X,y be VECTOR of Y;
thus ||. f.(x,y) .|| = ||. 0.Z .|| by A1
.= 0 * ||.x.|| * ||.y.||;
end;
take 0;
thus thesis by A2;
end;
theorem
for X,Y,Z be RealNormSpace holds
(the carrier of [:X,Y:]) --> 0.Z is BilinearOperator of X,Y,Z
by LOPBAN_8:9,def 3;
registration
let X, Y, Z be RealNormSpace;
cluster Lipschitzian for BilinearOperator of X,Y,Z;
existence
proof
set f=(the carrier of [:X,Y:]) --> 0.Z;
reconsider f as BilinearOperator of X,Y,Z by LOPBAN_8:9,def 3;
take f;
for x be VECTOR of X,y be VECTOR of Y
holds f.(x,y) = 0.Z
proof
let x be VECTOR of X,y be VECTOR of Y;
[x,y] is Point of [:X,Y:];
hence thesis by FUNCOP_1:7;
end;
hence thesis by Th21;
end;
end;
theorem EQSET:
for X, Y, Z be RealNormSpace, z be object holds
( z in BilinearOperators(X,Y,Z)
iff
z is BilinearOperator of X,Y,Z )
proof
let X, Y, Z be RealNormSpace, z be object;
reconsider X0 = X,Y0=Y,Z0=Z as RealLinearSpace;
hereby
assume z in BilinearOperators(X,Y,Z); then
z is BilinearOperator of X0,Y0,Z0 by Def6; then
consider g be Function of
[:the carrier of X0,the carrier of Y0:], the carrier of Z0
such that
A1: z = g & g is Bilinear by LOPBAN_8:def 2;
thus z is BilinearOperator of X,Y,Z by A1,LOPBAN_8:def 3;
end;
assume z is BilinearOperator of X,Y,Z; then
consider g be Function of
[:the carrier of X,the carrier of Y:], the carrier of Z such that
A1: z=g & g is Bilinear by LOPBAN_8:def 3;
reconsider w=g as BilinearOperator of X0,Y0,Z0
by LOPBAN_8:def 2,A1;
w in BilinearOperators(X,Y,Z) by Def6;
hence z in BilinearOperators(X,Y,Z) by A1;
end;
definition
let X, Y, Z be RealNormSpace;
func BoundedBilinearOperators(X,Y,Z)
-> Subset of R_VectorSpace_of_BilinearOperators(X,Y,Z) means :Def9:
for x being set holds x in it
iff x is Lipschitzian BilinearOperator of X,Y,Z;
existence
proof
defpred P[object] means $1 is Lipschitzian BilinearOperator of X,Y,Z;
consider IT being set such that
A1: for x being object holds x in IT
iff x in BilinearOperators(X,Y,Z) & P[x]
from XBOOLE_0:sch 1;
take IT;
for x be object st x in IT holds x in BilinearOperators(X,Y,Z) by A1;
hence IT is Subset of R_VectorSpace_of_BilinearOperators(X,Y,Z)
by TARSKI:def 3;
let x be set;
thus x in IT implies x is Lipschitzian BilinearOperator of X,Y,Z by A1;
assume x is Lipschitzian BilinearOperator of X,Y,Z;
hence thesis by A1,EQSET;
end;
uniqueness
proof
let X1,X2 be Subset of R_VectorSpace_of_BilinearOperators(X,Y,Z);
assume that
A3: for x being set holds x in X1
iff x is Lipschitzian BilinearOperator of X,Y,Z and
A4: for x being set holds x in X2
iff x is Lipschitzian BilinearOperator of X,Y,Z;
A5: X2 c= X1
proof
let x be object;
assume x in X2; then
x is Lipschitzian BilinearOperator of X,Y,Z by A4;
hence thesis by A3;
end;
X1 c= X2
proof
let x be object;
assume x in X1; then
x is Lipschitzian BilinearOperator of X,Y,Z by A3;
hence thesis by A4;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
end;
registration
let X, Y, Z be RealNormSpace;
cluster BoundedBilinearOperators(X,Y,Z) -> non empty;
coherence
proof
set f = (the carrier of [:X,Y:]) --> 0.Z;
reconsider f as BilinearOperator of X,Y,Z by LOPBAN_8:9,def 3;
for x be VECTOR of X, y be VECTOR of Y holds f.(x,y) = 0.Z
proof
let x be VECTOR of X,y be VECTOR of Y;
[x,y] is Point of [:X,Y:];
hence thesis by FUNCOP_1:7;
end; then
f is Lipschitzian by Th21;
hence thesis by Def9;
end;
end;
registration
let X, Y, Z be RealNormSpace;
cluster BoundedBilinearOperators(X,Y,Z) -> linearly-closed;
coherence
proof
set W = BoundedBilinearOperators(X,Y,Z);
A1: for v,u be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
st v in W & u in W
holds v + u in W
proof
let v,u be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z) such that
A2: v in W and
A3: u in W;
reconsider f=v+u as BilinearOperator of X,Y,Z by EQSET;
f is Lipschitzian
proof
reconsider v1=v as Lipschitzian BilinearOperator of X,Y,Z by A2,Def9;
consider K2 be Real such that
A4: 0 <= K2 and
A5: for x be VECTOR of X,y be VECTOR of Y
holds ||. v1.(x,y) .|| <= K2 * ||. x .|| * ||.y.|| by Def8;
reconsider u1=u as Lipschitzian BilinearOperator of X,Y,Z by A3,Def9;
consider K1 be Real such that
A6: 0 <= K1 and
A7: for x be VECTOR of X,y be VECTOR of Y
holds ||. u1.(x,y) .|| <= K1 * ||. x .|| * ||. y .|| by Def8;
take K3 = K1+K2;
now
let x be VECTOR of X,y be VECTOR of Y;
A8: ||. u1.(x,y) + v1.(x,y) .||
<= ||. u1.(x,y) .|| + ||. v1.(x,y) .|| by NORMSP_1:def 1;
A9: ||. v1.(x,y) .|| <= K2 * ||. x .|| * ||.y.|| by A5;
||. u1.(x,y) .|| <= K1 * ||. x .|| * ||.y.|| by A7; then
A10: ||. u1.(x,y) .|| + ||. v1.(x,y) .||
<= K1 * ||. x .|| * ||.y.|| + K2 * ||. x .|| * ||.y.||
by A9,XREAL_1:7;
||. f.(x,y) .|| =||. u1.(x,y) + v1.(x,y) .|| by Th16;
hence ||. f.(x,y) .|| <= K3 * ||. x .|| * ||.y.||
by A8,A10,XXREAL_0:2;
end;
hence thesis by A4,A6;
end;
hence thesis by Def9;
end;
for a be Real
for v be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
st v in W holds a * v in W
proof
let a be Real;
let v be VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z) such that
A11: v in W;
reconsider f = a*v as BilinearOperator of X,Y,Z by EQSET;
f is Lipschitzian
proof
reconsider v1=v as Lipschitzian BilinearOperator of X,Y,Z by A11,Def9;
consider K be Real such that
A12: 0 <= K and
A13: for x be VECTOR of X,
y be VECTOR of Y
holds ||. v1 .(x,y) .|| <= K * ||. x .|| * ||.y.|| by Def8;
take |.a.| * K;
A14: now
let x be VECTOR of X,y be VECTOR of Y;
0 <=|.a.| by COMPLEX1:46; then
A15: |.a.| * ||. v1.(x,y) .||
<= |.a.| * (K * ||. x .|| * ||.y.||) by A13,XREAL_1:64;
||. a * v1.(x,y) .|| = |.a.| * ||. v1.(x,y) .|| by NORMSP_1:def 1;
hence ||. f.(x,y) .|| <= (|.a.| * K) * ||. x .|| * ||.y.||
by A15,Th17;
end;
0 <= |.a.| by COMPLEX1:46;
hence thesis by A12,A14;
end;
hence thesis by Def9;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
end;
definition
let X, Y, Z be RealNormSpace;
func R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) -> strict RLSStruct
equals
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;
end;
theorem
for X, Y, Z be 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;
coherence;
end;
registration
let X, Y, Z be RealNormSpace;
cluster R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) ->
Abelian add-associative right_zeroed
right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by RSSPACE:11;
end;
registration
let X,Y, Z be RealNormSpace;
cluster R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) ->
constituted-Functions;
coherence 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,w be VECTOR of Y;
redefine func f.(v,w) -> VECTOR of Z; :: redefines . (BINOP_1, definition)
coherence
proof
reconsider f as BilinearOperator of X,Y,Z by Def9;
f.(v,w) is VECTOR of Z;
hence thesis;
end;
end;
theorem Th24:
for X, Y, Z be RealNormSpace
for f,g,h be VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
holds
h = f+g
iff
for x be VECTOR of X, y be VECTOR of Y
holds h.(x,y) = f.(x,y) + g.(x,y)
proof
let X, Y, Z be RealNormSpace;
let f,g,h be VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z);
A1: R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
is Subspace of R_VectorSpace_of_BilinearOperators(X,Y,Z)
by RSSPACE:11; then
reconsider f1=f as
VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z) by RLSUB_1:10;
reconsider h1=h as VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
by A1,RLSUB_1:10;
reconsider g1=g as VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
by A1,RLSUB_1:10;
hereby
assume
A2: h = f+g;
let x be Element of X,y be Element of Y;
h1 = f1+g1 by A1,A2,RLSUB_1:13;
hence h.(x,y) = f.(x,y) + g.(x,y) by Th16;
end;
assume for x be Element of X,y be Element of Y
holds h.(x,y) = f.(x,y)+g.(x,y);
then h1=f1+g1 by Th16;
hence thesis by A1,RLSUB_1:13;
end;
theorem Th25:
for X, Y, Z be RealNormSpace
for f,h be VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
for a be Real holds
h = a * f
iff
for x be VECTOR of X,y be VECTOR of Y holds
h.(x,y) = a * f.(x,y)
proof
let X, Y, Z be RealNormSpace;
let f,h be VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z);
let a be Real;
A1: R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
is Subspace of R_VectorSpace_of_BilinearOperators(X,Y,Z)
by RSSPACE:11; then
reconsider f1=f as VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
by RLSUB_1:10;
reconsider h1=h as VECTOR of R_VectorSpace_of_BilinearOperators(X,Y,Z)
by A1,RLSUB_1:10;
hereby
assume
A2: h = a*f;
let x be Element of X,y be Element of Y;
h1 = a*f1 by A1,A2,RLSUB_1:14;
hence h.(x,y) = a*f.(x,y) by Th17;
end;
assume for x be Element of X,y be Element of Y
holds h.(x,y)=a*f.(x,y); then
h1 = a*f1 by Th17;
hence thesis by A1,RLSUB_1:14;
end;
theorem Th26:
for X, Y, Z be RealNormSpace holds
0.R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
= (the carrier of [:X,Y:]) --> 0.Z
proof
let X, Y, Z be RealNormSpace;
A1: 0.R_VectorSpace_of_BilinearOperators(X,Y,Z)
= ((the carrier of [:X,Y:]) -->0.Z) by Th18;
R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
is Subspace of R_VectorSpace_of_BilinearOperators(X,Y,Z) by RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
definition
let X,Y,Z be RealNormSpace;
let f be object such that
A1: f in BoundedBilinearOperators(X,Y,Z);
func modetrans(f,X,Y,Z) -> Lipschitzian BilinearOperator of X,Y,Z
equals :Def11:
f;
coherence by A1,Def9;
end;
definition
let X, Y, Z be RealNormSpace;
let u be BilinearOperator of X,Y,Z;
func PreNorms(u) -> non empty Subset of REAL equals
{||.u.(t,s) .|| where t is VECTOR of X, s is VECTOR of Y
: ||.t.|| <= 1 & ||.s.|| <= 1 };
coherence
proof
A1: now
let x be object;
now
assume x in {||.u.(t,s).||
where t is VECTOR of X, s is VECTOR of Y
: ||.t.|| <= 1 & ||.s.|| <= 1 }; then
ex t be VECTOR of X,s be VECTOR of Y
st x = ||.u.(t,s).|| & ||.t.|| <= 1 & ||.s.|| <= 1;
hence x in REAL;
end;
hence x in {||.u.(t,s) .|| where t is VECTOR of X, s is VECTOR of Y
: ||.t.|| <= 1 & ||.s.|| <= 1 }
implies x in REAL;
end;
||.0.X.|| = 0 & ||.0.Y.|| = 0; then
||.u.(0.X,0.Y).|| in {||.u.(t,s) .|| where t is VECTOR of X,
s is VECTOR of Y : ||.t.|| <= 1 & ||.s.|| <= 1 };
hence thesis by A1,TARSKI:def 3;
end;
end;
registration
let X, Y, Z be RealNormSpace;
let g be Lipschitzian BilinearOperator of X,Y,Z;
cluster PreNorms(g) -> bounded_above;
coherence
proof
consider K be Real such that
A1: 0 <= K and
A2: for x be VECTOR of X,y be VECTOR of Y
holds ||. g.(x,y) .|| <= K * ||. x .|| * ||. y .|| by Def8;
take K;
let r be ExtReal;
assume r in PreNorms(g);
then consider t be VECTOR of X, s be VECTOR of Y such that
A3: r = ||. g.(t,s) .|| and
A4: ||.t.|| <= 1 & ||.s.|| <= 1;
A5: ||.g.(t,s).|| <= K * ||. t .|| * ||. s .|| by A2;
||. t .|| * ||. s .|| <= 1*1 by XREAL_1:66,A4; then
K * ( ||. t .|| * ||. s .|| ) <= K * 1 by A1,XREAL_1:64;
hence r <= K by A3,A5,XXREAL_0:2;
end;
end;
theorem
for X, Y, Z be RealNormSpace
for g be BilinearOperator of X,Y,Z
holds g is Lipschitzian iff PreNorms(g) is bounded_above
proof
let X, Y, Z be RealNormSpace;
let g be BilinearOperator of X,Y,Z;
now
reconsider K = upper_bound PreNorms(g) as Real;
assume
A1: PreNorms(g) is bounded_above;
A2: now
let t be VECTOR of X,s be VECTOR of Y;
now
per cases;
case
A3: t = 0.X or s = 0.Y; then
A4: ||.t.|| = 0 or ||.s.|| = 0;
t = 0*t or s = 0*s by A3; then
g.(t,s) = 0*g.(t,s) by LOPBAN_8:12
.= 0.Z by RLVECT_1:10;
hence ||.g.(t,s).|| <= K * ||.t.|| * ||.s.|| by A4;
end;
case
A5: t <> 0.X & s <> 0.Y;
reconsider t1 = ( ||.t.||") * t as VECTOR of X;
reconsider s1 = ( ||.s.||") * s as VECTOR of Y;
A6: ||.t.|| <> 0 & ||.s.|| <> 0 by A5,NORMSP_0:def 5; then
A7: ||.t.|| * ||.s.|| <> 0 by XCMPLX_1:6;
A8: ||.g.(t,s).|| / (||.t.||*||.s.||) * (||.t.||*||.s.||)
= ||.g.(t,s).|| * (||.t.||*||.s.||)" * (||.t.||*||.s.||)
by XCMPLX_0:def 9
.= ||.g.(t,s).|| * ((||.t.||*||.s.||)" * (||.t.||*||.s.||))
.= ||.g.(t,s).|| * 1 by A7,XCMPLX_0:def 7
.= ||.g.(t,s).||;
A9: |. ||.t.||".| = |. 1 * ||.t.||".|
.= |. 1 / ||.t.||.| by XCMPLX_0:def 9
.= 1 / ||.t.|| by ABSVALUE:def 1
.= 1 * ||.t.||" by XCMPLX_0:def 9
.= ||.t.||";
A10: |. ||.s.||".| = |. 1 * ||.s.||".|
.= |. 1 / ||.s.|| .| by XCMPLX_0:def 9
.= 1 / ||.s.|| by ABSVALUE:def 1
.= 1 * ||.s.||" by XCMPLX_0:def 9
.= ||.s.||";
A11: |. ( ||.t.|| * ||.s.|| )".|
= |. ||.t.||" * ||.s.||" .| by XCMPLX_1:204
.= ||.t.||" * ||.s.||" by A9,A10,COMPLEX1:65
.= ( ||.t.|| * ||.s.|| ) " by XCMPLX_1:204;
A12: ||.t1.|| = |. ||.t.||" .| * ||.t.|| by NORMSP_1:def 1
.= 1 by A6,A9,XCMPLX_0:def 7;
||.s1.|| = |. ||.s.||" .| * ||.s.|| by NORMSP_1:def 1
.= 1 by A6,A10,XCMPLX_0:def 7; then
A13: ||.g.(t1,s1).|| in {||.g.(t,s) .||
where t is VECTOR of X, s is VECTOR of Y
: ||.t.|| <= 1 & ||.s.|| <= 1} by A12;
||.g.(t,s).|| / ( ||.t.|| * ||.s.|| )
= ||.g.(t,s).|| * ( ||.t.|| * ||.s.|| )" by XCMPLX_0:def 9
.= ||. ( ||.t.|| * ||.s.|| )" * g.(t,s).|| by A11,NORMSP_1:def 1
.= ||. ( ||.t.||" * ||.s.||" ) * g.(t,s).|| by XCMPLX_1:204
.= ||. ||.t.||" * ( ||.s.||" * g.(t,s)).|| by RLVECT_1:def 7
.= ||. ||.t.||" * ( g.(t,s1)).|| by LOPBAN_8:12
.= ||.g.(t1,s1).|| by LOPBAN_8:12; then
||.g.(t,s).|| / (||.t.|| * ||.s.||) <= K by A1,A13,SEQ_4:def 1;
hence ||.g.(t,s).|| <= K * ( ||.t.|| * ||.s.|| ) by A8,XREAL_1:64;
end;
end;
hence ||.g.(t,s) .|| <= K * ||.t.|| * ||.s.||;
end;
take K;
0 <= K
proof
consider r0 be object such that
A14: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A14;
now
let r be Real;
assume r in PreNorms(g); then
ex t be VECTOR of X, s be VECTOR of Y
st r = ||.g.(t,s).|| & ||.t.|| <= 1 & ||.s.|| <= 1;
hence 0 <= r;
end; then
0 <= r0 by A14;
hence thesis by A1,A14,SEQ_4:def 1;
end;
hence g is Lipschitzian by A2;
end;
hence thesis;
end;
definition
let X, Y, Z be RealNormSpace;
func BoundedBilinearOperatorsNorm(X,Y,Z)
-> Function of BoundedBilinearOperators(X,Y,Z), REAL means :Def13:
for x be object st x in BoundedBilinearOperators(X,Y,Z) holds
it.x = upper_bound PreNorms(modetrans(x,X,Y,Z));
existence
proof
deffunc F(object) = upper_bound PreNorms(modetrans($1,X,Y,Z));
A1: for z be object st z in BoundedBilinearOperators(X,Y,Z) holds
F(z) in REAL by XREAL_0:def 1;
thus ex f being Function of BoundedBilinearOperators(X,Y,Z),REAL
st for x being object st x in BoundedBilinearOperators(X,Y,Z)
holds f.x = F(x)
from FUNCT_2:sch 2(A1);
end;
uniqueness
proof
let NORM1,NORM2 be Function of BoundedBilinearOperators(X,Y,Z),REAL
such that
A2: for x be object st x in BoundedBilinearOperators(X,Y,Z) holds NORM1.x =
upper_bound PreNorms(modetrans(x,X,Y,Z)) and
A3: for x be object st x in BoundedBilinearOperators(X,Y,Z) holds NORM2.x =
upper_bound PreNorms(modetrans(x,X,Y,Z));
A4: for z be object st z in BoundedBilinearOperators(X,Y,Z)
holds NORM1.z = NORM2.z
proof
let z be object such that
A5: z in BoundedBilinearOperators(X,Y,Z);
NORM1.z = upper_bound PreNorms(modetrans(z,X,Y,Z)) by A2,A5;
hence thesis by A3,A5;
end;
dom NORM1 = BoundedBilinearOperators(X,Y,Z) by FUNCT_2:def 1;
hence thesis by A4,FUNCT_2:def 1;
end;
end;
Th29:
for X, Y, Z be RealNormSpace
for f be Lipschitzian BilinearOperator of X,Y,Z
holds modetrans(f,X,Y,Z)=f
proof
let X, Y, Z be RealNormSpace;
let f be Lipschitzian BilinearOperator of X,Y,Z;
f in BoundedBilinearOperators(X,Y,Z) by Def9;
hence thesis by Def11;
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 by Th29;
end;
theorem Th30:
for X, Y, Z be RealNormSpace for f be Lipschitzian BilinearOperator of X,Y,Z
holds BoundedBilinearOperatorsNorm(X,Y,Z).f = upper_bound PreNorms(f)
proof
let X, Y, Z be RealNormSpace;
let f be Lipschitzian BilinearOperator of X,Y,Z;
reconsider f9 = f as set;
f in BoundedBilinearOperators(X,Y,Z) by Def9;
hence BoundedBilinearOperatorsNorm(X,Y,Z).f
= upper_bound PreNorms(modetrans(f9,X,Y,Z)) by Def13
.= upper_bound PreNorms(f);
end;
definition
let X, Y, Z be RealNormSpace;
func R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) -> non empty NORMSTR
equals
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;
end;
theorem Th31:
for X,Y,Z be RealNormSpace holds
(the carrier of [:X,Y:]) --> 0.Z
= 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
proof
let X, Y, Z be RealNormSpace;
((the carrier of [:X,Y:]) --> 0.Z)
= 0.R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) by Th26
.= 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
hence thesis;
end;
theorem Th32:
for X,Y,Z be RealNormSpace
for f being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
for g be Lipschitzian BilinearOperator of X,Y,Z st g=f
holds
for t be VECTOR of X, s be VECTOR of Y
holds ||.g.(t,s).|| <= ||.f.|| * ||.t.|| * ||.s.||
proof
let X, Y, Z be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
let g be Lipschitzian BilinearOperator of X,Y,Z such that
A1: g = f;
now
let t be VECTOR of X,s be VECTOR of Y;
now
per cases;
case
A3: t = 0.X or s = 0.Y; then
A4: ||.t.|| = 0 or ||.s.|| = 0;
t = 0 * t or s = 0*s by A3; then
g.(t,s) = 0 * g.(t,s) by LOPBAN_8:12
.= 0.Z by RLVECT_1:10;
hence ||.g.(t,s).|| <= ||.f.|| * ||.t.|| * ||.s.|| by A4;
end;
case
A5: t <> 0.X & s <> 0.Y;
reconsider t1 = ( ||.t.||") * t as VECTOR of X;
reconsider s1 = ( ||.s.||") * s as VECTOR of Y;
A6: ||.t.|| <> 0 & ||.s.|| <> 0 by A5,NORMSP_0:def 5; then
A7: ||.t.|| * ||.s.|| <> 0 by XCMPLX_1:6;
A8: |. ||.t.||" .| = |. 1 * ||.t.||".|
.= |. 1 / ||.t.|| .| by XCMPLX_0:def 9
.= 1 / ||.t.|| by ABSVALUE:def 1
.= 1 * ||.t.||" by XCMPLX_0:def 9
.= ||.t.||";
A9: |. ||.s.||".| = |. 1 * ||.s.||".|
.= |. 1 / ||.s.||.| by XCMPLX_0:def 9
.= 1 / ||.s.|| by ABSVALUE:def 1
.= 1 * ||.s.||" by XCMPLX_0:def 9
.= ||.s.||";
A10: |. ( ||.t.|| * ||.s.|| )".|
= |. ||.t.||" * ||.s.||" .| by XCMPLX_1:204
.= ||.t.||" * ||.s.||" by A8,A9,COMPLEX1:65
.= ( ||.t.|| * ||.s.|| )" by XCMPLX_1:204;
A11: ||.t1.|| = |. ||.t.||".| * ||.t.|| by NORMSP_1:def 1
.= 1 by A6,A8,XCMPLX_0:def 7;
A12: ||.s1.|| = |. ||.s.||".| * ||.s.|| by NORMSP_1:def 1
.= 1 by A6,A9,XCMPLX_0:def 7;
||.g.(t,s).|| / ( ||.t.|| * ||.s.|| )
= ||.g.(t,s).|| * ( ||.t.|| * ||.s.|| )" by XCMPLX_0:def 9
.= ||. ( ||.t.|| * ||.s.|| )" * g.(t,s) .|| by A10,NORMSP_1:def 1
.= ||. ( ||.t.||" * ||.s.||" ) * g.(t,s) .|| by XCMPLX_1:204
.= ||. ||.t.||" * ( ||.s.||" * g.(t,s)) .|| by RLVECT_1:def 7
.= ||. ||.t.||" * ( g.(t,s1)) .|| by LOPBAN_8:12
.= ||. g.(t1,s1) .|| by LOPBAN_8:12;
then
||.g.(t,s).|| / ( ||.t.||*||.s.||)
in {||.g.(t,s).|| where t is VECTOR of X, s is VECTOR of Y
: ||.t.|| <= 1 & ||.s.|| <= 1 } by A11,A12;
then
||.g.(t,s).|| / (||.t.|| * ||.s.||) <= upper_bound PreNorms(g)
by SEQ_4:def 1;
then
A13: ||.g.(t,s).|| / (||.t.|| * ||.s.||) <= ||.f.|| by A1,Th30;
||.g.(t,s).|| / (||.t.|| * ||.s.||) * (||.t.|| * ||.s.||)
= ||.g.(t,s).|| * (||.t.|| * ||.s.||)" * (||.t.|| * ||.s.||)
by XCMPLX_0:def 9
.= ||.g.(t,s).|| * ((||.t.|| * ||.s.||)" * (||.t.|| * ||.s.||))
.= ||.g.(t,s).|| * 1 by A7,XCMPLX_0:def 7
.= ||.g.(t,s).||;
hence ||.g.(t,s).|| <= ||.f.|| * ( ||.t.|| * ||.s.|| )
by A13,XREAL_1:64;
end;
end;
hence ||.g.(t,s).|| <= ||.f.||*||.t.||*||.s.||;
end;
hence thesis;
end;
theorem Th33:
for X,Y,Z be RealNormSpace
for f being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
holds 0 <= ||.f.||
proof
let X,Y,Z be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
reconsider g=f as Lipschitzian BilinearOperator of X,Y,Z by Def9;
consider r0 be object such that
A1: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A1;
A3: BoundedBilinearOperatorsNorm(X,Y,Z).f
= upper_bound PreNorms(g) by Th30;
now
let r be Real;
assume r in PreNorms(g); then
ex t be VECTOR of X,s be VECTOR of Y
st r = ||.g.(t,s).|| & ||.t.|| <= 1 & ||.s.|| <= 1;
hence 0 <= r;
end;
then 0 <= r0 by A1;
hence thesis by A1,A3,SEQ_4:def 1;
end;
theorem Th34:
for X, Y, Z be 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
let X,Y,Z be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
such that
A1: f = 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
reconsider g=f as Lipschitzian BilinearOperator of X,Y,Z by Def9;
set z = (the carrier of [:X,Y:]) --> 0.Z;
reconsider z as Function of the carrier of [:X,Y:],the carrier of Z;
consider r0 be object such that
A2: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A2;
A3: (for s be Real st s in PreNorms(g) holds s <= 0)
implies upper_bound PreNorms(g) <= 0 by SEQ_4:45;
A5: z=g by A1,Th31;
A6: now
let r be Real;
assume r in PreNorms(g); then
consider t be VECTOR of X,s be VECTOR of Y such that
A7: r = ||.g.(t,s).|| and
||.t.|| <= 1 & ||.s.|| <= 1;
[t,s] is Point of [:X,Y:]; then
g.(t,s) = 0.Z by FUNCOP_1:7,A5;
hence 0 <= r & r <=0 by A7;
end;
then 0 <= r0 by A2;
then upper_bound PreNorms(g) = 0 by A6,A2,A3,SEQ_4:def 1;
hence thesis by Th30;
end;
registration
let X,Y,Z be RealNormSpace;
cluster -> Function-like Relation-like for Element of
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
coherence;
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,w be VECTOR of Y;
redefine func f.(v,w) -> VECTOR of Z; :: redefines . (BINOP_1, definition)
coherence
proof
reconsider f as BilinearOperator of X,Y,Z by Def9;
f.(v,w) is VECTOR of Z;
hence thesis;
end;
end;
theorem Th35:
for X, Y, Z be RealNormSpace
for f,g,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
holds
h = f+g
iff
for x be VECTOR of X,y be VECTOR of Y
holds h.(x,y) = f.(x,y) + g.(x,y)
proof
let X, Y, Z be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
reconsider f1=f, g1=g, h1=h
as VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z);
h=f+g iff h1=f1+g1;
hence thesis by Th24;
end;
theorem Th36:
for X, Y, Z be RealNormSpace
for f,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
for a be Real
holds
h = a*f
iff
for x be VECTOR of X,y be VECTOR of Y
holds h.(x,y) = a * f.(x,y)
proof
let X,Y,Z be RealNormSpace;
let f,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
let a be Real;
reconsider f1=f
as VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z);
reconsider h1=h
as VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z);
h = a*f iff h1 = a*f1;
hence thesis by Th25;
end;
theorem Th37:
for X,Y,Z be RealNormSpace
for f, g being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
for a be Real
holds
( ||.f.|| = 0 iff f = 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) )
& ||.a*f.|| = |.a.| * ||.f.||
& ||.f+g.|| <= ||.f.|| + ||.g.||
proof
let X,Y,Z be RealNormSpace;
let f, g being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
let a be Real;
A1: now
assume
A2: f = 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
thus ||.f.|| = 0
proof
reconsider g=f as Lipschitzian BilinearOperator of X,Y,Z by Def9;
set z = (the carrier of [:X,Y:]) --> 0.Z;
reconsider z as Function of the carrier of [:X,Y:], the carrier of Z;
consider r0 be object such that
A3: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A3;
A4: (for s be Real st s in PreNorms(g) holds s <= 0)
implies upper_bound PreNorms(g) <= 0 by SEQ_4:45;
A6: z=g by A2,Th31;
A7: now
let r be Real;
assume r in PreNorms(g); then
consider t be VECTOR of X, s be VECTOR of Y such that
A8: r = ||.g.(t,s).|| and
||.t.|| <= 1 & ||.s.|| <= 1;
[t,s] is Point of [:X,Y:]; then
g.(t,s) = 0.Z by A6,FUNCOP_1:7;
hence 0 <= r & r <=0 by A8;
end;
then 0<=r0 by A3;
then upper_bound PreNorms(g) = 0 by A3,A4,A7,SEQ_4:def 1;
hence thesis by Th30;
end;
end;
A9: ||.f+g.|| <= ||.f.|| + ||.g.||
proof
reconsider f1=f, g1=g, h1=f+g
as Lipschitzian BilinearOperator of X,Y,Z by Def9;
A10: ( for s be Real st s in PreNorms(h1)
holds s <= ||.f.|| + ||.g.||)
implies upper_bound PreNorms(h1) <= ||.f.|| + ||.g.|| by SEQ_4:45;
A11: now
let t be VECTOR of X,s be VECTOR of Y such that
A12: ||.t.|| <= 1 & ||.s.|| <= 1;
A13: ||.t.|| * ||.s.|| <= 1 * 1 by A12,XREAL_1:66;
0 <= ||.g.|| by Th33; then
A14: ||.g.|| * ( ||.t.|| * ||.s.|| ) <= ||.g.|| * 1 by A13,XREAL_1:64;
0 <= ||.f.|| by Th33; then
||.f.|| * ( ||.t.|| * ||.s.|| ) <= ||.f.|| * 1 by A13,XREAL_1:64; then
A15: ||.f.|| * ||.t.|| * ||.s.|| + ||.g.|| * ||.t.|| * ||.s.||
<= ||.f.|| * 1 + ||.g.|| * 1 by A14,XREAL_1:7;
A16: ||.f1.(t,s)+g1.(t,s).|| <= ||.f1.(t,s).|| + ||.g1.(t,s).||
by NORMSP_1:def 1;
A17: ||.g1.(t,s).|| <= ||.g.|| * ||.t.|| * ||.s.|| by Th32;
||.f1.(t,s).|| <= ||.f.||*||.t.||*||.s.|| by Th32; then
||.f1.(t,s).||+||.g1.(t,s).||
<= ||.f.|| * ||.t.|| * ||.s.|| + ||.g.|| * ||.t.|| * ||.s.||
by A17,XREAL_1:7; then
A18: ||.f1.(t,s).|| + ||.g1.(t,s).||
<= ||.f.|| + ||.g.|| by A15,XXREAL_0:2;
||.h1.(t,s).|| = ||.f1.(t,s) + g1.(t,s).|| by Th35;
hence ||.h1.(t,s).|| <= ||.f.|| + ||.g.|| by A16,A18,XXREAL_0:2;
end;
now
let r be Real;
assume r in PreNorms(h1); then
ex t be VECTOR of X,s be VECTOR of Y
st r = ||.h1.(t,s).|| & ||.t.|| <= 1 & ||.s.|| <= 1;
hence r <= ||.f.|| + ||.g.|| by A11;
end;
hence thesis by A10,Th30;
end;
A20: ||.a*f.|| = |.a.| * ||.f.||
proof
reconsider f1=f, h1=a*f
as Lipschitzian BilinearOperator of X,Y,Z by Def9;
A21: (for s be Real st s in PreNorms(h1) holds s <= |.a.| * ||.f.|| )
implies upper_bound PreNorms(h1) <= |.a.| * ||.f.||
by SEQ_4:45;
A22: now
A23: 0 <= ||.f.|| by Th33;
let t be VECTOR of X,s be VECTOR of Y;
assume ||.t.|| <= 1 & ||.s.|| <= 1; then
||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66; then
A24: ||.f.|| * (||.t.|| * ||.s.|| ) <= ||.f.|| * 1 by A23,XREAL_1:64;
||.f1.(t,s).||<= ||.f.|| * ||.t.|| * ||.s.|| by Th32; then
A25: ||.f1.(t,s).|| <= ||.f.|| by A24,XXREAL_0:2;
A26: ||.a * f1.(t,s).|| =|.a.| * ||.f1.(t,s).|| by NORMSP_1:def 1;
A27: 0 <= |.a.| by COMPLEX1:46;
||.h1.(t,s).|| = ||.a * f1.(t,s).|| by Th36;
hence ||.h1.(t,s).|| <= |.a.| * ||.f.|| by A25,A26,A27,XREAL_1:64;
end;
A28: now
let r be Real;
assume r in PreNorms(h1); then
ex t be VECTOR of X, s be VECTOR of Y
st r = ||.h1.(t,s).||
& ||.t.|| <= 1
& ||.s.|| <= 1;
hence r <= |.a.|*||.f.|| by A22;
end;
A29: now
per cases;
case
A30: a <> 0;
A31: now
A32: 0 <= ||.a*f.|| by Th33;
let t be VECTOR of X,s be VECTOR of Y;
assume ||.t.|| <= 1 & ||.s.|| <= 1; then
||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66; then
A33: ||.a * f.|| * ( ||.t.|| * ||.s.|| )
<= ||.a * f.|| * 1 by A32,XREAL_1:64;
||.h1.(t,s).||<= ||.a*f.||*||.t.||*||.s.|| by Th32; then
A34: ||.h1.(t,s).|| <= ||.a*f.|| by A33,XXREAL_0:2;
h1.(t,s) = a * f1.(t,s) by Th36; then
A35: a"*h1.(t,s) = ( a"* a) * f1.(t,s) by RLVECT_1:def 7
.= 1 * f1.(t,s) by A30,XCMPLX_0:def 7
.= f1.(t,s) by RLVECT_1:def 8;
A36: |.a".| = |.1 * a".|
.= |. 1 / a .| by XCMPLX_0:def 9
.= 1 / |.a.| by ABSVALUE:7
.= 1 * |.a.|" by XCMPLX_0:def 9
.= |.a.|";
A37: 0 <= |.a".| by COMPLEX1:46;
||.a" * h1.(t,s).||
= |.a".| * ||.h1.(t,s).|| by NORMSP_1:def 1;
hence ||.f1.(t,s).||
<= |.a.|"*||.a*f.|| by A34,A35,A36,A37,XREAL_1:64;
end;
A38: now
let r be Real;
assume r in PreNorms(f1); then
ex t be VECTOR of X, s be VECTOR of Y
st r = ||.f1.(t,s).||
& ||.t.|| <= 1 & ||.s.|| <= 1;
hence r <= |.a.|"*||.a*f.|| by A31;
end;
A39: ( for s be Real st s in PreNorms(f1)
holds s <= |.a.|"* ||.a*f.|| )
implies upper_bound PreNorms(f1) <= |.a.|" * ||.a*f.||
by SEQ_4:45;
A40: 0 <= |.a.| by COMPLEX1:46;
||.f.|| <=|.a.|" * ||.a*f.|| by A38,A39,Th30; then
|.a.| * ||.f.|| <= |.a.| * (|.a.|" * ||.a*f.||)
by A40,XREAL_1:64; then
A41: |.a.| * ||.f.|| <= (|.a.| * |.a.|") * ||.a*f.||;
|.a.| <> 0 by A30,COMPLEX1:47; then
|.a.| * ||.f.|| <= 1 * ||.a*f.|| by A41,XCMPLX_0:def 7;
hence |.a.|* ||.f.|| <= ||.a*f.||;
end;
case
A42: a=0;
reconsider fz=f
as VECTOR of R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z);
A43: a*f = a*fz
.= 0.R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z)
by A42,RLVECT_1:10
.= 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
thus |.a.|* ||.f.|| = 0 * ||.f.|| by A42,ABSVALUE:2
.= ||.a*f.|| by A43,Th34;
end;
end;
||.a*f.|| <= |.a.| * ||.f.|| by A21,A28,Th30;
hence thesis by A29,XXREAL_0:1;
end;
now
reconsider g=f as Lipschitzian BilinearOperator of X,Y,Z by Def9;
set z = (the carrier of [:X,Y:] ) --> 0.Z;
reconsider z as Function of the carrier of [:X,Y:],the carrier of Z;
assume
A44: ||.f.|| = 0;
now
let t be VECTOR of X,s be VECTOR of Y;
A45: [t,s] is Point of [:X,Y:];
||.g.(t,s).|| <= ||.f.|| *||.t.||*||.s.|| by Th32; then
||.g.(t,s).|| = 0 by A44;
hence g.(t,s) = 0.Z by NORMSP_0:def 5
.= z.(t,s) by A45,FUNCOP_1:7;
end; then
g=z by BINOP_1:2;
hence f=0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) by Th31;
end;
hence thesis by A1,A9,A20;
end;
Th38:
for X,Y,Z be RealNormSpace holds
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) is
reflexive discerning RealNormSpace-like
proof
let X,Y,Z be RealNormSpace;
thus ||.0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z).|| = 0 by Th37;
for x, y being Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
for a be Real holds
( ||.x.|| = 0 iff x = 0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) )
& ||.a*x.|| = |.a.| * ||.x.||
& ||.x+y.|| <= ||.x.|| + ||.y.|| by Th37;
hence thesis by NORMSP_1:def 1,NORMSP_0:def 5;
end;
registration let X, Y, Z be RealNormSpace;
cluster R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) -> non empty;
coherence;
end;
registration let X, Y, Z be RealNormSpace;
cluster R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) ->
reflexive discerning RealNormSpace-like;
coherence by Th38;
end;
theorem Th39:
for X, Y, Z be RealNormSpace holds
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) is RealNormSpace
proof
let X, Y, Z be RealNormSpace;
R_VectorSpace_of_BoundedBilinearOperators(X,Y,Z) is RealLinearSpace;
hence thesis by RSSPACE3:2;
end;
registration
let X, Y, Z be RealNormSpace;
cluster R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) ->
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence by Th39;
end;
theorem Th40:
for X,Y,Z be RealNormSpace
for f,g,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
holds
h = f-g
iff
for x be VECTOR of X,y be VECTOR of Y
holds h.(x,y) = f.(x,y) - g.(x,y)
proof
let X, Y, Z be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
reconsider f9=f,g9=g,h9=h
as Lipschitzian BilinearOperator of X,Y,Z by Def9;
hereby
assume h=f-g; then
h+g=f-(g-g) by RLVECT_1:29; then
A1: h+g=f-0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
by RLVECT_1:15;
now
let x be VECTOR of X,y be VECTOR of Y;
f9.(x,y)=h9.(x,y) + g9.(x,y) by A1,Th35; then
f9.(x,y)-g9.(x,y)
= h9.(x,y) + (g9.(x,y)-g9.(x,y)) by RLVECT_1:def 3; then
f9.(x,y)-g9.(x,y)=h9.(x,y) + 0.Z by RLVECT_1:15;
hence f9.(x,y)-g9.(x,y)=h9.(x,y);
end;
hence for x be VECTOR of X,y be VECTOR of Y
holds h.(x,y) = f.(x,y) - g.(x,y);
end;
assume
A2: for x be VECTOR of X,y be VECTOR of Y
holds h.(x,y) = f.(x,y) - g.(x,y);
now
let x be VECTOR of X,y be VECTOR of Y;
h9.(x,y) = f9.(x,y) - g9.(x,y) by A2; then
h9.(x,y) + g9.(x,y)= f9.(x,y) - (g9.(x,y)- g9.(x,y))
by RLVECT_1:29; then
h9.(x,y) + g9.(x,y)= f9.(x,y) - 0.Z by RLVECT_1:15;
hence h9.(x,y) + g9.(x,y)= f9.(x,y);
end; then
f=h+g by Th35; then
f-g=h+(g-g) by RLVECT_1:def 3; then
f-g=h+0.R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) by RLVECT_1:15;
hence thesis;
end;
begin :: Real Banach Space of Bounded Bilinear Operators
Lm3: for e be Real, seq be Real_Sequence
st ( seq is convergent &
ex k be Nat
st for i be Nat st k <= i holds seq.i <= e )
holds lim seq <=e
proof
let e be Real;
let seq be Real_Sequence such that
A1: seq is convergent and
A2: ex k be Nat st for i be Nat st k <= i holds
seq.i <= e;
consider k be Nat such that
A3: for i be Nat st k <= i holds seq.i <= e by A2;
reconsider ee=e as Element of REAL by XREAL_0:def 1;
set cseq = seq_const e;
A4: lim cseq = cseq.1 by SEQ_4:26
.= e by SEQ_1:57;
A5: now
let i be Nat;
A6: (seq ^\k).i = seq.(k+i) by NAT_1:def 3;
seq.(k+i) <= e by A3,NAT_1:11;
hence (seq ^\k) .i <= cseq.i by A6,SEQ_1:57;
end;
lim (seq ^\k)=lim seq by A1,SEQ_4:20;
hence thesis by A1,A5,A4,SEQ_2:18;
end;
theorem Th42:
for X, Y, Z be RealNormSpace st Z is complete
for seq be sequence of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
st seq is Cauchy_sequence_by_Norm
holds seq is convergent
proof
let X, Y, Z be RealNormSpace such that
A1: Z is complete;
let vseq be sequence of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
such that
A2: vseq is Cauchy_sequence_by_Norm;
defpred P[set, set] means ex xseq be sequence of Z st
(for n be Nat holds xseq.n = (vseq.n).$1) &
xseq is convergent & $2= lim xseq;
A3: for xy be Element of [:X,Y:] ex z be Element of Z st P[xy,z]
proof
let xy be Element of [:X,Y:];
deffunc F(Nat) = modetrans((vseq.$1),X,Y,Z).xy;
consider xseq be sequence of Z such that
A4: for n be Element of NAT holds xseq.n = F(n)
from FUNCT_2:sch 4;
A5: for n be Nat holds xseq.n = (vseq.n).xy
proof
let n be Nat;
n in NAT by ORDINAL1:def 12; then
A6: xseq.n = modetrans((vseq.n),X,Y,Z).xy by A4;
vseq.n is Lipschitzian BilinearOperator of X,Y,Z by Def9;
hence thesis by A6;
end;
take lim xseq;
consider x be Point of X, y be Point of Y such that
A7: xy = [x,y] by PRVECT_3:18;
A8: for m,k be Nat holds ||.xseq.m-xseq.k.||
<= ||.vseq.m - vseq.k.|| * ( ||.x.||*||.y.|| )
proof
let m,k be Nat;
reconsider h1 = vseq.m-vseq.k
as Lipschitzian BilinearOperator of X,Y,Z by Def9;
A9: xseq.m = (vseq.m).(x,y) by A5,A7;
A10: xseq.k = (vseq.k).(x,y) by A5,A7;
xseq.m - xseq.k = h1.(x,y) by A9,A10,Th40; then
||.xseq.m - xseq.k.||
<= ||.vseq.m - vseq.k.|| * ||.x.|| * ||.y.|| by Th32;
hence thesis;
end;
now
let e be Real such that
A11: e > 0;
now
per cases;
case
A12: x=0.X or y =0.Y;
reconsider k=0 as Nat;
take k;
thus for n, m be Nat st n >= k & m >= k
holds ||.xseq.n - xseq.m.|| < e
proof
let n, m be Nat such that
n >= k and
m >= k;
A13: xseq.m = (vseq.m).(x,y) by A5,A7;
A14: vseq.m is Lipschitzian BilinearOperator of X,Y,Z
& vseq.n is Lipschitzian BilinearOperator of X,Y,Z
by Def9;
A15: x = 0*x or y = 0*y by A12; then
A16: (vseq.m).(x,y) = 0*(vseq.m).(x,y) by A14,LOPBAN_8:12
.= 0.Z by RLVECT_1:10;
A17: xseq.n = (vseq.n).(x,y) by A5,A7;
(vseq.n).(x,y) = 0*(vseq.n).(x,y) by A14,A15,LOPBAN_8:12
.= 0.Z by RLVECT_1:10;
hence thesis by A11,A13,A16,A17;
end;
end;
case
x <> 0.X & y <> 0.Y; then
||.x.|| <> 0 & ||.y.|| <> 0 by NORMSP_0:def 5; then
||.x.|| > 0 & ||.y.|| > 0; then
A18: 0 < ||.x.|| * ||.y.|| by XREAL_1:129; then
consider k be Nat such that
A19: for n, m be Nat st n >= k & m >= k
holds ||.(vseq.n) - (vseq.m).|| < e / (||.x.||*||.y.||)
by A2,A11,XREAL_1:139,RSSPACE3:8;
take k;
thus for n, m be Nat st n >= k & m >= k
holds ||.xseq.n - xseq.m.|| < e
proof
let n,m be Nat such that
A20: n >= k and
A21: m >= k;
||.(vseq.n) - (vseq.m).|| < e / (||.x.|| * ||.y.||)
by A19,A20,A21; then
A22: ||.(vseq.n) - (vseq.m).|| * (||.x.|| * ||.y.|| )
< e / (||.x.|| * ||.y.|| ) * (||.x.|| * ||.y.|| )
by A18,XREAL_1:68;
A23: e/(||.x.||*||.y.|| ) * (||.x.||*||.y.|| )
= e*(||.x.||*||.y.||)"* (||.x.||*||.y.|| ) by XCMPLX_0:def 9
.= e*((||.x.||*||.y.||)"* (||.x.||*||.y.|| ))
.= e*1 by A18,XCMPLX_0:def 7
.= e;
||.xseq.n-xseq.m.||
<= ||.(vseq.n) - (vseq.m).|| * (||.x.||*||.y.|| ) by A8;
hence thesis by A22,A23,XXREAL_0:2;
end;
end;
end;
hence ex k be Nat
st for n, m be Nat st n >= k & m >= k
holds ||.xseq.n -xseq.m.|| < e;
end; then
xseq is convergent by A1,RSSPACE3:8;
hence thesis by A5;
end;
consider f be Function of the carrier of [:X,Y:],
the carrier of Z such that
A24: for z be Element of [:X,Y:] holds P[z,f.z] from FUNCT_2:sch 3(A3);
reconsider tseq = f as Function of [:X,Y:],Z;
A25: for x1,x2 be Point of X, y be Point of Y
holds tseq.(x1+x2,y) = tseq.(x1,y) + tseq.(x2,y)
proof
let x1,x2 be Point of X, y be Point of Y;
reconsider x1y=[x1,y] as Point of [:X,Y:];
reconsider x2y=[x2,y] as Point of [:X,Y:];
reconsider x1x2y=[x1+x2,y] as Point of [:X,Y:];
consider sqx1y be sequence of Z such that
A26: for n be Nat holds sqx1y.n=(vseq.n).x1y
& sqx1y is convergent
& tseq.x1y = lim sqx1y by A24;
consider sqx2y be sequence of Z such that
A27: for n be Nat holds sqx2y.n=(vseq.n).x2y
& sqx2y is convergent
& tseq.x2y = lim sqx2y by A24;
consider sqx1x2y be sequence of Z such that
A28: for n be Nat holds sqx1x2y.n=(vseq.n).x1x2y
& sqx1x2y is convergent
& tseq.x1x2y = lim sqx1x2y by A24;
for n be Nat holds sqx1x2y.n = sqx1y.n + sqx2y.n
proof
let n be Nat;
A29: vseq.n is Lipschitzian BilinearOperator of X,Y,Z by Def9;
A30: sqx1y.n = (vseq.n).(x1,y) by A26;
A31: sqx2y.n = (vseq.n).(x2,y) by A27;
thus sqx1x2y.n = (vseq.n).(x1+x2,y) by A28
.= sqx1y.n + sqx2y.n by A29,A30,A31,LOPBAN_8:12;
end; then
A32: sqx1x2y = sqx1y + sqx2y by NORMSP_1:def 2;
thus tseq. (x1+x2,y) = tseq. (x1,y) + tseq. (x2,y)
by A26,A27,A28,A32,NORMSP_1:25;
end;
A33: for x be Point of X, y be Point of Y, a be Real
holds tseq.(a*x,y) = a * tseq.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
reconsider xy = [x,y] as Point of [:X,Y:];
reconsider axy = [a*x,y] as Point of [:X,Y:];
consider sqxy be sequence of Z such that
A34: for n be Nat holds sqxy.n = (vseq.n).xy
& sqxy is convergent
& tseq.xy = lim sqxy by A24;
consider sqaxy be sequence of Z such that
A35: for n be Nat holds sqaxy.n=(vseq.n).axy
& sqaxy is convergent
& tseq.axy = lim sqaxy by A24;
for n be Nat holds sqaxy.n = a*sqxy.n
proof
let n be Nat;
A36: vseq.n is Lipschitzian BilinearOperator of X,Y,Z by Def9;
sqaxy.n = (vseq.n).(a*x,y) by A35
.= a*(vseq.n).(x,y) by A36,LOPBAN_8:12;
hence sqaxy.n = a*sqxy.n by A34;
end;
then sqaxy = a*sqxy by NORMSP_1:def 5;
hence tseq.(a*x,y) = a * tseq.(x,y) by A34,A35,NORMSP_1:28;
end;
A40: for x be Point of X, y1,y2 be Point of Y
holds tseq.(x,y1+y2) = tseq.(x,y1) + tseq.(x,y2)
proof
let x be Point of X, y1,y2 be Point of Y;
reconsider x1y=[x,y1] as Point of [:X,Y:];
reconsider x2y=[x,y2] as Point of [:X,Y:];
reconsider x1x2y=[x,y1+y2] as Point of [:X,Y:];
consider sqx1y be sequence of Z such that
A41: for n be Nat holds sqx1y.n=(vseq.n).x1y
& sqx1y is convergent
& tseq.x1y = lim sqx1y by A24;
consider sqx2y be sequence of Z such that
A42: for n be Nat holds sqx2y.n=(vseq.n).x2y
& sqx2y is convergent
& tseq.x2y = lim sqx2y by A24;
consider sqx1x2y be sequence of Z such that
A43: for n be Nat holds sqx1x2y.n=(vseq.n).x1x2y
& sqx1x2y is convergent
& tseq.x1x2y = lim sqx1x2y by A24;
for n be Nat holds sqx1x2y.n = sqx1y.n + sqx2y.n
proof
let n be Nat;
A44: vseq.n is Lipschitzian BilinearOperator of X,Y,Z by Def9;
A45: sqx1y.n = (vseq.n).(x,y1) by A41;
A46: sqx2y.n = (vseq.n).(x,y2) by A42;
thus sqx1x2y.n = (vseq.n).(x,y1+y2) by A43
.= sqx1y.n + sqx2y.n by A44,A45,A46,LOPBAN_8:12;
end;
then sqx1x2y = sqx1y + sqx2y by NORMSP_1:def 2;
hence tseq.(x,y1+y2) = tseq.(x,y1) + tseq.(x,y2)
by A41,A42,A43,NORMSP_1:25;
end;
for x be Point of X, y be Point of Y, a be Real
holds tseq.(x,a*y) = a * tseq.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
reconsider xy = [x,y] as Point of [:X,Y:];
reconsider axy = [x,a*y] as Point of [:X,Y:];
consider sqxy be sequence of Z such that
A48: for n be Nat holds sqxy.n = (vseq.n).xy
& sqxy is convergent
& tseq.xy = lim sqxy by A24;
consider sqaxy be sequence of Z such that
A49: for n be Nat holds sqaxy.n = (vseq.n).axy
& sqaxy is convergent
& tseq.axy = lim sqaxy by A24;
for n be Nat holds sqaxy.n = a*sqxy.n
proof
let n be Nat;
A50: vseq.n is Lipschitzian BilinearOperator of X,Y,Z by Def9;
sqaxy.n = (vseq.n).(x,a*y) by A49
.= a*(vseq.n).(x,y) by A50,LOPBAN_8:12;
hence sqaxy.n = a*sqxy.n by A48;
end; then
sqaxy = a*sqxy by NORMSP_1:def 5;
hence tseq.(x,a*y) = a * tseq.(x,y) by A48,A49,NORMSP_1:28;
end;
then
reconsider tseq as BilinearOperator of X,Y,Z by A25,A33,A40,LOPBAN_8:12;
B53:
now
let e1 be Real such that
A54: e1 >0;
reconsider e =e1 as Real;
consider k be Nat such that
A55: for n, m be Nat st n >= k & m >= k holds
||.(vseq.n) - (vseq.m).|| < e by A2,A54,RSSPACE3:8;
reconsider k as Nat;
take k;
now
let m be Nat;
assume m >= k; then
A56: ||.(vseq.m) - (vseq.k).|| <e by A55;
A57: ||.vseq.m.||= ||.vseq.||.m by NORMSP_0:def 4;
A58: ||.vseq.k.||= ||.vseq.||.k by NORMSP_0:def 4;
|. ||.vseq.m.||- ||.vseq.k.|| .|
<= ||.(vseq.m) - (vseq.k).|| by NORMSP_1:9;
hence |. ||.vseq.||.m - ||.vseq.||.k .| <e1 by A56,A57,A58,XXREAL_0:2;
end;
hence for m be Nat st m >=k
holds |.||.vseq.||.m - ||.vseq.||.k .| < e1;
end; then
A59: ||.vseq.|| is convergent by SEQ_4:41;
A60: tseq is Lipschitzian
proof
take lim (||.vseq.|| );
A61: now
let x be Point of X, y be Point of Y;
reconsider xy = [x,y] as Point of [:X,Y:];
consider xyseq be sequence of Z such that
A62: for n be Nat holds xyseq.n = (vseq.n).xy and
A63: xyseq is convergent and
A64: tseq.xy = lim xyseq by A24;
A65: ||.tseq.xy.|| = lim ||.xyseq.|| by A63,A64,LOPBAN_1:20;
A66: for m be Nat
holds ||.xyseq.m.|| <= ||.vseq.m.|| * ( ||.x.|| * ||.y.|| )
proof
let m be Nat;
vseq.m is Lipschitzian BilinearOperator of X,Y,Z by Def9; then
||.(vseq.m).(x,y).|| <= ||.vseq.m.|| * ||.x.|| * ||.y.|| by Th32;
hence ||.xyseq.m.|| <= ||.vseq.m.|| * ( ||.x.|| * ||.y.|| ) by A62;
end;
A68: for n be Nat holds
||.xyseq.||.n <= ( (||.x.|| * ||.y.||)(#)||.vseq .||).n
proof
let n be Nat;
A69: ||.xyseq.||.n = ||.(xyseq.n).|| by NORMSP_0:def 4;
A70: ||.vseq.n.|| = ||.vseq.||.n by NORMSP_0:def 4;
||.(xyseq.n).|| <= ||.vseq.n.|| * (||.x.|| * ||.y.||) by A66;
hence thesis by A69,A70,SEQ_1:9;
end;
A72: lim ( ( ||.x.||*||.y.|| )(#)||.vseq.|| )
= lim (||.vseq.|| ) * ( ||.x.||*||.y.|| ) by B53,SEQ_2:8,SEQ_4:41;
||.xyseq.|| is convergent by A63,A64,LOPBAN_1:20;
hence ||.tseq.(x,y).|| <= lim (||.vseq.|| ) * ||.x.|| * ||.y.||
by A59,A65,A68,A72,SEQ_2:18;
end;
now
let n be Nat;
||.vseq.n.|| >= 0;
hence ||.vseq.||.n >= 0 by NORMSP_0:def 4;
end;
hence thesis by B53,A61,SEQ_2:17,SEQ_4:41;
end;
A73: for e be Real
st e > 0 ex k be Nat st for n be Nat st n >= k
holds for x be Point of X, y be Point of Y
holds ||.(vseq.n).(x,y) - tseq.(x,y) .|| <= e * ||.x.|| * ||.y.||
proof
let e be Real;
assume e > 0; then
consider k be Nat such that
A74: for n, m be Nat st n >= k & m >= k
holds ||.(vseq.n) - (vseq.m).|| < e by A2,RSSPACE3:8;
take k;
now
let n be Nat such that
A75: n >= k;
now
let x be Point of X, y be Point of Y;
reconsider xy = [x,y] as Point of [:X,Y:];
consider xyseq be sequence of Z such that
A76: for n be Nat holds xyseq.n=(vseq.n). xy and
A77: xyseq is convergent and
A78: tseq.xy = lim xyseq by A24;
A79: for m,k be Nat
holds ||.xyseq.m-xyseq.k.||
<= ||.vseq.m - vseq.k.|| * ( ||.x.|| * ||.y.|| )
proof
let m,k be Nat;
reconsider h1 = vseq.m-vseq.k
as Lipschitzian BilinearOperator of X,Y,Z by Def9;
xyseq.k = (vseq.k).xy by A76; then
xyseq.m - xyseq.k = (vseq.m).(x,y)-(vseq.k).(x,y) by A76
.= h1.(x,y) by Th40; then
||.xyseq.m-xyseq.k.||
<= ||.vseq.m - vseq.k.|| * ||.x.|| * ||.y.|| by Th32;
hence thesis;
end;
A81: for m be Nat st m >= k
holds ||.xyseq.n - xyseq.m.|| <= e * ||.x.|| * ||.y.||
proof
let m be Nat;
assume m >= k; then
A82: ||.vseq.n - vseq.m.|| < e by A74,A75;
A83: ||.xyseq.n - xyseq.m.||
<= ||.vseq.n - vseq.m.|| * ( ||.x.||*||.y.|| ) by A79;
||.vseq.n - vseq.m.|| * ( ||.x.||*||.y.|| )
<= e * ( ||.x.|| * ||.y.|| ) by A82,XREAL_1:64;
hence thesis by A83,XXREAL_0:2;
end;
||.xyseq.n - tseq.(x,y).|| <= e * ||.x.|| * ||.y.||
proof
deffunc F(Nat) = ||.xyseq.$1 - xyseq.n.||;
consider rseq be Real_Sequence such that
A84: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
now
let i be object;
assume i in NAT; then
reconsider k=i as Nat;
thus rseq.i = ||.xyseq.k - xyseq.n.|| by A84
.= ||.(xyseq - xyseq.n).k.|| by NORMSP_1:def 4
.= ||.(xyseq - xyseq.n).||.i by NORMSP_0:def 4;
end;
then
A85: rseq = ||.xyseq - xyseq.n.|| by FUNCT_2:12;
A86: xyseq - xyseq.n is convergent by A77,NORMSP_1:21;
lim (xyseq-xyseq.n) = tseq.(x,y) - xyseq.n
by A77,A78,NORMSP_1:27; then
A87: lim rseq = ||.tseq.(x,y)-xyseq.n.|| by A85,A86,LOPBAN_1:41;
for m be Nat st m >= k holds rseq.m <= e * ||.x.||*||.y.||
proof
let m be Nat such that
A88: m >= k;
rseq.m = ||.xyseq.m - xyseq.n.|| by A84
.= ||.xyseq.n - xyseq.m.|| by NORMSP_1:7;
hence thesis by A81,A88;
end; then
lim rseq <= e * ||.x.||*||.y.|| by A85,A86,LOPBAN_1:41,Lm3;
hence thesis by A87,NORMSP_1:7;
end;
hence ||.(vseq.n).(x,y) - tseq.(x,y).||
<= e * ||.x.|| * ||.y.|| by A76;
end;
hence
for x be Point of X, y be Point of Y
holds ||.(vseq.n).(x,y) - tseq.(x,y).|| <= e * ||.x.|| * ||.y.||;
end;
hence thesis;
end;
reconsider tseq as Lipschitzian BilinearOperator of X,Y,Z by A60;
reconsider tv = tseq as Point of
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) by Def9;
A89: for e be Real st e > 0
ex k be Nat
st for n be Nat st n >= k holds ||.vseq.n - tv.|| <= e
proof
let e be Real such that
A90: e > 0;
consider k be Nat such that
A91: for n be Nat st n >= k holds
for x be Point of X,y be Point of Y
holds ||.(vseq.n).(x,y) - tseq.(x,y) .||
<= e * ||.x.|| * ||.y.|| by A73,A90;
now
set g1 = tseq;
let n be Nat such that
A92: n >= k;
reconsider h1 = vseq.n-tv
as Lipschitzian BilinearOperator of X,Y,Z by Def9;
set f1 = vseq.n;
A93: now
let t be Point of X, s be Point of Y;
assume ||.t.|| <= 1 & ||.s.|| <= 1; then
||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66; then
A94: e * ( ||.t.|| * ||.s.|| ) <= e * 1 by A90,XREAL_1:64;
A95: ||.f1.(t,s)-g1.(t,s).|| <= e * ||.t.|| * ||.s.|| by A91,A92;
||.h1.(t,s).|| = ||.f1.(t,s)-g1.(t,s).|| by Th40;
hence ||.h1.(t,s) .|| <= e by A94,A95,XXREAL_0:2;
end;
A96: now
let r be Real;
assume r in PreNorms(h1); then
ex t be VECTOR of X, s be VECTOR of Y
st r = ||.h1.(t,s).|| & ||.t.|| <= 1 & ||.s.|| <= 1;
hence r <= e by A93;
end;
(for s be Real st s in PreNorms(h1) holds s <= e)
implies upper_bound PreNorms(h1) <= e by SEQ_4:45;
hence ||.vseq.n-tv.|| <=e by A96,Th30;
end;
hence thesis;
end;
for e be Real st e > 0
ex m be Nat
st for n be Nat st n >= m holds ||.(vseq.n) - tv.|| < e
proof
let e be Real such that
A98: e > 0;
consider m be Nat such that
A99: for n be Nat st n >= m holds ||.(vseq.n) - tv.|| <= e/2
by A89,A98,XREAL_1:215;
A100: e/2 < e by A98,XREAL_1:216;
now
let n be Nat;
assume n >= m;
then ||.(vseq.n) - tv.|| <= e/2 by A99;
hence ||.(vseq.n) - tv.|| < e by A100,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis by NORMSP_1:def 6;
end;
theorem Th43:
for X,Y be RealNormSpace, Z be RealBanachSpace
holds R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) is RealBanachSpace
proof
let X,Y be RealNormSpace;
let Z be RealBanachSpace;
for seq be sequence of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
st seq is Cauchy_sequence_by_Norm
holds seq is convergent by Th42;
hence thesis by LOPBAN_1:def 15;
end;
registration
let X,Y be RealNormSpace;
let Z be RealBanachSpace;
cluster R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) -> complete;
coherence by Th43;
end;
begin :: Isomorphic Mappings between the Space of Bilinear Operators
:: and the Space of Composition of Linear Operators
reserve X,Y,Z for RealLinearSpace;
theorem
ex I be 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 be Point of
R_VectorSpace_of_LinearOperators(X,R_VectorSpace_of_LinearOperators(Y,Z))
holds
for x be Point of X,y be Point of Y
holds (I.u).(x,y) = (u.x).y
proof
set XC = the carrier of X;
set YC = the carrier of Y;
set ZC = the carrier of Z;
consider I0 being Function of Funcs(XC,Funcs(YC,ZC)), Funcs([:XC,YC:],ZC)
such that
A1: I0 is bijective
& for f being Function of XC,Funcs(YC,ZC)
for d, e being object st d in XC & e in YC
holds (I0 . f) . (d, e) = (f . d) . e by NDIFF_6:1;
set LXYZ = the carrier of R_VectorSpace_of_LinearOperators
(X,R_VectorSpace_of_LinearOperators(Y,Z));
set BXYZ = the carrier of R_VectorSpace_of_BilinearOperators(X,Y,Z);
set LYZ = the carrier of R_VectorSpace_of_LinearOperators(Y,Z);
now
let x be object;
assume x in Funcs(XC, LYZ); then
consider f being Function such that
A5: x = f & dom f = XC & rng f c= LYZ by FUNCT_2:def 2;
rng f c= Funcs(YC, ZC) by A5,XBOOLE_1:1;
hence x in Funcs(XC, Funcs( YC,ZC)) by A5,FUNCT_2:def 2;
end; then
A6: Funcs(XC, LYZ) c= Funcs(XC, Funcs(YC,ZC)) by TARSKI:def 3; then
LXYZ c= Funcs(XC, Funcs( YC,ZC)) by XBOOLE_1:1; then
reconsider I = I0 | LXYZ as Function of LXYZ,Funcs ([:XC,YC:],ZC)
by FUNCT_2:32;
A7: for x being Element of LXYZ holds
( for p be Point of X,q be Point of Y holds
ex G be LinearOperator of Y,Z
st G = x.p & (I.x).(p,q) = G.q )
& I.x in BXYZ
proof
let f be Element of LXYZ;
A8: I.f = I0.f by FUNCT_1:49;
A9: f in Funcs(XC, Funcs( YC,ZC)) by A6,TARSKI:def 3,XBOOLE_1:1; then
A10: f is Function of XC, Funcs(YC,ZC) by FUNCT_2:66;
reconsider g = f as Function of XC, Funcs(YC,ZC) by A9,FUNCT_2:66;
reconsider F = f
as LinearOperator of X,R_VectorSpace_of_LinearOperators(Y,Z)
by LOPBAN_1:def 6;
thus for x be Point of X,y be Point of Y holds
ex G be LinearOperator of Y,Z
st G = f.x & (I . f) . (x,y) = G.y
proof
let x be Point of X,y be Point of Y;
g.x = F.x; then
reconsider G = g.x as LinearOperator of Y,Z by LOPBAN_1:def 6;
take G;
thus thesis by A1,A8;
end;
reconsider BL = I0.f as Function of [:X,Y:],Z by A9,FUNCT_2:5,66;
A14: for x1,x2 be Point of X, y be Point of Y
holds BL.(x1+x2,y) = BL.(x1,y) + BL.(x2,y)
proof
let x1,x2 be Point of X, y be Point of Y;
A15: BL.(x1,y) = (F.x1).y by A1,A10;
A16: BL.(x2,y) = (F.x2).y by A1,A10;
A17: BL.(x1+x2,y) = (F.(x1+x2)).y by A1,A10;
F.(x1+x2) = F.x1 + F.x2 by VECTSP_1:def 20;
hence thesis by A15,A16,A17,LOPBAN_1:16;
end;
A18: for x be Point of X, y be Point of Y, a be Real
holds BL.(a*x,y) = a * BL.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
A19: BL.(a*x,y) = (F.(a*x)).y by A1,A10;
A20: BL.(x,y) = (F.x).y by A1,A10;
F.(a*x) = a * F.x by LOPBAN_1:def 5;
hence thesis by A19,A20,LOPBAN_1:17;
end;
A21: for x be Point of X, y1,y2 be Point of Y
holds BL.(x,y1+y2) = BL.(x,y1) + BL.(x,y2)
proof
let x be Point of X, y1,y2 be Point of Y;
reconsider Fx = F.x as LinearOperator of Y,Z by LOPBAN_1:def 6;
A22: BL.(x,y1) = Fx.y1 by A1,A10;
A23: BL.(x,y2) = Fx.y2 by A1,A10;
BL.(x,y1+y2) = Fx.(y1+y2) by A1,A10;
hence thesis by A22,A23,VECTSP_1:def 20;
end;
A25: for x be Point of X, y be Point of Y, a be Real
holds BL.(x,a*y) = a * BL.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
reconsider Fx = F.x as LinearOperator of Y,Z by LOPBAN_1:def 6;
A26: BL.(x,y) = Fx.y by A1,A10;
BL. (x,a*y) = Fx.(a*y) by A1,A10;
hence thesis by A26,LOPBAN_1:def 5;
end;
reconsider BL as BilinearOperator of X,Y,Z
by A14,A18,A21,A25,LOPBAN_8:11;
BL in BXYZ by Def6;
hence I.f in BXYZ by FUNCT_1:49;
end; then
rng I c= BXYZ by FUNCT_2:114; then
reconsider I as Function of LXYZ,BXYZ by FUNCT_2:6;
A28: for x1,x2 be Element of LXYZ holds I.(x1+x2) = I.x1 + I.x2
proof
let x1,x2 be Element of LXYZ;
for p be Point of X,q be Point of Y
holds (I.(x1+x2)).(p,q) = (I.x1).(p,q) + (I.x2).(p,q)
proof
let p be Point of X,q be Point of Y;
consider Gx1p be LinearOperator of Y,Z such that
A29: Gx1p = x1.p & (I.x1).(p,q) = Gx1p.q by A7;
consider Gx2p be LinearOperator of Y,Z such that
A30: Gx2p = x2.p & (I.x2).(p,q) = Gx2p.q by A7;
consider Gx1x2p be LinearOperator of Y,Z such that
A31: Gx1x2p = (x1+x2).p & (I.(x1+x2)).(p,q) = Gx1x2p.q by A7;
(x1+x2).p = x1.p + x2.p by LOPBAN_1:16;
hence thesis by A29,A30,A31,LOPBAN_1:16;
end;
hence thesis by Th16;
end;
for x be Element of LXYZ, a be Real holds I.(a*x) = a * I.x
proof
let x be Element of LXYZ, a be Real;
for p be Point of X,q be Point of Y
holds (I.(a*x)).(p,q) = a * (I.x).(p,q)
proof
let p be Point of X, q be Point of Y;
consider Gxp be LinearOperator of Y,Z such that
A33: Gxp = x.p & (I.x).(p,q) = Gxp.q by A7;
consider Gxap be LinearOperator of Y,Z such that
A34: Gxap = (a*x).p & (I.(a*x)).(p,q) = Gxap.q by A7;
(a*x).p = a * x.p by LOPBAN_1:17;
hence thesis by A33,A34,LOPBAN_1:17;
end;
hence thesis by Th17;
end;
then
reconsider I as LinearOperator of
R_VectorSpace_of_LinearOperators(X,
R_VectorSpace_of_LinearOperators(Y,Z)),
R_VectorSpace_of_BilinearOperators(X,Y,Z)
by A28,LOPBAN_1:def 5,VECTSP_1:def 20;
A36: for u be Point of R_VectorSpace_of_LinearOperators
(X,R_VectorSpace_of_LinearOperators(Y,Z)) holds
for x be Point of X,y be Point of Y holds
(I.u).(x,y) = (u.x).y
proof
let u be Point of R_VectorSpace_of_LinearOperators
(X,R_VectorSpace_of_LinearOperators(Y,Z));
let p be Point of X,q be Point of Y;
consider G be LinearOperator of Y,Z such that
A37: G = u.p & (I.u).(p,q) = G.q by A7;
thus (I.u).(p,q) = (u.p).q by A37;
end;
for y being object st y in BXYZ holds
ex x being object st x in LXYZ & y = I.x
proof
let y be object;
assume
A39: y in BXYZ; then
y in Funcs ([:XC,YC:],ZC); then
y in rng I0 by A1,FUNCT_2:def 3; then
consider f be object such that
A40: f in Funcs (XC,Funcs (YC,ZC)) & I0 . f = y by FUNCT_2:11;
reconsider f as Function of XC,Funcs (YC,ZC) by A40,FUNCT_2:66;
reconsider BL = y as BilinearOperator of X,Y,Z by A39,Def6;
reconsider BLp = BL
as Point of R_VectorSpace_of_BilinearOperators(X,Y,Z)
by Def6;
A42: dom f = XC by FUNCT_2:def 1;
for x being object st x in XC holds f . x in LYZ
proof
let x be object;
assume
A43: x in XC; then
reconsider fx = f.x as Function of YC,ZC by FUNCT_2:5,66;
reconsider xp = x as Point of X by A43;
A44: for p be Point of Y,q be Point of Y
holds fx.(p+q) = fx.p + fx.q
proof
let p be Point of Y,q be Point of Y;
A45: BL.(xp,p) = fx.p by A1,A40;
A46: BL.(xp,q) = fx.q by A1,A40;
BL.(xp,p+q) = fx.(p+q) by A1,A40;
hence fx.(p+q) = fx.p +fx.q by A45,A46,LOPBAN_8:11;
end;
for p be Point of Y,a be Real holds fx.(a*p) = a * fx.p
proof
let p be Point of Y,a be Real;
A48: BL.(xp,p) = fx.p by A1,A40;
BL.(xp,a*p) = fx.(a*p) by A1,A40;
hence fx.(a*p) = a * fx.p by A48,LOPBAN_8:11;
end; then
reconsider fx as LinearOperator of Y,Z
by A44,LOPBAN_1:def 5,VECTSP_1:def 20;
fx in LYZ by LOPBAN_1:def 6;
hence f.x in LYZ;
end; then
reconsider f as Function of XC,LYZ by A42,FUNCT_2:3;
A50: for x1,x2 be Point of X holds f.(x1+x2) = f.x1 + f.x2
proof
let x1,x2 be Point of X;
reconsider fx1x2 = f.(x1+x2)
as LinearOperator of Y,Z by LOPBAN_1:def 6;
reconsider fx1 = f.x1 as LinearOperator of Y,Z by LOPBAN_1:def 6;
reconsider fx2 = f.x2 as LinearOperator of Y,Z by LOPBAN_1:def 6;
for y be Point of Y holds fx1x2.y = fx1.y + fx2.y
proof
let y be Point of Y;
A51: BL.(x1,y) = fx1.y by A1,A40;
A52: BL.(x2,y) = fx2.y by A1,A40;
BL.(x1+x2,y) = fx1x2.y by A1,A40;
hence fx1x2.y = fx1.y + fx2.y by A51,A52,LOPBAN_8:11;
end;
hence f.(x1+x2) = f.x1 + f.x2 by LOPBAN_1:16;
end;
for x be Point of X,a be Real holds f.(a*x) = a*f.x
proof
let x be Point of X,a be Real;
reconsider fx = f.x as LinearOperator of Y,Z by LOPBAN_1:def 6;
reconsider fax = f.(a*x) as LinearOperator of Y,Z by LOPBAN_1:def 6;
for y be Point of Y holds fax.y = a * fx.y
proof
let y be Point of Y;
A54: BL.(x,y) = fx.y by A1,A40;
BL.(a*x,y) = fax.y by A1,A40;
hence fax.y = a * fx.y by A54,LOPBAN_8:11;
end;
hence f.(a*x) = a * f.x by LOPBAN_1:17;
end; then
reconsider f as LinearOperator of X,
R_VectorSpace_of_LinearOperators(Y,Z)
by A50,LOPBAN_1:def 5,VECTSP_1:def 20;
A56: f in LXYZ by LOPBAN_1:def 6;
take f;
thus thesis by A40,A56,FUNCT_1:49;
end; then
A58: rng I = BXYZ by FUNCT_2:10;
reconsider I as LinearOperator of R_VectorSpace_of_LinearOperators
(X,R_VectorSpace_of_LinearOperators(Y,Z)),
R_VectorSpace_of_BilinearOperators(X,Y,Z);
take I;
I is one-to-one onto by A1,A58,FUNCT_1:52,FUNCT_2:def 3;
hence thesis by A36;
end;
reserve X,Y,Z for RealNormSpace;
theorem
ex I be 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 be Point of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z))
holds
||.u.|| = ||. I.u .||
& for x be Point of X,y be Point of Y
holds (I.u).(x,y) = (u.x).y
proof
set XC = the carrier of X;
set YC = the carrier of Y;
set ZC = the carrier of Z;
consider I0 being Function of Funcs (XC,Funcs (YC,ZC)),Funcs ([:XC,YC:],ZC)
such that
A1: I0 is bijective
& for f being Function of XC,Funcs (YC,ZC)
for d, e being object st d in XC & e in YC holds
(I0 . f) . (d, e) = (f . d) . e by NDIFF_6:1;
set LXYZ = the carrier of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z));
set BXYZ = the carrier of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z);
set LYZ = the carrier of R_NormSpace_of_BoundedLinearOperators(Y,Z);
A3: LYZ c= Funcs(YC,ZC) by XBOOLE_1:1;
A4: LXYZ c= Funcs(XC, LYZ) by XBOOLE_1:1;
Funcs(XC, LYZ) c= Funcs(XC, Funcs(YC,ZC))
proof
let x be object;
assume x in Funcs(XC, LYZ); then
consider f being Function such that
A6: x = f & dom f = XC & rng f c= LYZ by FUNCT_2:def 2;
rng f c= Funcs(YC, ZC) by A3,A6,XBOOLE_1:1;
hence x in Funcs(XC, Funcs(YC,ZC)) by A6,FUNCT_2:def 2;
end; then
A7: LXYZ c= Funcs(XC, Funcs( YC,ZC)) by A4,XBOOLE_1:1; then
reconsider I = I0 | LXYZ as Function of LXYZ,Funcs ([:XC,YC:],ZC)
by FUNCT_2:32;
A8: for x being Element of LXYZ holds
( for p be Point of X,q be Point of Y
holds
ex G be Lipschitzian LinearOperator of Y,Z
st G = x.p
& (I.x).(p,q) = G.q )
& I.x is Lipschitzian BilinearOperator of X,Y,Z
& I.x in BXYZ
& ex Ix be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
st Ix = I.x & ||.x.|| = ||.Ix.||
proof
let f being Element of LXYZ;
A9: I.f = I0.f by FUNCT_1:49;
A10: f in Funcs(XC, Funcs(YC,ZC)) by A7,TARSKI:def 3;
A11: f is Function of XC, Funcs(YC,ZC)
by A7,TARSKI:def 3,FUNCT_2:66;
reconsider g = f as Function of XC, Funcs(YC,ZC)
by A7,TARSKI:def 3,FUNCT_2:66;
reconsider F = f as Lipschitzian LinearOperator of
X,R_NormSpace_of_BoundedLinearOperators(Y,Z) by LOPBAN_1:def 9;
thus for x be Point of X,y be Point of Y holds
ex G be Lipschitzian LinearOperator of Y,Z
st G = f.x & (I . f) . (x,y) = G.y
proof
let x be Point of X,y be Point of Y;
g.x = F.x; then
reconsider G = g.x
as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
take G;
thus thesis by A1,A9;
end;
reconsider BL = I0.f as Function of [:X,Y:],Z by A10,FUNCT_2:5,66;
A15: for x1,x2 be Point of X, y be Point of Y
holds BL. (x1+x2,y) = BL. (x1,y) + BL. (x2,y)
proof
let x1,x2 be Point of X, y be Point of Y;
A16: BL.(x1,y) = (F.x1).y by A1,A11;
A17: BL.(x2,y) = (F.x2).y by A1,A11;
A18: BL.(x1+x2,y) = (F.(x1+x2)).y by A1,A11;
F.(x1+x2) = F.x1 + F.x2 by VECTSP_1:def 20;
hence thesis by A16,A17,A18,LOPBAN_1:35;
end;
A19: for x be Point of X, y be Point of Y, a be Real
holds BL.(a*x,y) = a * BL.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
A20: BL.(a*x,y) = (F.(a*x)).y by A1,A11;
A21: BL.(x,y) = (F.x).y by A1,A11;
F.(a*x) = a * F.x by LOPBAN_1:def 5;
hence thesis by A20,A21,LOPBAN_1:36;
end;
A22: for x be Point of X, y1,y2 be Point of Y
holds BL.(x,y1+y2) = BL.(x,y1) + BL.(x,y2)
proof
let x be Point of X, y1,y2 be Point of Y;
reconsider Fx = F.x
as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
A23: BL.(x,y1) = Fx.y1 by A1,A11;
A24: BL.(x,y2) = Fx.y2 by A1,A11;
BL.(x,y1+y2) = Fx.(y1+y2) by A1,A11;
hence thesis by A23,A24,VECTSP_1:def 20;
end;
A26: for x be Point of X, y be Point of Y, a be Real
holds BL. (x,a*y) = a* BL.(x,y)
proof
let x be Point of X, y be Point of Y, a be Real;
reconsider Fx = F.x as Lipschitzian LinearOperator of Y,Z
by LOPBAN_1:def 9;
A27: BL.(x,y) = Fx.y by A1,A11;
BL. (x,a*y) = Fx.(a*y) by A1,A11;
hence thesis by A27,LOPBAN_1:def 5;
end;
reconsider BL as BilinearOperator of X,Y,Z
by A15,A19,A22,A26,LOPBAN_8:12;
A29: for x be Point of X, y be Point of Y
holds ||.BL.(x,y) .|| <= ||.f.|| * ||.x.|| * ||.y.||
proof
let x be Point of X, y be Point of Y;
reconsider Fx = F.x as Lipschitzian LinearOperator of Y,Z
by LOPBAN_1:def 9;
A30: BL.(x,y) = Fx.y by A1,A11;
A31: ||.Fx.y .|| <= ||.F.x.||* ||.y.|| by LOPBAN_1:32;
||.F.x.|| * ||.y.|| <= ||.f.|| * ||.x.|| * ||.y.||
by LOPBAN_1:32,XREAL_1:64;
hence ||.BL.(x,y) .|| <= ||.f.|| * ||.x.|| * ||.y.||
by A30,A31,XXREAL_0:2;
end;
then
reconsider BL as Lipschitzian BilinearOperator of X,Y,Z
by Def8;
reconsider BLp = BL as Point of
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) by Def9;
I.f = BL by FUNCT_1:49;
hence I.f is Lipschitzian BilinearOperator of X,Y,Z;
BLp in BXYZ;
hence I.f in BXYZ by FUNCT_1:49;
A33: ||.BLp.|| = upper_bound (PreNorms(modetrans(BL,X,Y,Z))) by Def13
.= upper_bound (PreNorms(BL));
now
let r be Real;
assume r in PreNorms(BL); then
consider t be VECTOR of X,s be VECTOR of Y such that
A34: r = ||. BL.(t,s) .|| and
A35: ||.t.|| <= 1 & ||.s.|| <= 1;
A36: ||.BL.(t,s).|| <= ||.f.|| * ||. t .|| * ||. s .|| by A29;
||. t .|| * ||. s .|| <= 1 * 1 by A35,XREAL_1:66; then
||.f.|| * ( ||. t .|| * ||. s .|| ) <= ||.f.|| * 1
by XREAL_1:64;
hence r <= ||.f.|| by A34,A36,XXREAL_0:2;
end; then
A37: ||.BLp.|| <= ||.f.|| by A33,SEQ_4:45;
A39: ||.f.|| = upper_bound (PreNorms
(modetrans(F,X,R_NormSpace_of_BoundedLinearOperators(Y,Z))))
by LOPBAN_1:def 13
.= upper_bound(PreNorms(F) ) by LOPBAN_1:29;
now
let r be Real;
assume r in PreNorms(F); then
consider x be VECTOR of X such that
A40: r = ||. F.x .|| and
A41: ||.x.|| <= 1;
reconsider Fx = F.x
as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
A42: ||.F.x.|| = upper_bound(PreNorms(Fx)) by LOPBAN_1:30;
now
let s be Real;
assume s in PreNorms(Fx); then
consider y be Point of Y such that
B42: s = ||. Fx.y .|| and
A43: ||.y.|| <= 1;
A44: ||. Fx.y .|| = ||. BL.(x,y) .|| by A1,A11;
A45: ||. BL.(x,y) .|| <= ||.BLp.|| * ||.x.||*||.y.|| by Th32;
||. x .|| * ||. y .|| <= 1 * 1 by A41,A43,XREAL_1:66; then
||.BLp.|| * ( ||. x .|| * ||. y .|| )
<= ||.BLp.|| * 1 by XREAL_1:64;
hence s <= ||.BLp.|| by B42,A44,A45,XXREAL_0:2;
end;
hence r <= ||.BLp.|| by A40,A42,SEQ_4:45;
end; then
A46: ||.f.|| <= ||.BLp.|| by A39,SEQ_4:45;
take BLp;
thus BLp=I.f & ||.f.|| = ||.BLp.|| by A37,A46,FUNCT_1:49,XXREAL_0:1;
end;
then
rng I c= BXYZ by FUNCT_2:114; then
reconsider I as Function of LXYZ,BXYZ by FUNCT_2:6;
A47: for x1,x2 be Element of LXYZ holds I.(x1+x2) = I.x1 + I.x2
proof
let x1,x2 be Element of LXYZ;
for p be Point of X,q be Point of Y
holds (I.(x1+x2)).(p,q) = (I.x1).(p,q) + (I.x2).(p,q)
proof
let p be Point of X,q be Point of Y;
consider Gx1p be Lipschitzian LinearOperator of Y,Z such that
A48: Gx1p = x1.p & (I.x1).(p,q) = Gx1p.q by A8;
consider Gx2p be Lipschitzian LinearOperator of Y,Z such that
A49: Gx2p = x2.p & (I.x2).(p,q) = Gx2p.q by A8;
consider Gx1x2p be Lipschitzian LinearOperator of Y,Z such that
A50: Gx1x2p = (x1+x2).p & (I.(x1+x2)).(p,q) = Gx1x2p.q by A8;
(x1+x2).p = x1.p + x2.p by LOPBAN_1:35;
hence thesis by A48,A49,A50,LOPBAN_1:35;
end;
hence thesis by Th35;
end;
for x be Element of LXYZ, a be Real holds I.(a*x) = a * I.x
proof
let x be Element of LXYZ, a be Real;
for p be Point of X,q be Point of Y
holds (I.(a*x)).(p,q) = a * (I.x).(p,q)
proof
let p be Point of X,q be Point of Y;
consider Gxp be Lipschitzian LinearOperator of Y,Z such that
A52: Gxp = x.p & (I.x).(p,q) = Gxp.q by A8;
consider Gxap be Lipschitzian LinearOperator of Y,Z such that
A53: Gxap = (a*x).p & (I.(a*x)).(p,q) = Gxap.q by A8;
(a*x).p = a * x.p by LOPBAN_1:36;
hence thesis by A52,A53,LOPBAN_1:36;
end;
hence thesis by Th36;
end;
then
reconsider I as LinearOperator of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z)),
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
by A47,LOPBAN_1:def 5,VECTSP_1:def 20;
A55: for u be Point of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z))
holds
||.u.|| = ||. I.u .||
& for x be Point of X,y be Point of Y
holds (I.u).(x,y) = (u.x).y
proof
let u be Point of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z));
consider Iu be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
such that
A56: Iu =I.u & ||.u.|| = ||.Iu.|| by A8;
thus ||.u.|| = ||. I.u .|| by A56;
let p be Point of X,q be Point of Y;
consider G be Lipschitzian LinearOperator of Y,Z such that
A57: G = u.p & (I.u).(p,q) = G.q by A8;
thus (I.u).(p,q) = (u.p).q by A57;
end;
for y being object st y in BXYZ holds
ex x being object st x in LXYZ & y = I . x
proof
let y be object;
assume
A59: y in BXYZ; then
y in Funcs ([:XC,YC:],ZC) by TARSKI:def 3; then
y in rng I0 by A1,FUNCT_2:def 3; then
consider f be object such that
A60: f in Funcs (XC,Funcs (YC,ZC)) & I0 . f = y by FUNCT_2:11;
reconsider f as Function of XC,Funcs (YC,ZC) by A60,FUNCT_2:66;
reconsider BL = y as Lipschitzian BilinearOperator of X,Y,Z
by A59,Def9;
reconsider BLp = BL as Point of
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) by Def9;
A62: dom f = XC by FUNCT_2:def 1;
for x being object st x in XC holds f.x in LYZ
proof
let x be object;
assume
A63: x in XC; then
reconsider fx = f.x as Function of YC,ZC by FUNCT_2:5,66;
reconsider xp = x as Point of X by A63;
A64: for p be Point of Y,q be Point of Y
holds fx.(p+q) = fx.p + fx.q
proof
let p be Point of Y,q be Point of Y;
A65: BL.(xp,p) = fx.p by A60,A1;
A66: BL.(xp,q) = fx.q by A60,A1;
BL.(xp,p+q) = fx.(p+q) by A60,A1;
hence fx.(p+q) = fx.p +fx.q by A65,A66,LOPBAN_8:12;
end;
for p be Point of Y,a be Real holds fx.(a*p) = a * fx.p
proof
let p be Point of Y,a be Real;
A68: BL.(xp,p) = fx.p by A60,A1;
BL.(xp,a*p) = fx.(a*p) by A60,A1;
hence fx.(a*p) = a * fx.p by A68,LOPBAN_8:12;
end; then
reconsider fx as LinearOperator of Y,Z
by A64,LOPBAN_1:def 5,VECTSP_1:def 20;
for p be Point of Y
holds ||.fx.p.|| <= (||.BLp.|| * ||.xp.|| ) * ||.p.||
proof
let p be Point of Y;
BL.(xp,p) = fx.p by A60,A1;
hence thesis by Th32;
end; then
reconsider fx as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 8;
fx in LYZ by LOPBAN_1:def 9;
hence f.x in LYZ;
end; then
reconsider f as Function of XC,LYZ by A62,FUNCT_2:3;
A71: for x1,x2 be Point of X holds f.(x1+x2) = f.x1 + f.x2
proof
let x1,x2 be Point of X;
reconsider fx1x2 = f.(x1+x2)
as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
reconsider fx1 = f.x1 as
Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
reconsider fx2 = f.x2 as
Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
for y be Point of Y holds fx1x2.y = fx1.y + fx2.y
proof
let y be Point of Y;
A72: BL.(x1,y) = fx1.y by A60,A1;
A73: BL.(x2,y) = fx2.y by A60,A1;
BL.(x1+x2,y) = fx1x2.y by A60,A1;
hence fx1x2.y = fx1.y + fx2.y by A72,A73,LOPBAN_8:12;
end;
hence f.(x1+x2) = f.x1 + f.x2 by LOPBAN_1:35;
end;
for x be Point of X,a be Real holds f.(a*x) = a * f.x
proof
let x be Point of X,a be Real;
reconsider fx = f.x as Lipschitzian LinearOperator of Y,Z
by LOPBAN_1:def 9;
reconsider fax = f.(a*x) as Lipschitzian LinearOperator of Y,Z
by LOPBAN_1:def 9;
for y be Point of Y holds fax.y = a * fx.y
proof
let y be Point of Y;
A75: BL.(x,y) = fx.y by A60,A1;
BL.(a*x,y) = fax.y by A60,A1;
hence fax.y = a * fx.y by A75,LOPBAN_8:12;
end;
hence f.(a*x) = a * f.x by LOPBAN_1:36;
end; then
reconsider f as LinearOperator of X,
R_NormSpace_of_BoundedLinearOperators(Y,Z)
by A71,LOPBAN_1:def 5,VECTSP_1:def 20;
for x be Point of X
holds ||.f.x.|| <= ||.BLp.|| * ||.x.||
proof
let x be Point of X;
reconsider fx = f.x as Lipschitzian LinearOperator of Y,Z
by LOPBAN_1:def 9;
A78: for y be Point of Y
holds ||.fx.y.|| <= ||.BLp.|| * ||.x.|| * ||.y.||
proof
let y be Point of Y;
BL.(x,y) = fx.y by A60,A1;
hence ||.fx.y.|| <= ||.BLp.|| * ||.x.|| * ||.y.|| by Th32;
end;
A79: ||.f.x.|| = upper_bound (PreNorms(fx)) by LOPBAN_1:30;
now
let s be Real;
assume s in PreNorms(fx); then
consider y be Point of Y such that
A80: s = ||. fx.y .|| and
A81: ||.y.|| <= 1;
A82: ||.fx.y.|| <= ( ||.BLp.|| * ||.x.|| ) * ||.y.|| by A78;
( ||.BLp.|| * ||.x.|| ) * ||. y .|| <= ( ||.BLp.|| * ||.x.|| ) * 1
by A81,XREAL_1:66;
hence s <= ||.BLp.|| * ||.x.|| by A80,A82,XXREAL_0:2;
end;
hence ||.f.x.|| <= ||.BLp.|| * ||.x.|| by A79,SEQ_4:45;
end; then
reconsider f as Lipschitzian LinearOperator of X,
R_NormSpace_of_BoundedLinearOperators(Y,Z)
by LOPBAN_1:def 8;
A83: f in LXYZ by LOPBAN_1:def 9;
take f;
thus thesis by A60,A83,FUNCT_1:49;
end; then
A85: rng I = BXYZ by FUNCT_2:10;
for u be Point of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z))
holds ||. I.u .|| <= 1 * ||.u.|| by A55;
then
reconsider I as Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z)),
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z) by LOPBAN_1:def 8;
take I;
I is one-to-one onto by A1,A85,FUNCT_1:52,FUNCT_2:def 3;
hence thesis by A55;
end;