:: Isomorphism between Spaces of Multilinear Maps and Nested Compositions
:: over Real Normed Vector Spaces
:: by Kazuhisa Nakasho and Yuichi Futa
::
:: Received April 30, 2022
:: Copyright (c) 2022-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 LOPBAN12, LOPBAN10, NUMBERS, REAL_1, NORMSP_1, PRE_TOPC, FUNCT_1,
SUBSET_1, RELAT_1, LOPBAN_1, TARSKI, ARYTM_3, GROUP_2, FUNCT_4, VECTMETR,
FUNCT_2, ARYTM_1, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, SEQ_4, XXREAL_0,
FINSEQ_1, RLVECT_1, NDIFF_7, PRVECT_1, PRVECT_2, CARD_3, PDIFF_1,
MONOID_0, REWRITE1, MSSUBFAM, NAT_1, FUNCOP_1, LOPBAN_8, LOPBAN_9,
ZFMISC_1, ORDINAL4, LOPBAN14;
notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
FUNCT_7, FUNCOP_1, MONOID_0, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, NAT_D, CARD_3, FINSEQ_1, SEQ_4, STRUCT_0, PRE_TOPC,
VECTSP_1, RLVECT_1, NORMSP_0, NORMSP_1, MAZURULM, RVSUM_1, LOPBAN_1,
PRVECT_1, PRVECT_2, NDIFF_5, NDIFF_7, LOPBAN_8, LOPBAN_9, LOPBAN10;
constructors SEQ_4, RELSET_1, RSSPACE3, NDIFF_5, ABIAN, NDIFF_7, MONOID_0,
LOPBAN_9, LOPBAN10, NAT_D;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FINSEQ_1, FUNCT_2,
FUNCOP_1, NUMBERS, XBOOLE_0, NDIFF_5, LOPBAN_1, PRVECT_1, PRVECT_2,
PRVECT_3, NDIFF_7, CARD_3, NORMSP_1, MONOID_0, FUNCT_7, RVSUM_1,
LOPBAN_9, LOPBAN10, LOPBAN12, ORDINAL1, FUNCT_1, INT_1, VALUED_0,
RELAT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities LOPBAN_1, LOPBAN_9, LOPBAN10, FINSEQ_1;
expansions FUNCT_2, VECTSP_1;
theorems TARSKI, RLVECT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, LOPBAN_1,
VECTSP_1, PRVECT_3, NDIFF_5, NDIFF_7, XREAL_0, RVSUM_1, LOPBAN_2,
XBOOLE_1, PRVECT_1, FINSEQ_3, RLAFFIN3, NAT_1, XXREAL_0, CARD_3, SEQ_4,
PRVECT_2, FUNCT_7, LOPBAN_9, LOPBAN10, LOPBAN12, NORMSP_1, INT_1,
NDIFF_6, XREAL_1, NORMSP_0, NAT_4, MONOID_0, ORDINAL1;
schemes FUNCT_1, FUNCT_2, NAT_1;
begin :: Preliminaries
Th1:
for X be RealLinearSpace-Sequence,
i be Element of dom X,
x be Element of product X
holds
for r be Element of X.i holds
reproj(i,x).r = x +* (i,r) by LOPBAN12:2;
definition
let X be RealLinearSpace;
func IsoCPRLSP(X) -> LinearOperator of X,product <*X*> means
:Def1:
for x be Point of X holds it.x = <*x*>;
existence
proof
consider I be Function of X, product <*X*> such that
I is one-to-one onto and
A1: for x be Point of X holds I.x = <*x*> and
A2: for v,w be Point of X holds I.(v+w) = I.v + I.w and
A3: for v be Point of X, r be Element of REAL
holds
I.(r*v) = r*(I.v) and
0. product <*X*> = I.(0.X) by PRVECT_3:11;
now
let v be Point of X, r be Real;
reconsider r0=r as Element of REAL by XREAL_0:def 1;
thus I.(r*v)
= r0 * I.v by A3
.= r * I.v;
end; then
reconsider I as LinearOperator of X, product <*X*>
by A2,LOPBAN_1:def 5,VECTSP_1:def 20;
take I;
thus thesis by A1;
end;
uniqueness
proof
let I1, I2 be LinearOperator of X,product <*X*>;
assume that
A4: for x be Point of X holds I1.x = <*x*> and
A5: for x be Point of X holds I2.x = <*x*>;
for x be set st x in the carrier of X
holds I1.x = I2.x
proof
let x be set;
assume x in the carrier of X;
then reconsider x1 = x as Point of X;
thus I1.x
= <*x1*> by A4
.= I2.x by A5;
end;
hence I1 = I2;
end;
end;
theorem Th2:
for X be RealLinearSpace
holds 0.(product <*X*>) = (IsoCPRLSP(X)).(0.X)
proof
let X be RealLinearSpace;
consider I be Function of X, product <*X*> such that
I is one-to-one onto and
A1: for x be Point of X holds I.x = <*x*> and
A2: for v,w be Point of X holds I.(v+w) = I.v + I.w and
A3: for v be Point of X, r be Element of REAL
holds I.(r*v) = r*(I.v) and
A4: 0.(product <*X*>) = I.(0.X) by PRVECT_3:11;
now
let v be Point of X, r be Real;
reconsider r0 = r as Element of REAL by XREAL_0:def 1;
thus I.(r*v)
= r0 * I.v by A3
.= r * I.v;
end; then
reconsider I as LinearOperator of X, product <*X*>
by A2,LOPBAN_1:def 5,VECTSP_1:def 20;
for a be Element of X holds I.a = (IsoCPRLSP(X)).a by A1,Def1;
hence thesis by A4;
end;
registration
let X be RealLinearSpace;
cluster IsoCPRLSP(X) -> one-to-one onto;
correctness
proof
consider I be Function of X, product <*X*> such that
A1: I is one-to-one onto and
A2: for x be Point of X holds I.x = <*x*> and
A3: for v,w be Point of X holds I.(v+w) = I.v + I.w and
A4: for v be Point of X, r be Element of REAL
holds I.(r*v) = r*(I.v) and
0.(product <*X*>) = I.(0.X) by PRVECT_3:11;
now
let v be Point of X, r be Real;
reconsider r0=r as Element of REAL by XREAL_0:def 1;
thus I.(r*v)
= r0 * I.v by A4
.= r * I.v;
end; then
reconsider I as LinearOperator of X, product <*X*>
by A3,LOPBAN_1:def 5,VECTSP_1:def 20;
I = IsoCPRLSP(X) by A2,Def1;
hence thesis by A1;
end;
end;
registration
let X be RealLinearSpace;
cluster one-to-one onto for
LinearOperator of X,product <*X*>;
correctness
proof
take IsoCPRLSP(X);
thus thesis;
end;
end;
definition
let X be RealLinearSpace;
let f be bijective LinearOperator of X, product <*X*>;
redefine func f" -> LinearOperator of product <*X*>, X; :: redefines " (FUNCT_1, definition)
correctness
proof
consider J be LinearOperator of product <*X*>, X such that
A1: J = f" and
J is bijective by LOPBAN12:4;
thus f" is LinearOperator of product <*X*>, X by A1;
end;
end;
registration
let X be RealLinearSpace;
let f be one-to-one onto
LinearOperator of X, product <*X*>;
cluster f" -> bijective
for LinearOperator of product <*X*>, X;
correctness
proof
consider J be LinearOperator of product <*X*>, X such that
A1: J = f" and
A2: J is bijective by LOPBAN12:4;
thus thesis by A1,A2;
end;
end;
registration
let X be RealLinearSpace;
cluster one-to-one onto
for LinearOperator of product <*X*>, X;
correctness
proof
set f = (IsoCPRLSP X)";
take f;
thus thesis;
end;
end;
theorem
for X be RealLinearSpace,
x be Point of X
holds (IsoCPRLSP X)" . <*x*> = x
proof
let X be RealLinearSpace;
set I = IsoCPRLSP(X);
set J = I";
A1: dom I = the carrier of X by FUNCT_2:def 1;
for x be Point of X holds J.<*x*> = x
proof
let x be Point of X;
A2: I.x = <*x*> by Def1;
reconsider z = x as Point of X;
thus thesis by A1,A2,FUNCT_1:34;
end;
hence thesis;
end;
theorem
for X be RealLinearSpace holds
(IsoCPRLSP X)".(0.(product <*X*>)) = 0.X
proof
let X be RealLinearSpace;
set I = IsoCPRLSP(X);
set J = I";
A1: dom I = the carrier of X by FUNCT_2:def 1;
J.(0.(product <*X*>)) = J.(I.(0.X)) by Th2;
hence thesis by A1,FUNCT_1:34;
end;
theorem
for G be RealLinearSpace holds
( for x be set holds
( x is Point of product <*G*>
iff ex x1 be Point of G st x = <*x1*> ) )
& ( for x,y be Point of product <*G*>,
x1,y1 be Point of G
st x = <*x1*> & y = <*y1*>
holds x+y = <*x1+y1*> )
& 0.(product <*G*>) = <* 0.G *>
& ( for x be Point of product <*G*>, x1 be Point of G
st x = <*x1*>
holds -x = <* -x1 *> )
& ( for x be Point of product <*G*>, x1 be Point of G,
a be Real
st x = <*x1*>
holds a*x = <* a*x1 *> )
proof
let G be RealLinearSpace;
consider I be Function of G, product <*G*> such that
A1: I is one-to-one onto
& for x be Point of G holds I.x = <*x*>
& for v,w be Point of G holds I.(v+w) = I.v + I.w
& for v be Point of G, r be Element of REAL
holds I.(r*v) = r * (I.v)
& 0.(product <*G*>) = I.(0.G) by PRVECT_3:11;
thus
A2: for x be set holds
( x is Point of product <*G*>
iff ex x1 be Point of G st x = <*x1*> )
proof
let y be set;
hereby
assume y is Point of product <*G*>; then
consider x be Element of the carrier of G such that
A3: y = I.x by A1,FUNCT_2:113;
take x;
thus y = <*x*> by A1,A3;
end;
now
assume ex x1 be Point of G st y = <*x1*>; then
consider x1 be Point of G such that
A4: y = <*x1*>;
I.x1 = <*x1*> by A1;
hence y is Point of product <*G*> by A4;
end;
hence thesis;
end;
thus
A5: for x,y be Point of product <*G*>,
x1,y1 be Point of G
st x = <*x1*> & y = <*y1*>
holds x+y = <*x1+y1*>
proof
let x,y be Point of product <*G*>;
let x1,y1 be Point of G;
assume
A6: x = <*x1*> & y = <*y1*>;
I.(x1+y1) = <* x1+y1 *>
& I.(x1) = <*x1*> & I.(y1) = <*y1*> by A1;
hence <* x1+y1 *> = x+y by A1,A6;
end;
thus
0. product <*G*> = <* 0.G *> by A1;
thus
for x be Point of product <*G*>, x1 be Point of G
st x = <*x1*>
holds -x = <* -x1 *>
proof
let x be Point of product <*G*>;
let x1 be Point of G;
assume
A7: x = <* x1 *>;
reconsider y = <* -x1 *> as Point of product <*G*> by A2;
x+y
= <* x1+-x1 *> by A5,A7
.= <* 0.G *> by RLVECT_1:def 10
.= 0.(product <*G*>) by A1;
hence thesis by RLVECT_1:def 10;
end;
thus
for x be Point of product <*G*>,
x1 be Point of G, a be Real
st x = <*x1*>
holds a*x = <* a*x1 *>
proof
let x be Point of product <*G*>;
let x1 be Point of G, a be Real;
assume
A8: x = <*x1*>;
reconsider a0 = a as Element of REAL by XREAL_0:def 1;
A9: <*x1*> = I.x1 by A1;
I.(a0*x1) = <* a0*x1 *> by A1;
hence thesis by A1,A8,A9;
end;
end;
theorem Th6:
for X,Y be RealLinearSpace,
f be Function of X,Y
holds
f is LinearOperator of X,Y
iff f * (IsoCPRLSP X)" is LinearOperator of product <*X*>,Y
proof
let X,Y be RealLinearSpace,
f be Function of X,Y;
thus
f is LinearOperator of X,Y implies
f * (IsoCPRLSP X)" is LinearOperator of product <*X*>,Y
by LOPBAN_2:1;
assume f * (IsoCPRLSP X)" is LinearOperator of product <*X*>,Y; then
reconsider g = f * (IsoCPRLSP X)" as LinearOperator of product <*X*>,Y;
rng (IsoCPRLSP X) = the carrier of product <*X*> by FUNCT_2:def 3; then
A1: (IsoCPRLSP X)" * (IsoCPRLSP X) = id the carrier of X by FUNCT_2:29;
g * (IsoCPRLSP X)
= f * ((IsoCPRLSP X)" * (IsoCPRLSP X)) by RELAT_1:36
.= f by A1,FUNCT_2:17;
hence thesis by LOPBAN_2:1;
end;
theorem Th7:
for X,Y be RealLinearSpace,
f be Function of product <*X*>,Y
holds
f is LinearOperator of product <*X*>,Y
iff f * (IsoCPRLSP X) is LinearOperator of X,Y
proof
let X,Y be RealLinearSpace,
f be Function of product <*X*>,Y;
set g = f * (IsoCPRLSP X);
rng(IsoCPRLSP X) = the carrier of product <*X*> by FUNCT_2:def 3; then
A1: (IsoCPRLSP X) * (IsoCPRLSP X)"
= id the carrier of product <*X*> by FUNCT_2:29;
g * (IsoCPRLSP X) "
= f * ((IsoCPRLSP X) * (IsoCPRLSP X)") by RELAT_1:36
.= f by A1,FUNCT_2:17;
hence thesis by Th6;
end;
theorem Th8:
for X be RealLinearSpace,
s be Point of product <*X*>,
i be Element of dom <*X*>
holds reproj(i,s) = IsoCPRLSP(X)
proof
let X be RealLinearSpace,
s be Point of product <*X*>,
i be Element of dom <*X*>;
A1: i = 1 by FINSEQ_1:90;
A2: <*X*>.i = X by A1;
for x be Element of X
holds (reproj(i,s)).x = (IsoCPRLSP X).x
proof
let x be Element of X;
s in the carrier of product <*X*>; then
s in rng(IsoCPRLSP X) by FUNCT_2:def 3; then
consider y be object such that
A3: y in the carrier of X
& s = (IsoCPRLSP X).y by FUNCT_2:11;
reconsider y as Point of X by A3;
A4: (IsoCPRLSP X).y = <*y*> by Def1;
dom s = Seg 1 by A3,A4,FINSEQ_1:38; then
A5: i in dom s by A1;
dom(s +* (i,x))
= dom s by FUNCT_7:30
.= Seg 1 by A3,A4,FINSEQ_1:38; then
A6: len(s +* (i,x)) = 1 by FINSEQ_1:def 3;
A7: (s +* (i,x)).1 = x by A1,A5,FUNCT_7:31;
thus (reproj(i,s)).x
= s +* (i,x) by A2,Th1
.= <*x*> by A6,A7,FINSEQ_1:40
.= (IsoCPRLSP X).x by Def1;
end;
hence reproj(i,s) = IsoCPRLSP(X) by A2;
end;
theorem Th9:
for X,Y be RealLinearSpace,
f be object
holds
f is LinearOperator of product <*X*>,Y
iff f is MultilinearOperator of <*X*>,Y
proof
let X,Y be RealLinearSpace,
f be object;
A1: dom <*X*> = {1} by FINSEQ_1:2,38;
hereby
assume f is LinearOperator of product <*X*>,Y; then
reconsider f0 = f as LinearOperator of product <*X*>,Y;
for i be Element of dom <*X*>,
s be Element of product <*X*>
holds f0 * reproj(i,s) is LinearOperator of <*X*>.i,Y
proof
let i be Element of dom <*X*>,
s be Element of product <*X*>;
A2: i = 1 by A1,TARSKI:def 1; then
A3: <*X*>.i = X;
for x be Element of X
holds (reproj(i,s)).x = (IsoCPRLSP X).x
proof
let x be Element of X;
s in the carrier of product <*X*>; then
s in rng(IsoCPRLSP X) by FUNCT_2:def 3; then
consider x0 be object such that
A4: x0 in the carrier of X
& s = (IsoCPRLSP X).x0 by FUNCT_2:11;
reconsider x0 as Point of X by A4;
A5: (IsoCPRLSP X).x0 = <*x0*> by Def1;
A6: dom s = Seg 1 by A4,A5,FINSEQ_1:38;
dom(s +* (i,x))
= dom s by FUNCT_7:30
.= Seg 1 by A4,A5,FINSEQ_1:38; then
A7: len(s +* (i,x)) = 1 by FINSEQ_1:def 3;
A8: (s +* (i,x)).1 = x by A1,A2,A6,FINSEQ_1:2,FUNCT_7:31;
thus
(reproj(i,s)).x
= s +* (i,x) by A3,Th1
.= <*x*> by A7,A8,FINSEQ_1:40
.= (IsoCPRLSP X).x by Def1;
end; then
reproj(i,s) = IsoCPRLSP(X) by A3;
hence f0 * reproj(i,s) is LinearOperator of <*X*>.i,Y by A3,Th7;
end;
hence f is MultilinearOperator of <*X*>,Y by LOPBAN10:def 3;
end;
assume f is MultilinearOperator of <*X*>,Y; then
reconsider f1 = f as MultilinearOperator of <*X*>,Y;
reconsider i = 1 as Element of dom <*X*> by A1,TARSKI:def 1;
set s = the Element of product <*X*>;
A9: reproj(i,s) = IsoCPRLSP(X) by Th8;
f1 * reproj(i,s) is LinearOperator of <*X*>.i,Y by LOPBAN10:def 3;
hence f is LinearOperator of product <*X*>,Y by A9,Th7;
end;
theorem Th10:
for X,Y be RealLinearSpace holds
MultilinearOperators(<*X*>,Y) = LinearOperators(product <*X*>,Y)
proof
let X,Y be RealLinearSpace;
for f be object holds
f in MultilinearOperators(<*X*>,Y)
iff f in LinearOperators(product <*X*>,Y)
proof
let f be object;
f is LinearOperator of product <*X*>,Y
iff f is MultilinearOperator of <*X*>,Y by Th9;
hence thesis by LOPBAN_1:def 6,LOPBAN10:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem
for X,Y be RealLinearSpace holds
R_VectorSpace_of_MultilinearOperators(<*X*>,Y)
= R_VectorSpace_of_LinearOperators(product <*X*>,Y)
proof
let X,Y be RealLinearSpace;
MultilinearOperators(<*X*>,Y) = LinearOperators(product <*X*>,Y) by Th10;
hence thesis;
end;
theorem Th12:
for G be RealNormSpace holds
( for x be set holds
( x is Point of product <*G*>
iff ex x1 be Point of G st x = <*x1*> ) )
& ( for x,y be Point of product <*G*>, x1,y1 be Point of G
st x = <*x1*> & y = <*y1*>
holds x+y = <* x1+y1 *> )
& 0.(product <*G*>) = <* 0.G *>
& ( for x be Point of product <*G*>, x1 be Point of G
st x = <*x1*>
holds -x = <* -x1 *> )
& ( for x be Point of product <*G*>,
x1 be Point of G, a be Real
st x = <*x1*>
holds a*x = <* a*x1 *> )
& ( for x be Point of product <*G*>, x1 be Point of G
st x = <*x1*> holds ||.x.|| = ||.x1.|| )
proof
let G be RealNormSpace;
consider I be Function of G,(product <*G*>) such that
A1: I is one-to-one & I is onto
& ( for x be Point of G holds I.x = <*x*> )
& ( for v, w be Point of G holds I.(v + w) = I.v + I.w )
& ( for v be Point of G for r be Element of REAL
holds I.(r * v) = r * (I.v) )
& 0.(product <*G*>) = I.(0.G)
& ( for v be Point of G holds ||. I.v.|| = ||.v.|| )
by PRVECT_3:16;
thus
A2: for x be set holds
( x is Point of product <*G*>
iff ex x1 be Point of G st x = <*x1*> )
proof
let y be set;
hereby
assume y is Point of product <*G*>; then
consider x be Element of the carrier of G such that
A3: y = I.x by A1,FUNCT_2:113;
take x;
thus y = <*x*> by A1,A3;
end;
hereby
assume ex x1 be Point of G st y = <*x1*>; then
consider x1 be Point of G such that
A4: y = <*x1*>;
I.x1 = <*x1*> by A1;
hence y is Point of product <*G*> by A4;
end;
end;
thus
A5: for x,y be Point of product <*G*>,
x1,y1 be Point of G
st x = <*x1*> & y = <*y1*> holds x+y = <* x1+y1 *>
proof
let x,y be Point of product <*G*>;
let x1,y1 be Point of G;
assume
A6: x = <*x1*> & y = <*y1*>;
A7: I.(x1+y1) = <* x1+y1 *> by A1;
I.x1 = <*x1*> & I.y1 = <*y1*> by A1;
hence <* x1+y1 *> = x+y by A1,A6,A7;
end;
thus
0. product <*G*> = <* 0.G *> by A1;
thus
for x be Point of product <*G*>,
x1 be Point of G
st x = <*x1*> holds -x = <* -x1 *>
proof
let x be Point of product <*G*>;
let x1 be Point of G;
assume
A8: x = <*x1*>;
reconsider y = <* -x1 *> as Point of product <*G*> by A2;
x+y
= <* x1+-x1 *> by A5,A8
.= <* 0.G *> by RLVECT_1:def 10
.= 0.(product <*G*>) by A1;
hence thesis by RLVECT_1:def 10;
end;
thus
for x be Point of product <*G*>,
x1 be Point of G, a be Real
st x = <*x1*> holds a*x = <* a*x1 *>
proof
let x be Point of product <*G*>;
let x1 be Point of G, a be Real;
assume
A9: x = <*x1*>;
reconsider a0 = a as Element of REAL by XREAL_0:def 1;
A10: <*x1*> = I.x1 by A1;
I.(a0*x1) = <* a0*x1 *> by A1;
hence thesis by A1,A9,A10;
end;
thus
for x be Point of product <*G*>,
x1 be Point of G
st x = <*x1*>
holds ||.x.|| = ||.x1.||
proof
let x be Point of product <*G*>;
let x1 be Point of G;
assume
A11: x = <*x1*>;
||.I.x1.|| = ||.x.|| by A1,A11;
hence ||.x.|| = ||.x1.|| by A1;
end;
end;
definition
let X be RealNormSpace;
func IsoCPNrSP(X) -> LinearOperator of X,product <*X*> means
:Def2:
for x be Point of X holds it.x = <*x*>;
existence
proof
consider I be Function of X, product <*X*> such that
I is one-to-one onto and
A1: for x be Point of X holds I.x = <*x*> and
A2: for v,w be Point of X holds I.(v+w) = I.v + I.w and
A3: for v be Point of X, r be Element of REAL
holds I.(r*v) = r*(I.v) and
0.(product <*X*>) = I.(0.X) and
for v be Point of X holds ||.I.v.|| = ||.v.|| by PRVECT_3:16;
now
let v be Point of X, r be Real;
reconsider r0 = r as Element of REAL by XREAL_0:def 1;
thus
I.(r*v)
= r0 * I.v by A3
.= r * I.v;
end; then
reconsider I as LinearOperator of X, product <*X*>
by A2,LOPBAN_1:def 5,VECTSP_1:def 20;
take I;
thus thesis by A1;
end;
uniqueness
proof
let I1, I2 be LinearOperator of X,product <*X*>;
assume that
A4: for x be Point of X holds I1.x = <*x*> and
A5: for x be Point of X holds I2.x = <*x*>;
for x be set st x in the carrier of X
holds I1.x = I2.x
proof
let x be set;
assume x in the carrier of X; then
reconsider x1 = x as Point of X;
thus
I1.x
= <*x1*> by A4
.= I2.x by A5;
end;
hence I1 = I2;
end;
end;
theorem
for X be RealNormSpace holds
0.(product <*X*>) = (IsoCPNrSP X).(0.X)
proof
let X be RealNormSpace;
consider I be Function of X, product <*X*> such that
I is one-to-one onto and
A1: for x be Point of X holds I.x = <*x*> and
A2: for v,w be Point of X holds I.(v+w) = I.v + I.w and
A3: for v be Point of X, r be Element of REAL
holds I.(r*v) = r*(I.v) and
A4: 0. product <*X*> = I.(0.X) and
for v be Point of X holds ||.I.v.|| = ||.v.|| by PRVECT_3:16;
now
let v be Point of X, r be Real;
reconsider r0 = r as Element of REAL by XREAL_0:def 1;
thus
I.(r*v)
= r0 * I.v by A3
.= r * I.v;
end; then
reconsider I as LinearOperator of X, product <*X*>
by A2,LOPBAN_1:def 5,VECTSP_1:def 20;
for a be Element of X holds I.a = (IsoCPNrSP X).a by A1,Def2;
hence thesis by A4;
end;
registration
let X be RealNormSpace;
cluster IsoCPNrSP(X) -> one-to-one onto isometric;
correctness
proof
consider I be Function of X, product <*X*> such that
A1: I is one-to-one onto and
A2: for x be Point of X holds I.x = <*x*> and
A3: for v,w be Point of X holds I.(v+w) = I.v + I.w and
A4: for v be Point of X, r be Element of REAL
holds I.(r*v) = r*(I.v) and
0. product <*X*> = I.(0.X) and
A5: for v be Point of X holds ||.I.v.|| = ||.v.|| by PRVECT_3:16;
now
let v be Point of X, r be Real;
reconsider r0 = r as Element of REAL by XREAL_0:def 1;
thus
I.(r*v)
= r0 * I.v by A4
.= r * I.v;
end; then
reconsider I as LinearOperator of X, product <*X*>
by A3,LOPBAN_1:def 5,VECTSP_1:def 20;
I = IsoCPNrSP(X) by A2,Def2;
hence thesis by A1,A5,NDIFF_7:7;
end;
end;
registration
let X be RealNormSpace;
cluster one-to-one onto isometric
for LinearOperator of X,product <*X*>;
correctness
proof
take IsoCPNrSP(X);
thus thesis;
end;
end;
definition
let X be RealNormSpace;
let I be one-to-one onto isometric
LinearOperator of X,product <*X*>;
redefine func I" -> LinearOperator of product <*X*>,X; :: redefines " (FUNCT_1, definition)
correctness
proof
consider J be LinearOperator of product <*X*>,X such that
A1: J = I" and
J is one-to-one onto isometric by NDIFF_7:9;
thus thesis by A1;
end;
end;
registration
let X be RealNormSpace;
let I be one-to-one onto isometric
LinearOperator of X,product <*X*>;
cluster I" -> one-to-one onto isometric
for LinearOperator of product <*X*>,X;
correctness
proof
consider J be LinearOperator of product <*X*>,X such that
A1: J = I" and
A2: J is one-to-one onto and
A3: J is isometric by NDIFF_7:9;
thus thesis by A1,A2,A3;
end;
end;
registration
let X be RealNormSpace;
cluster one-to-one onto isometric
for LinearOperator of product <*X*>,X;
correctness
proof
set J = (IsoCPNrSP X)";
take J;
thus thesis;
end;
end;
theorem Th14:
for X,Y be RealNormSpace,
f be Function of X,Y
holds
f is LinearOperator of X,Y
iff f * (IsoCPNrSP X)" is LinearOperator of product <*X*>,Y
proof
let X,Y be RealNormSpace,
f be Function of X,Y;
thus
f is LinearOperator of X,Y implies
f * (IsoCPNrSP X)" is LinearOperator of product <*X*>,Y
by LOPBAN_2:1;
assume f * (IsoCPNrSP X)" is LinearOperator of product <*X*>,Y; then
reconsider g = f * (IsoCPNrSP X)" as LinearOperator of product <*X*>,Y;
rng(IsoCPNrSP X) = the carrier of product <*X*> by FUNCT_2:def 3; then
A1: (IsoCPNrSP X)" * (IsoCPNrSP X) = id the carrier of X by FUNCT_2:29;
g * (IsoCPNrSP X)
= f * ((IsoCPNrSP X)" * (IsoCPNrSP X)) by RELAT_1:36
.= f by A1,FUNCT_2:17;
hence thesis by LOPBAN_2:1;
end;
theorem Th15:
for X,Y be RealNormSpace,
f be Function of X,Y
holds
f is Lipschitzian LinearOperator of X,Y
iff f * (IsoCPNrSP X)" is Lipschitzian LinearOperator of product <*X*>,Y
proof
let X,Y be RealNormSpace,
f be Function of X,Y;
thus
f is Lipschitzian LinearOperator of X,Y implies
f * (IsoCPNrSP X)" is Lipschitzian LinearOperator of product <*X*>,Y
by LOPBAN_2:2;
assume f * (IsoCPNrSP X)" is Lipschitzian LinearOperator of
product <*X*>,Y;
then
reconsider g = f * (IsoCPNrSP X)"
as Lipschitzian LinearOperator of product <*X*>,Y;
rng(IsoCPNrSP X) = the carrier of product <*X*> by FUNCT_2:def 3; then
A1: (IsoCPNrSP X)" * (IsoCPNrSP X) = id the carrier of X by FUNCT_2:29;
g * (IsoCPNrSP X)
= f * ((IsoCPNrSP X)" * (IsoCPNrSP X)) by RELAT_1:36
.= f by A1,FUNCT_2:17;
hence thesis by LOPBAN_2:2;
end;
theorem Th16:
for X,Y be RealNormSpace,
f be Function of product <*X*>,Y
holds
f is LinearOperator of product <*X*>,Y
iff f * (IsoCPNrSP X) is LinearOperator of X,Y
proof
let X,Y be RealNormSpace,
f be Function of product <*X*>,Y;
set g = f * (IsoCPNrSP X);
rng(IsoCPNrSP X) = the carrier of product <*X*> by FUNCT_2:def 3; then
A1: (IsoCPNrSP X) * (IsoCPNrSP X)" = id the carrier of product <*X*>
by FUNCT_2:29;
g * (IsoCPNrSP X)"
= f* ((IsoCPNrSP X) * (IsoCPNrSP X)") by RELAT_1:36
.= f by A1,FUNCT_2:17;
hence thesis by Th14;
end;
theorem Th17:
for X,Y be RealNormSpace,
f be Function of product <*X*>,Y
holds
f is Lipschitzian LinearOperator of product <*X*>,Y
iff f * (IsoCPNrSP X) is Lipschitzian LinearOperator of X,Y
proof
let X,Y be RealNormSpace,
f be Function of product <*X*>,Y;
set g = f * (IsoCPNrSP X);
rng(IsoCPNrSP X) = the carrier of product <*X*> by FUNCT_2:def 3; then
A1: (IsoCPNrSP X) * (IsoCPNrSP X)" = id the carrier of product <*X*>
by FUNCT_2:29;
g * (IsoCPNrSP X)"
= f * ((IsoCPNrSP X) * (IsoCPNrSP X)") by RELAT_1:36
.= f by A1,FUNCT_2:17;
hence thesis by Th15;
end;
theorem Th18:
for X be RealNormSpace,
s be Point of product <*X*>,
i be Element of dom <*X*>
holds reproj(i,s) = IsoCPNrSP(X)
proof
let X be RealNormSpace,
s be Point of product <*X*>,
i be Element of dom <*X*>;
A1: i = 1 by FINSEQ_1:90;
A2: <*X*>.i = X by A1;
for x be Element of X
holds (reproj(i,s)).x = (IsoCPNrSP X).x
proof
let x be Element of X;
s in the carrier of product <*X*>; then
s in rng(IsoCPNrSP X) by FUNCT_2:def 3; then
consider x0 be object such that
A3: x0 in the carrier of X
& s = (IsoCPNrSP X).x0 by FUNCT_2:11;
reconsider x0 as Point of X by A3;
A4: (IsoCPNrSP X).x0 = <*x0*> by Def2;
dom s = Seg 1 by A3,A4,FINSEQ_1:38; then
A5: i in dom s by A1;
dom(s +* (i,x))
= dom s by FUNCT_7:30
.= Seg 1 by A3,A4,FINSEQ_1:38; then
A6: len(s +* (i,x)) = 1 by FINSEQ_1:def 3;
A7: (s +* (i,x)).1 = x by A1,A5,FUNCT_7:31;
thus
(reproj(i,s)).x
= s +* (i,x) by A2,NDIFF_5:def 4
.= <*x*> by A6,A7,FINSEQ_1:40
.= (IsoCPNrSP X).x by Def2;
end;
hence reproj(i,s) = IsoCPNrSP(X) by A2;
end;
theorem Th19:
for X be RealNormSpace,
x be Point of product <*X*>
holds NrProduct x = ||.x.||
proof
let X be RealNormSpace,
x be Point of product <*X*>;
A1: dom <*X*> = {1} by FINSEQ_1:2,38;
consider x1 be Point of X such that
A3: x = <*x1*> by Th12;
rng <*||.x1.||*> c= REAL; then
reconsider Nx = <*||.x1.||*> as FinSequence of REAL by FINSEQ_1:def 4;
A4: dom Nx = {1} by FINSEQ_1:2,38;
A5: now
let i be Element of dom <*X*>;
A6: i = 1 by A1,TARSKI:def 1;
hence
Nx.i = ||.x1.||
.= ||.x.i.|| by A3,A6;
end;
Product Nx = ||.x1.||;
hence thesis by A1,A3,A4,A5,Th12,LOPBAN10:def 9;
end;
theorem Th20:
for X,Y be RealNormSpace,
f be object
holds
f is LinearOperator of product <*X*>,Y
iff f is MultilinearOperator of <*X*>,Y
proof
let X,Y be RealNormSpace,
f be object;
A1: dom <*X*> = {1} by FINSEQ_1:2,38;
hereby
assume f is LinearOperator of product <*X*>,Y; then
reconsider f0 = f as LinearOperator of product <*X*>,Y;
for i be Element of dom <*X*>,
s be Element of product <*X*>
holds f0 * reproj(i,s) is LinearOperator of <*X*>.i,Y
proof
let i be Element of dom <*X*>,
s be Element of product <*X*>;
A2: i = 1 by A1,TARSKI:def 1; then
A3: <*X*>.i = X;
for x be Element of X holds (reproj(i,s)).x = (IsoCPNrSP X).x
proof
let x be Element of X;
s in the carrier of product <*X*>; then
s in rng(IsoCPNrSP X) by FUNCT_2:def 3; then
consider x0 be object such that
A4: x0 in the carrier of X
& s = (IsoCPNrSP X).x0 by FUNCT_2:11;
reconsider x0 as Point of X by A4;
A5: (IsoCPNrSP X).x0 = <*x0*> by Def2;
A6: dom s = Seg 1 by A4,A5,FINSEQ_1:38;
dom(s +* (i,x))
= dom s by FUNCT_7:30
.= Seg 1 by A4,A5,FINSEQ_1:38; then
A7: len(s +* (i,x)) = 1 by FINSEQ_1:def 3;
A8: (s +* (i,x)).1 = x by A1,A2,A6,FINSEQ_1:2,FUNCT_7:31;
thus
(reproj(i,s)).x
= s +* (i,x) by A3,NDIFF_5:def 4
.= <*x*> by A7,A8,FINSEQ_1:40
.= (IsoCPNrSP X).x by Def2;
end; then
reproj(i,s) = IsoCPNrSP(X) by A3;
hence f0 * reproj(i,s) is LinearOperator of <*X*>.i,Y by A3,Th16;
end;
hence f is MultilinearOperator of <*X*>,Y by LOPBAN10:def 6;
end;
assume f is MultilinearOperator of <*X*>,Y; then
reconsider f0 = f as MultilinearOperator of <*X*>,Y;
reconsider i = 1 as Element of dom <*X*> by A1,TARSKI:def 1;
set s = the Element of product <*X*>;
A9: reproj(i,s) = IsoCPNrSP(X) by Th18;
f0 * reproj(i,s) is LinearOperator of X,Y by LOPBAN10:def 6;
hence f is LinearOperator of product <*X*>,Y by A9,Th16;
end;
theorem Th21:
for X,Y be RealNormSpace, f be object
holds
f is Lipschitzian LinearOperator of product <*X*>,Y
iff f is Lipschitzian MultilinearOperator of <*X*>,Y
proof
let X,Y be RealNormSpace,
f be object;
A1: dom <*X*> = {1} by FINSEQ_1:2,38;
hereby
assume f is Lipschitzian LinearOperator of product <*X*>,Y; then
reconsider f0 = f as Lipschitzian LinearOperator of product <*X*>,Y;
for i be Element of dom <*X*>,
s be Element of product <*X*>
holds f0 * reproj(i,s) is LinearOperator of <*X*>.i,Y
proof
let i be Element of dom <*X*>,
s be Element of product <*X*>;
A2: i = 1 by A1,TARSKI:def 1; then
A3: <*X*>.i = X;
for z be Element of X
holds (reproj(i,s)).z = (IsoCPNrSP X).z
proof
let z be Element of X;
s in the carrier of product <*X*>; then
s in rng(IsoCPNrSP X) by FUNCT_2:def 3; then
consider y be object such that
A4: y in the carrier of X
& s = (IsoCPNrSP X).y by FUNCT_2:11;
reconsider y as Point of X by A4;
A5: (IsoCPNrSP X).y = <*y*> by Def2;
A6: dom s= Seg 1 by A4,A5,FINSEQ_1:38;
dom(s +* (i,z))
= dom s by FUNCT_7:30
.= Seg 1 by A4,A5,FINSEQ_1:38; then
A7: len(s +* (i,z)) = 1 by FINSEQ_1:def 3;
A8: (s +* (i,z)).1 = z by A1,A2,A6,FINSEQ_1:2,FUNCT_7:31;
thus
(reproj(i,s)).z
= s +* (i,z) by A3,NDIFF_5:def 4
.= <*z*> by A7,A8,FINSEQ_1:40
.= (IsoCPNrSP X).z by Def2;
end; then
reproj(i,s) = IsoCPNrSP(X) by A3;
hence f0 * reproj(i,s) is LinearOperator of <*X*>.i,Y by A3,Th17;
end; then
reconsider f1 = f0 as MultilinearOperator of <*X*>,Y by LOPBAN10:def 6;
consider M be Real such that
A9: 0 <= M
& for x be VECTOR of product <*X*>
holds ||.f0.x.|| <= M * ||.x.||
by LOPBAN_1:def 8;
now
let x be VECTOR of product <*X*>;
NrProduct x = ||.x.|| by Th19;
hence ||.f1.x.|| <= M * (NrProduct x) by A9;
end;
hence f is Lipschitzian MultilinearOperator of <*X*>,Y
by A9,LOPBAN10:def 10;
end;
assume f is Lipschitzian MultilinearOperator of <*X*>,Y; then
reconsider f0 = f as Lipschitzian MultilinearOperator of <*X*>,Y;
reconsider i = 1 as Element of dom <*X*> by A1,TARSKI:def 1;
set s = the Element of product <*X*>;
A10: reproj(i,s) = IsoCPNrSP(X) by Th18;
reconsider g = f0 * IsoCPNrSP(X) as LinearOperator of X,Y
by A10,LOPBAN10:def 6;
consider M be Real such that
A11: 0 <= M
& for x be Point of product <*X*>
holds ||.f0.x.|| <= M * (NrProduct x)
by LOPBAN10:def 10;
now
let x be VECTOR of X;
reconsider s = <*x*> as Point of product <*X*> by Th12;
A12: g.x
= f0.((IsoCPNrSP X).x) by FUNCT_2:15
.= f0.s by Def2;
NrProduct s
= ||.s.|| by Th19
.= ||.x.|| by Th12;
hence ||.g.x.|| <= M * ||.x.|| by A11,A12;
end; then
g is Lipschitzian by A11,LOPBAN_1:def 8;
hence f is Lipschitzian LinearOperator of product <*X*>,Y
by Th17;
end;
theorem Th22:
for X,Y be RealNormSpace holds
MultilinearOperators(<*X*>,Y) = LinearOperators(product <*X*>,Y)
proof
let X,Y be RealNormSpace;
for f be object holds
f in MultilinearOperators(<*X*>,Y)
iff f in LinearOperators(product <*X*>,Y)
proof
let f be object;
f is LinearOperator of product <*X*>,Y
iff f is MultilinearOperator of <*X*>,Y by Th20;
hence thesis by LOPBAN_1:def 6,LOPBAN10:def 7;
end;
hence thesis by TARSKI:2;
end;
theorem Th23:
for X,Y be RealNormSpace holds
BoundedMultilinearOperators(<*X*>,Y)
= BoundedLinearOperators(product <*X*>,Y)
proof
let X,Y be RealNormSpace;
for f be object holds
f in BoundedMultilinearOperators(<*X*>,Y)
iff f in BoundedLinearOperators(product <*X*>,Y)
proof
let f be object;
f is Lipschitzian LinearOperator of product <*X*>,Y
iff f is Lipschitzian MultilinearOperator of <*X*>,Y
by Th21;
hence thesis by LOPBAN_1:def 9,LOPBAN10:def 11;
end;
hence thesis by TARSKI:2;
end;
theorem Th24:
for X,Y be RealNormSpace holds
BoundedMultilinearOperatorsNorm(<*X*>,Y)
= BoundedLinearOperatorsNorm(product <*X*>,Y)
proof
let X,Y be RealNormSpace;
set n1 = BoundedMultilinearOperatorsNorm(<*X*>,Y);
set n2 = BoundedLinearOperatorsNorm(product <*X*>,Y);
A1: BoundedMultilinearOperators(<*X*>,Y)
= BoundedLinearOperators(product <*X*>,Y) by Th23;
A2: dom <*X*> = {1} by FINSEQ_1:2,38; then
reconsider i = 1 as Element of dom <*X*> by TARSKI:def 1;
for f be object st f in BoundedMultilinearOperators(<*X*>,Y)
holds n1.f = n2.f
proof
let f be object;
assume
A4: f in BoundedMultilinearOperators(<*X*>,Y);
reconsider f1 = f
as Lipschitzian MultilinearOperator of <*X*>,Y
by A4,LOPBAN10:def 11;
A5: modetrans(f,<*X*>,Y) = f1;
A6: n1.f = upper_bound PreNorms(f1) by A4,A5,LOPBAN10:def 15;
reconsider f2 = f
as Lipschitzian LinearOperator of product <*X*>,Y
by A1,A4,LOPBAN_1:def 9;
A7: modetrans(f,product <*X*>,Y) = f2 by A1,A4,LOPBAN_1:def 11;
A8: n2.f = upper_bound(PreNorms(f2)) by A1,A4,A7,LOPBAN_1:def 13;
for n be object holds n in PreNorms(f1) iff n in PreNorms(f2)
proof
let n be object;
hereby
assume n in PreNorms(f1); then
consider x be VECTOR of product <*X*> such that
A9: n = ||.f1.x.||
& for i be Element of dom <*X*> holds ||.x.i.|| <= 1;
consider x1 be Point of X such that
A10: x = <*x1*> by Th12;
A11: ||.x.|| = ||.x1.|| by A10,Th12;
||.x.i.|| <= 1 by A9; then
||.x1.|| <= 1 by A10;
hence n in PreNorms(f2) by A9,A11;
end;
assume n in PreNorms(f2); then
consider s be VECTOR of product <*X*> such that
A12: n = ||.f2.s.|| & ||.s.|| <= 1;
consider s1 be Point of X such that
A13: s = <*s1*> by Th12;
A14: ||.s.|| = ||.s1.|| by A13,Th12;
for i be Element of dom <*X*> holds ||.s.i.|| <= 1
proof
let i be Element of dom <*X*>;
A15: i = 1 by A2,TARSKI:def 1;
thus ||.s.i.|| <= 1 by A12,A13,A14,A15;
end;
hence n in PreNorms(f1) by A12;
end;
hence n1.f = n2.f by A6,A8,TARSKI:2;
end;
hence n1 = n2 by Th23;
end;
theorem Th25:
for X,Y be RealNormSpace holds
R_VectorSpace_of_MultilinearOperators(<*X*>,Y)
= R_VectorSpace_of_LinearOperators(product <*X*>,Y)
proof
let X,Y be RealNormSpace;
MultilinearOperators(<*X*>,Y) = LinearOperators(product <*X*>,Y) by Th22;
hence thesis;
end;
theorem Th26:
for X,Y be RealNormSpace holds
R_NormSpace_of_BoundedMultilinearOperators(<*X*>,Y)
= R_NormSpace_of_BoundedLinearOperators(product <*X*>,Y)
proof
let X,Y be RealNormSpace;
A1: R_VectorSpace_of_MultilinearOperators(<*X*>,Y)
= R_VectorSpace_of_LinearOperators(product <*X*>,Y) by Th25;
BoundedMultilinearOperatorsNorm(<*X*>,Y)
= BoundedLinearOperatorsNorm(product <*X*>,Y) by Th24;
hence thesis by A1;
end;
theorem
for X be RealNormSpace st X is complete
holds product <*X*> is complete
proof
let X be RealNormSpace;
A1: dom <*X*> = {1} by FINSEQ_1:2,38; then
reconsider i = 1 as Element of dom <*X*> by TARSKI:def 1;
assume
A2: X is complete;
now
let i be Element of dom <*X*>;
i = 1 by A1,TARSKI:def 1;
hence <*X*>.i is complete by A2;
end;
hence product <*X*> is complete by PRVECT_2:14;
end;
begin :: Spaces of multilinear maps and nested compositions over real normed vector spaces
theorem
for X,Y be RealNormSpace-Sequence,
Z be RealNormSpace,
f be Lipschitzian BilinearOperator of product X, product Y, Z
holds
f * (IsoCPNrSP(product X,product Y)) " is
Lipschitzian MultilinearOperator of <*product X,product Y*>,Z
by LOPBAN12:13;
theorem
for X,Y be RealNormSpace-Sequence,
Z be RealNormSpace,
f be Point of
R_NormSpace_of_BoundedBilinearOperators(product X, product Y, Z)
holds
f * (IsoCPNrSP(product X, product Y)) " is Point of
R_NormSpace_of_BoundedMultilinearOperators(<* product X, product Y *>,Z)
proof
let X,Y be RealNormSpace-Sequence,
Z be RealNormSpace,
f be Point of
R_NormSpace_of_BoundedBilinearOperators(product X,product Y,Z);
f is Lipschitzian BilinearOperator of product X,product Y,Z
by LOPBAN_9:def 4;
then
f * (IsoCPNrSP(product X, product Y))" is Lipschitzian MultilinearOperator
of <*product X,product Y*>,Z
by LOPBAN12:13;
hence thesis by LOPBAN10:def 11;
end;
theorem Th30:
for X,Y be RealLinearSpace-Sequence
holds carr(X^Y) = (carr X) ^ (carr Y)
proof
let X,Y be RealLinearSpace-Sequence;
reconsider CX = carr X, CY = carr Y as FinSequence;
A1: len CX = len X
& len CY = len Y
& len carr(X^Y) = len(X^Y) by PRVECT_1:def 11;
len carr(X^Y) = len X + len Y
& len(CX^CY) = len X + len Y by A1,FINSEQ_1:22;
then
A2: dom carr(X^Y) = dom(CX^CY) by FINSEQ_3:29;
for i be Nat st i in dom carr(X^Y)
holds carr (X^Y).i = (CX^CY).i
proof
let i be Nat;
assume
A3: i in dom carr(X^Y); then
reconsider i1 = i as Element of dom(X^Y) by A1,FINSEQ_3:29;
A4: carr (X^Y).i = the carrier of (X^Y).i1 by PRVECT_1:def 11;
A5: i in dom(X^Y) by A1,A3,FINSEQ_3:29;
per cases by A5,FINSEQ_1:25;
suppose
A6: i in dom X; then
A7: i in dom CX by A1,FINSEQ_3:29;
reconsider i2 = i1 as Element of dom X by A6;
thus carr (X^Y).i = the carrier of X.i2 by A4,FINSEQ_1:def 7
.= CX.i by PRVECT_1:def 11
.= (CX^CY).i by A7,FINSEQ_1:def 7;
end;
suppose
ex n be Nat st n in dom Y & i = len X + n;
then consider n be Nat such that
A8: n in dom Y & i = len X + n;
A9: n in dom CY by A1,A8,FINSEQ_3:29;
reconsider n1 = n as Element of dom Y by A8;
thus carr (X^Y).i = the carrier of Y.n1 by A4,A8,FINSEQ_1:def 7
.= CY.n by PRVECT_1:def 11
.= (CX^CY).i by A1,A8,A9,FINSEQ_1:def 7;
end;
end;
hence carr(X^Y) = (carr X) ^ (carr Y) by A2,FINSEQ_1:13;
end;
theorem Th31:
for X be RealLinearSpace
holds
len carr <*X*> = len <*X*>
& len carr <*X*> = 1
& carr <*X*> = <* the carrier of X *>
proof
let X be RealLinearSpace;
thus len carr <*X*> = len <*X*> by PRVECT_1:def 11;
hence
A1: len carr <*X*> = 1 by FINSEQ_1:40;
A2: dom <*X*> = {1} by FINSEQ_1:2,def 8;
A3: <*X*>.1 = X;
1 in {1} by TARSKI:def 1;
then (carr <*X*>).1 = the carrier of X by A2,A3,PRVECT_1:def 11;
hence carr <*X*> = <* the carrier of X *> by A1,FINSEQ_1:40;
end;
theorem Th32:
for X be RealNormSpace-Sequence,
x be Element of product X,
Y be RealNormSpace,
z be Element of product(X ^ <*Y*>),
i be Element of dom X,
j be Element of dom(X ^ <*Y*>),
xi be Element of X.i,
y be Point of Y
st i = j & z = x ^ <*y*>
holds
reproj(j,z).xi = (reproj(i,x).xi) ^ <*y*>
proof
let X be RealNormSpace-Sequence,
x be Element of product X,
Y be RealNormSpace,
z be Element of product(X ^ <*Y*>),
i be Element of dom X,
j be Element of dom(X ^ <*Y*>),
xi be Element of X.i,
y be Point of Y;
assume
A1: i = j & z = x ^ <*y*>;
set CX = carr X;
A2: product X = NORMSTR(# product(carr X),
zeros X,
[:(addop X):],
[:(multop X):],
productnorm X #) by PRVECT_2:6;
A3: ex x1 be Function
st x1 = x
& dom x1 = dom CX
& for i be object st i in dom CX
holds x1.i in CX.i by A2,CARD_3:def 5;
dom x = Seg len CX by A3,FINSEQ_1:def 3;
then
A4: len x = len CX by FINSEQ_1:def 3;
A5: len X = len CX by PRVECT_1:def 11;
i in dom X;
then i in Seg len X by FINSEQ_1:def 3;
then
A6: 1 <= i & i <= len X by FINSEQ_1:1;
reconsider xj = xi as Element of (X ^ <*Y*>).j by A1,FINSEQ_1:def 7;
A7: dom(reproj(j,z).xj)
= dom(z +* (j,xj)) by NDIFF_5:def 4
.= dom z by FUNCT_7:30;
then dom(reproj(j,z).xj) = Seg len z by FINSEQ_1:def 3;
then
A8: len(reproj(j,z).xj) = len z by FINSEQ_1:def 3;
A9: dom(reproj(i,x).xi)
= dom(x +* (i,xi)) by NDIFF_5:def 4
.= dom x by FUNCT_7:30;
then
A10: dom(reproj(i,x).xi) = Seg len x by FINSEQ_1:def 3;
then
A11: len(reproj(i,x).xi) = len x by FINSEQ_1:def 3;
A12: len z
= len x + len <*y*> by FINSEQ_1:22,A1
.= len x + 1 by FINSEQ_1:40;
A13: len(reproj(i,x).xi ^ <*y*>)
= len(reproj(i,x).xi) + len <*y*> by FINSEQ_1:22
.= len(reproj(i,x).xi) + 1 by FINSEQ_1:40;
A14: dom(reproj(i,x).xi ^ <*y*>)
= Seg len(reproj(i,x).xi ^ <*y*>) by FINSEQ_1:def 3
.= Seg len(reproj(j,z).xj) by A8,A10,A12,A13,FINSEQ_1:def 3
.= dom(reproj(j,z).xj) by FINSEQ_1:def 3;
for k be object st k in dom(reproj(i,x).xi ^ <*y*>)
holds (reproj(i,x).xi ^ <*y*>).k = (reproj(j,z).xj).k
proof
let k be object;
assume
A15: k in dom(reproj(i,x).xi ^<*y*>);
then
A16: k in Seg len(reproj(i,x).xi ^<*y*>) by FINSEQ_1:def 3;
reconsider k1 = k as Nat by A15;
A17: (reproj(j,z).xj).k1 = (z +* (j,xj)).k1 by NDIFF_5:def 4;
A18: 1 <= k1 & k1 <= len(reproj(i,x).xi) + 1 by A13,A16,FINSEQ_1:1;
per cases;
suppose
k1 <= len(reproj(i,x).xi); then
A19: k1 in Seg len(reproj(i,x).xi) by A18;
then k1 in dom(reproj(i,x).xi) by FINSEQ_1:def 3;
then
A20: (reproj(i,x).xi ^ <*y*>).k1
= (reproj(i,x).xi).k1 by FINSEQ_1:def 7
.= (x +* (i,xi)).k1 by NDIFF_5:def 4;
A21: k1 in dom x by A9,A19,FINSEQ_1:def 3;
per cases;
suppose
A22: k1 = i; then
(reproj(i,x).xi ^ <*y*>).k1 = xi by A20,A21,FUNCT_7:31;
hence (reproj(i,x).xi ^ <*y*>).k = (reproj(j,z).xj).k
by A1,A7,A14,A15,A17,A22,FUNCT_7:31;
end;
suppose
A24: k1 <> i;
(reproj(j,z).xj).k1
= z.k1 by A1,A17,A24,FUNCT_7:32
.= x.k1 by A1,A21,FINSEQ_1:def 7;
hence
(reproj(i,x).xi ^ <*y*>).k
= (reproj(j,z).xj).k by A20,A24,FUNCT_7:32;
end;
end;
suppose
A25: len(reproj(i,x).xi) < k1;
then
A26: len(reproj(i,x).xi) + 1 <= k1 by NAT_1:13;
then
A27: len(reproj(i,x).xi) + 1 = k1 by A18,XXREAL_0:1;
A28: j <> k1 by A1,A4,A5,A6,A10,A25,FINSEQ_1:def 3;
A29: len x + 1 = k1 by A11,A18,A26,XXREAL_0:1;
(reproj(j,z).xj).k1
= z.k1 by A17,A28,FUNCT_7:32
.= y by A1,A29,FINSEQ_1:42;
hence (reproj(i,x).xi ^ <*y*>).k
= (reproj(j,z).xj).k by A27,FINSEQ_1:42;
end;
end;
hence thesis by A14,FUNCT_1:2;
end;
theorem Th33:
for X be RealNormSpace-Sequence,
x be Element of product X,
Y be RealNormSpace,
z be Element of product(X ^ <*Y*>),
j be Element of dom(X ^ <*Y*>),
y be Element of Y,
y0 be Point of Y
st z = x ^ <*y0*> & j = len x + 1
holds
reproj(j,z).y = x ^ <*y*>
proof
let X be RealNormSpace-Sequence,
x be Element of product X,
Y be RealNormSpace,
z be Element of product(X ^ <*Y*>),
j be Element of dom(X ^ <*Y*>),
y be Element of Y,
y0 be Point of Y;
assume
A1: z = x ^ <*y0*> & j = len x + 1;
set CX = carr X;
A2: product X = NORMSTR(# product(carr X),
zeros X,
[:(addop X):],
[:(multop X):],
productnorm X #) by PRVECT_2:6;
A3: ex x1 be Function
st x = x1
& dom x1 = dom CX
& for i be object st i in dom CX
holds x1.i in CX.i by A2,CARD_3:def 5;
dom x = Seg len CX by A3,FINSEQ_1:def 3;
then
A4: len x = len CX by FINSEQ_1:def 3;
A5: len X = len CX by PRVECT_1:def 11;
reconsider y1 = y as Element of ((X ^ <*Y*>).j)
by A1,A4,A5,FINSEQ_1:42;
A6: dom(reproj(j,z).y1)
= dom(z +* (j,y1)) by NDIFF_5:def 4
.= dom z by FUNCT_7:30;
then
A7: dom(reproj(j,z).y1) = Seg len z by FINSEQ_1:def 3;
A8: len z
= len x + len <*y0*> by FINSEQ_1:22,A1
.= len x + 1 by FINSEQ_1:40;
then
A9: len(reproj(j,z).y1) = len x + 1 by A7,FINSEQ_1:def 3;
A10: len(x ^ <*y*>)
= len x + len <*y*> by FINSEQ_1:22
.= len x + 1 by FINSEQ_1:40;
A11: dom(reproj(j,z).y1) = dom(x ^ <*y*>) by A7,A8,A10,FINSEQ_1:def 3;
for k be object st k in dom(reproj(j,z).y1)
holds (reproj(j,z).y1).k = (x ^ <*y*>).k
proof
let k be object;
assume
A12: k in dom(reproj(j,z).y1);
then
A13: k in Seg len(reproj(j,z).y1) by FINSEQ_1:def 3;
reconsider k1 = k as Nat by A12;
A14: (reproj(j,z).y1).k1 = (z +* (j,y1)).k1 by NDIFF_5:def 4;
A15: 1 <= k1 & k1 <= len(reproj(j,z).y1) by A13,FINSEQ_1:1;
per cases;
suppose
A16: k1 <= len x;
then k1 in Seg len x by A15;
then
A17: k1 in dom x by FINSEQ_1:def 3;
A18: len x + 0 < len x + 1 by XREAL_1:8;
(reproj(j,z).y1).k1
= z.k1 by A1,A14,A16,A18,FUNCT_7:32
.= x.k1 by A1,A17,FINSEQ_1:def 7;
hence (reproj(j,z).y1).k = (x ^ <*y*>).k by A17,FINSEQ_1:def 7;
end;
suppose
len x < k1;
then len x + 1 <= k1 by NAT_1:13;
then
A19: len x + 1 = k1 by A9,A15,XXREAL_0:1;
then (x ^ <*y*>).k1 = y by FINSEQ_1:42;
hence (reproj(j,z).y1).k = (x ^ <*y*>).k
by A1,A6,A12,A14,A19,FUNCT_7:31;
end;
end;
hence thesis by FUNCT_1:2,A11;
end;
theorem Th34:
for X be RealNormSpace-Sequence,
x be Element of product X,
Y be RealNormSpace,
y be Point of Y
holds
x ^ <*y*> is Point of product(X ^ <*Y*>)
proof
let X be RealNormSpace-Sequence,
x be Element of product X,
Y be RealNormSpace,
y be Point of Y;
set CX = carr X;
set CY = the carrier of Y;
A1: product X = NORMSTR(# product(carr X),
zeros X,
[:(addop X):],
[:(multop X):],
productnorm X #) by PRVECT_2:6;
product(X ^ <*Y*>) = NORMSTR(# product(carr(X ^ <*Y*>)),
zeros(X ^ <*Y*>),
[:addop(X ^ <*Y*>):],
[:multop(X ^ <*Y*>):],
productnorm(X ^ <*Y*>) #) by PRVECT_2:6;
then
A2: the carrier of product(X ^ <*Y*>)
= product((carr X) ^ carr <*Y*>) by Th30
.= product(CX ^ <*CY*>) by Th31;
A3: ex x1 be Function
st x = x1
& dom x1 = dom CX
& for i be object st i in dom CX
holds x1.i in CX.i by A1,CARD_3:def 5;
A4: len (x ^ <*y*>)
= len x + len <*y*> by FINSEQ_1:22
.= len x + 1 by FINSEQ_1:40;
A5: dom x = Seg len CX by A3,FINSEQ_1:def 3;
then
A6: len x = len CX by FINSEQ_1:def 3;
A7: len(CX ^ <*CY*>)
= len CX + len <*CY*> by FINSEQ_1:22
.= len CX + 1 by FINSEQ_1:40;
A8: dom(x ^ <*y*>)
= Seg len(x ^ <*y*>) by FINSEQ_1:def 3
.= Seg len(CX ^ <*CY*>) by A4,A5,A7,FINSEQ_1:def 3
.= dom(CX ^ <*CY*>) by FINSEQ_1:def 3;
for i be object st i in dom (CX ^ <*CY*>)
holds (x ^ <*y*>).i in (CX ^ <*CY*>).i
proof
let i be object;
assume
A9: i in dom(CX ^ <*CY*>);
then
A10: i in Seg len(CX ^ <*CY*>) by FINSEQ_1:def 3;
reconsider i1 = i as Nat by A9;
per cases;
suppose
A11: i1 <= len x;
1 <= i1 & i1 <= len(CX ^ <*CY*>) by A10,FINSEQ_1:1;
then
A12: i1 in Seg len x by A11;
then i1 in dom x by FINSEQ_1:def 3;
then
A13: (x ^ <*y*>).i1 = x.i1 by FINSEQ_1:def 7;
A15: i1 in dom CX by A3,FINSEQ_1:def 3,A12;
i1 in dom x by A12,FINSEQ_1:def 3; then
x.i1 in CX.i1 by A3;
hence (x ^ <*y*>).i in (CX ^ <*CY*>).i
by A13,A15,FINSEQ_1:def 7;
end;
suppose
len x < i1;
then
A17: len x + 1 <= i1 by NAT_1:13;
1 <= i1 & i1 <= len(CX ^ <*CY*>) by A10,FINSEQ_1:1;
then
A19: i1 = len x + 1 by A6,A7,A17,XXREAL_0:1;
then
A20: (x ^ <*y*>).i1 = y by FINSEQ_1:42;
(CX ^ <*CY*>).i1 = CY by A6,A19,FINSEQ_1:42;
hence (x ^ <*y*>).i in (CX ^ <*CY*>).i by A20;
end;
end;
hence thesis by A2,A8,CARD_3:def 5;
end;
theorem Th35:
for X be RealNormSpace-Sequence,
x be Element of product X,
Y be RealNormSpace,
z be Element of product(X ^ <*Y*>),
y be Point of Y
st z = x ^ <*y*>
holds NrProduct z = ||.y.|| * (NrProduct x)
proof
let X be RealNormSpace-Sequence,
x be Element of product X,
Y be RealNormSpace,
z be Element of product(X ^ <*Y*>),
y be Point of Y;
assume
A1: z = x ^ <*y*>;
consider nz be FinSequence of REAL such that
A2: dom nz = dom(X ^ <*Y*>)
& ( for i be Element of dom(X ^ <*Y*>)
holds nz.i = ||.z.i.|| )
& NrProduct z = Product nz by LOPBAN10:def 9;
set nx = nz | (len x);
A3: product X = NORMSTR(# product(carr X),
zeros X,
[:(addop X):],
[:(multop X):],
productnorm X #) by PRVECT_2:6;
set CX = carr X;
consider x1 be Function such that
A4: x = x1
& dom x1 = dom CX
& for i be object st i in dom CX
holds x1.i in CX.i by A3,CARD_3:def 5;
A5: dom x1 = Seg len CX by A4,FINSEQ_1:def 3;
reconsider x1 as FinSequence by A4;
A6: len x
= len CX by A4,A5,FINSEQ_1:def 3
.= len X by PRVECT_1:def 11;
dom nz = Seg len(X ^ <*Y*>) by A2,FINSEQ_1:def 3;
then
A7: len nz
= len(X ^ <*Y*>) by FINSEQ_1:def 3
.= len X + len <*Y*> by FINSEQ_1:22
.= len X + 1 by FINSEQ_1:40;
then
A8: len nx = len x by NAT_1:11,A6,FINSEQ_1:59;
A9: len(X ^ <*Y*>)
= len X + len <*Y*> by FINSEQ_1:22
.= len X + 1 by FINSEQ_1:40;
A10: dom x
= Seg len x by FINSEQ_1:def 3
.= dom X by A6,FINSEQ_1:def 3;
A11: dom nz
= Seg(len X + 1) by A7,FINSEQ_1:def 3
.= dom(X ^ <*Y*>) by A9,FINSEQ_1:def 3;
A12: len nz = len nx + 1 by A6,A7,NAT_1:11,FINSEQ_1:59;
A13: dom nx
= Seg len x by A8,FINSEQ_1:def 3
.= dom X by A6,FINSEQ_1:def 3;
A14: for i be Element of dom X
holds nx.i = ||.x.i.||
proof
let i be Element of dom X;
i in dom X;
then
A15: i in Seg len X by FINSEQ_1:def 3;
then
A16: 1 <= i & i <= len X by FINSEQ_1:1;
len X <= len X + 1 by NAT_1:11;
then i <= len X + 1 by A16,XXREAL_0:2;
then i in Seg(len X + 1 ) by A16;
then reconsider j = i as Element of dom(X ^ <*Y*>)
by A9,FINSEQ_1:def 3;
A17: (X ^ <*Y*>).i = X.i by FINSEQ_1:def 7;
thus nx.i
= nz.i by A6,A15,FUNCT_1:49
.= ||.z.j.|| by A2
.= ||.x.i.|| by A1,A10,A17,FINSEQ_1:def 7;
end;
0 <= Product nx
proof
per cases;
suppose
ex i be Nat st i in dom nx & nx.i = 0;
hence 0 <= Product nx by RVSUM_1:103;
end;
suppose
A18: for i be Nat
holds not i in dom nx or not nx.i = 0;
for i be Element of NAT st i in dom nx
holds nx.i > 0
proof
let i be Element of NAT;
assume
A19: i in dom nx;
reconsider i1 = i as Element of dom X by A13,A19;
A20: 0 <= ||.x.i1.|| by NORMSP_1:4;
nx.i = ||.x.i1.|| by A14;
hence nx.i > 0 by A18,A19,A20,XXREAL_0:1;
end;
hence 0 <= Product nx by NAT_4:42;
end;
end;
then Product nx is non negative by XXREAL_0:def 7;
then
A21: NrProduct x = Product nx by A13,A14,LOPBAN10:def 9;
A22: len(nx ^ <* ||.y.|| *>)
= len nx + len <* ||.y.|| *> by FINSEQ_1:22
.= len X + len <* ||.y.|| *> by A6,A7,NAT_1:11,FINSEQ_1:59
.= len X + 1 by FINSEQ_1:40;
A23: dom(nx ^ <* ||.y.|| *>)
= Seg (len X + 1) by A22,FINSEQ_1:def 3
.= dom nz by A7,FINSEQ_1:def 3;
for i be object st i in dom (nx ^ <* ||.y.|| *>)
holds (nx ^ <* ||.y.|| *>).i = nz.i
proof
let i be object;
assume
A24: i in dom (nx ^ <* ||.y.|| *>);
then
A25: i in Seg len nz by A23,FINSEQ_1:def 3;
reconsider i1 = i as Nat by A24;
per cases;
suppose
A26: i1 <= len nx;
A27: 1 <= i1 & i1 <= len nx + 1 by A12,A25,FINSEQ_1:1;
then
A28: i1 in Seg len nx by A26;
reconsider i2 = i1 as Element of dom X
by A6,A8,A28,FINSEQ_1:def 3;
A29: i2 in dom nx by A28,FINSEQ_1:def 3;
A30: i2 in Seg len X by A6,A8,A26,A27;
(nx ^ <* ||.y.|| *>).i2
= nx.i1 by A29,FINSEQ_1:def 7
.= nz.i2 by A6,A30,FUNCT_1:49;
hence (nx ^ <* ||.y.|| *>).i = nz.i;
end;
suppose
len nx < i1;
then
A31: len nx + 1 <= i1 by NAT_1:13;
1 <= i1 & i1 <= len nx + 1 by A25,FINSEQ_1:1,A12;
then
A32: i1 = len nx + 1 by A31,XXREAL_0:1;
reconsider i2 = i1 as Element of dom(X ^ <*Y*>) by A11,A23,A24;
A33: (X ^ <*Y*>).i2 = Y by A6,A8,A32,FINSEQ_1:42;
nz.i2
= ||.z.i2.|| by A2
.= ||.y.|| by A1,A8,A32,A33,FINSEQ_1:42;
hence (nx ^ <* ||.y.|| *>).i = nz.i by FINSEQ_1:42,A32;
end;
end;
then
nx ^ <* ||.y.|| *> = nz by A23,FUNCT_1:2;
hence thesis by A2,A21,RVSUM_1:96;
end;
theorem Th36:
for X,Z be RealNormSpace,
Y be RealNormSpace-Sequence
holds
ex I be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,
R_NormSpace_of_BoundedMultilinearOperators(Y,Z)),
R_NormSpace_of_BoundedMultilinearOperators(Y ^ <*X*>, Z)
st I is one-to-one onto isometric
& for u be Point of R_NormSpace_of_BoundedLinearOperators(X,
R_NormSpace_of_BoundedMultilinearOperators(Y,Z))
holds
||.u.|| = ||.I.u.||
& for y be Point of product Y,
x be Point of X
holds (I.u).(y ^ <*x*>) = (u.x).y
proof
let X,Z be RealNormSpace,
Y be RealNormSpace-Sequence;
set CX = the carrier of X;
set CY = carr Y;
set CZ = the carrier of Z;
consider J be Function of Funcs(CX, Funcs(product CY,CZ)),
Funcs(product(CY ^ <*CX*>),CZ)
such that
A1: J is bijective
& for f be Function of CX,Funcs(product CY,CZ)
for y be FinSequence
for x be object
st y in product CY & x in CX
holds (J.f).(y ^ <*x*>) = (f.x).y by NDIFF_6:6;
set LXYZ = the carrier of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedMultilinearOperators(Y,Z));
set BXYZ = the carrier of R_NormSpace_of_BoundedMultilinearOperators
(Y ^ <*X*>, Z);
set LYZ = the carrier of R_NormSpace_of_BoundedMultilinearOperators(Y,Z);
product <*X*> = NORMSTR(# product(carr <*X*>),
zeros <*X*>,
[: addop <*X*> :],
[: multop <*X*> :],
productnorm <*X*> #) by PRVECT_2:6;
then
A2: the carrier of product <*X*>
= product <* the carrier of X *> by Th31;
A3: product Y = NORMSTR(# product(carr Y),
zeros Y,
[: addop Y :],
[: multop Y :],
productnorm Y #) by PRVECT_2:6;
A4: LYZ c= Funcs(product CY,CZ) by A3,XBOOLE_1:1;
A5: LXYZ c= Funcs(CX, LYZ) by XBOOLE_1:1;
product(Y ^ <*X*>) = NORMSTR(# product carr(Y ^ <*X*>),
zeros(Y ^ <*X*>),
[: addop(Y ^ <*X*>) :],
[: multop(Y ^ <*X*>) :],
productnorm(Y ^ <*X*>) #) by PRVECT_2:6;
then
A6: the carrier of product(Y ^ <*X*>)
= product((carr Y) ^ carr <*X*> ) by Th30
.= product(CY ^ <*CX*>) by Th31;
Funcs(CX, LYZ) c= Funcs(CX, Funcs(product CY,CZ))
proof
let f be object;
assume f in Funcs(CX, LYZ); then
consider f1 be Function such that
A7: f = f1 & dom f1 = CX & rng f1 c= LYZ by FUNCT_2:def 2;
rng f1 c= Funcs(product CY, CZ) by A4,A7,XBOOLE_1:1;
hence f in Funcs(CX, Funcs(product CY,CZ)) by A7,FUNCT_2:def 2;
end;
then
A8: LXYZ c= Funcs(CX, Funcs(product CY,CZ)) by A5,XBOOLE_1:1; then
reconsider I = J | LXYZ as Function of LXYZ,Funcs(product(CY ^ <*CX*>),CZ)
by FUNCT_2:32;
A9: for f be Element of LXYZ
holds
( for x be Point of X
holds
ex g be Lipschitzian MultilinearOperator of Y,Z
st g = f.x
& for y be Point of product Y
holds (I.f).(y ^ <*x*>) = g.y )
& I.f is Lipschitzian MultilinearOperator of Y ^ <*X*>,Z
& I.f in BXYZ
& ex If be Point of
R_NormSpace_of_BoundedMultilinearOperators(Y ^ <*X*>,Z)
st If = I.f & ||.f.|| = ||.If.||
proof
let f be Element of LXYZ;
A10: I.f = J.f by FUNCT_1:49;
A11: f in Funcs(CX, Funcs(product CY,CZ)) by A8,TARSKI:def 3;
reconsider f0 = f as Function of CX, Funcs(product CY,CZ)
by A8,TARSKI:def 3,FUNCT_2:66;
reconsider f1 = f as Lipschitzian LinearOperator of
X,R_NormSpace_of_BoundedMultilinearOperators(Y,Z)
by LOPBAN_1:def 9;
thus
A12: for x be Point of X holds
ex g be Lipschitzian MultilinearOperator of Y,Z
st g = f.x
& for y be Point of product Y
holds (I.f).(y ^ <*x*>) = g.y
proof
let x be Point of X;
f1.x in BoundedMultilinearOperators(Y,Z);
then reconsider g = f0.x
as Lipschitzian MultilinearOperator of Y,Z
by LOPBAN10:def 11;
take g;
thus g = f.x;
let y be Point of product Y;
thus thesis by A1,A3,A10;
end;
A13: J.f is Function of product(CY ^ <*CX*>),CZ by A11,FUNCT_2:5,66;
reconsider Jf = J.f as Function of product(Y ^ <*X*>),Z
by A6,A11,FUNCT_2:5,66;
for i be Element of dom(Y ^ <*X*>)
for z be Element of product(Y ^ <*X*>)
holds Jf * reproj(i,z) is LinearOperator of (Y ^ <*X*>).i,Z
proof
let i be Element of dom(Y ^ <*X*>);
let z be Element of product(Y ^ <*X*>);
consider y, px be FinSequence such that
A14: z = y ^ px & y in product CY & px in product <*CX*>
by RLAFFIN3:2,A6;
reconsider y as Point of product Y by A3,A14;
consider x be Point of X such that
A15: px = <*x*> by A2,A14,Th12;
consider cy be Function such that
A16: y = cy
& dom cy = dom CY
& for i be object st i in dom CY
holds cy.i in CY.i by A14,CARD_3:def 5;
A17: dom cy = Seg len CY by A16,FINSEQ_1:def 3;
reconsider cy as FinSequence by A16;
A18: len y
= len CY by A16,A17,FINSEQ_1:def 3
.= len Y by PRVECT_1:def 11;
A19: dom(Y ^ <*X*>)
= Seg(len(Y ^ <*X*>)) by FINSEQ_1:def 3
.= Seg(len Y + len <*X*>) by FINSEQ_1:22
.= Seg(len Y + 1) by FINSEQ_1:40;
A20: 1 <= i & i <= len Y + 1 by A19,FINSEQ_1:1;
per cases;
suppose
i <= len y;
then i in Seg len Y by A18,A20;
then reconsider i0 = i as Element of dom Y by FINSEQ_1:def 3;
consider g be Lipschitzian MultilinearOperator of Y,Z such that
A21: g = f.x
& for py be Point of product Y
holds (I.f).(py ^ <*x*>) = g.py by A12;
A22: (Y ^ <*X*>).i = Y.i0 by FINSEQ_1:def 7;
then reconsider L = Jf * reproj(i,z) as Function of Y.i0,Z;
dom(I.f) = the carrier of product(Y ^ <*X*>)
by A6,A10,A13,FUNCT_2:def 1;
then rng reproj(i,z) c= dom(I.f);
then
A23: dom(I.f * reproj(i,z))
= dom(reproj(i,z)) by RELAT_1:27
.= the carrier of (Y ^ <*X*>).i by FUNCT_2:def 1;
A24: dom(g * reproj(i0,y)) = the carrier of Y.i0
by FUNCT_2:def 1;
for w be object
st w in dom(I.f * reproj(i,z))
holds (I.f * reproj(i,z)).w = (g * reproj(i0,y)).w
proof
let w be object;
assume
A25: w in dom(I.f * reproj(i,z));
then
reconsider w1 = w as Point of (Y ^ <*X*>).i;
reconsider w2 = w as Point of Y.i0 by A25,FINSEQ_1:def 7;
A26: reproj(i,z).w1 = reproj(i0,y).w2 ^ <*x*> by A14,A15,Th32;
thus (I.f * reproj(i,z)).w
= (I.f).(reproj(i,z).w1) by FUNCT_2:15
.= g.(reproj(i0,y).w2) by A21,A26
.= (g * reproj(i0,y)).w by FUNCT_2:15;
end; then
I.f * reproj(i,z) = g * reproj(i0,y) by A22,A23,A24,FUNCT_1:2;
hence Jf * reproj(i,z) is LinearOperator of (Y ^ <*X*>).i,Z
by A10,A22,LOPBAN10:def 6;
end;
suppose
len y < i;
then
A28: len y + 1 <= i by NAT_1:13;
then
A29: i = len y + 1 by A20,A18,XXREAL_0:1;
then
A30: (Y ^ <*X*>).i = X by A18,FINSEQ_1:42;
then reconsider h = Jf * reproj(i,z) as Function of X,Z;
A31: dom reproj(i,z)
= the carrier of (Y ^ <*X*>).i by FUNCT_2:def 1
.= the carrier of X by A18,A29,FINSEQ_1:42;
for x1,x2 be Point of X
holds h.(x1 + x2) = h.x1 + h.x2
proof
let x1,x2 be Point of X;
consider g1 be Lipschitzian MultilinearOperator of Y,Z
such that
A32: g1 = f.x1
& for py be Point of product Y
holds (I.f).(py ^ <*x1*>) = g1.py by A12;
consider g2 be Lipschitzian MultilinearOperator of Y,Z
such that
A33: g2 = f.x2
& for py be Point of product Y
holds (I.f).(py ^ <*x2*>) = g2.py by A12;
consider g12 be Lipschitzian MultilinearOperator of Y,Z
such that
A34: g12 = f.(x1 + x2)
& for py be Point of product Y
holds (I.f).(py ^ <*x1 + x2*>) = g12.py by A12;
A35: f1 is additive;
A36: g12 = f.x1 + f.x2 by A34,A35;
A37: h.(x1 + x2)
= (I.f).(reproj(i,z).(x1 + x2)) by FUNCT_1:13,A10,A31
.= (I.f).(y ^ <*x1 + x2*>)
by A14,A15,A18,A20,A28,Th33,XXREAL_0:1
.= (f.x1 + f.x2).y by A34,A36
.= g1.y + g2.y by A32,A33,LOPBAN10:48;
A38: h.x1
= (I.f).(reproj(i,z).x1) by FUNCT_1:13,A10,A31
.= (I.f).(y ^ <*x1*>) by A14,A15,A18,A20,A28,Th33,XXREAL_0:1
.= g1.y by A32;
h.x2
= (I.f).(reproj(i,z).x2) by A10,A31,FUNCT_1:13
.= (I.f).(y ^ <*x2*>) by A14,A15,A18,A20,A28,Th33,XXREAL_0:1
.= g2.y by A33;
hence h.(x1 + x2) = h.x1+ h.x2 by A37,A38;
end; then
A40: h is additive;
for x0 be Point of X, a be Real
holds h.(a * x0) = a * h.x0
proof
let x0 be Point of X, a be Real;
consider g1 be Lipschitzian MultilinearOperator of Y,Z
such that
A41: g1 = f.x0
& for py be Point of product Y
holds (I.f).(py ^ <*x0*>) = g1.py by A12;
consider g2 be Lipschitzian MultilinearOperator of Y,Z
such that
A42: g2 = f.(a * x0)
& for py be Point of product Y
holds (I.f).(py ^ <* a * x0 *>) = g2.py by A12;
A43: g2 = a * f1.x0 by A42,LOPBAN_1:def 5;
A44: h.(a * x0)
= (I.f).(reproj(i,z).(a * x0)) by A10,A31,FUNCT_1:13
.= (I.f).(y ^ <* a * x0 *>)
by A14,A15,A18,A20,A28,Th33,XXREAL_0:1
.= (a * f.x0).y by A42,A43
.= a * g1.y by A41,LOPBAN10:49;
h.x0
= (I.f).(reproj(i,z).x0) by A10,A31,FUNCT_1:13
.= (I.f).(y ^ <*x0*>) by A14,A15,A18,A20,A28,Th33,XXREAL_0:1
.= g1.y by A41;
hence h.(a * x0) = a * h.x0 by A44;
end;
hence Jf * reproj(i,z) is LinearOperator of (Y ^ <*X*>).i,Z
by A30,A40,LOPBAN_1:def 5;
end;
end;
then
reconsider If = I.f as MultilinearOperator of Y ^ <*X*>,Z
by A10,LOPBAN10:def 6;
set K = ||.f.||;
A46: 0 <= K by LOPBAN_1:33;
A47: for z be Point of product(Y ^ <*X*>)
holds ||.If.z.|| <= K * NrProduct(z)
proof
let z be Element of product(Y ^ <*X*>);
consider py, px be FinSequence such that
A48: z = py ^ px & py in product CY & px in product <*CX*>
by A6,RLAFFIN3:2;
reconsider py as Point of product Y by A3,A48;
consider x1 be Point of X such that
A49: px = <*x1*> by A2,A48,Th12;
consider cy be Function such that
A50: py = cy
& dom cy = dom CY
& for i be object st i in dom CY
holds cy.i in CY.i by A48,CARD_3:def 5;
reconsider cy as FinSequence by A50;
consider g be Lipschitzian MultilinearOperator of Y,Z
such that
A51: g = f.x1
& for p be Point of product Y
holds (I.f).(p ^ <*x1*>) = g.p by A12;
A52: (I.f).z = g.py by A51,A48,A49;
A53: ||.g.py.|| <= ||.f.x1.|| * NrProduct(py) by A51,LOPBAN10:45;
A54: 0 <= NrProduct(py) by XXREAL_0:def 7;
||.f1.x1.|| <= ||.f.|| * ||.x1.|| by LOPBAN_1:32;
then
A55: ||.f.x1.|| * NrProduct(py)
<= ||.f.|| * ||.x1.|| * NrProduct(py) by A54,XREAL_1:64;
||.x1.|| * NrProduct(py) = NrProduct(z) by A48,A49,Th35;
hence ||.If.z.|| <= ||.f.|| * NrProduct(z) by A52,A53,A55,XXREAL_0:2;
end;
hence
A56: I.f is Lipschitzian MultilinearOperator of Y ^ <*X*>,Z
by LOPBAN10:def 10,LOPBAN_1:33;
hence I.f in BXYZ by LOPBAN10:def 11;
reconsider If1 = I.f as Point of
R_NormSpace_of_BoundedMultilinearOperators(Y ^ <*X*>,Z)
by A56,LOPBAN10:def 11;
reconsider If2 = I.f as Lipschitzian MultilinearOperator of Y ^ <*X*>,Z
by A47,LOPBAN10:def 10,LOPBAN_1:33;
now
let r be Real;
assume r in PreNorms If2;
then consider z be VECTOR of product(Y ^ <*X*>)
such that
A57: r = ||.If2.z.||
& for i be Element of dom(Y ^ <*X*>) holds ||.z.i.|| <= 1;
0 <= NrProduct(z) <= 1 by A57,LOPBAN10:35;
then
A58: K * NrProduct(z) <= K * 1 by A46,XREAL_1:64;
||.If2.z.|| <= K * NrProduct(z) by A47;
hence r <= K by A57,A58,XXREAL_0:2;
end;
then
A59: upper_bound(PreNorms If2) <= K by SEQ_4:45;
A60: BoundedMultilinearOperatorsNorm(Y ^ <*X*>,Z).If2
= ||.If1.|| by NORMSP_0:def 1;
A61: ||.If1.|| <= ||.f.|| by A59,A60,LOPBAN10:43;
set SLYZ = R_NormSpace_of_BoundedMultilinearOperators(Y,Z);
reconsider f1 = f as Lipschitzian LinearOperator of X,SLYZ
by LOPBAN_1:def 9;
now
let r be Real;
assume r in PreNorms f1;
then consider x1 be VECTOR of X
such that
A62: r = ||.f1.x1.|| & ||.x1.|| <= 1;
consider g be Lipschitzian MultilinearOperator of Y,Z
such that
A63: g = f.x1
& for p be Point of product Y
holds (I.f).(p ^ <*x1*>) = g.p by A12;
A64: 0 <= ||.If1.|| & 0 <= ||.x1.|| by NORMSP_1:4;
now
let r be Real;
assume r in PreNorms g;
then consider py be VECTOR of product(Y)
such that
A65: r = ||.g.py.||
& for i be Element of dom(Y) holds ||.py.i.|| <= 1;
reconsider pz = py ^ <*x1*> as Point of product(Y^<*X*>) by Th34;
||.g.py.|| = ||.If2.pz.|| by A63;
then
A66: ||.g.py.|| <= ||.If1.|| * NrProduct(pz) by LOPBAN10:45;
A67: ||.x1.|| * NrProduct(py) = NrProduct pz by Th35;
0 <= NrProduct(py) & NrProduct(py) <=1 by A65,LOPBAN10:35;
then ||.x1.|| * NrProduct(py) <= ||.x1.|| * 1 by A64,XREAL_1:64;
then ||.If1.|| * NrProduct(pz) <= ||.If1.|| * ||.x1.||
by A64,A67,XREAL_1:64;
hence r <= ||.If1.|| * ||.x1.|| by A65,A66,XXREAL_0:2;
end;
then
A68: upper_bound(PreNorms g) <= ||.If1.|| * ||.x1.|| by SEQ_4:45;
A69: BoundedMultilinearOperatorsNorm(Y,Z).g = ||.f.x1.||
by A63,NORMSP_0:def 1;
A70: ||.f.x1.|| <= ||.If1.|| * ||.x1.|| by LOPBAN10:43,A68,A69;
||.If1.|| * ||.x1.|| <= ||.If1.|| * 1 by A62,A64,XREAL_1:64;
hence r <= ||.If1.|| by A62,A70,XXREAL_0:2;
end;
then
A71: upper_bound(PreNorms f1) <= ||.If1.|| by SEQ_4:45;
A72: BoundedLinearOperatorsNorm(X,SLYZ).f = ||.f.|| by NORMSP_0:def 1;
BoundedLinearOperatorsNorm(X,SLYZ).f1 = upper_bound(PreNorms f1)
by LOPBAN_1:30;
hence
ex If be Point of R_NormSpace_of_BoundedMultilinearOperators(Y ^ <*X*>,Z)
st If = I.f & ||.f.|| = ||.If.|| by A61,A71,A72,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;
A73: for f1,f2 be Element of LXYZ
holds I.(f1 + f2) = I.f1 + I.f2
proof
let f1,f2 be Element of LXYZ;
for z be Point of product(Y ^ <*X*>)
holds I.(f1 + f2).z = (I.f1).z + (I.f2).z
proof
let z be Point of product(Y ^ <*X*>);
consider py, px be FinSequence such that
A74: z = py ^ px & py in product CY & px in product <*CX*>
by A6,RLAFFIN3:2;
reconsider py as Point of product Y by A3,A74;
consider x1 be Point of X such that
A75: px = <*x1*> by A2,A74,Th12;
consider g1 be Lipschitzian MultilinearOperator of Y,Z
such that
A76: g1 = f1.x1
& for p be Point of product Y
holds (I.f1).(p ^ <*x1*>) = g1.p by A9;
consider g2 be Lipschitzian MultilinearOperator of Y,Z
such that
A77: g2 = f2.x1
& for ppy be Point of product Y
holds (I.f2).(ppy ^ <*x1*>) = g2.ppy by A9;
consider g12 be Lipschitzian MultilinearOperator of Y,Z
such that
A78: g12 = (f1 + f2).x1
& for p be Point of product Y
holds (I.(f1 + f2)).(p ^ <*x1*>) = g12.p by A9;
A79: (I.f2).z = g2.py by A74,A75,A77;
A80: (I.(f1 + f2)).z = g12.py by A74,A75,A78;
(f1.x1).py + (f2.x1).py
= (f1.x1 + f2.x1).py by LOPBAN10:48
.= g12.py by A78,LOPBAN_1:35;
hence (I.(f1 + f2)).z = (I.f1).z + (I.f2).z
by A74,A75,A76,A77,A79,A80;
end;
hence
I.(f1 + f2) = I.f1 + I.f2 by LOPBAN10:48;
end;
for f1 be Element of LXYZ, a be Real
holds I.(a * f1) = a * I.f1
proof
let f1 be Element of LXYZ,
a be Real;
for z be Point of product(Y^<*X*>)
holds I.(a * f1).z = a * (I.f1).z
proof
let z be Point of product(Y^<*X*>);
consider py, px be FinSequence such that
A82: z = py ^ px & py in product CY & px in product <*CX*>
by A6,RLAFFIN3:2;
reconsider py as Point of product Y by A3,A82;
consider ppx be Point of X such that
A83: px = <*ppx*> by A2,A82,Th12;
consider g1 be Lipschitzian MultilinearOperator of Y,Z
such that
A84: g1 = f1.ppx
& for p be Point of product Y
holds (I.f1).(p ^ <*ppx*>) = g1.p by A9;
consider g2 be Lipschitzian MultilinearOperator of Y,Z
such that
A85: g2 = (a * f1).ppx
& for p be Point of product Y
holds I.(a * f1).(p ^ <*ppx*>) = g2.p by A9;
A86: (I.(a * f1)).z = g2.py by A82,A83,A85;
a * (f1.ppx).py
= (a * f1.ppx).py by LOPBAN10:49
.= g2.py by A85,LOPBAN_1:36;
hence I.(a * f1).z = a * (I.f1).z by A82,A83,A84,A86;
end;
hence I.(a * f1) = a * (I.f1) by LOPBAN10:49;
end;
then reconsider I as LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,
R_NormSpace_of_BoundedMultilinearOperators(Y,Z)),
R_NormSpace_of_BoundedMultilinearOperators(Y ^ <*X*>,Z)
by A73,LOPBAN_1:def 5,VECTSP_1:def 20;
A88: for u be Point of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedMultilinearOperators(Y,Z))
holds
||.u.|| = ||.I.u.||
& for y be Point of product Y,
x be Point of X
holds (I.u).(y ^ <*x*>) = (u.x).y
proof
let u be Point of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedMultilinearOperators(Y,Z));
ex Iu be Point of R_NormSpace_of_BoundedMultilinearOperators(Y^<*X*>,Z)
st Iu = I.u & ||.u.|| = ||.Iu.|| by A9;
hence ||.u.|| = ||.I.u.||;
let y be Point of product Y;
let x be Point of X;
ex G be Lipschitzian MultilinearOperator of Y,Z
st G = u.x
& for y be Point of product Y
holds (I.u).(y ^ <*x*>) = G.y by A9;
hence (I.u).(y ^ <*x*>) = (u.x).y;
end;
A89: for If be object st If in BXYZ
holds ex f be object st f in LXYZ & If = I.f
proof
let If be object;
assume
A90: If in BXYZ;
then reconsider Iu = If
as Lipschitzian MultilinearOperator of Y ^ <*X*>,Z by LOPBAN10:def 11;
reconsider Lu = If as Point of
R_NormSpace_of_BoundedMultilinearOperators(Y ^ <*X*>, Z) by A90;
defpred P[object,object] means
ex x1 be Point of X,
g be Lipschitzian MultilinearOperator of Y,Z
st $1 = x1
& $2 = g
& for py be Point of product Y
holds Iu.(py ^ <*x1*>) = g.py;
set LYZ = the carrier of
R_NormSpace_of_BoundedMultilinearOperators(Y, Z);
A91: for v be Element of the carrier of X
holds ex w be Element of LYZ st P[v,w]
proof
let x1 be Element of the carrier of X;
defpred Q[object,object] means
ex py be Point of product Y
st $1 = py & $2 = Iu.(py ^ <*x1*>);
A92: for v be Element of the carrier of product Y
holds ex w be Element of the carrier of Z st Q[v,w]
proof
let v be Element of the carrier of product Y;
reconsider If = v ^ <*x1*> as Point of product(Y ^ <*X*>) by Th34;
Iu.If is Point of Z;
hence thesis;
end;
consider g1 be Function of the carrier of product Y,the carrier of Z
such that
A93: for py be Element of the carrier of product Y
holds Q[py, g1.py] from FUNCT_2:sch 3(A92);
for i be Element of dom(Y)
for py be Element of product(Y)
holds g1 * reproj(i,py) is LinearOperator of Y.i,Z
proof
let i be Element of dom Y;
let py be Element of product Y;
consider cy be Function such that
A94: py = cy
& dom cy = dom CY
& for i be object st i in dom CY
holds cy.i in CY.i by A3,CARD_3:def 5;
reconsider cy as FinSequence by A94;
A95: dom (Y ^ <*X*>)
= Seg(len(Y ^ <*X*>)) by FINSEQ_1:def 3
.= Seg(len Y + len <*X*>) by FINSEQ_1:22
.= Seg(len Y + 1) by FINSEQ_1:40;
i in dom Y;
then i in Seg(len Y) by FINSEQ_1:def 3;
then
A96: 1 <= i & i <= len Y by FINSEQ_1:1;
len Y <= len Y + 1 by NAT_1:11;
then i <= len Y + 1 by XXREAL_0:2,A96;
then i in Seg (len Y + 1) by A96;
then reconsider i0 = i as Element of dom(Y ^ <*X*>) by A95;
reconsider z = py ^ <*x1*> as Point of product(Y ^ <*X*>) by Th34;
A97: (Y ^ <*X*>).i0 = Y.i by FINSEQ_1:def 7;
reconsider L = g1 * reproj(i,py) as Function of Y.i,Z;
A98: dom reproj(i0,z)
= the carrier of (Y ^ <*X*>).i0 by FUNCT_2:def 1
.= the carrier of Y.i by FINSEQ_1:def 7;
dom Iu = the carrier of product(Y ^ <*X*>) by FUNCT_2:def 1;
then rng reproj(i0,z) c= dom Iu;
then
A99: dom(Iu * reproj(i0,z)) = the carrier of Y.i by A98,RELAT_1:27;
for t be object st t in dom(Iu * reproj(i0,z))
holds (Iu * reproj(i0,z)).t = (g1 * reproj(i,py)).t
proof
let t be object;
assume
A100: t in dom(Iu * reproj(i0,z));
then
reconsider t1 = t as Point of (Y ^ <*X*>).i0;
reconsider t2 = t as Point of Y.i by A100,FINSEQ_1:def 7;
A101: Q[reproj(i,py).t2, g1.(reproj(i,py).t2)] by A93;
thus (Iu * reproj(i0,z)).t
= Iu.(reproj(i0,z).t1) by FUNCT_2:15
.= g1.(reproj(i,py).t2) by A101,Th32
.= (g1* reproj(i,py)).t by FUNCT_2:15;
end;
then
Iu * reproj(i0,z) = g1 * reproj(i,py) by A97,A99;
hence g1 * reproj(i,py) is LinearOperator of Y.i,Z
by A97,LOPBAN10:def 6;
end;
then
reconsider g1 as MultilinearOperator of Y,Z by LOPBAN10:def 6;
set K = ||.x1.|| * ||.Lu.||;
A102: 0 <= ||.Lu.||
& 0 <= ||.x1.|| by NORMSP_1:4;
for py be Point of product Y
holds ||.g1.py.|| <= K * NrProduct(py)
proof
let py be Element of product(Y);
consider cy be Function such that
A103: py = cy & dom cy = dom CY
& for i be object st i in dom CY
holds cy.i in CY.i by A3,CARD_3:def 5;
reconsider cy as FinSequence by A103;
reconsider z = py ^ <*x1*> as Point of product(Y ^ <*X*>) by Th34;
A104: Q[py, g1.py] by A93;
A105: ||.Iu.z.|| <= ||.Lu.|| * NrProduct(z) by LOPBAN10:45;
||.x1.|| * NrProduct(py) = NrProduct(z) by Th35;
hence ||.g1.py.|| <= K * NrProduct(py) by A104,A105;
end;
then
reconsider g1 as Lipschitzian MultilinearOperator of Y,Z
by A102,LOPBAN10:def 10,XREAL_1:127;
reconsider g2 = g1 as Element of LYZ by LOPBAN10:def 11;
take g2;
for py be Point of product Y
holds Iu.(py ^ <*x1*>) = g1.py
proof
let py be Point of product Y;
Q[py, g1.py] by A93;
hence Iu.(py ^ <*x1*>) = g1.py;
end;
hence thesis;
end;
consider f0 be Function of the carrier of X,LYZ
such that
A106: for x be Element of the carrier of X
holds P[x,f0.x] from FUNCT_2:sch 3(A91);
A107: for x0 be Point of X
holds
for y0 be Point of product Y
holds Iu.(y0 ^ <*x0*>) = (f0.x0).y0
proof
let x0 be Point of X;
ex x1 be Point of X,
g be Lipschitzian MultilinearOperator of Y,Z
st x1 = x0 & f0.x0 = g
& for py be Point of product Y
holds Iu.(py ^ <*x1*>) = g.py by A106;
hence
for py be Point of product Y
holds Iu.(py ^ <*x0*>) = (f0.x0).py;
end;
for x1,x2 be Point of X
holds f0.(x1 + x2) = f0.x1 + f0.x2
proof
let x1,x2 be Point of X;
for py be Point of product Y holds
(f0.(x1 + x2)).py = (f0.x1).py + (f0.x2).py
proof
let py be Point of product Y;
consider cy be Function such that
A108: py = cy & dom cy = dom CY
& for i be object st i in dom CY
holds cy.i in CY.i by A3,CARD_3:def 5;
A109: dom cy = Seg len CY by A108,FINSEQ_1:def 3;
reconsider cy as FinSequence by A108;
A110: len py
= len CY by A108,A109,FINSEQ_1:def 3
.= len Y by PRVECT_1:def 11;
A111: Iu.(py ^ <*x1*>) = (f0.x1).py by A107;
A112: Iu.(py ^ <*x2*>) = (f0.x2).py by A107;
A113: Iu.(py ^ <*x1 + x2*>) = (f0.(x1 + x2)).py by A107;
A114: len (Y ^ <*X*>)
= len Y + len <*X*> by FINSEQ_1:22
.= len Y + 1 by FINSEQ_1:40;
reconsider z1 = py ^ <*x1*> as Point of product(Y ^ <*X*>) by Th34;
reconsider z2 = py ^ <*x2*> as Point of product(Y ^ <*X*>) by Th34;
reconsider z12 = py ^ <*x1 + x2*> as Point of product(Y ^ <*X*>)
by Th34;
len Y + 1 in Seg(len Y + 1) by FINSEQ_1:4;
then reconsider j = len py + 1 as Element of dom(Y ^ <*X*>)
by A110,A114,FINSEQ_1:def 3;
A115: (Y ^ <*X*>).j = X by A110,FINSEQ_1:42;
A116: Iu.(py ^ <*x1*>)
= Iu.(reproj(j,z1).x1) by Th33
.= (Iu*reproj(j,z1)).x1 by A115,FUNCT_2:15;
A117: Iu.(py ^ <*x2*>)
= Iu.(reproj(j,z1).x2) by Th33
.= (Iu * reproj(j,z1)).x2 by A115,FUNCT_2:15;
A118: Iu.(py ^ <*x1 + x2*>)
= Iu.(reproj(j,z1).(x1 + x2)) by Th33
.= (Iu*reproj(j,z1)).(x1 + x2) by A115,FUNCT_2:15;
reconsider L = Iu * reproj(j,z1)
as LinearOperator of X,Z by A115,LOPBAN10:def 6;
L is additive;
hence (f0.(x1 + x2)).py = (f0.x1).py + (f0.x2).py
by A116,A117,A118,A111,A112,A113;
end;
hence f0.(x1 + x2) = f0.x1 + f0.x2 by LOPBAN10:48;
end;
then
A119: f0 is additive;
for x1 be Point of X,a be Real
holds f0.(a * x1) = a * f0.x1
proof
let x1 be Point of X, a be Real;
for py be Point of product Y
holds (f0.(a * x1)).py = a * (f0.x1).py
proof
let py be Point of product Y;
consider cy be Function such that
A120: py = cy & dom cy = dom CY
& for i be object st i in dom CY
holds cy.i in CY.i by A3, CARD_3:def 5;
A121: dom cy = Seg len CY by A120,FINSEQ_1:def 3;
reconsider cy as FinSequence by A120;
A122: len py
= len CY by A120,A121,FINSEQ_1:def 3
.= len Y by PRVECT_1:def 11;
A123: Iu.(py ^ <*a*x1*>) = (f0.(a * x1)).py by A107;
A124: len(Y ^ <*X*>)
= len Y + len <*X*> by FINSEQ_1:22
.= len Y + 1 by FINSEQ_1:40;
reconsider z1 = py ^ <*x1*> as Point of product(Y ^ <*X*>) by Th34;
reconsider z2 = py ^ <*a*x1*> as Point of product(Y ^ <*X*>) by Th34;
len Y + 1 in Seg(len Y + 1) by FINSEQ_1:4;
then reconsider j = len py + 1 as Element of dom(Y ^ <*X*>)
by A122,A124,FINSEQ_1:def 3;
A125: (Y ^ <*X*>).j = X by A122,FINSEQ_1:42;
A126: Iu.(py ^ <*x1*>)
= Iu.(reproj(j,z1).x1) by Th33
.= (Iu * reproj(j,z1)).x1 by A125,FUNCT_2:15;
A127: Iu.(py ^ <*a*x1*>)
= Iu.(reproj(j,z1).(a*x1)) by Th33
.= (Iu * reproj(j,z1)).(a*x1) by A125,FUNCT_2:15;
reconsider L = Iu * (reproj(j,z1))
as LinearOperator of X,Z by A125,LOPBAN10:def 6;
L.(a * x1) = a * L.x1 by LOPBAN_1:def 5;
hence (f0.(a * x1)).py = a * (f0.x1).py by A107,A123,A126,A127;
end;
hence f0.(a * x1) = a * f0.x1 by LOPBAN10:49;
end;
then
reconsider f0 as LinearOperator of
X,R_NormSpace_of_BoundedMultilinearOperators(Y,Z)
by A119,LOPBAN_1:def 5;
consider K be Real such that
A128: 0 <= K
& for z1 be Point of product(Y ^ <*X*>)
holds ||.Iu.z1.|| <= K * NrProduct(z1)
by LOPBAN10:def 10;
for x1 be Point of X
holds ||.f0.x1.|| <= K * ||.x1.||
proof
let x1 be Point of X;
reconsider fx1 = f0.x1 as Lipschitzian MultilinearOperator of Y,Z
by LOPBAN10:def 11;
reconsider fx2 = f0.x1 as Point of
R_NormSpace_of_BoundedMultilinearOperators(Y,Z);
0 <= ||.x1.|| by NORMSP_1:4;
then
A129: 0 <= K * ||.x1.|| by XREAL_1:127,A128;
A130: for px be Point of product Y
holds ||.fx1.px.|| <= (K * ||.x1.||) * NrProduct(px)
proof
let py be Point of product Y;
consider cy be Function such that
A131: py = cy & dom cy = dom CY
& for i be object st i in dom CY
holds cy.i in CY.i by A3,CARD_3:def 5;
reconsider cy as FinSequence by A131;
reconsider z1 = py ^ <*x1*> as Point of product(Y ^ <*X*>) by Th34;
A132: ||.Iu.z1.|| <= K * NrProduct(z1) by A128;
||.x1.|| * NrProduct(py) = NrProduct(z1) by Th35;
hence ||. fx1.py .|| <= (K * ||.x1.||) * NrProduct(py) by A107,A132;
end;
now
let r be Real;
assume r in PreNorms(fx1);
then consider py be VECTOR of product(Y) such that
A133: r = ||.fx1.py.||
& for i be Element of dom Y holds ||.py.i.|| <= 1;
0 <= NrProduct(py) & NrProduct(py) <= 1 by A133,LOPBAN10:35;
then
A134: (K * ||.x1.||) * NrProduct(py) <= (K * ||.x1.||) * 1
by A129,XREAL_1:64;
||.fx1.py.|| <= (K * ||.x1.||) * NrProduct(py) by A130;
hence r <= K * ||.x1.|| by A133,A134,XXREAL_0:2;
end;
then
A135: upper_bound(PreNorms fx1) <= K * ||.x1.|| by SEQ_4:45;
BoundedMultilinearOperatorsNorm(Y,Z).fx1 = ||.f0.x1.||
by NORMSP_0:def 1;
hence ||.f0.x1.|| <= K * ||.x1.|| by A135,LOPBAN10:43;
end;
then
reconsider f0 as Lipschitzian LinearOperator of X,
R_NormSpace_of_BoundedMultilinearOperators(Y,Z)
by A128,LOPBAN_1:def 8;
take f0;
thus
f0 in LXYZ by LOPBAN_1:def 9;
reconsider f = f0 as Element of LXYZ by LOPBAN_1:def 9;
reconsider L = I.f as Lipschitzian MultilinearOperator of Y ^ <*X*>,Z
by LOPBAN10:def 11;
for z be Element of product(Y ^ <*X*>)
holds L.z = Iu.z
proof
let z be Point of product(Y ^ <*X*>);
consider py, px be FinSequence such that
A136: z = py ^ px
& py in product CY
& px in product <*CX*> by A6,RLAFFIN3:2;
reconsider py as Point of product Y by A3,A136;
consider x1 be Point of X such that
A137:px = <*x1*> by A2,A136,Th12;
consider x2 be Point of X,
g1 be Lipschitzian MultilinearOperator of Y,Z
such that
A138: x1 = x2
& f0.x1 = g1
& for py be Point of product Y
holds Iu.(py ^ <*x2*>) = g1.py by A106;
A139: Iu.z = g1.py by A136,A137,A138;
consider g be Lipschitzian MultilinearOperator of Y,Z
such that
A140: g = f.x1
& for py be Point of product Y
holds (I.f).(py ^ <*x1*>) = g.py by A9;
thus thesis by A136,A137,A138,A139,A140;
end;
then L = Iu;
hence If = I.f0;
end;
for u be Point of R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedMultilinearOperators(Y,Z))
holds ||. I.u .|| <= 1 * ||.u.|| by A88;
then
reconsider I as Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators
(X,R_NormSpace_of_BoundedMultilinearOperators(Y,Z)),
R_NormSpace_of_BoundedMultilinearOperators(Y ^ <*X*>,Z)
by LOPBAN_1:def 8;
take I;
thus I is one-to-one onto by A1,A89,FUNCT_1:52,FUNCT_2:10;
thus thesis by A88,NDIFF_7:7;
end;
definition
let Y be RealNormSpace,
X be RealNormSpace-Sequence;
func NestingLB(X,Y) -> RealNormSpace means
:Def3:
ex f be Function
st dom f = NAT
& it = f.(len X)
& f.0 = Y
& for i be Nat st i < len X
holds
ex fi be RealNormSpace,
j be Element of dom X
st fi = f.i
& i + 1 = j
& f.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j, fi);
existence
proof
defpred S1[set] means
for X be RealNormSpace-Sequence
st len X = $1
holds
ex fn be RealNormSpace,
f be Function
st dom f = NAT
& fn = f.(len X)
& f.0 = Y
& for i be Nat st i < len X
ex fi be RealNormSpace,
j be Element of dom X
st fi = f.i
& i + 1 = j
& f.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi);
A1: for n be Nat st S1[n] holds S1[n + 1]
proof
let n be Nat;
assume
A2: for X be RealNormSpace-Sequence st len X = n
holds
ex fn be RealNormSpace, f be Function
st dom f = NAT
& fn = f.(len X)
& f.0 = Y
& for i be Nat st i < len X
holds
ex fi be RealNormSpace,
j be Element of dom X
st fi = f.i
& i + 1 = j
& f.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi);
let X be RealNormSpace-Sequence;
assume
A3: len X = n + 1;
then
A4: dom X = Seg(n + 1) by FINSEQ_1:def 3;
then
A5: n + 1 in dom X by FINSEQ_1:4;
reconsider n1 = n + 1 as Element of dom X by A4,FINSEQ_1:4;
per cases;
suppose
A6: n = 0;
then
reconsider d1 = 1 as Element of dom X by A4,FINSEQ_1:4;
reconsider f0 = NAT --> Y as Function;
set f = f0 +* (1,R_NormSpace_of_BoundedLinearOperators(X.d1,Y));
A7: dom f
= dom f0 by FUNCT_7:30
.= NAT;
A8: f.0
= f0.0 by FUNCT_7:32
.= Y;
A9: 1 in dom f0;
then
reconsider fn = f.1 as RealNormSpace by FUNCT_7:31;
take fn = R_NormSpace_of_BoundedLinearOperators(X.d1,Y);
take f;
thus dom f = NAT by A7;
thus fn = f.(len X) by A3,A6,A9,FUNCT_7:31;
thus f.0 = Y by A8;
let i be Nat;
assume
A10: i < len X;
then
A11: i = 0 by A3,A6,NAT_1:14;
take fi = Y;
1 <= i + 1 & i + 1 <= len X by A10,NAT_1:11,NAT_1:13;
then i + 1 in Seg len X;
then reconsider j = i + 1 as Element of dom X by FINSEQ_1:def 3;
take j;
thus fi = f.i by A3,A6,A10,NAT_1:14,A8;
thus i + 1 = j;
thus f.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi)
by A9,A11,FUNCT_7:31;
end;
suppose
A12: 0 <> n;
set XN = X | n;
A13: n < n + 1 by NAT_1:13;
for x be set st x in rng XN holds x is RealNormSpace
proof
let x be set;
assume x in rng XN;
then x in rng X by RELAT_1:70,TARSKI:def 3;
hence x is RealNormSpace by PRVECT_2:def 10;
end;
then
reconsider XN as RealNormSpace-Sequence by A12,PRVECT_2:def 10;
consider fn be RealNormSpace,
f be Function
such that
A14: dom f = NAT
& fn = f.(len XN)
& f.0 = Y
and
A15: for i be Nat st i < len XN
holds
ex fi be RealNormSpace, j be Element of dom XN
st fi = f.i
& i + 1 = j
& f.(i + 1) = R_NormSpace_of_BoundedLinearOperators(XN.j,fi)
by A2,A3,A13,FINSEQ_1:59;
defpred S2[object, object] means
for i be Nat st $1 = i
holds
(i < n + 1 implies $2 = f.$1)
& (n + 1 <= i implies
ex xn1,fn be RealNormSpace
st xn1 = X.(n + 1)
& fn = f.(len XN)
& $2 = R_NormSpace_of_BoundedLinearOperators(xn1,fn));
A16: for x, y1, y2 be object
st x in NAT & S2[x,y1] & S2[x,y2]
holds y1 = y2
proof
let x, y1, y2 be object;
assume
A17: x in NAT & S2[x,y1] & S2[x,y2];
reconsider i = x as Nat by A17;
per cases;
suppose
A18: i < n + 1;
hence y1
= f.x by A17
.= y2 by A17,A18;
end;
suppose
A19: n + 1 <= i;
then
A20: ex xn1,fn be RealNormSpace
st xn1 = X.(n + 1)
& fn = f.(len XN)
& y1 = R_NormSpace_of_BoundedLinearOperators(xn1,fn) by A17;
ex xn1,fn be RealNormSpace
st xn1 = X.(n + 1)
& fn = f.(len XN)
& y2 = R_NormSpace_of_BoundedLinearOperators(xn1,fn) by A17,A19;
hence y1 = y2 by A20;
end;
end;
A21: for x be object st x in NAT
holds ex y be object st S2[x,y]
proof
let x be object;
assume x in NAT;
then reconsider x0 = x as Nat;
per cases;
suppose
A22: x0 < n + 1;
take y2 = f.x;
let i be Nat;
assume
A23: x = i;
thus i < n + 1 implies y2 = f.x;
thus n + 1 <= i implies
ex xn1,fn be RealNormSpace
st xn1 = X.(n + 1)
& fn = f.(len XN)
& y2 = R_NormSpace_of_BoundedLinearOperators(xn1,fn) by A22,A23;
end;
suppose
A24: n + 1 <= x0;
X.(n + 1) in rng X by A5,FUNCT_1:def 3;
then reconsider xn1 = X.(n + 1)
as RealNormSpace by PRVECT_2:def 10;
take
y2 = R_NormSpace_of_BoundedLinearOperators(xn1,fn);
let i be Nat;
assume x = i;
hence i < n + 1 implies y2 = f.x by A24;
thus n + 1 <= i implies
ex xn1,fn be RealNormSpace
st xn1 = X.(n + 1)
& fn = f.(len XN)
& y2 = R_NormSpace_of_BoundedLinearOperators(xn1,fn) by A14;
end;
end;
consider f1 be Function such that
A26: dom f1 = NAT
and
A27: for j be object st j in NAT holds S2[j,f1.j]
from FUNCT_1:sch 2(A16,A21);
A28: for j be Nat holds S2[j,f1.j]
proof
let j be Nat;
j in NAT by ORDINAL1:def 12;
hence S2[j,f1.j] by A27;
end;
set z = f1.(n + 1);
ex xn1,fn be RealNormSpace
st xn1 = X.(n + 1)
& fn = f.(len XN)
& f1.(n + 1) = R_NormSpace_of_BoundedLinearOperators(xn1,fn) by A28;
then
reconsider z as RealNormSpace;
take z;
take f2 = f1;
thus dom f2 = NAT by A26;
thus z = f2.(len X) by A3;
0 <= n by NAT_1:2;
then 0 + 0 < n + 1 by XREAL_1:8;
hence f2.0 = Y by A14,A28;
let i be Nat;
assume
A29: i < len X;
then
A30: i + 1 <= len X by NAT_1:13;
1 <= i + 1 by NAT_1:11;
then
A31: i + 1 in Seg len X by A30;
A32: len XN = n by A3,A13,FINSEQ_1:17;
A33:
now
assume
A34: i = n;
reconsider j = i + 1 as Element of dom X by A31,FINSEQ_1:def 3;
A35: ex xn1,fn be RealNormSpace
st xn1 = X.(n + 1)
& fn = f.(len XN)
& f2.j = R_NormSpace_of_BoundedLinearOperators(xn1,fn)
by A28,A34;
i < n + 1 by A34,NAT_1:13;
then f2.i = f.(len XN) by A28,A32,A34;
hence
ex fi be RealNormSpace,
j be Element of dom X
st fi = f2.i
& i + 1 = j
& f2.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi)
by A34,A35;
end;
A36:
now
assume
A37: i < n;
then
A38: i + 1 < n + 1 by XREAL_1:6;
i < len XN by A3,A13,A37,FINSEQ_1:17;
then
consider fi be RealNormSpace,
j be Element of dom XN
such that
A39: fi = f.i
& i + 1 = j
& f.(i + 1) = R_NormSpace_of_BoundedLinearOperators(XN.j,fi)
by A15;
i < n + 1 by A37, NAT_1:13;
then
A40: f2.i = f.i by A28;
reconsider j0 = j as Element of dom X by RELAT_1:60,TARSKI:def 3;
A41: X.j0 = XN.j by FUNCT_1:47;
f2.(i+1) = f.(i+1) by A28,A38;
hence
ex fi be RealNormSpace, j0 be Element of dom X
st fi = f2.i
& i + 1 = j0
& f2.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j0,fi)
by A39,A40,A41;
end;
i <= n by A3,A29,NAT_1:13;
hence
ex fi be RealNormSpace, j be Element of dom X
st fi = f2.i
& i + 1 = j
& f2.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi)
by XXREAL_0:1,A33,A36;
end;
end;
A42: S1[0]
proof
reconsider f = NAT --> Y as Function;
let X be RealNormSpace-Sequence;
assume
A43: len X = 0;
reconsider fn = f.(len X) as RealNormSpace;
take fn;
take f;
thus dom f = NAT;
thus fn = f.(len X) & f.0 = Y;
let i be Nat;
assume i < len X;
hence
ex fi be RealNormSpace,
j be Element of dom X
st fi = f.i
& i + 1 = j
& f.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi)
by A43,NAT_1:2;
end;
for n be Nat holds S1[n] from NAT_1:sch 2(A42, A1);
hence
ex fn be RealNormSpace,
f be Function
st dom f = NAT
& fn = f.(len X)
& f.0 = Y
& for i be Nat st i < len X
ex fi be RealNormSpace,
j be Element of dom X
st fi = f.i
& i + 1 = j
& f.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi);
end;
uniqueness
proof
let v1,v2 be RealNormSpace;
given f1 be Function such that
A44: dom f1 = NAT & v1 = f1.(len X) and
A45: f1.0 = Y and
A46: for i be Nat st i < len X
ex fi be RealNormSpace,
j be Element of dom X
st fi = f1.i
& i + 1 = j
& f1.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi);
given f2 be Function such that
A47: dom f2 = NAT & v2 = f2.(len X) and
A48: f2.0 = Y and
A49: for i be Nat st i < len X
ex fi be RealNormSpace,
j be Element of dom X
st fi = f2.i
& i + 1 = j
& f2.(i + 1) = R_NormSpace_of_BoundedLinearOperators(X.j,fi);
defpred S1[Nat] means
$1 <= len X implies f1.$1 = f2.$1;
now
let j be Nat;
assume A50: j <= len X implies f1.j = f2.j;
assume A51: j + 1 <= len X;
A52: ex fi be RealNormSpace,
j1 be Element of dom X
st fi = f1.j
& j + 1 = j1
& f1.(j + 1) = R_NormSpace_of_BoundedLinearOperators(X.j1,fi)
by A46,A51,NAT_1:13;
ex fi be RealNormSpace,
j1 be Element of dom X
st fi = f2.j
& j + 1 = j1
& f2.(j + 1) = R_NormSpace_of_BoundedLinearOperators(X.j1,fi)
by A49,A51,NAT_1:13;
hence f1.(j + 1) = f2.(j + 1) by A50,A51,A52,NAT_1:13;
end;
then
A53: for j be Nat st S1[j] holds S1[j + 1];
A54: S1[0] by A45,A48;
for j be Nat holds S1[j] from NAT_1:sch 2(A54, A53);
hence v1 = v2 by A44, A47;
end;
end;
theorem Th37:
for X,Y,Z be RealNormSpace,
I be Lipschitzian LinearOperator of Y,Z
st I is one-to-one onto isometric
holds
ex L be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(X,Z)
st L is one-to-one onto isometric
& for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds L.f = I * f
proof
let X,Y,Z be RealNormSpace,
I be Lipschitzian LinearOperator of Y,Z;
assume
A1: I is one-to-one onto isometric;
then
consider J be LinearOperator of Z,Y
such that
A2: J = I" and
J is one-to-one onto and
A3: J is isometric by NDIFF_7:9;
reconsider J as Lipschitzian LinearOperator of Z,Y by A3;
set F = the carrier of R_NormSpace_of_BoundedLinearOperators(X,Y);
set G = the carrier of R_NormSpace_of_BoundedLinearOperators(X,Z);
defpred P1[Function,Function] means $2 = I * $1;
A4: for f be Element of F
ex g be Element of G st P1[f,g]
proof
let f be Element of F;
reconsider f as Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
I * f is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2;
then reconsider g = I * f as Element of G by LOPBAN_1:def 9;
take g;
thus thesis;
end;
consider L be Function of F,G such that
A5: for f be Element of F holds P1[f, L.f] from FUNCT_2:sch 3(A4);
A6: for f1, f2 be object
st f1 in F & f2 in F & L.f1 = L.f2
holds f1 = f2
proof
let f1, f2 be object;
assume
A7: f1 in F & f2 in F & L.f1 = L.f2; then
reconsider u1 = f1, u2 = f2 as Point of
R_NormSpace_of_BoundedLinearOperators(X,Y);
reconsider v1 = u1, v2 = u2 as Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
L.v1 = I * v1 by A5;
then I * v1 = I * v2 by A5,A7;
then J * (I * v1) = (J * I) * v2 by RELAT_1:36;
then
A8: J * I * v1 = J * I * v2 by RELAT_1:36;
A9: J * I = id the carrier of Y by A1,A2,FUNCT_2:29;
then J * I * v1 = v1 by FUNCT_2:17;
hence thesis by A8,A9,FUNCT_2:17;
end;
A10: for g be object st g in G holds
ex f be object st f in F & g = L.f
proof
let g be object;
assume g in G;
then reconsider g1 = g as Point of
R_NormSpace_of_BoundedLinearOperators(X,Z);
reconsider g2 = g1 as Lipschitzian LinearOperator of X,Z
by LOPBAN_1:def 9;
reconsider f1 = J * g2 as Lipschitzian LinearOperator of X,Y
by LOPBAN_2:2;
reconsider f = f1 as Point of
R_NormSpace_of_BoundedLinearOperators(X,Y)
by LOPBAN_1:def 9;
take f;
thus f in F;
A11: I * J = id the carrier of Z by A1,A2,FUNCT_2:29;
thus L.f
= I * (J * g2) by A5
.= (I * J) * g2 by RELAT_1:36
.= g by A11,FUNCT_2:17;
end;
A12: for f1,f2 be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds L.(f1 + f2) = L.f1 + L.f2
proof
let f1,f2 be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
reconsider ff1 = f1, ff2 = f2, f12 = f1 + f2
as Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
A13: L.f1 = I * f1 by A5;
A14: L.f2 = I * f2 by A5;
A15: L.(f1 + f2) = I * (f1 + f2) by A5;
set g1 = L.f1, g2 = L.f2, g12 = L.(f1 + f2);
for x be VECTOR of X holds g12.x = g1.x + g2.x
proof
let x be VECTOR of X;
A16: g1.x = I.(ff1.x) by A13,FUNCT_2:15;
A17: g2.x = I.(ff2.x) by A14,FUNCT_2:15;
g12.x = I.(f12.x) by A15,FUNCT_2:15
.= I.(ff1.x + ff2.x) by LOPBAN_1:35;
hence g12.x = g1.x + g2.x by A16,A17,VECTSP_1:def 20;
end;
hence thesis by LOPBAN_1:35;
end;
for f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
a be Real
holds L.(a * f) = a * L.f
proof
let f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
a be Real;
reconsider f1 = f, af = a * f as Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
A18: L.f = I * f by A5;
A19: L.(a * f) = I * (a * f) by A5;
set g = L.f, ag = L.(a * f);
for t be VECTOR of X holds ag.t = a * g.t
proof
let t be VECTOR of X;
A20: g.t = I.(f1.t) by A18,FUNCT_2:15;
ag.t = I.(af.t) by A19,FUNCT_2:15
.= I.(a * f.t) by LOPBAN_1:36;
hence ag.t = a * g.t by A20,LOPBAN_1:def 5;
end;
hence thesis by LOPBAN_1:36;
end;
then reconsider L as LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(X,Z)
by A12,LOPBAN_1:def 5,VECTSP_1:def 20;
A21: for f be Element of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds ||.L.f.|| = ||.f.||
proof
let f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
reconsider f1 = f as Lipschitzian LinearOperator of X,Y
by LOPBAN_1:def 9;
reconsider g = L.f as Lipschitzian LinearOperator of X,Z
by LOPBAN_1:def 9;
A22: ||.f.||
= BoundedLinearOperatorsNorm(X,Y).f by NORMSP_0:def 1
.= upper_bound PreNorms(f1) by LOPBAN_1:30;
A23: ||.L.f.||
= BoundedLinearOperatorsNorm(X,Z).g by NORMSP_0:def 1
.= upper_bound PreNorms(g) by LOPBAN_1:30;
for z be object holds z in PreNorms(f1) iff z in PreNorms(g)
proof
let z be object;
hereby
assume z in PreNorms(f1);
then consider x be VECTOR of X such that
A24: z = ||.f1.x.|| & ||.x.|| <= 1;
g = I * f by A5;
then
||.g.x.||
= ||.I.(f1.x).|| by FUNCT_2:15
.= ||.f1.x.|| by A1,NDIFF_7:7;
hence z in PreNorms(g) by A24;
end;
assume z in PreNorms(g);
then consider x be VECTOR of X such that
A25: z = ||.g.x.|| & ||.x.|| <= 1;
||.g.x.||
= ||.(I * f1).x.|| by A5
.= ||.I.(f1.x).|| by FUNCT_2:15
.= ||.f1.x.|| by NDIFF_7:7,A1;
hence z in PreNorms(f1) by A25;
end;
hence thesis by A22,A23,TARSKI:2;
end;
then L is isometric by NDIFF_7:7;
then reconsider L as Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(X,Z);
take L;
thus thesis by A5,A10,A21,NDIFF_7:7,A6,FUNCT_2:10,FUNCT_2:19;
end;
theorem Th38:
for X,Y,Z be RealNormSpace,
I be Lipschitzian LinearOperator of Y,Z
st I is one-to-one onto isometric
holds
ex L be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(Y,X),
R_NormSpace_of_BoundedLinearOperators(Z,X)
st L is one-to-one onto isometric
& for f be Point of R_NormSpace_of_BoundedLinearOperators(Y,X)
holds L.f = f * I"
proof
let X,Y,Z be RealNormSpace,
I be Lipschitzian LinearOperator of Y,Z;
assume
A1: I is one-to-one onto isometric;
then
consider J be LinearOperator of Z,Y such that
A2: J = I" and
J is one-to-one onto and
A3: J is isometric by NDIFF_7:9;
reconsider J as Lipschitzian LinearOperator of Z,Y by A3;
set F = the carrier of R_NormSpace_of_BoundedLinearOperators(Y,X);
set G = the carrier of R_NormSpace_of_BoundedLinearOperators(Z,X);
defpred P1[Function,Function] means $2 = $1 * J;
A4: for f be Element of F
ex g be Element of G st P1[f,g]
proof
let f be Element of F;
reconsider f1 = f as Lipschitzian LinearOperator of Y,X
by LOPBAN_1:def 9;
f1 * J is Lipschitzian LinearOperator of Z,X by LOPBAN_2:2;
then reconsider g = f1 * J as Element of G by LOPBAN_1:def 9;
take g;
thus thesis;
end;
consider L be Function of F,G such that
A5: for f be Element of F holds P1[f,L.f] from FUNCT_2:sch 3(A4);
A6: for f1, f2 be object
st f1 in F & f2 in F & L.f1 = L.f2
holds f1 = f2
proof
let f1, f2 be object;
assume
A7: f1 in F & f2 in F & L.f1 = L.f2;
then
reconsider u1 = f1, u2 = f2 as Point of
R_NormSpace_of_BoundedLinearOperators(Y,X);
reconsider v1 = u1, v2 = u2 as
Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 9;
L.v1 = v1 * J by A5;
then v1 * J = v2 * J by A5,A7;
then (v1 * J) * I = v2 * (J * I) by RELAT_1:36;
then
A8: v1 * (J * I) = v2 * (J * I) by RELAT_1:36;
A9: J * I = id the carrier of Y by A1,A2,FUNCT_2:29;
then v1 * (J * I) = v1 by FUNCT_2:17;
hence thesis by A8,A9,FUNCT_2:17;
end;
A10: for g be object st g in G holds
ex f be object st f in F & g = L.f
proof
let g be object;
assume g in G; then
reconsider g1 = g as Point of
R_NormSpace_of_BoundedLinearOperators(Z,X);
reconsider g2 = g1 as Lipschitzian LinearOperator of Z,X
by LOPBAN_1:def 9;
reconsider f1 = g2 * I
as Lipschitzian LinearOperator of Y,X by LOPBAN_2:2;
reconsider f = f1 as Point of
R_NormSpace_of_BoundedLinearOperators(Y,X)
by LOPBAN_1:def 9;
take f;
thus f in F;
A11: I * J = id the carrier of Z by A1,A2,FUNCT_2:29;
thus L.f
= (g2 * I) * J by A5
.= g2 * (I * J) by RELAT_1:36
.= g by A11,FUNCT_2:17;
end;
A12: for f1,f2 be Point of R_NormSpace_of_BoundedLinearOperators(Y,X)
holds L.(f1 + f2) = L.f1 + L.f2
proof
let f1,f2 be Point of R_NormSpace_of_BoundedLinearOperators(Y,X);
reconsider u1 = f1, u2 = f2, u12 = f1 + f2
as Lipschitzian LinearOperator of Y,X
by LOPBAN_1:def 9;
A13: L.f1 = f1 * J by A5;
A14: L.f2 = f2 * J by A5;
A15: L.(f1 + f2) = (f1 + f2) * J by A5;
set g1 = L.f1, g2 = L.f2, g12 = L.(f1 + f2);
for z be VECTOR of Z holds g12.z = g1.z + g2.z
proof
let z be VECTOR of Z;
A16: g2.z = u2.(J.z) by A14,FUNCT_2:15;
g12.z = u12.(J.z) by A15,FUNCT_2:15
.= u1.(J.z) + u2.(J.z) by LOPBAN_1:35;
hence g12.z = g1.z + g2.z by A13,FUNCT_2:15,A16;
end;
hence thesis by LOPBAN_1:35;
end;
for f be Point of R_NormSpace_of_BoundedLinearOperators(Y,X),
a be Real
holds L.(a * f) = a * L.f
proof
let f be Point of R_NormSpace_of_BoundedLinearOperators(Y,X),
a be Real;
reconsider f1 = f, af = a * f
as Lipschitzian LinearOperator of Y,X
by LOPBAN_1:def 9;
A17: L.f = f * J by A5;
A18: L.(a * f) = (a * f) * J by A5;
set g = L.f, ag = L.(a * f);
for t be VECTOR of Z holds ag.t = a * g.t
proof
let t be VECTOR of Z;
ag.t = af.(J.t) by A18,FUNCT_2:15
.= a * f1.(J.t) by LOPBAN_1:36;
hence ag.t = a * g.t by A17,FUNCT_2:15;
end;
hence thesis by LOPBAN_1:36;
end; then
reconsider L as LinearOperator of
R_NormSpace_of_BoundedLinearOperators(Y,X),
R_NormSpace_of_BoundedLinearOperators(Z,X)
by A12,LOPBAN_1:def 5,VECTSP_1:def 20;
A19: for f be Element of R_NormSpace_of_BoundedLinearOperators(Y,X)
holds ||.L.f.|| = ||.f.||
proof
let f be Point of R_NormSpace_of_BoundedLinearOperators(Y,X);
reconsider f1 = f as Lipschitzian LinearOperator of Y,X
by LOPBAN_1:def 9;
reconsider g = L.f as Lipschitzian LinearOperator of Z,X
by LOPBAN_1:def 9;
A20: ||.f.||
= BoundedLinearOperatorsNorm(Y,X).f by NORMSP_0:def 1
.= upper_bound PreNorms(f1) by LOPBAN_1:30;
A21: ||.L.f.||
= BoundedLinearOperatorsNorm(Z,X).g by NORMSP_0:def 1
.= upper_bound PreNorms(g) by LOPBAN_1:30;
for n be object holds n in PreNorms(f1) iff n in PreNorms(g)
proof
let n be object;
hereby
assume n in PreNorms(f1);
then
consider y be VECTOR of Y such that
A22: n = ||.f1.y.|| & ||.y.|| <= 1;
g = f * J by A5;
then
A23: ||.g.(I.y).||
= ||.f1.(J.(I.y)).|| by FUNCT_2:15
.= ||.f1.y.|| by A1,A2,FUNCT_2:26;
||.I.y.|| = ||.y.|| by A1,NDIFF_7:7;
hence n in PreNorms(g) by A23,A22;
end;
assume n in PreNorms(g);
then
consider z be VECTOR of Z such that
A24: n = ||.g.z.|| & ||.z.|| <= 1;
A25: ||.g.z.||
= ||.(f1 * J).z.|| by A5
.= ||.f1.(J.z).|| by FUNCT_2:15;
||.J.z.||= ||.z.|| by A3,NDIFF_7:7;
hence n in PreNorms(f1) by A24,A25;
end;
hence thesis by A20,A21,TARSKI:2;
end;
then L is isometric by NDIFF_7:7;
then reconsider L as Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(Y,X),
R_NormSpace_of_BoundedLinearOperators(Z,X);
take L;
thus thesis by A2,A5,A6,A10,A19,NDIFF_7:7,FUNCT_2:10,FUNCT_2:19;
end;
theorem Th39:
for X,Y be RealNormSpace holds
ex I be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(product <*X*>,Y)
st I is one-to-one onto isometric
& (for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
x be Point of X
holds (I.u).<*x*> = u.x)
& for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds ||.u.|| = ||.I.u.||
proof
let X,Y be RealNormSpace;
set J = IsoCPNrSP(X);
consider I be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(product <*X*>,Y)
such that
A1: I is one-to-one onto isometric
& for x be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds I.x = x * J" by Th38;
A2: for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
x be Point of X
holds (I.u).<*x*> = u.x
proof
let u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
x be Point of X;
A3: (IsoCPNrSP(X)).x = <*x*> by Def2;
reconsider px = <*x*> as Point of product <*X*> by Th12;
thus (I.u).<*x*>
= (u * J").px by A1
.= u.(J".px) by FUNCT_2:15
.= u.x by A3,FUNCT_2:26;
end;
take I;
thus I is one-to-one onto isometric by A1;
thus
for u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y),
x be Point of X
holds (I.u).<*x*> = u.x by A2;
let u be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
thus thesis by A1,NDIFF_7:7;
end;
theorem
for X,Y,Z,W be RealNormSpace,
I be Lipschitzian LinearOperator of X,Z,
J be Lipschitzian LinearOperator of Y,W
st I is one-to-one onto isometric
& J is one-to-one onto isometric
holds
ex K be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(Z,W)
st K is one-to-one onto isometric
& for x be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds K.x = J * (x * I")
proof
let X,Y,Z,W be RealNormSpace,
I be Lipschitzian LinearOperator of X,Z,
J be Lipschitzian LinearOperator of Y,W;
assume
A1: I is one-to-one onto isometric
& J is one-to-one onto isometric;
consider H be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(Z,Y)
such that
A2: H is one-to-one onto isometric
& for x be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds H.x = x * I" by A1,Th38;
consider L be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(Z,Y),
R_NormSpace_of_BoundedLinearOperators(Z,W)
such that
A3: L is one-to-one onto isometric
& for x be Point of R_NormSpace_of_BoundedLinearOperators(Z,Y)
holds L.x = J * x by A1,Th37;
reconsider K = L * H as Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X,Y),
R_NormSpace_of_BoundedLinearOperators(Z,W) by LOPBAN_2:2;
take K;
thus K is one-to-one onto by A2,A3,FUNCT_2:27;
for x be Point of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds ||.K.x.|| = ||.x.||
proof
let x be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
thus ||.K.x.||
= ||.L.(H.x).|| by FUNCT_2:15
.= ||.H.x.|| by NDIFF_7:7,A3
.= ||.x.|| by A2,NDIFF_7:7;
end;
hence K is isometric by NDIFF_7:7;
let x be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
thus K.x
= L.(H.x) by FUNCT_2:15
.= J * (H.x) by A3
.= J * (x * I") by A2;
end;
theorem Th41:
for n be Nat,
A,B be RealNormSpace-Sequence,
X,Y be RealNormSpace
st len A = n + 1 & A|n = B & X = A.(n + 1)
holds NestingLB(A,Y)
= R_NormSpace_of_BoundedLinearOperators(X,NestingLB(B,Y))
proof
let n be Nat,
A,B be RealNormSpace-Sequence,
X,Y be RealNormSpace;
assume
A1: len A = n + 1 & A|n = B & X = A.(n + 1);
consider f be Function such that
A2: dom f = NAT
& NestingLB(A,Y) = f.(len A)
& f.0 = Y
& for j be Nat st j < len A holds
ex V be RealNormSpace, k be Element of dom A
st V = f.j & j + 1 = k
& f.(j + 1) = R_NormSpace_of_BoundedLinearOperators(A.k,V) by Def3;
A3: len B = n by A1,FINSEQ_3:53;
then len B < len A by A1,NAT_1:13;
then consider V be RealNormSpace, k be Element of dom A
such that
A4: V = f.(len B) & (len B) + 1 = k
& f.((len B) + 1) = R_NormSpace_of_BoundedLinearOperators(A.k,V) by A2;
A5: for j be Nat st j < len B holds
ex V be RealNormSpace, k be Element of dom B
st V = f.j & j + 1 = k
& f.(j + 1) = R_NormSpace_of_BoundedLinearOperators(B.k,V)
proof
let j be Nat;
assume
A6: j < len B;
then j < len A by A1,A3,NAT_1:13;
then consider V be RealNormSpace, k be Element of dom A
such that
A7: V = f.j & j + 1 = k
& f.(j + 1) = R_NormSpace_of_BoundedLinearOperators(A.k,V) by A2;
A8: j + 1 <= len B by A6,NAT_1:13;
1 <= j + 1 by NAT_1:11;
then
A9: j + 1 in Seg len B by A8;
then reconsider k1 = j + 1 as Element of dom B by FINSEQ_1:def 3;
A.k = B.k1 by A1,A7,A9,FUNCT_1:49,A3;
hence thesis by A7;
end;
A10: A.k = X by A1,A4,FINSEQ_3:53;
thus NestingLB(A,Y)
= f.k by A1,A2,A4,FINSEQ_3:53
.= R_NormSpace_of_BoundedLinearOperators(X,NestingLB(B,Y))
by A2,A4,A5,A10,Def3;
end;
registration
let Y be RealNormSpace,
X be RealNormSpace-Sequence;
cluster NestingLB(X,Y) -> constituted-Functions;
coherence
proof
consider f be Function such that
A1: dom f = NAT
& NestingLB(X,Y) = f.(len X)
& f.0 = Y
& for j be Nat st j < len X holds
ex V be RealNormSpace, k be Element of dom X
st V = f.j
& j + 1 = k
& f.(j + 1) = R_NormSpace_of_BoundedLinearOperators(X.k,V) by Def3;
for g be object st g in the carrier of NestingLB(X,Y)
holds g is Function
proof
let g be object;
assume
A2: g in the carrier of NestingLB(X,Y);
1 <= len X by FINSEQ_1:20;
then len X - 1 in NAT by INT_1:3,XREAL_1:48;
then reconsider n = len X - 1 as Nat;
len X - 1 < len X - 0 by XREAL_1:15;
then consider V be RealNormSpace, k be Element of dom X
such that
A3: V = f.n
& n + 1 = k
& f.(n + 1) = R_NormSpace_of_BoundedLinearOperators(X.k,V) by A1;
thus thesis by A1,A2,A3;
end;
hence NestingLB(X,Y) is constituted-Functions
by FUNCT_1:def 13,MONOID_0:80;
end;
end;
Lm1:
for Y be RealNormSpace,
X be RealNormSpace-Sequence
ex I be Lipschitzian LinearOperator of
NestingLB(X,Y),R_NormSpace_of_BoundedMultilinearOperators(X,Y)
st I is one-to-one onto isometric
& (for u be Element of NestingLB(X,Y)
holds ||.I.u.|| = ||.u.||)
& for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X & g.1 = u
& (for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | ((len X)-'i + 1)
& h = g.i
& g.(i + 1) = h.(x.(len X-'i + 1 )))
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*>
& h = g.(len X)
& (I.u).x = h.(x.1)
proof
let Y be RealNormSpace;
defpred P[Nat] means
for X be RealNormSpace-Sequence
st $1 = len X & 1 <= len X
holds
ex I be Lipschitzian LinearOperator of
NestingLB(X,Y),R_NormSpace_of_BoundedMultilinearOperators(X,Y)
st I is one-to-one onto isometric
& for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X
& g.1 = u
& (for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | ((len X)-'i +1)
& h = g.i
& g.(i+1) = h.(x.(len X-'i+1)))
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*>
& h = g.(len X)
& (I.u).x = h.(x.1);
A1: P[0];
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: for X be RealNormSpace-Sequence
st n = len X & 1 <= len X
holds
ex I be Lipschitzian LinearOperator of
NestingLB(X,Y),R_NormSpace_of_BoundedMultilinearOperators(X,Y)
st I is one-to-one onto isometric
& for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X
& g.1 = u
& ( for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi =X| ((len X)-'i+1) & h=g.i
& g.(i+1) = h.(x.(len X-'i+1)) )
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*>
& h = g.(len X)
& (I.u).x = h.(x.1);
let X be RealNormSpace-Sequence;
assume
A4: n + 1 = len X & 1 <= len X;
set K = X | n;
A5: X = K ^ <* X.(n+1) *> by A4,FINSEQ_3:55;
A6: len K = n by A4,FINSEQ_3:53;
per cases;
suppose
A7: n = 0;
1 in Seg len X by A4;
then 1 in dom X by FINSEQ_1:def 3;
then X.1 in rng X by FUNCT_1:3;
then reconsider X1 = X.1 as RealNormSpace by PRVECT_2:def 10;
A8: X = <*X1*> by A4,A7,FINSEQ_1:40;
consider f be Function such that
A9: dom f = NAT
& NestingLB(X,Y) = f.(len X)
& f.0 = Y
& for j be Nat st j < len X holds
ex V be RealNormSpace, k be Element of dom X
st V = f.j
& j + 1 = k
& f.(j + 1) = R_NormSpace_of_BoundedLinearOperators(X.k,V)
by Def3;
consider V be RealNormSpace, k be Element of dom X
such that
A10: V = f.0
& 0 + 1 = k
& f.(0 + 1) = R_NormSpace_of_BoundedLinearOperators(X.k,V)
by A4,A7,A9;
consider I be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X1,Y),
R_NormSpace_of_BoundedLinearOperators(product <*X1*>,Y)
such that
A12: I is one-to-one onto isometric
& (for u be Point of R_NormSpace_of_BoundedLinearOperators(X1,Y),
x1 be Point of X1
holds (I.u).<*x1*> = u.x1)
& for u be Point of R_NormSpace_of_BoundedLinearOperators(X1,Y)
holds ||.u.|| = ||.I.u.|| by Th39;
A13: R_NormSpace_of_BoundedLinearOperators(product <*X1*>,Y)
= R_NormSpace_of_BoundedMultilinearOperators(<*X1*>,Y) by Th26;
reconsider I as Lipschitzian LinearOperator of
NestingLB(X,Y),R_NormSpace_of_BoundedMultilinearOperators(X,Y)
by A4,A7,A8,A9,A10,A13;
take I;
thus I is one-to-one onto isometric by A4,A7,A8,A9,A10,A12,A13;
thus
for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X
& g.1 = u
& ( for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | ((len X)-'i+1)
& h = g.i
& g.(i+1) = h.(x.(len X-'i+1)) )
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*>
& h = g.(len X)
& (I.u).x = h.(x.1)
proof
let u be Point of NestingLB(X,Y),
x be Point of product X;
set g = <*u*>;
take g;
thus len g = len X by FINSEQ_1:40,A7,A4;
thus g.1 = u;
thus
for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X| ((len X)-'i+1)
& h = g.i
& g.(i+1) = h.(x.(len X-'i+1)) by A4,A7;
reconsider XX1 = <*X.1*> as RealNormSpace-Sequence
by A4,A7,FINSEQ_1:40;
reconsider h = u as Point of NestingLB(XX1,Y)
by A4,A7,FINSEQ_1:40;
take XX1,h;
thus XX1 = <*X.1*> & h = g.(len X) by A4,A7;
consider x1 be Point of X1 such that
A14: x = <*x1*> by A8,Th12;
thus (I.u).x
= u.x1 by A4,A7,A9,A10,A12,A14
.= h.(x.1) by A14;
end;
end;
suppose
A15: n <> 0;
then
A16: 1 <= n by NAT_1:14;
n + 1 in Seg(n + 1) by FINSEQ_1:4;
then
reconsider n1 = n + 1 as Element of dom X by A4,FINSEQ_1:def 3;
reconsider Xn1 = X.n1 as RealNormSpace;
for x be set st x in rng K
holds x is RealNormSpace
proof
let x be set;
assume x in rng K;
then x in rng X by RELAT_1:70,TARSKI:def 3;
hence x is RealNormSpace by PRVECT_2:def 10;
end;
then
reconsider K as RealNormSpace-Sequence by A15,PRVECT_2:def 10;
set CXn1 = the carrier of Xn1;
set CK = carr K;
product <*Xn1*> = NORMSTR(# product(carr <*Xn1*>),
zeros <*Xn1*>,
[:(addop <*Xn1*>):],
[:(multop <*Xn1*>):],
productnorm <*Xn1*> #) by PRVECT_2:6;
then
A17: the carrier of product <*Xn1*>
= product <* the carrier of Xn1 *> by Th31;
A18: product K = NORMSTR(# product(carr K),
zeros K,
[:(addop K):],
[:(multop K):],
productnorm K #) by PRVECT_2:6;
product(K ^ <*Xn1*>) = NORMSTR(# product(carr(K ^ <*Xn1*>)),
zeros(K ^ <*Xn1*>),
[:(addop(K ^ <*Xn1*>)):],
[:(multop(K ^ <*Xn1*>)):],
productnorm(K ^ <*Xn1*>) #)
by PRVECT_2:6;
then
A19: the carrier of product(K ^ <*Xn1*>)
= product(carr(K) ^ carr <*Xn1*>) by Th30
.= product(CK ^ <*CXn1*>) by Th31;
set KY = R_NormSpace_of_BoundedMultilinearOperators(K,Y);
A20: NestingLB(X,Y)
= R_NormSpace_of_BoundedLinearOperators(X.n1,NestingLB(K,Y))
by A4,Th41;
consider I0 be Lipschitzian LinearOperator of NestingLB(K,Y),KY
such that
A21: I0 is one-to-one onto isometric
&
for u be Point of NestingLB(K,Y),
k be Point of product K
ex g be FinSequence
st len g = len K
& g.1 = u
& (for i be Element of NAT
st 1 <= i < len K
holds
ex Ki be RealNormSpace-Sequence,
h be Point of NestingLB(Ki,Y)
st Ki = K | ((len K)-'i+1)
& h = g.i
& g.(i+1) = h.(k.(len K-'i+1)))
& ex K1 be RealNormSpace-Sequence,
h be Point of NestingLB(K1,Y)
st K1 = <*K.1*>
& h = g.(len K)
& (I0.u).k = h.(k.1) by A3,A6,A15,NAT_1:14;
consider I1 be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X.n1,NestingLB(K,Y)),
R_NormSpace_of_BoundedLinearOperators(X.n1,KY)
such that
A22: I1 is one-to-one onto isometric
& for v be Point of
R_NormSpace_of_BoundedLinearOperators(X.n1,NestingLB(K,Y))
holds I1.v = I0 * v by A21,Th37;
consider I2 be Lipschitzian LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X.n1,KY),
R_NormSpace_of_BoundedMultilinearOperators(K^<*X.n1*>, Y)
such that
A23: I2 is one-to-one onto isometric
& for u be Point of
R_NormSpace_of_BoundedLinearOperators(X.n1,KY)
holds ||.u.|| = ||.I2.u.||
& for k be Point of product K,
x be Point of X.n1
holds (I2.u).(k ^ <*x*>) = (u.x).k by Th36;
set I = I2 * I1;
reconsider I as LinearOperator of
R_NormSpace_of_BoundedLinearOperators(X.n1, NestingLB(K,Y)),
R_NormSpace_of_BoundedMultilinearOperators(K ^ <*X.n1*>, Y)
by LOPBAN_2:1;
A24: for v be Element of
R_NormSpace_of_BoundedLinearOperators(X.n1, NestingLB(K,Y))
holds ||.I.v.|| = ||.v.||
proof
let v be Element of
R_NormSpace_of_BoundedLinearOperators(X.n1, NestingLB(K,Y));
thus ||.I.v.||
= ||.I2.(I1.v).|| by FUNCT_2:15
.= ||.I1.v.|| by A23
.= ||.v.|| by A22,NDIFF_7:7;
end;
then
I is isometric by NDIFF_7:7;
then
reconsider I as Lipschitzian LinearOperator of
NestingLB(X,Y),
R_NormSpace_of_BoundedMultilinearOperators(X,Y) by A20,A5;
take I;
thus I is one-to-one onto isometric
by A5,A20,A22,A23,A24,FUNCT_2:27,NDIFF_7:7;
thus
for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X & g.1 = u
& (for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | ((len X)-'i+1)
& h = g.i
& g.(i+1) = h.(x.(len X-'i+1)))
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*>
& h = g.(len X)
& (I.u).x = h.(x.1)
proof
let u be Point of NestingLB(X,Y),
x be Point of product X;
consider pk, pxn1 be FinSequence such that
A25: x = pk ^ pxn1
& pk in product CK
& pxn1 in product <*CXn1*> by A5,A19,RLAFFIN3:2;
reconsider pk as Point of product K by A18,A25;
consider y be Point of Xn1 such that
A26: pxn1 = <*y*> by A17,A25,Th12;
ex g be Function st pk = g & dom g = dom CK &
for i be object st i in dom CK
holds g.i in CK.i by A18,CARD_3:def 5;
then dom pk = Seg len CK by FINSEQ_1:def 3;
then
A27: len pk
= len CK by FINSEQ_1:def 3
.= len K by PRVECT_1:def 11
.= n by A4,FINSEQ_3:53;
reconsider xn1 = x.(n+1) as Point of Xn1
by A25,A26,A27,FINSEQ_1:42;
reconsider u1 = u as Lipschitzian LinearOperator of
Xn1, NestingLB(K,Y) by A20,LOPBAN_1:def 9;
reconsider uxn1 = u1.xn1 as Point of NestingLB(K,Y);
consider g1 be FinSequence such that
A28: len g1 = len K
& g1.1 = uxn1
& (for i be Element of NAT
st 1 <= i & i < len K
holds
ex Ki be RealNormSpace-Sequence,
h1 be Point of NestingLB(Ki,Y)
st Ki = K | ((len K)-'i+1)
& h1 = g1.i
& g1.(i+1) = h1.(pk.(len K-'i+1)))
& ex K1 be RealNormSpace-Sequence,
h1 be Point of NestingLB(K1,Y)
st K1 = <*K.1*>
& h1 = g1.(len K)
& (I0.uxn1).pk = h1.(pk.1) by A21;
set g = <*u*> ^ g1;
take g;
thus
len g = len <*u*> + len g1 by FINSEQ_1:22
.= 1 + len g1 by FINSEQ_1:40
.= len X by A4,A28,FINSEQ_3:53;
thus
A29: g.1 = u by FINSEQ_1:41;
thus
for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | ((len X)-'i+1)
& h = g.i
& g.(i+1) = h.(x.(len X-'i+1))
proof
let i be Element of NAT;
assume
A30: 1 <= i & i < len X;
A31: i <= n by A30,A4,NAT_1:13;
A32: i-'1 = i-1 by A30,XREAL_1:48,XREAL_0:def 2;
per cases;
suppose
A33: 2 <= i;
then
A34: 2-1 <= i-1 by XREAL_1:13;
then
A35: 1 <= (i-'1) by A30,XREAL_1:48,XREAL_0:def 2;
i -1 < i - 0 by XREAL_1:15;
then
A36: (i-'1) < len K by A31,A6,A32,XXREAL_0:2;
then
consider Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
such that
A37: Xi = K | ((len K) -' (i -' 1) + 1)
& h = g1.(i -' 1)
& g1.((i-'1) + 1) = h.(pk.(len K-'(i-'1) + 1)) by A28,A35;
take Xi,h;
A39: (len K)-'(i-'1) + 1
= (len K) - (i-1) + 1 by A32,A36,XREAL_1:48,XREAL_0:def 2
.= len K + 1 -i + 1
.= len X -i + 1 by A4,FINSEQ_3:53
.= (len X) -' i + 1 by A30,XREAL_1:48,XREAL_0:def 2;
len K - (i-'1) <= len K -1 by A35,XREAL_1:13;
then len K - (i-'1) + 1 <= len K - 1 + 1 by XREAL_1:7;
then
A40: len K - (i-'1) + 1 <= n by A4,FINSEQ_3:53;
A41: len K -' (i-'1) + 1 = len K - (i-'1) + 1
by A36,XREAL_1:48,XREAL_0:def 2;
A43: len <*u*> = 1 by FINSEQ_1:40;
A44: len <*u*> + 1 = 1 + 1 by FINSEQ_1:40;
i <= i + 1 by NAT_1:11;
then
A45: len <*u*> + 1 <= i + 1 by A33,A44,XXREAL_0:2;
A46: i+1 <= len g1 + 1 by A4,A6,A28,A30,NAT_1:13;
A47: (len X) -' i +1
= len X -i +1 by A30,XREAL_1:48,XREAL_0:def 2
.= n - (i-1) + 1 by A4;
n - (i-1) <= n - 1 by A34,XREAL_1:13; then
A48: n - (i-1) + 1 <= n - 1 + 1 by XREAL_1:7;
i - 1 < i - 0 by XREAL_1:15; then
A49: n-i < n-(i-1) by XREAL_1:15;
0 <= n-i by A31,XREAL_1:48;
then 0 < n-(i-1) by A49,XXREAL_0:2;
then 0+1 <= n-(i-1) + 1 by XREAL_1:8;
then (len X) -' i + 1 in Seg n by A47,A48;
then
A50: len X-'i + 1 in dom pk by A27,FINSEQ_1:def 3;
A51: g1.(i-'1)
= g1.(i-1) by A30,XREAL_1:48,XREAL_0:def 2
.= g.i by A4,A6,A28,A30,A33,A44,FINSEQ_1:23;
g.(i+1) = g1.(i+1-1) by A43,A45,A46,FINSEQ_1:23
.= h.(x.(len X-'i+1)) by A25,A32,A37,A39,A50,FINSEQ_1:def 7;
hence Xi = X| ((len X)-'i+1)
& h = g.i
& g.(i+1) = h.(x.(len X-'i+1))
by A37,A39,A40,A41,A51,FINSEQ_1:82;
end;
suppose
i < 2;
then i < 1+1; then
A53: i <= 1 by NAT_1:13; then
A54: i = 1 by A30,XXREAL_0:1;
A55: len <*u*> = 1 by FINSEQ_1:40;
A56: i+1 <= len g1 + 1 by A4,A6,A28,A30,NAT_1:13;
A57: g.(i+1)
= g1.(i+1-1) by A54,A55,A56,FINSEQ_1:23
.= uxn1 by A30,A53,XXREAL_0:1,A28;
A58: len X-'i = len X-i by A30,XREAL_1:48,XREAL_0:def 2;
take X,u;
thus X = X | ((len X)-'i+1) by A54,A58,FINSEQ_1:58;
thus u = g.i by A29,A30,A53,XXREAL_0:1;
thus g.(i+1) = u.(x.(len X-'i+1)) by A4,A54,A57,A58;
end;
end;
consider K1 be RealNormSpace-Sequence,
h1 be Point of NestingLB(K1,Y)
such that
A59: K1 = <*K.1*>
& h1 = g1.(len K)
& (I0.uxn1).pk = h1.(pk.1) by A28;
A60: 1 in Seg n by A16;
then
A61: <*X.1*> = <*K.1*> by FUNCT_1:49;
A62: 1 + len <*u*> <= len K + len <*u*> by A6,A16,XREAL_1:7;
A63: len <*u*> = 1 by FINSEQ_1:40;
A64: g.(len X)
= g.(len K+1) by A4,FINSEQ_3:53
.= g1.(len K+1 -1) by A28,A62,A63,FINSEQ_1:23
.= g1.(len K);
1 in dom pk by A27,A60,FINSEQ_1:def 3;
then
A65: pk.1 = x.1 by A25,FINSEQ_1:def 7;
A66: I.u = I2.(I1.u) by A20,FUNCT_2:15;
reconsider v = I1.u as Point of
R_NormSpace_of_BoundedLinearOperators(X.n1,KY)
by A20,FUNCT_2:5;
reconsider sn11 = xn1 as Point of X.n1;
(I.u).x
= (I2.v).(pk^<*xn1*>) by A25,A26,A27,A66,FINSEQ_1:42
.= (v.sn11).pk by A23
.= ((I0 * u1).xn1).pk by A20,A22
.= (I0.uxn1).pk by FUNCT_2:15;
hence
ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*>
& h = g.(len X)
& (I.u).x = h.(x.1) by A59,A61,A64,A65;
end;
end;
end;
A68: for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
let X be RealNormSpace-Sequence;
consider I be Lipschitzian LinearOperator of
NestingLB(X,Y),R_NormSpace_of_BoundedMultilinearOperators(X,Y)
such that
A69: I is one-to-one onto isometric
& for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X
& g.1 = u
& (for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | ((len X)-'i+1)
& h = g.i
& g.(i+1) = h.(x.(len X-'i+1)))
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*>
& h = g.(len X)
& (I.u).x = h.(x.1) by A68,FINSEQ_1:20;
for u be Element of NestingLB(X,Y)
holds ||.I.u.|| = ||.u.|| by A69,NDIFF_7:7;
hence thesis by A69;
end;
definition
let Y be RealNormSpace,
X be RealNormSpace-Sequence;
func NestMult(X,Y) -> Lipschitzian LinearOperator of
NestingLB(X,Y),R_NormSpace_of_BoundedMultilinearOperators(X,Y)
means
it is one-to-one onto isometric
&
(for u being Element of NestingLB(X,Y)
holds ||.it.u.|| = ||.u.||)
&
for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X & g.1 = u
& (for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | (len X -' i + 1) & h = g.i
& g.(i + 1) = h.(x.(len X -' i + 1)))
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*> & h = g.(len X)
& (it.u).x = h.(x.1);
existence by Lm1;
uniqueness
proof
let I1,I2 be Lipschitzian LinearOperator of
NestingLB(X,Y),R_NormSpace_of_BoundedMultilinearOperators(X,Y);
assume
A1: I1 is one-to-one onto isometric
& (for u being Element of NestingLB(X,Y)
holds ||.I1.u.|| = ||.u.||)
& for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X & g.1 = u
& ( for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | (len X -' i + 1) & h = g.i
& g.(i + 1) = h.(x.(len X -' i + 1)) )
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*> & h = g.(len X)
& (I1.u).x = h.(x.1);
assume
A2: I2 is one-to-one onto isometric
& ( for u being Element of NestingLB(X,Y)
holds ||.I2.u.|| = ||.u.|| )
& for u be Point of NestingLB(X,Y),
x be Point of product X
ex g be FinSequence
st len g = len X & g.1 = u
& ( for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | (len X -' i + 1) & h = g.i
& g.(i+1) = h.(x.(len X -' i + 1)) )
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*> & h = g.(len X)
& (I2.u).x = h.(x.1);
for u be Point of NestingLB(X,Y)
holds I1.u = I2.u
proof
let u be Point of NestingLB(X,Y);
reconsider I1u = I1.u, I2u = I2.u as
Multilinear Function of (product X),Y by LOPBAN10:def 11;
now
let x be Point of product X;
consider g1 be FinSequence such that
A3: len g1 = len X & g1.1 = u
& ( for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | (len X -' i + 1) & h = g1.i
& g1.(i+1) = h.(x.(len X -' i + 1)) )
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*> & h = g1.(len X)
& (I1.u).x = h.(x.1) by A1;
consider g2 be FinSequence such that
A4: len g2 = len X & g2.1 = u
& ( for i be Element of NAT
st 1 <= i & i < len X
holds
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | (len X -' i + 1) & h = g2.i
& g2.(i+1) = h.(x.(len X -' i + 1)) )
& ex X1 be RealNormSpace-Sequence,
h be Point of NestingLB(X1,Y)
st X1 = <*X.1*> & h = g2.(len X)
& (I2.u).x = h.(x.1) by A2;
defpred P[Nat] means
1 <= $1 & $1 <= len g1
implies g1.$1 = g2.$1;
A5: P[0];
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A7: P[k];
assume
A8: 1 <= k+1 & k+1 <= len g1;
per cases;
suppose
k = 0;
hence g1.(k+1) = g2.(k+1) by A3,A4;
end;
suppose
A11: k <> 0;
A12: k + 0 < k + 1 by XREAL_1:8; then
A13: k < len g1 by A8,XXREAL_0:2;
A15: k is Element of NAT by ORDINAL1:def 12;
k < len X by A3,A8,A12,XXREAL_0:2; then
A17: ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | (len X -' k + 1) & h = g1.k
& g1.(k+1) = h.(x.(len X -' k + 1))
by A3,A11,A15,NAT_1:14;
ex Xi be RealNormSpace-Sequence,
h be Point of NestingLB(Xi,Y)
st Xi = X | (len X -' k + 1) & h = g2.k
& g2.(k+1) = h.(x.(len X -' k + 1)) by A3,A4,A11,A13,A15,NAT_1:14;
hence g1.(k+1) = g2.(k+1)
by A7,A8,A11,A12,A17,NAT_1:14,XXREAL_0:2;
end;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A6);
hence I1u.x = I2u.x by A3,A4,FINSEQ_1:14;
end;
hence I1.u =I2.u by FUNCT_2:63;
end;
hence I1 = I2;
end;
end;