:: Isomorphisms from the Space of Multilinear Operators
:: by Kazuhisa Nakasho
::
:: Received May 27, 2019
:: Copyright (c) 2019 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 LOPBAN12, LOPBAN10, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1,
PRE_TOPC, FUNCT_1, SUBSET_1, RELAT_1, LOPBAN_1, ARYTM_3, GROUP_2,
FUNCT_4, VECTMETR, FUNCT_2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, SEQ_4,
MONOID_0, XXREAL_0, FINSEQ_1, RLVECT_1, NDIFF_7, PRVECT_1, PRVECT_2,
CARD_3, PDIFF_1, LOPBAN_8, LOPBAN_9;
notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_7,
BINOP_1, NUMBERS, MONOID_0, XCMPLX_0, XXREAL_0, XREAL_0, CARD_3,
FINSEQ_1, SEQ_4, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1,
MAZURULM, RVSUM_1, LOPBAN_1, PRVECT_1, PRVECT_2, PRVECT_3, NDIFF_5,
NDIFF_7, LOPBAN_8, LOPBAN_9, LOPBAN10;
constructors SEQ_4, RELSET_1, RSSPACE3, NDIFF_5, DOMAIN_1, ABIAN, NDIFF_7,
MONOID_0, LOPBAN_9, LOPBAN10;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, FINSEQ_1,
NUMBERS, XBOOLE_0, RELAT_1, NDIFF_5, LOPBAN_1, PRVECT_2, PRVECT_3,
NDIFF_7, CARD_3, MONOID_0, FUNCT_7, LOPBAN_9, LOPBAN10, FUNCT_2;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
begin :: Plain Isomorphisms from the Space of Multilinear Operators
reserve X,Y,Z,E,F,G,S,T for RealLinearSpace;
registration
let G be RealLinearSpace-Sequence;
cluster product G -> constituted-FinSeqs;
end;
theorem :: LOPBAN12:1
for s being Element of product <*E,F*>,
i being Element of dom <*E,F*>,
x1 being object holds
len(s +* (i,x1)) = 2;
theorem :: LOPBAN12:2
for G be RealLinearSpace-Sequence,
i be Element of dom G,
x be Element of product G holds
for r being Element of (G.i) holds
reproj (i,x) . r = x +* (i,r);
definition
let X, Y be RealLinearSpace;
func IsoCPRLSP(X,Y) -> LinearOperator of [:X,Y:],product <*X,Y*> means
:: LOPBAN12:def 1
for x be Point of X, y be Point of Y holds it.(x,y) = <*x,y*>;
end;
theorem :: LOPBAN12:3
for X, Y be RealLinearSpace holds
0.product <*X,Y*> = IsoCPRLSP(X,Y).(0.[:X,Y:]);
registration
let X, Y be RealLinearSpace;
cluster IsoCPRLSP(X,Y) -> bijective;
end;
registration
let X, Y be RealLinearSpace;
cluster bijective for LinearOperator of [:X,Y:],product <*X,Y*>;
end;
theorem :: LOPBAN12:4
for I be LinearOperator of S, T st I is bijective holds
ex J be LinearOperator of T, S st J = I" & J is bijective;
definition
let X, Y be RealLinearSpace;
let f be bijective LinearOperator of [:X,Y:],product <*X,Y*>;
redefine func f" -> LinearOperator of product <*X,Y*>,[:X,Y:];
end;
registration
let X, Y be RealLinearSpace;
let f be bijective LinearOperator of [:X,Y:],product <*X,Y*>;
cluster f" -> bijective for LinearOperator of product <*X,Y*>,[:X,Y:];
end;
registration
let X, Y be RealLinearSpace;
cluster bijective for LinearOperator of product <*X,Y*>,[:X,Y:];
end;
theorem :: LOPBAN12:5
for X, Y be RealLinearSpace,
x be Point of X, y be Point of Y holds
(IsoCPRLSP(X,Y)").<*x,y*> = [x,y];
theorem :: LOPBAN12:6
for X, Y be RealLinearSpace holds
(IsoCPRLSP(X,Y)").(0. product <*X,Y*>) = 0.[:X,Y:];
theorem :: LOPBAN12:7
for u be MultilinearOperator of <*E,F*>,G
holds u * (IsoCPRLSP (E,F)) is BilinearOperator of E,F,G;
theorem :: LOPBAN12:8
for u be BilinearOperator of E,F,G
holds u * (IsoCPRLSP (E,F))" is MultilinearOperator of <*E,F*>,G;
theorem :: LOPBAN12:9
ex I be LinearOperator of
R_VectorSpace_of_BilinearOperators(X,Y,Z),
R_VectorSpace_of_MultilinearOperators(<*X,Y*>,Z)
st I is bijective
& for u be Point of R_VectorSpace_of_BilinearOperators(X,Y,Z)
holds I.u = u * (IsoCPRLSP(X,Y))";
theorem :: LOPBAN12:10
ex I be LinearOperator of R_VectorSpace_of_LinearOperators
(X,R_VectorSpace_of_LinearOperators(Y,Z)),
R_VectorSpace_of_MultilinearOperators(<*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;
begin :: Extensions to Isometric Isomorphism from the Normed Space of
:: Multilinear Operators
reserve X,Y,Z,E,F,G for RealNormSpace;
reserve S,T for RealNormSpace-Sequence;
theorem :: LOPBAN12:11
for s being Point of product <*E,F*>,
i being Element of dom <*E,F*>,
x1 being object holds
len(s +* (i,x1)) = 2;
theorem :: LOPBAN12:12
for u be Lipschitzian MultilinearOperator of <*E,F*>,G holds
u * (IsoCPNrSP(E,F)) is Lipschitzian BilinearOperator of E,F,G;
theorem :: LOPBAN12:13
for u be Lipschitzian BilinearOperator of E,F,G
holds u * (IsoCPNrSP(E,F))" is Lipschitzian MultilinearOperator of <*E,F*>,G;
theorem :: LOPBAN12:14
ex I be LinearOperator of
R_NormSpace_of_BoundedBilinearOperators(X,Y,Z),
R_NormSpace_of_BoundedMultilinearOperators(<*X,Y*>,Z)
st I is bijective isometric
& for u be Point of R_NormSpace_of_BoundedBilinearOperators(X,Y,Z)
holds I.u = u * (IsoCPNrSP(X,Y))";
theorem :: LOPBAN12:15
ex I be LinearOperator of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedLinearOperators(Y,Z)),
R_NormSpace_of_BoundedMultilinearOperators(<*X,Y*>,Z)
st I is bijective isometric
& 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;
theorem :: LOPBAN12:16
for X,Y being RealNormSpace-Sequence,
Z being RealNormSpace
ex I be LinearOperator of R_NormSpace_of_BoundedLinearOperators
(product X,R_NormSpace_of_BoundedLinearOperators(product Y,Z)),
R_NormSpace_of_BoundedMultilinearOperators(<*product X,product Y*>,Z)
st I is bijective isometric
& for u be Point of R_NormSpace_of_BoundedLinearOperators
(product X,R_NormSpace_of_BoundedLinearOperators(product Y,Z ))
holds ||.u.|| = ||. I.u .||
& for x be Point of product X,y be Point of product Y
holds (I.u).<*x,y*> = (u.x).y;