:: Multilinear Operator and Its Basic Properties
:: by Kazuhisa Nakasho
::
:: Received February 27, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies LOPBAN10, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC,
PARTFUN1, FUNCT_1, ORDINAL4, NAT_1, SUBSET_1, FINSEQ_2, RELAT_1,
LOPBAN_1, TARSKI, ARYTM_3, GROUP_2, FUNCT_4, FUNCT_2, ARYTM_1, SUPINF_2,
FCONT_1, STRUCT_0, CARD_1, UNIALG_1, FUNCOP_1, SEQ_4, XXREAL_2, FUNCSDOM,
RLSUB_1, RSSPACE, RELAT_2, METRIC_1, ALGSTR_0, MONOID_0, XXREAL_0,
XBOOLE_0, FINSEQ_1, RLVECT_1, PRVECT_1, PRVECT_2, CARD_3, PDIFF_1,
COMPLEX1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
PARTFUN1, FUNCT_2,
FUNCT_7, FUNCOP_1, NUMBERS, MONOID_0, XCMPLX_0, XXREAL_0, XXREAL_2,
XREAL_0, CARD_3, NAT_1, COMPLEX1, FINSEQ_1, FINSEQ_2, SEQ_4, STRUCT_0,
ALGSTR_0, PRE_TOPC, RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, RSSPACE,
RVSUM_1, LOPBAN_1, PRVECT_1, PRVECT_2, NDIFF_5;
constructors SEQ_4, RLSUB_1, RELSET_1, DUALSP01, NAT_D, RSSPACE3, NDIFF_5,
MONOID_0, FUNCT_7, FUNCT_4;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_0,
FINSEQ_2, FUNCT_2, NUMBERS, XBOOLE_0, RELAT_1, ORDINAL1, PRVECT_2,
NORMSP_0, NAT_1, CARD_3, NORMSP_1, FINSEQ_1, RLVECT_1, MONOID_0, NDIFF_5,
PRVECT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XXREAL_2, NORMSP_0, FUNCT_1, LOPBAN_1;
equalities RLVECT_1, LOPBAN_1, NORMSP_0, BINOP_1, PRVECT_2, STRUCT_0,
ALGSTR_0, FINSEQ_1;
expansions FINSEQ_1, FUNCT_1;
theorems TARSKI, XBOOLE_0, RLVECT_1, FUNCT_1, FUNCT_2, FINSEQ_1, LOPBAN_1,
PARTFUN1, VECTSP_1, COMPLEX1, XXREAL_0, NAT_1, XCMPLX_1, FINSEQ_2,
ABSVALUE, NORMSP_0, NDIFF_5, RSSPACE3, FUNCOP_1, RSSPACE, MONOID_0,
XCMPLX_0, XREAL_0, SEQ_4, PRVECT_1, NORMSP_1, RLSUB_1, XREAL_1, RVSUM_1,
LOPBAN_7, PRVECT_2, FUNCT_7, CARD_3, NAT_4, CARD_1, FINSEQ_3;
schemes XBOOLE_0, FUNCT_2, NAT_1, FINSEQ_1, FINSEQ_4, PARTFUN1;
begin :: Multilinear Operator on Real Linear Spaces
definition
let X be non empty non-empty FinSequence;
let i be object;
let x be Element of product X;
func reproj (i,x) -> Function of X.i, product X means :Def1:
for r being object st r in X.i holds it . r = x +* (i,r);
existence
proof
deffunc H1(object) = x +* (i,$1);
A1: for r being object st r in X.i holds H1(r) in product X
proof
let r be object;
assume
A2: r in X.i;
per cases;
suppose
not i in dom x; then
H1(r) = x by FUNCT_7:def 3;
hence H1(r) in product X;
end;
suppose
A4: i in dom x;
consider g being Function such that
A5: x = g & dom g = dom X
& for j being object st j in dom X holds
g.j in X.j by CARD_3:def 5;
A6: dom H1(r) = dom X by A5,FUNCT_7:30;
for j being object st j in dom X holds H1(r) . j in X.j
proof
let j be object;
assume
A7: j in dom X;
per cases;
suppose
j=i;
hence H1(r).j in X.j by A2,A4,FUNCT_7:31;
end;
suppose
j<>i; then
H1(r).j = x.j by FUNCT_7:32;
hence H1(r).j in X.j by A5,A7;
end;
end;
hence H1(r) in product X by A6,CARD_3:def 5;
end;
end;
consider f be Function of X.i, product X such that
A9: for r being object st r in X.i holds
f.r = H1(r) from FUNCT_2:sch 2(A1);
take f;
thus thesis by A9;
end;
uniqueness
proof
let f, g be Function of X.i,product X;
assume that
A10: for r being object st r in X.i holds f.r =x +* (i,r) and
A11: for r being object st r in X.i holds g.r = x +* (i,r);
now
let r be object;
assume
A12: r in X.i;
hence f.r = x +* (i,r) by A10
.= g.r by A11,A12;
end;
hence f=g by FUNCT_2:12;
end;
end;
theorem Th1:
for X be non empty non-empty FinSequence,
x be Element of product X,
i be Element of dom X,
r be object st r in X.i holds
(reproj (i,x).r ).i = r
proof
let X be non empty non-empty FinSequence,
x be Element of product X,
i be Element of dom X,
r be object;
assume r in X.i; then
A1: reproj (i,x).r = x +* (i,r) by Def1;
ex g being Function st x = g & dom g = dom X
& for j being object st j in dom X holds
g.j in X.j by CARD_3:def 5;
hence (reproj (i,x).r).i = r by A1,FUNCT_7:31;
end;
theorem Th2:
for X be non empty non-empty FinSequence,
x be Element of product X,
i,j be Element of dom X,
r be object
st r in X.i & i <> j
holds
( reproj (i,x).r ).j = x.j
proof
let X be non empty non-empty FinSequence,
x be Element of product X,
i,j be Element of dom X,
r be object;
assume
A1: r in X.i & i<> j; then
reproj (i,x).r = x +* (i,r) by Def1;
hence thesis by A1,FUNCT_7:32;
end;
theorem Th2X:
for X be non empty non-empty FinSequence,
x be Element of product X,
i be Element of dom X
holds
reproj (i,x).(x.i) = x
proof
let X be non empty non-empty FinSequence,
x be Element of product X,
i be Element of dom X;
reproj (i,x).(x.i) = x +* (i,(x.i)) by Def1;
hence reproj (i,x).(x.i) = x by FUNCT_7:35;
end;
definition
let X be RealLinearSpace-Sequence;
let i be Element of dom X;
let x be Element of product X;
func reproj(i,x) -> Function of X.i, product X means :Def20:
ex x0 be Element of product carr X st x0 = x & it = reproj(i,x0);
existence
proof
reconsider x0 = x as Element of product carr X;
A1: reproj(i,x0) is Function of (carr X).i, product carr X;
(carr X).i = the carrier of (X.i) by PRVECT_1:def 11;
hence thesis by A1;
end;
uniqueness;
end;
LemmaX:
for X being RealLinearSpace-Sequence holds dom carr X = dom X
proof
let X be RealLinearSpace-Sequence;
dom carr X = Seg len carr X by FINSEQ_1:def 3
.= Seg len X by PRVECT_1:def 11
.= dom X by FINSEQ_1:def 3;
hence thesis;
end;
theorem Th3:
for X being RealLinearSpace-Sequence,
i be Element of dom X,
x be Element of product X,
r be Element of X.i,
F be Function
st F = reproj(i,x).r
holds F.i = r
proof
let X be RealLinearSpace-Sequence,
i be Element of dom X,
x be Element of product X,
r be Element of X.i,
F be Function;
assume
A1: F = reproj(i,x).r;
A2: dom carr X = dom X by LemmaX;
A3: (carr X).i = the carrier of (X.i) by PRVECT_1:def 11;
consider x0 be Element of product carr X such that
A4: x0 = x & reproj(i,x)= reproj(i,x0) by Def20;
thus F.i = r by A1,A2,A3,A4,Th1;
end;
theorem Th4:
for X being RealLinearSpace-Sequence,
i,j be Element of dom X,
x be Element of product X,
r be Element of X.i,
F,s be Function
st F = reproj (i,x).r & x = s & i <> j
holds F.j = s.j
proof
let X be RealLinearSpace-Sequence,
i,j be Element of dom X,
x be Element of product X,
r be Element of X.i,
F,s be Function;
assume
A1: F = reproj (i,x).r & x = s & i <> j;
A2: dom carr X = dom X by LemmaX;
A3: (carr X).i = the carrier of (X.i) by PRVECT_1:def 11;
consider x0 be Element of product carr X such that
A4: x0 = x & reproj(i,x) = reproj(i,x0) by Def20;
thus F.j = s.j by A1,A2,A3,A4,Th2;
end;
theorem Th4X:
for X being RealLinearSpace-Sequence,
i be Element of dom X,
x be Element of product X,
s be Function
st x = s
holds reproj (i,x).(s.i)= x
proof
let X be RealLinearSpace-Sequence,
i be Element of dom X,
x be Element of product X,
s be Function;
assume
A1: x = s;
A2: dom carr X = dom X by LemmaX;
consider x0 be Element of product carr X such that
A4: x0 = x & reproj (i,x)= reproj (i,x0) by Def20;
thus reproj (i,x).(s.i) = x by A1,A2,A4,Th2X;
end;
definition
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace,
f be Function of product X,Y;
attr f is Multilinear means :Def3:
for i be Element of dom X,
x be Element of product X
holds
f * reproj(i,x) is LinearOperator of X.i,Y;
end;
registration
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
cluster Multilinear for Function of product X,Y;
correctness
proof
set g = (the carrier of product X) --> 0.Y;
take g;
now
let i be Element of dom X,
x be Element of product X;
set F = g * reproj (i,x);
for z being object st z in dom F holds F.z = 0.Y
proof
let z be object;
assume z in dom F; then
A2: z in the carrier of X.i by FUNCT_2:def 1;
thus F.z = g.(reproj (i,x).z) by A2,FUNCT_2:15
.= 0.Y by A2,FUNCOP_1:7,FUNCT_2:5;
end; then
F = (dom F) --> 0.Y by FUNCOP_1:11; then
A4: F = (the carrier of X.i) --> 0.Y by FUNCT_2:def 1;
reconsider f = g * reproj(i,x) as Function of (the carrier of X.i),Y;
A5: now
let x, y be VECTOR of X.i;
thus f . (x + y) = (0. Y) + (0. Y) by A4,FUNCOP_1:7
.= (f . x) + (0. Y) by A4,FUNCOP_1:7
.= (f . x) + (f . y) by A4,FUNCOP_1:7;
end;
now
let x be VECTOR of X.i;
let r be Real;
thus f . (r * x) = r * (0. Y) by A4,FUNCOP_1:7
.= r * (f . x) by A4,FUNCOP_1:7;
end;
hence g * reproj(i,x) is LinearOperator of X.i,Y
by A5,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
hence g is Multilinear;
end;
end;
definition
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
mode MultilinearOperator of X,Y is Multilinear Function of product X,Y;
end;
theorem LOPBAN73:
for X, Y being RealLinearSpace
for f being LinearOperator of X,Y
holds 0.Y = f.(0. X)
proof
let X, Y be RealLinearSpace;
let f be LinearOperator of X,Y;
(f /. (0. X)) + (0. Y)
= f /. ((0. X) + (0. X))
.= (f /. (0. X)) + (f /. (0. X)) by VECTSP_1:def 20;
hence 0.Y = f.(0. X) by RLVECT_1:8;
end;
theorem
for X being RealLinearSpace-Sequence,
Y being RealLinearSpace,
g be MultilinearOperator of X,Y,
t be Point of product X,
s be Element of product carr X
st s = t
& ex i be Element of dom X st s.i = 0.(X.i)
holds g.t = 0.Y
proof
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace,
g be MultilinearOperator of X,Y,
t be Point of product X,
s be Element of product carr X;
assume that
A1: s = t and
A2: ex i be Element of dom X st s.i = 0.(X.i);
consider i be Element of dom X such that
A3: s.i = 0.(X.i) by A2;
A7: ( g * reproj(i,t) ). ( 0.(X.i) )
= g.(reproj (i,t).( 0.(X.i) ) ) by FUNCT_2:15
.= g.t by A1,A3,Th4X;
g * reproj(i,t) is LinearOperator of X.i,Y by Def3;
hence g.t = 0.Y by A7,LOPBAN73;
end;
theorem
for X being RealLinearSpace-Sequence,
Y being RealLinearSpace,
g be MultilinearOperator of X,Y,
a be FinSequence of REAL
st dom a = dom X
holds
for t,t1 be Point of product X,
s,s1 be Element of product carr X
st t = s & t1 = s1
& for i be Element of dom X holds s1.i = (a/.i) * s.i
holds g.t1 = (Product a) * g.t
proof
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace,
g be MultilinearOperator of X,Y,
a be FinSequence of REAL;
assume
A1: dom a = dom X;
A4: dom carr X = dom X by LemmaX;
defpred P[Nat] means
for t,t1 be Point of product X,
s,s1 be Element of product carr X,
b be FinSequence of REAL
st t = s & t1 = s1 & b = a | $1 & $1 <= len a
& ( for i be Element of dom X holds
( ( i in Seg $1 implies s1.i = (a/.i) * s.i )
& ( not i in Seg $1 implies s1.i = s.i )))
holds
g.t1 = (Product b) * g.t;
A6: P[0]
proof
let t,t1 be Point of product X,
s,s1 be Element of product carr X,
b be FinSequence of REAL;
assume
A7: t = s & t1 = s1 & b = a | 0 & 0 <= len a
& for i be Element of dom X holds
( ( i in Seg 0 implies s1.i= (a/.i)*s.i )
& ( not i in Seg 0 implies s1.i= s.i ) );
A10: ex g being Function
st s1 = g
& dom g = dom carr X
& for y being object st y in dom carr X holds
g.y in (carr X).y by CARD_3:def 5;
A11: ex g being Function
st s = g
& dom g = dom carr X
& for y being object st y in dom carr X holds
g.y in (carr X).y by CARD_3:def 5;
s1 = s by A4,A7,A10,A11;
hence g.t1 = (Product b) * g.t by A7,RVSUM_1:94,RLVECT_1:def 8;
end;
A16: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A17: P[k];
let t,t1 be Point of product X,
s,s1 be Element of product carr X,
b be FinSequence of REAL;
assume
A18: t = s & t1 = s1 & b = a | (k+1) & (k+1) <= len a
& for i be Element of dom X holds
( ( i in Seg (k+1) implies s1.i= (a/.i)*s.i )
& ( not i in Seg (k+1) implies s1.i= s.i ) );
reconsider b2 = a | k as FinSequence of REAL;
A19: k <= k+1 by NAT_1:11;
1 <= k+1 & k+1 <= len a by A18,NAT_1:11; then
B20: k+1 in Seg len a; then
A21: k+1 in dom a by FINSEQ_1:def 3;
A23: b2 = b | k by A18,FINSEQ_1:82,NAT_1:11;
A25: b = b2^<*b.(k+1)*> by A18,A23,FINSEQ_1:59,FINSEQ_3:55
.= b2^<*a.(k+1)*> by A18,FINSEQ_1:4,FUNCT_1:49
.= b2^<*a/.(k+1)*> by A21,PARTFUN1:def 6;
defpred LP1[object] means $1 in Seg k;
deffunc F1(Element of dom X ) = a/.$1 * s.$1;
deffunc F2(Element of dom X) = s.$1;
consider s2 be Function such that
A26: dom s2 = dom X
& for i being Element of dom X holds
( LP1[i] implies s2. i = F1(i) )
& ( not LP1[i] implies s2.i = F2(i) ) from PARTFUN1:sch 4;
for y being object st y in dom carr X holds s2.y in (carr X). y
proof
let y be object;
assume y in dom carr X; then
reconsider i = y as Element of dom X by LemmaX;
per cases;
suppose
LP1[i]; then
s2.y = a/.i * s.i by A26; then
s2.y in the carrier of (X.i);
hence s2.y in (carr X). y by PRVECT_1:def 11;
end;
suppose
not LP1[i]; then
s2.y = s.i by A26; then
s2.y in the carrier of (X.i);
hence s2.y in (carr X). y by PRVECT_1:def 11;
end;
end; then
reconsider s2 as Element of product carr X by A4,A26,CARD_3:def 5;
reconsider t2 = s2 as Point of product X;
reconsider k1 = k+1 as Element of dom X by A1,B20,FINSEQ_1:def 3;
k+0 < k+1 by XREAL_1:8; then
not k1 in Seg k by FINSEQ_1:1; then
A30: s2.k1 = s.k1 by A26;
A31: g*reproj(k1,t2) is LinearOperator of X.k1,Y by Def3;
set RK = reproj(k1,t2) . ((a/.k1) * s.k1);
A32: ex g being Function st s1 = g & dom g = dom carr X
& for y being object st y in dom carr X holds
g.y in (carr X).y by CARD_3:def 5;
A33: ex g being Function st RK = g & dom g = dom carr X
& for y being object st y in dom carr X holds
g.y in (carr X).y by CARD_3:def 5;
reconsider RK as Function;
A51: for x be object st x in dom s1 holds s1.x = RK.x
proof
let x be object;
assume x in dom s1; then
reconsider i = x as Element of dom X by LemmaX,A32;
A38: ( i in Seg k implies s2. i = (a/.i) * s.i )
& ( not i in Seg k implies s2. i = s.i ) by A26;
A40: i <> k1 implies RK.i = s2.i by Th4;
per cases;
suppose
A41:i in Seg (k+1); then
A42: s1.i = (a/.i) * s.i by A18;
per cases;
suppose
A43: i = k+1; then
RK.i = (a/.k1) * s.k1 by Th3
.= s1.i by A18,A41,A43;
hence s1.x = RK.x;
end;
suppose
A44: i <> k+1;
1<=i & i <=k+1 by A41,FINSEQ_1:1; then
1<=i & i < k+1 by A44,XXREAL_0:1; then
1<=i & i <= k by NAT_1:13;
hence s1.x = RK.x by A38,A42,A44,Th4;
end;
end;
suppose
A46: not i in Seg(k+1);
i in dom X; then
i in Seg len X by FINSEQ_1:def 3; then
A47: 1 <= i & i <= len X by FINSEQ_1:1;
A49: k+1 < i by A46,A47;
k <= k+1 by NAT_1:11; then
k < i by A49,XXREAL_0:2;
hence s1.x = RK.x by A18,A38,A40,A46,A47,FINSEQ_1:1;
end;
end;
A54: g.t1
= g.(reproj(k1,t2).((a/.k1)*s.k1)) by A18,A32,A33,A51,FUNCT_1:2
.= (g * reproj(k1,t2)) . ((a/.k1)*s.k1) by FUNCT_2:15
.= (a/.k1) * (g * reproj(k1,t2)).(s.k1) by A31,LOPBAN_1:def 5
.= (a/.(k+1)) * ( g.((reproj(k1,t2)).(s.k1)) ) by FUNCT_2:15
.= (a/.(k+1)) * g.t2 by A30,Th4X;
thus g.t1
= (a/.(k+1)) * ((Product b2 ) * g.t) by A17,A18,A19,A26,A54,XXREAL_0:2
.= ((a/.(k+1)) * (Product b2 )) * g.t by RLVECT_1:def 7
.= (Product b) * g.t by A25,RVSUM_1:96;
end;
A55: for k be Nat holds P[k] from NAT_1:sch 2(A6,A16);
let t,t1 be Point of product X,
s,s1 be Element of product carr X;
assume
A56: t = s & t1 = s1
& for i be Element of dom X holds s1.i = (a/.i) * s.i;
set b = a | len a;
A57: b = a & len a <= len a by FINSEQ_2:20;
for i be Element of dom X holds
( i in Seg len a implies s1.i = (a/.i) * s.i )
& ( not i in Seg len a implies s1.i = s.i )
proof
let i be Element of dom X;
thus i in Seg len a implies s1.i = (a/.i) * s.i by A56;
thus not (i in Seg len a) implies s1.i = s.i
proof
assume not i in Seg len a; then
not i in dom X by A1,FINSEQ_1:def 3;
hence s1.i = s.i;
end;
end;
hence g.t1 = (Product a) * g.t by A55,A56,A57;
end;
definition
let X be RealLinearSpace-Sequence, Y be RealLinearSpace;
func MultilinearOperators(X,Y)
-> Subset of RealVectSpace(the carrier of product X,Y) means :Def6:
for x being set holds x in it iff x is MultilinearOperator of X,Y;
existence
proof
defpred P[object] means $1 is
MultilinearOperator of X,Y;
consider IT being set such that
A1: for x being object holds x in IT
iff x in Funcs(the carrier of product X, the
carrier of Y) & P[x] from XBOOLE_0:sch 1;
take IT;
for x be object st x in IT
holds x in Funcs(the carrier of product X,
the carrier of Y) by A1;
hence IT is Subset of RealVectSpace(the carrier of product X,
Y) by TARSKI:def 3;
let x be set;
thus x in IT implies x is MultilinearOperator of X,Y by A1;
assume
A2: x is MultilinearOperator of X,Y; then
x in Funcs(the carrier of product X,the carrier of Y) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of RealVectSpace(the carrier of product X, Y);
assume that
A3: for x being set holds x in X1 iff x is MultilinearOperator of X,Y and
A4: for x being set holds x in X2 iff x is MultilinearOperator of X,Y;
A5: X2 c= X1
proof
let x be object;
assume x in X2; then
x is MultilinearOperator of X,Y by A4;
hence thesis by A3;
end;
X1 c= X2
proof
let x be object;
assume x in X1; then
x is MultilinearOperator of X,Y by A3;
hence thesis by A4;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
end;
LM14:
for X be RealLinearSpace,
x1,x2,x3,x4 be Point of X
holds (x1+x2) + (x3+x4) = (x1+x3) + (x2+x4)
proof
let X be RealLinearSpace,
x1,x2,x3,x4 be Point of X;
thus (x1+x2) + (x3+x4)
= (x1+x2+x3)+x4 by RLVECT_1:def 3
.= (x1+x3+x2)+x4 by RLVECT_1:def 3
.= (x1+x3)+(x2+x4) by RLVECT_1:def 3;
end;
registration
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
cluster MultilinearOperators(X,Y) -> non empty functional;
coherence
proof
set f = the MultilinearOperator of X,Y;
f in MultilinearOperators(X,Y) by Def6;
hence MultilinearOperators(X,Y) is non empty;
let x be object;
assume x in MultilinearOperators(X,Y);
hence thesis;
end;
cluster MultilinearOperators(X,Y) -> linearly-closed;
coherence
proof
set W = MultilinearOperators(X,Y);
A1: for v,u be VECTOR of RealVectSpace(the carrier of product X,Y)
st v in MultilinearOperators(X,Y)
& u in MultilinearOperators(X,Y)
holds v + u in MultilinearOperators(X,Y)
proof
let v,u be VECTOR of RealVectSpace(the carrier of product X,Y) such that
A2: v in W and
A3: u in W;
reconsider u1=u as MultilinearOperator of X,Y by A3,Def6;
reconsider v1=v as MultilinearOperator of X,Y by A2,Def6;
v+u is MultilinearOperator of X,Y
proof
reconsider L0=v+u as Function of product X,Y by FUNCT_2:66;
now
let i be Element of dom X,x be Point of product X;
reconsider L = L0 * reproj(i,x) as Function of X.i,Y;
A4: u1 * reproj(i,x) is LinearOperator of X.i,Y
& v1 * reproj(i,x) is LinearOperator of X.i,Y by Def3;
A5: for x1,x2 be Point of X.i holds L.(x1+x2) = L.x1 + L.x2
proof
let x1,x2 be Point of X.i;
thus L. (x1+x2) = L0.(reproj(i,x).(x1+x2)) by FUNCT_2:15
.= u1. (reproj(i,x).(x1+x2)) + v1.(reproj(i,x).(x1+x2))
by LOPBAN_1:1
.= (u1*reproj(i,x)).(x1+x2)+ v1.(reproj(i,x).(x1+x2))
by FUNCT_2:15
.= (u1*reproj(i,x)).(x1+x2) + (v1*reproj(i,x)).(x1+x2)
by FUNCT_2:15
.= (u1*reproj(i,x)).x1
+ (u1*reproj(i,x)).x2 + (v1*reproj(i,x)).(x1+x2)
by A4,VECTSP_1:def 20
.= (u1*reproj(i,x)).x1 + (u1*reproj(i,x)).x2
+ ((v1*reproj(i,x)).x1 + (v1*reproj(i,x)).x2)
by A4,VECTSP_1:def 20
.= (u1*reproj(i,x)).x1 + (v1*reproj(i,x)).x1
+ ((u1*reproj(i,x)).x2 + (v1*reproj(i,x)).x2) by LM14
.= u1.(reproj(i,x).x1) + (v1*reproj(i,x)).x1
+ ((u1*reproj(i,x)).x2 + (v1*reproj(i,x)).x2) by FUNCT_2:15
.= u1.(reproj(i,x).x1) + v1.(reproj(i,x).x1)
+ ((u1*reproj(i,x)).x2 + (v1*reproj(i,x)).x2) by FUNCT_2:15
.= u1.(reproj(i,x).x1) + v1.(reproj(i,x).x1)
+ (u1.(reproj(i,x).x2) + (v1*reproj(i,x)).x2) by FUNCT_2:15
.= u1.(reproj(i,x).x1) + v1.(reproj(i,x).x1)
+ (u1.(reproj(i,x).x2) +v1.(reproj(i,x).x2)) by FUNCT_2:15
.= L0.(reproj(i,x).x1) + (u1.(reproj(i,x).x2) +v1.(reproj(i,x).x2))
by LOPBAN_1:1
.= L0.(reproj(i,x).x1) + L0.(reproj(i,x).x2) by LOPBAN_1:1
.= L.x1 + (u+v).(reproj(i,x).x2) by FUNCT_2:15
.= L. x1 + L.x2 by FUNCT_2:15;
end;
for x be Point of X.i, a be Real holds L. (a*x) = a*L.x
proof
let x1 be Point of X.i, a be Real;
thus L. (a*x1) = L0.(reproj(i,x).(a*x1)) by FUNCT_2:15
.= u1.(reproj(i,x).(a*x1)) + v1.(reproj(i,x).(a*x1))
by LOPBAN_1:1
.= (u1*reproj(i,x)).(a*x1) + v1.(reproj(i,x).(a*x1))
by FUNCT_2:15
.= (u1*reproj(i,x)).(a*x1) + (v1*reproj(i,x)).(a*x1)
by FUNCT_2:15
.= a*(u1*reproj(i,x)).x1 + (v1*reproj(i,x)).(a*x1)
by A4,LOPBAN_1:def 5
.= a*(u1*reproj(i,x)).x1 + a*(v1*reproj(i,x)).x1
by A4,LOPBAN_1:def 5
.= a*u1.(reproj(i,x).x1) + a*(v1*reproj(i,x)).x1
by FUNCT_2:15
.= a*u1.(reproj(i,x).x1) + a*v1.(reproj(i,x).x1)
by FUNCT_2:15
.= a*(u1.(reproj(i,x).x1) + v1.(reproj(i,x).x1))
by RLVECT_1:def 5
.= a*L0.(reproj(i,x).x1) by LOPBAN_1:1
.= a*L.x1 by FUNCT_2:15;
end;
hence L0 * reproj(i,x) is LinearOperator of X.i,Y
by A5,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
hence thesis by Def3;
end;
hence thesis by Def6;
end;
for b be Real
for v be VECTOR of RealVectSpace(the carrier of product X,Y)
st v in W
holds b * v in W
proof
let b be Real;
let v be VECTOR of RealVectSpace(the carrier of product X,Y) such that
A9: v in W;
reconsider v1 = v as MultilinearOperator of X,Y by A9,Def6;
b*v is MultilinearOperator of X,Y
proof
reconsider L0 = b*v as Function of product X,Y by FUNCT_2:66;
now
let i be Element of dom X,x be Point of product X;
reconsider L = L0 * reproj(i,x) as Function of X.i,Y;
A10: v1*reproj(i,x) is LinearOperator of X.i,Y by Def3;
A11: for x1,x2 be Point of X.i holds L.(x1+x2) = L.x1 + L.x2
proof
let x1,x2 be Point of X.i;
thus L.(x1+x2)
= L0.(reproj(i,x).(x1+x2)) by FUNCT_2:15
.= b*v1.(reproj(i,x).(x1+x2)) by LOPBAN_1:2
.= b*(v1*reproj(i,x)).(x1+x2) by FUNCT_2:15
.= b*((v1*reproj(i,x)).x1 +(v1*reproj(i,x)).x2)
by A10,VECTSP_1:def 20
.= b*(v1*reproj(i,x)).x1 +b*(v1*reproj(i,x)).x2 by RLVECT_1:def 5
.= b*v1.(reproj(i,x).x1) +b*(v1*reproj(i,x)).x2 by FUNCT_2:15
.= b*v1.(reproj(i,x).x1) +b*v1.(reproj(i,x).x2) by FUNCT_2:15
.= L0.(reproj(i,x).x1) + b*v1.(reproj(i,x).x2) by LOPBAN_1:2
.= L0.(reproj(i,x).x1) + L0.(reproj(i,x).x2) by LOPBAN_1:2
.= L.x1 + L0.(reproj(i,x).x2) by FUNCT_2:15
.= L.x1 + L.x2 by FUNCT_2:15;
end;
for z be Point of X.i, a be Real holds L.(a*z) = a * L.z
proof
let x1 be Point of X.i, a be Real;
thus L. (a*x1)
= L0.(reproj(i,x).(a*x1)) by FUNCT_2:15
.= b * v1.(reproj(i,x).(a*x1)) by LOPBAN_1:2
.= b * (v1 * reproj(i,x)).(a*x1) by FUNCT_2:15
.= b * (a*(v1*reproj(i,x)).x1) by A10,LOPBAN_1:def 5
.= (b*a) * (v1*reproj(i,x)).x1 by RLVECT_1:def 7
.= a * (b*(v1*reproj(i,x)).x1) by RLVECT_1:def 7
.= a * (b*v1.(reproj(i,x).x1)) by FUNCT_2:15
.= a * L0.(reproj(i,x).x1) by LOPBAN_1:2
.= a * L.x1 by FUNCT_2:15;
end;
hence L0*reproj(i,x) is LinearOperator of X.i,Y
by A11,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
hence thesis by Def3;
end;
hence thesis by Def6;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
end;
definition
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
func R_VectorSpace_of_MultilinearOperators(X,Y) -> strict RLSStruct
equals
RLSStruct(# MultilinearOperators(X,Y),
Zero_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Add_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Mult_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)) #);
coherence;
end;
theorem
for X being RealLinearSpace-Sequence,
Y be RealLinearSpace holds
RLSStruct(# MultilinearOperators(X,Y),
Zero_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Add_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Mult_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)) #)
is Subspace of RealVectSpace(the carrier of product X,Y) by RSSPACE:11;
registration
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
cluster R_VectorSpace_of_MultilinearOperators(X,Y) -> non empty;
coherence;
end;
registration
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
cluster R_VectorSpace_of_MultilinearOperators(X,Y)
-> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative
scalar-unital;
coherence by RSSPACE:11;
end;
registration
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
cluster R_VectorSpace_of_MultilinearOperators(X,Y) -> constituted-Functions;
coherence by MONOID_0:80;
end;
definition
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
let f be Element of R_VectorSpace_of_MultilinearOperators(X,Y);
let v be VECTOR of product X;
redefine func f.v -> VECTOR of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as MultilinearOperator of X,Y by Def6;
f.v is VECTOR of Y;
hence thesis;
end;
end;
theorem
for X being RealLinearSpace-Sequence,
Y be RealLinearSpace
for f,g,h be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y)
holds
h = f + g
iff
for x be VECTOR of product X holds h.x = f.x + g.x
proof
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
let f,g,h be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y);
reconsider f9=f,g9=g,h9=h as MultilinearOperator of X,Y by Def6;
A1: R_VectorSpace_of_MultilinearOperators(X,Y) is
Subspace of RealVectSpace(the carrier of product X,Y)
by RSSPACE:11; then
reconsider f1=f, h1=h, g1=g as VECTOR of
RealVectSpace(the carrier of product X,Y) by RLSUB_1:10;
A2: now
assume
A3: h = f+g;
let x be Element of product X;
h1 = f1+g1 by A1,A3,RLSUB_1:13;
hence h9.x = f9.x + g9.x by LOPBAN_1:1;
end;
now
assume for x be Element of product X holds h9.x = f9.x + g9.x;
then h1 = f1+g1 by LOPBAN_1:1;
hence h = f+g by A1,RLSUB_1:13;
end;
hence thesis by A2;
end;
theorem
for X being RealLinearSpace-Sequence,
Y be RealLinearSpace
for f,h be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y)
for a be Real
holds
h = a*f
iff
for x be VECTOR of product X holds h.x = a * f.x
proof
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
let f,h be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y);
reconsider f9=f,h9=h as MultilinearOperator of X,Y by Def6;
let a be Real;
A1: R_VectorSpace_of_MultilinearOperators(X,Y)
is Subspace of RealVectSpace(the carrier of product X,Y)
by RSSPACE:11; then
reconsider f1=f, h1=h as VECTOR of
RealVectSpace(the carrier of product X,Y) by RLSUB_1:10;
A2: now
assume
A3: h = a*f;
let x be Element of product X;
h1 = a * f1 by A1,A3,RLSUB_1:14;
hence h9.x = a * f9.x by LOPBAN_1:2;
end;
now
assume for x be Element of product X holds h9.x = a * f9.x; then
h1 = a * f1 by LOPBAN_1:2;
hence h = a * f by A1,RLSUB_1:14;
end;
hence thesis by A2;
end;
theorem
for X being RealLinearSpace-Sequence,
Y be RealLinearSpace
holds 0.R_VectorSpace_of_MultilinearOperators(X,Y)
= (the carrier of product X) --> 0.Y
proof
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
A1: 0.RealVectSpace(the carrier of product X,Y)
= ((the carrier of product X) -->0.Y);
R_VectorSpace_of_MultilinearOperators(X,Y)
is Subspace of RealVectSpace(the carrier of product X,Y)
by RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
theorem
for X being RealLinearSpace-Sequence,
Y be RealLinearSpace
holds (the carrier of product X) --> 0.Y is MultilinearOperator of X,Y
proof
let X be RealLinearSpace-Sequence,
Y be RealLinearSpace;
set f0 = (the carrier of product X) --> 0.Y;
now
let i be Element of dom X, u be Element of product X;
set F = f0 * reproj(i,u);
A1: dom F = the carrier of X.i by FUNCT_2:def 1;
A4: for z being object st z in dom F holds F.z = 0.Y
proof
let z be object;
assume z in dom F; then
A2: z in the carrier of X.i by FUNCT_2:def 1;
thus F.z = f0.(reproj (i,u).z) by A2,FUNCT_2:15
.= 0.Y by A2,FUNCT_2:5,FUNCOP_1:7;
end;
reconsider f = f0 * reproj(i,u) as Function of X.i,Y;
A5: f is homogeneous
proof
let x be VECTOR of X.i, r be Real;
thus f.(r*x) = r * 0.Y by A1,A4
.= r * f.x by A1,A4;
end;
now
let x,y be VECTOR of X.i;
thus f.(x+y) = 0.Y by A1,A4
.= f.x+0.Y by A1,A4
.= f.x+f.y by A1,A4;
end;
hence f0 * reproj(i,u) is LinearOperator of X.i,Y
by A5,VECTSP_1:def 20;
end;
hence thesis by Def3;
end;
begin :: Bounded Multilinear Operator on Normed Linear Spaces
Def2:
for X being RealNormSpace-Sequence,
i be Element of dom X,
x be Element of product X
holds
ex x0 be Element of product carr X
st x0 = x & reproj(i,x) = reproj(i,x0)
proof
let X be RealNormSpace-Sequence,
i be Element of dom X,
x be Element of product X;
A1: product X = NORMSTR(# (product (carr X)),
(zeros X),
[:(addop X):],
[:(multop X):],
(productnorm X) #) by PRVECT_2:6;
then
reconsider x0 = x as Element of product carr X;
take x0;
A5: (carr X).i = the carrier of (X.i) by PRVECT_1:def 11;
now
let r be Element of X.i;
thus reproj (i,x).r = x +* (i,r) by NDIFF_5:def 4
.= reproj(i,x0).r by A5,Def1;
end;
hence thesis by A1,A5,FUNCT_2:63;
end;
theorem Th3:
for X being RealNormSpace-Sequence,
i be Element of dom X,
x be Element of product X,
r be Element of X.i,
F be Function
st F = reproj(i,x).r
holds F.i = r
proof
let X be RealNormSpace-Sequence,
i be Element of dom X,
x be Element of product X,
r be Element of X.i,
F be Function;
assume
A1: F = reproj (i,x).r;
A2: dom carr X = dom X by LemmaX;
A3: (carr X).i = the carrier of (X.i) by PRVECT_1:def 11;
consider x0 be Element of product carr X such that
A4: x0 = x & reproj(i,x) = reproj(i,x0) by Def2;
thus F.i = r by A1,A2,A3,A4,Th1;
end;
theorem Th4:
for X being RealNormSpace-Sequence,
i,j be Element of dom X,
x be Element of product X,
r be Element of X.i,
F,s be Function
st F = reproj (i,x).r & x = s & i <> j
holds F.j = s.j
proof
let X be RealNormSpace-Sequence,
i,j be Element of dom X,
x be Element of product X,
r be Element of X.i,
F,s be Function;
assume
A1: F = reproj(i,x).r & x = s & i <> j;
A2: dom carr X = dom X by LemmaX;
A3: (carr X).i = the carrier of (X.i) by PRVECT_1:def 11;
consider x0 be Element of product carr X such that
A4: x0 = x & reproj (i,x) = reproj(i,x0) by Def2;
thus F.j = s.j by A1,A2,A3,A4,Th2;
end;
theorem Th4X:
for X being RealNormSpace-Sequence,
i be Element of dom X,
x be Element of product X,
s be Function
st x = s
holds reproj(i,x).(s.i)= x
proof
let X be RealNormSpace-Sequence,
i be Element of dom X,
x be Element of product X,
s be Function;
assume
A1: x = s;
A2: dom carr X = dom X by LemmaX;
consider x0 be Element of product carr X such that
A4: x0 = x & reproj(i,x) = reproj(i,x0) by Def2;
thus reproj (i,x).(s.i) = x by A1,A2,A4,Th2X;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace,
f be Function of product X,Y;
attr f is Multilinear means :Def3:
for i be Element of dom X,
x be Element of product X
holds f * reproj(i,x) is LinearOperator of X.i,Y;
end;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster Multilinear for Function of product X,Y;
correctness
proof
set g = (the carrier of product X) --> 0.Y;
take g;
now
let i be Element of dom X,
x be Element of product X;
set F = g * reproj(i,x);
A1: dom F = the carrier of X.i by FUNCT_2:def 1;
A4: for z being object st z in dom F holds F.z = 0.Y
proof
let z be object;
assume z in dom F; then
A2: z in the carrier of X.i by FUNCT_2:def 1;
thus F.z = g.(reproj(i,x).z) by A2,FUNCT_2:15
.= 0.Y by A2,FUNCOP_1:7,FUNCT_2:5;
end;
reconsider f = g * reproj(i,x) as Function of (the carrier of X.i),Y;
A5: now
let x, y be VECTOR of X.i;
thus f . (x + y) = 0. Y by A1,A4
.= (f . x) + (0. Y) by A1,A4
.= (f . x) + (f . y) by A1,A4;
end;
now
let x be VECTOR of X.i;
let r be Real;
thus f . (r * x) = r * (0. Y) by A1,A4
.= r * (f . x) by A1,A4;
end;
hence g * reproj(i,x) is LinearOperator of X.i,Y
by A5,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
hence g is Multilinear;
end;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
mode MultilinearOperator of X,Y is Multilinear Function of product X,Y;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
func MultilinearOperators(X,Y)
-> Subset of RealVectSpace(the carrier of product X,Y) means :Def6:
for x being set holds x in it iff x is MultilinearOperator of X,Y;
existence
proof
defpred P[object] means $1 is MultilinearOperator of X,Y;
consider IT being set such that
A1: for x being object holds x in IT iff
x in Funcs(the carrier of product X, the
carrier of Y) & P[x] from XBOOLE_0:sch 1;
take IT;
for x be object st x in IT
holds x in Funcs(the carrier of product X, the carrier of Y) by A1;
hence IT is Subset of RealVectSpace(the carrier of product X, Y)
by TARSKI:def 3;
let x be set;
thus x in IT implies x is MultilinearOperator of X,Y by A1;
assume
A2: x is MultilinearOperator of X,Y; then
x in Funcs(the carrier of product X,the carrier of Y) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of RealVectSpace(the carrier of product X, Y);
assume that
A3: for x being set holds x in X1 iff x is MultilinearOperator of X,Y and
A4: for x being set holds x in X2 iff x is MultilinearOperator of X,Y;
A5: X2 c= X1
proof
let x be object;
assume x in X2; then
x is MultilinearOperator of X,Y by A4;
hence thesis by A3;
end;
X1 c= X2
proof
let x be object;
assume x in X1; then
x is MultilinearOperator of X,Y by A3;
hence thesis by A4;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
end;
LM14:
for X be RealNormSpace, x1,x2,x3,x4 be Point of X
holds (x1+x2) + (x3+x4) = (x1+x3) + (x2+x4)
proof
let X be RealNormSpace,
x1,x2,x3,x4 be Point of X;
thus (x1+x2) + (x3+x4) = (x1+x2+x3)+x4 by RLVECT_1:def 3
.= (x1+x3+x2)+x4 by RLVECT_1:def 3
.= (x1+x3)+(x2+x4) by RLVECT_1:def 3;
end;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster MultilinearOperators(X,Y) -> non empty functional;
coherence
proof
set f = the MultilinearOperator of X,Y;
f in MultilinearOperators(X,Y) by Def6;
hence MultilinearOperators(X,Y) is non empty;
let x be object;
assume x in MultilinearOperators(X,Y);
hence thesis;
end;
cluster MultilinearOperators(X,Y) -> linearly-closed;
coherence
proof
set W = MultilinearOperators(X,Y);
A1: for v,u be VECTOR of RealVectSpace(the carrier of product X,Y)
st v in MultilinearOperators(X,Y)
& u in MultilinearOperators(X,Y)
holds v + u in MultilinearOperators(X,Y)
proof
let v,u be VECTOR of RealVectSpace(the carrier of product X,Y) such that
A2: v in W and
A3: u in W;
reconsider u1=u as MultilinearOperator of X,Y by A3,Def6;
reconsider v1=v as MultilinearOperator of X,Y by A2,Def6;
v+u is MultilinearOperator of X,Y
proof
reconsider L0=v+u as Function of product X,Y by FUNCT_2:66;
now
let i be Element of dom X,x be Point of product X;
reconsider L = L0 * reproj(i,x) as Function of X.i,Y;
A4: u1 * reproj(i,x) is LinearOperator of X.i,Y
& v1 * reproj(i,x) is LinearOperator of X.i,Y by Def3;
A5: for x1,x2 be Point of X.i holds L.(x1+x2) = L.x1 + L.x2
proof
let x1,x2 be Point of X.i;
thus L.(x1+x2) = L0.(reproj(i,x).(x1+x2)) by FUNCT_2:15
.= u1.(reproj(i,x).(x1+x2)) + v1.(reproj(i,x).(x1+x2))
by LOPBAN_1:1
.= (u1*reproj(i,x)).(x1+x2) + v1.(reproj(i,x).(x1+x2))
by FUNCT_2:15
.= (u1*reproj(i,x)).(x1+x2) + (v1*reproj(i,x)).(x1+x2)
by FUNCT_2:15
.= (u1*reproj(i,x)).x1 + (u1*reproj(i,x)).x2
+ (v1*reproj(i,x)).(x1+x2) by A4,VECTSP_1:def 20
.= (u1*reproj(i,x)).x1 + (u1*reproj(i,x)).x2
+ ((v1*reproj(i,x)).x1 + (v1*reproj(i,x)).x2)
by A4,VECTSP_1:def 20
.= (u1*reproj(i,x)).x1 + (v1*reproj(i,x)).x1
+ ((u1*reproj(i,x)).x2 + (v1*reproj(i,x)).x2) by LM14
.= u1.(reproj(i,x).x1) + (v1*reproj(i,x)).x1
+ ((u1*reproj(i,x)).x2 + (v1*reproj(i,x)).x2) by FUNCT_2:15
.= u1.(reproj(i,x).x1) + v1.(reproj(i,x).x1)
+ ((u1*reproj(i,x)).x2 + (v1*reproj(i,x)).x2) by FUNCT_2:15
.= u1.(reproj(i,x).x1) + v1.(reproj(i,x).x1)
+ (u1.(reproj(i,x).x2) + (v1*reproj(i,x)).x2) by FUNCT_2:15
.= u1.(reproj(i,x).x1) + v1.(reproj(i,x).x1)
+ (u1.(reproj(i,x).x2) + v1.(reproj(i,x).x2)) by FUNCT_2:15
.= L0.(reproj(i,x).x1)
+ (u1.(reproj(i,x).x2) + v1.(reproj(i,x).x2)) by LOPBAN_1:1
.= L0.(reproj(i,x).x1) + L0.(reproj(i,x).x2) by LOPBAN_1:1
.= L.x1 + (u+v).(reproj(i,x).x2) by FUNCT_2:15
.= L.x1+ L.x2 by FUNCT_2:15;
end;
for x be Point of X.i, a be Real holds L.(a*x) = a * L.x
proof
let x1 be Point of X.i, a be Real;
thus L.(a*x1) = L0.(reproj(i,x).(a*x1)) by FUNCT_2:15
.= u1.(reproj(i,x).(a*x1)) + v1.(reproj(i,x).(a*x1)) by LOPBAN_1:1
.= (u1*reproj(i,x)).(a*x1) + v1.(reproj(i,x).(a*x1))
by FUNCT_2:15
.= (u1*reproj(i,x)).(a*x1) + (v1*reproj(i,x)).(a*x1)
by FUNCT_2:15
.= a*(u1*reproj(i,x)).x1 + (v1*reproj(i,x)).(a*x1)
by A4,LOPBAN_1:def 5
.= a*(u1*reproj(i,x)).x1 + a*(v1*reproj(i,x)).x1
by A4,LOPBAN_1:def 5
.= a*u1.(reproj(i,x).x1) + a*(v1*reproj(i,x)).x1 by FUNCT_2:15
.= a*u1.(reproj(i,x).x1) + a*v1.(reproj(i,x).x1) by FUNCT_2:15
.= a*(u1.(reproj(i,x).x1) + v1.(reproj(i,x).x1)) by RLVECT_1:def 5
.= a*L0.(reproj(i,x).x1) by LOPBAN_1:1
.= a*L.x1 by FUNCT_2:15;
end;
hence L0 * reproj(i,x) is LinearOperator of X.i,Y
by A5,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
hence thesis by Def3;
end;
hence thesis by Def6;
end;
for b be Real
for v be VECTOR of RealVectSpace(the carrier of product X,Y)
st v in W holds b * v in W
proof
let b be Real;
let v be VECTOR of RealVectSpace(the carrier of product X,Y) such that
A9: v in W;
reconsider v1=v as MultilinearOperator of X,Y by A9,Def6;
b*v is MultilinearOperator of X,Y
proof
reconsider L0=b*v as Function of product X,Y by FUNCT_2:66;
now
let i be Element of dom X,x be Point of product X;
reconsider L = L0 * reproj(i,x) as Function of X.i,Y;
A10: v1 * reproj(i,x) is LinearOperator of X.i,Y by Def3;
A11: for x1,x2 be Point of X.i holds L. (x1+x2) = L.x1 + L.x2
proof
let x1,x2 be Point of X.i;
thus L. (x1+x2) = L0.(reproj(i,x).(x1+x2)) by FUNCT_2:15
.= b*v1.(reproj(i,x).(x1+x2) ) by LOPBAN_1:2
.= b*(v1*reproj(i,x)).(x1+x2) by FUNCT_2:15
.= b*( (v1*reproj(i,x)).x1 + (v1*reproj(i,x)).x2)
by A10,VECTSP_1:def 20
.= b*(v1*reproj(i,x)).x1 + b*(v1*reproj(i,x)).x2 by RLVECT_1:def 5
.= b*v1.(reproj(i,x).x1) + b*(v1*reproj(i,x)).x2 by FUNCT_2:15
.= b*v1.(reproj(i,x).x1) + b*v1.(reproj(i,x).x2) by FUNCT_2:15
.= L0.(reproj(i,x).x1) + b*v1.(reproj(i,x).x2) by LOPBAN_1:2
.= L0.(reproj(i,x).x1) + L0.(reproj(i,x).x2) by LOPBAN_1:2
.= L.x1 + L0.(reproj(i,x).x2) by FUNCT_2:15
.= L.x1 + L.x2 by FUNCT_2:15;
end;
for z be Point of X.i, a be Real holds L.(a*z) = a * L.z
proof
let x1 be Point of X.i, a be Real;
thus L. (a*x1) = L0.(reproj(i,x).(a*x1)) by FUNCT_2:15
.= b * v1.(reproj(i,x).(a*x1)) by LOPBAN_1:2
.= b * (v1*reproj(i,x)).(a*x1) by FUNCT_2:15
.= b * (a*(v1*reproj(i,x)).x1) by A10,LOPBAN_1:def 5
.= (b*a) * (v1*reproj(i,x)).x1 by RLVECT_1:def 7
.= a * (b*(v1*reproj(i,x)).x1) by RLVECT_1:def 7
.= a * (b*v1.(reproj(i,x).x1)) by FUNCT_2:15
.= a * L0.(reproj(i,x).x1) by LOPBAN_1:2
.= a * L.x1 by FUNCT_2:15;
end;
hence L0 * reproj(i,x) is LinearOperator of X.i,Y
by A11,LOPBAN_1:def 5,VECTSP_1:def 20;
end;
hence thesis by Def3;
end;
hence thesis by Def6;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
end;
theorem
for X being RealNormSpace-Sequence,
Y be RealNormSpace
holds RLSStruct(# MultilinearOperators(X,Y),
Zero_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Add_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Mult_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)) #)
is Subspace of RealVectSpace(the carrier of product X,Y) by RSSPACE:11;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster RLSStruct(# MultilinearOperators(X,Y),
Zero_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Add_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Mult_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)) #)
-> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence by RSSPACE:11;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
func R_VectorSpace_of_MultilinearOperators(X,Y) -> strict RealLinearSpace
equals
RLSStruct (# MultilinearOperators(X,Y),
Zero_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Add_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)),
Mult_(MultilinearOperators(X,Y),
RealVectSpace(the carrier of product X,Y)) #);
coherence;
end;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster R_VectorSpace_of_MultilinearOperators(X,Y) -> constituted-Functions;
coherence by MONOID_0:80;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be Element of R_VectorSpace_of_MultilinearOperators(X,Y);
let v be VECTOR of product X;
redefine func f.v -> VECTOR of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as MultilinearOperator of X,Y by Def6;
f.v is VECTOR of Y;
hence thesis;
end;
end;
theorem Th16:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f,g,h be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y)
holds
h = f+g
iff
for x be VECTOR of product X holds h.x = f.x + g.x
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f,g,h be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y);
reconsider f9=f,g9=g,h9=h as MultilinearOperator of X,Y by Def6;
A1: R_VectorSpace_of_MultilinearOperators(X,Y) is Subspace of
RealVectSpace(the carrier of product X,Y) by RSSPACE:11; then
reconsider f1=f, h1=h, g1=g as VECTOR of
RealVectSpace(the carrier of product X,Y) by RLSUB_1:10;
A2: now
assume
A3: h = f+g;
let x be Element of product X;
h1 = f1+g1 by A1,A3,RLSUB_1:13;
hence h9.x=f9.x+g9.x by LOPBAN_1:1;
end;
now
assume for x be Element of product X holds h9.x = f9.x + g9.x; then
h1 = f1 + g1 by LOPBAN_1:1;
hence h = f + g by A1,RLSUB_1:13;
end;
hence thesis by A2;
end;
theorem Th17:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f,h be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y)
for a be Real
holds
h = a*f
iff
for x be VECTOR of product X holds h.x = a * f.x
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f,h be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y);
reconsider f9=f,h9=h as MultilinearOperator of X,Y by Def6;
let a be Real;
A1: R_VectorSpace_of_MultilinearOperators(X,Y)
is Subspace of RealVectSpace(the carrier of product X,Y)
by RSSPACE:11; then
reconsider f1=f,h1=h as VECTOR of
RealVectSpace(the carrier of product X,Y) by RLSUB_1:10;
A2: now
assume
A3: h = a * f;
let x be Element of product X;
h1 = a * f1 by A1,A3,RLSUB_1:14;
hence h9.x = a * f9.x by LOPBAN_1:2;
end;
now
assume for x be Element of product X holds h9.x = a * f9.x; then
h1 = a * f1 by LOPBAN_1:2;
hence h = a * f by A1,RLSUB_1:14;
end;
hence thesis by A2;
end;
theorem Th18:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
holds 0.R_VectorSpace_of_MultilinearOperators(X,Y)
= (the carrier of product X) --> 0.Y
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
A1: 0.RealVectSpace(the carrier of product X,Y)
= ((the carrier of product X) -->0.Y);
R_VectorSpace_of_MultilinearOperators(X,Y)
is Subspace of RealVectSpace(the carrier of product X,Y)
by RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
theorem Th19:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
holds (the carrier of product X) --> 0.Y is MultilinearOperator of X,Y
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
set f0 = (the carrier of product X) --> 0.Y;
now
let i be Element of dom X, u be Element of product X;
set F = f0 * reproj(i,u);
A1: dom F = the carrier of X.i by FUNCT_2:def 1;
A4: for z being object st z in dom F holds F.z = 0.Y
proof
let z being object;
assume z in dom F; then
A2: z in the carrier of X.i by FUNCT_2:def 1;
thus F.z = f0.(reproj (i,u).z) by A2,FUNCT_2:15
.= 0.Y by A2,FUNCT_2:5,FUNCOP_1:7;
end;
reconsider f = f0 * reproj(i,u) as Function of X.i,Y;
A5: f is homogeneous
proof
let x be VECTOR of X.i, r be Real;
thus f.(r*x) = r * 0.Y by A1,A4
.= r * f.x by A1,A4;
end;
now
let x,y be VECTOR of X.i;
thus f.(x+y) = 0.Y by A1,A4
.= f.x+0.Y by A1,A4
.= f.x+f.y by A1,A4;
end;
hence f0 * reproj(i,u) is LinearOperator of X.i,Y
by A5,VECTSP_1:def 20;
end;
hence thesis by Def3;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let IT be MultilinearOperator of X,Y;
let x be VECTOR of product X;
redefine func IT.x -> Point of Y; :: redefines . (FUNCT_1, definition)
correctness
proof
IT.x in the carrier of Y;
hence thesis;
end;
end;
registration
let X be RealNormSpace-Sequence;
cluster product X -> constituted-Functions;
coherence;
end;
definition
let X be RealNormSpace-Sequence;
let x be Point of product X;
let i be Element of dom X;
redefine func x.i -> Point of X.i; :: redefines . (FUNCT_1, definition)
correctness
proof
A1: product X = NORMSTR(# product carr X,zeros X,[:addop X:],[:multop X:],
productnorm X #) by PRVECT_2:6;
reconsider s = x as Element of product carr X by A1;
s.i is Point of X.i;
hence thesis;
end;
end;
EXTh10:
for G being RealNormSpace-Sequence holds
the carrier of product G = product carr G
proof
let G be RealNormSpace-Sequence;
product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
productnorm G #) by PRVECT_2:6;
hence thesis;
end;
theorem EXTh12:
for G be RealNormSpace-Sequence,
p,q,r be Point of product G
holds
p+q = r
iff
for i be Element of dom G holds r.i = p.i + q.i
proof
let G be RealNormSpace-Sequence, p,q,r be Point of product G;
reconsider p0 = p, q0 = q, r0 = r as Element of product carr G by EXTh10;
A2: product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:],
productnorm G #) by PRVECT_2:6;
hereby
assume
A3: p+q = r;
hereby
let i be Element of dom G;
reconsider i0=i as Element of dom carr G by LemmaX;
(addop G).i0 = the addF of (G.i0) by PRVECT_1:def 12;
hence r.i = p.i + q.i by A2,A3,PRVECT_1:def 8;
end;
end;
assume
A4: for i be Element of dom G holds r.i = p.i + q.i;
reconsider pq = p+q as Element of product carr G by EXTh10;
A5: ex g be Function
st pq = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
A6: ex g be Function
st r0 = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
now
let i0 be object;
assume
A7: i0 in dom pq; then
reconsider i1= i0 as Element of dom G by LemmaX,A5;
reconsider i = i0 as Element of dom carr G by A5,A7;
(addop G).i = the addF of (G.i) by PRVECT_1:def 12; then
pq.i0 = p0.i1 + q0.i1 by A2,PRVECT_1:def 8;
hence pq.i0 = r0.i0 by A4;
end;
hence p+q = r by A5,A6;
end;
theorem EXTh13:
for G be RealNormSpace-Sequence, p, r be Point of product G, a be Real
holds
a * p = r
iff
for i be Element of dom G holds r.i = a * (p.i)
proof
let G be RealNormSpace-Sequence,
p,r be Point of product G,
a be Real;
reconsider p0 = p, r0 = r as Element of product carr G by EXTh10;
hereby
assume
A1: a * p = r;
hereby
let i be Element of dom G;
reconsider i0 = i as Element of dom carr G by LemmaX;
A2: (multop G).i0 = the Mult of (G.i0) by PRVECT_2:def 8;
reconsider rr = a as Element of REAL by XREAL_0:def 1;
product G = NORMSTR(# product carr G,zeros G,[:addop G:],
[:multop G:], productnorm G #) by PRVECT_2:6;
hence r.i = rr * (p0.i) by A1,A2,PRVECT_2:def 2
.= a * (p.i);
end;
end;
assume
A3: for i be Element of dom G holds r.i = a * (p.i);
reconsider rp = a * p as Element of product carr G by EXTh10;
A4: ex g be Function
st rp = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
A5: ex g be Function
st r0 = g & dom g = dom carr G
& for i be object st i in dom carr G holds g.i in (carr G).i
by CARD_3:def 5;
now
let i0 be object;
assume
A6: i0 in dom rp; then
reconsider i1 = i0 as Element of dom G by A4,LemmaX;
reconsider i = i0 as Element of dom carr G by A4,A6;
A7: product G = NORMSTR(# product carr G,zeros G,[:addop G:],
[:multop G:], productnorm G #) by PRVECT_2:6;
reconsider a as Element of REAL by XREAL_0:def 1;
(multop G).i = the Mult of (G.i) by PRVECT_2:def 8; then
rp.i0 = a * (p0.i1) by A7,PRVECT_2:def 2;
hence rp.i0 = r0.i0 by A3;
end;
hence a * p = r by A4,A5;
end;
theorem
for G be RealNormSpace-Sequence,
p be Point of product G
holds
0.(product G) = p
iff
for i be Element of dom G holds p.i = 0.(G.i)
proof
let G be RealNormSpace-Sequence,
p be Point of product G;
reconsider p0 = p as Element of product carr G by EXTh10;
A1: dom carr G = dom G by LemmaX;
A2: product G = NORMSTR(# product carr G,zeros G,[:addop G:],
[:multop G:], productnorm G #) by PRVECT_2:6;
hence 0.(product G) = p
implies for i be Element of dom G holds p.i = 0.(G.i)
by A1,PRVECT_1:def 14;
assume
A3: for i be Element of dom G holds p.i = 0.(G.i);
now
let i0 be Element of dom carr G;
reconsider i = i0 as Element of dom G by LemmaX;
p0.i0 = 0.(G.i) by A3;
hence p0.i0 = 0.(G.i0);
end;
hence 0.(product G)=p by A2,PRVECT_1:def 14;
end;
theorem
for G be RealNormSpace-Sequence,
p,q,r be Point of product G
holds
p-q = r
iff
for i be Element of dom G holds r.i = p.i - q.i
proof
let G be RealNormSpace-Sequence,
p,q,r be Point of product G;
reconsider p0 = p, q0 = q, r0 = r as Element of product carr G by EXTh10;
reconsider qq0 = (-1)*q as Element of product carr G by EXTh10;
A2: p-q = p+(-1)*q by RLVECT_1:16;
hereby
assume
A3: p-q = r;
thus for i be Element of dom G holds r.i = p.i - q.i
proof
let i be Element of dom G;
A4: r0.i = p0.i + qq0.i by EXTh12,A3,A2;
qq0.i = (-1)*(q0.i) by EXTh13;
hence thesis by A4,RLVECT_1:16;
end;
end;
assume
A5: for i be Element of dom G holds r.i = p.i - q.i;
now
let i be Element of dom G;
A6: qq0.i = (-1)*(q0.i) by EXTh13;
r0.i = p0.i - q0.i by A5;
hence r0.i = p0.i + qq0.i by A6,RLVECT_1:16;
end;
hence p-q = r by A2,EXTh12;
end;
definition
let X be RealNormSpace-Sequence,
x be Point of product X;
func NrProduct x -> non negative Real means :DefNrPro:
ex Nx be FinSequence of REAL
st dom Nx = dom X
& (for i be Element of dom X holds Nx.i = ||.x.i.||)
& it = Product Nx;
existence
proof
product X = NORMSTR(# (product (carr X)),(zeros X),
[:(addop X):],[:(multop X):],(productnorm X) #)
by PRVECT_2:6; then
reconsider s = x as Element of product carr X;
defpred P1[object, object] means
ex i be Element of dom X
st $1 = i & $2=||.x.i.||;
A7: for n being Nat st n in Seg len X holds
ex d being Element of REAL st P1[n,d]
proof
let n be Nat;
assume n in Seg len X; then
reconsider i = n as Element of dom X by FINSEQ_1:def 3;
reconsider d = ||.x.i.|| as Element of REAL;
take d;
thus P1[n,d];
end;
consider F being FinSequence of REAL such that
A8: len F = len X
& for n being Nat st n in Seg len X holds
P1[n,F /. n] from FINSEQ_4:sch 1(A7);
A9: dom F = dom X by A8,FINSEQ_3:29;
A10: for i be Element of dom X holds F.i = ||.x.i.||
proof
let i be Element of dom X;
i in dom X; then
A11: i in Seg len X by FINSEQ_1:def 3;
reconsider n = i as Nat;
consider j be Element of dom X such that
A12: n = j & F/.n = ||.x.j.|| by A8,A11;
thus F.i = ||.x.i.|| by A9,A12,PARTFUN1:def 6;
end;
set R = Product F;
0 <= Product F
proof
per cases;
suppose
ex i be Nat st i in dom F & F.i = 0;
hence 0 <= Product F by RVSUM_1:103;
end;
suppose
A15: not ex i be Nat st i in dom F & F.i = 0;
for k being Element of NAT st k in dom F holds F . k > 0
proof
let k be Element of NAT;
assume
A17: k in dom F; then
A18: F.k <> 0 by A15;
reconsider i = k as Element of dom X by A8,FINSEQ_3:29,A17;
F.i = ||.x.i.|| by A10;
hence F.k > 0 by A18;
end;
hence 0 <= Product F by NAT_4:42;
end;
end;
then
reconsider R as non negative Real;
take R;
thus thesis by A9,A10;
end;
uniqueness
proof
let N1,N2 be non negative Real;
given Nx1 be FinSequence of REAL such that
A21: dom Nx1 = dom X
& (for i be Element of dom X holds Nx1.i = ||.x.i.||)
& N1 = Product Nx1;
given Nx2 be FinSequence of REAL such that
A22: dom Nx2 = dom X
& (for i be Element of dom X holds Nx2.i = ||.x.i.||)
& N2 = Product Nx2;
for i be Nat st i in dom Nx1 holds Nx1.i = Nx2.i
proof
let k be Nat;
assume k in dom Nx1; then
reconsider i = k as Element of dom X by A21;
Nx1.i = ||.x.i.|| by A21;
hence thesis by A22;
end; then
Nx1 = Nx2 by A21,A22;
hence thesis by A21,A22;
end;
end;
theorem
for X be RealNormSpace-Sequence,
x be Point of product X
holds
( (ex i be Element of dom X st x.i = 0.(X.i)) iff NrProduct x = 0 )
& ( not (ex i be Element of dom X st x.i = 0.(X.i)) implies 0 < NrProduct x )
proof
let X be RealNormSpace-Sequence,
x be Point of product X;
consider Nx be FinSequence of REAL such that
A1: dom Nx = dom X & (for i be Element of dom X holds Nx.i = ||.x.i.||) and
A2: NrProduct x = Product Nx by DefNrPro;
thus ( ex i be Element of dom X st x.i=0.(X.i) ) iff NrProduct x = 0
proof
hereby
assume ex i be Element of dom X st x.i=0.(X.i); then
consider i be Element of dom X such that
A3: x.i = 0.(X.i);
Nx.i = ||.0.(X.i).|| by A1,A3
.= 0;
hence NrProduct x = 0 by A1,A2,RVSUM_1:103;
end;
assume NrProduct x = 0; then
consider k be Nat such that
A5: k in dom Nx & Nx.k = 0 by A2,RVSUM_1:103;
reconsider i = k as Element of dom X by A1,A5;
||.x.i.|| = 0 by A1,A5; then
x.i = 0.(X.i) by NORMSP_0:def 5;
hence thesis;
end;
thus not (ex i be Element of dom X st x.i = 0.(X.i))
implies 0 < NrProduct x
proof
assume
A7: not ex i be Element of dom X st x.i=0.(X.i);
for k being Element of NAT st k in dom Nx holds Nx.k > 0
proof
let k be Element of NAT;
assume k in dom Nx; then
reconsider i = k as Element of dom X by A1;
A9: Nx.i = ||.x.i.|| by A1;
x.i <> 0.(X.i) by A7; then
Nx.k <> 0 by A9,NORMSP_0:def 5;
hence Nx.k > 0 by A9;
end;
hence 0 < NrProduct x by A2,NAT_4:42;
end;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let IT be MultilinearOperator of X,Y;
attr IT is Lipschitzian means :Def8:
ex K being Real
st 0 <= K
& for x being Point of product X
holds ||. IT.x .|| <= K * NrProduct x;
end;
theorem Th21:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f be MultilinearOperator of X,Y
st (for x be VECTOR of product X holds f.x = 0.Y)
holds f is Lipschitzian
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be MultilinearOperator of X,Y such that
A1: for x be VECTOR of product X holds f.x=0.Y;
A2: now
let x be VECTOR of product X;
thus ||. f.x .|| = ||. 0.Y .|| by A1
.= 0 * NrProduct x;
end;
take 0;
thus thesis by A2;
end;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster Lipschitzian for MultilinearOperator of X,Y;
existence
proof
set f = (the carrier of product X) --> 0.Y;
reconsider f as MultilinearOperator of X,Y by Th19;
take f;
for x be VECTOR of product X holds f. x = 0.Y by FUNCOP_1:7;
hence thesis by Th21;
end;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
func BoundedMultilinearOperators(X,Y) -> Subset of
R_VectorSpace_of_MultilinearOperators(X,Y) means :Def9:
for x being set holds x in it
iff
x is Lipschitzian MultilinearOperator of X,Y;
existence
proof
defpred P[object] means $1 is Lipschitzian MultilinearOperator of X,Y;
consider IT being set such that
A1: for x being object holds x in IT
iff x in MultilinearOperators(X,Y) & P[x] from XBOOLE_0:sch 1;
take IT;
for x be object st x in IT holds x in MultilinearOperators(X,Y) by A1;
hence IT is Subset of R_VectorSpace_of_MultilinearOperators(X,Y)
by TARSKI:def 3;
let x be set;
thus x in IT implies
x is Lipschitzian MultilinearOperator of X,Y by A1;
assume
A2: x is Lipschitzian MultilinearOperator of X,Y; then
x in MultilinearOperators(X,Y) by Def6;
hence thesis by A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of R_VectorSpace_of_MultilinearOperators(X,Y);
assume that
A3: for x being set holds x in X1
iff x is Lipschitzian MultilinearOperator of X,Y and
A4: for x being set holds x in X2
iff x is Lipschitzian MultilinearOperator of X,Y;
A5: X2 c= X1
proof
let x be object;
assume x in X2; then
x is Lipschitzian MultilinearOperator of X,Y by A4;
hence thesis by A3;
end;
X1 c= X2
proof
let x be object;
assume x in X1;
then x is Lipschitzian MultilinearOperator of X,Y by A3;
hence thesis by A4;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
end;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster BoundedMultilinearOperators(X,Y) -> non empty;
coherence
proof
set f = (the carrier of product X) --> 0.Y;
reconsider f as MultilinearOperator of X,Y by Th19;
for x be VECTOR of product X holds f.x = 0.Y by FUNCOP_1:7; then
f is Lipschitzian by Th21;
hence thesis by Def9;
end;
cluster BoundedMultilinearOperators(X,Y) -> linearly-closed;
coherence
proof
set W = BoundedMultilinearOperators(X,Y);
A1: for v,u be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y)
st v in W & u in W holds v + u in W
proof
let v,u be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y) such that
A2: v in W and
A3: u in W;
reconsider f = v+u as MultilinearOperator of X,Y by Def6;
f is Lipschitzian
proof
reconsider v1=v as Lipschitzian MultilinearOperator of X,Y by A2,Def9;
consider K2 be Real such that
A4: 0 <= K2 and
A5: for x being Point of product X
holds ||. v1.x .|| <= K2 * NrProduct x by Def8;
reconsider u1=u as Lipschitzian MultilinearOperator of X,Y by A3,Def9;
consider K1 be Real such that
A6: 0 <= K1 and
A7: for x being Point of product X
holds ||. u1.x .|| <= K1 * NrProduct x by Def8;
take K3 = K1+K2;
now
let x be VECTOR of product X;
A8: ||. u1.x + v1.x .||
<= ||. u1.x .|| + ||. v1.x .|| by NORMSP_1:def 1;
A9: ||. v1.x .|| <= K2 * NrProduct x by A5;
||. u1.x .|| <= K1 * NrProduct x by A7; then
A10: ||. u1.x .|| + ||. v1.x .||
<= K1 * NrProduct x + K2 * NrProduct x by A9,XREAL_1:7;
||. f.x .|| = ||. u1.x + v1.x .|| by Th16;
hence ||. f.x .|| <= K3 * NrProduct x by A8,A10,XXREAL_0:2;
end;
hence thesis by A4,A6;
end;
hence thesis by Def9;
end;
for a be Real
for v be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y)
st v in W
holds a * v in W
proof
let a be Real;
let v be VECTOR of R_VectorSpace_of_MultilinearOperators(X,Y) such that
A11: v in W;
reconsider f = a*v as MultilinearOperator of X,Y by Def6;
f is Lipschitzian
proof
reconsider v1=v as Lipschitzian MultilinearOperator of X,Y by A11,Def9;
consider K be Real such that
A12: 0 <= K and
A13: for x being Point of product X
holds ||. v1.x .|| <= K * NrProduct x by Def8;
take |.a.| * K;
A14: now
let x be VECTOR of product X;
0 <= |.a.| by COMPLEX1:46; then
A16: |.a.| * ||. v1.x .||
<= |.a.| * (K * NrProduct x) by A13,XREAL_1:64;
||. a * v1.x .|| = |.a.| * ||. v1.x .|| by NORMSP_1:def 1;
hence ||. f.x .|| <= (|.a.|* K) * NrProduct x by A16,Th17;
end;
0 <= |.a.| by COMPLEX1:46;
hence thesis by A12,A14;
end;
hence thesis by Def9;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
end;
theorem
for X being RealNormSpace-Sequence,
Y be RealNormSpace holds
RLSStruct (# BoundedMultilinearOperators(X,Y),
Zero_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Add_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Mult_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)) #)
is Subspace of R_VectorSpace_of_MultilinearOperators(X,Y)
by RSSPACE:11;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster RLSStruct(# BoundedMultilinearOperators(X,Y),
Zero_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Add_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Mult_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)) #) ->
Abelian add-associative right_zeroed
right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by RSSPACE:11;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
func R_VectorSpace_of_BoundedMultilinearOperators(X,Y) ->
strict RealLinearSpace equals
RLSStruct(# BoundedMultilinearOperators(X,Y),
Zero_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Add_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Mult_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)) #);
coherence;
end;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster -> Function-like Relation-like for Element of
R_VectorSpace_of_BoundedMultilinearOperators(X,Y);
coherence;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be Element of R_VectorSpace_of_BoundedMultilinearOperators(X,Y);
let v be VECTOR of product X;
redefine func f.v -> VECTOR of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as MultilinearOperator of X,Y by Def9;
f.v is VECTOR of Y;
hence thesis;
end;
end;
theorem Th24:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f,g,h be VECTOR of R_VectorSpace_of_BoundedMultilinearOperators(X,Y)
holds
h = f+g
iff
for x be VECTOR of product X
holds h.x = f.x + g.x
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f,g,h be VECTOR of R_VectorSpace_of_BoundedMultilinearOperators(X,Y);
A1: R_VectorSpace_of_BoundedMultilinearOperators(X,Y) is Subspace of
R_VectorSpace_of_MultilinearOperators(X,Y) by RSSPACE:11; then
reconsider f1 = f, h1=h, g1=g as VECTOR of
R_VectorSpace_of_MultilinearOperators(X,Y) by RLSUB_1:10;
hereby
assume
A2: h = f+g;
let x be Element of product X;
h1 = f1+g1 by A1,A2,RLSUB_1:13;
hence h.x = f.x+g.x by Th16;
end;
assume for x be Element of product X holds h.x = f.x+g.x; then
h1 = f1+g1 by Th16;
hence thesis by A1,RLSUB_1:13;
end;
theorem Th25:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f,h be VECTOR of R_VectorSpace_of_BoundedMultilinearOperators(X,Y)
for a be Real
holds
h = a * f
iff
for x be VECTOR of product X holds
h.x = a * f.x
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f,h be VECTOR of R_VectorSpace_of_BoundedMultilinearOperators(X,Y);
let a be Real;
A1: R_VectorSpace_of_BoundedMultilinearOperators(X,Y) is Subspace of
R_VectorSpace_of_MultilinearOperators(X,Y) by RSSPACE:11; then
reconsider f1=f, h1=h as VECTOR of
R_VectorSpace_of_MultilinearOperators(X,Y) by RLSUB_1:10;
hereby
assume
A2: h = a * f;
let x be Element of product X;
h1 = a * f1 by A1,A2,RLSUB_1:14;
hence h.x = a * f.x by Th17;
end;
assume for x be Element of product X holds h.x = a * f.x; then
h1 = a * f1 by Th17;
hence thesis by A1,RLSUB_1:14;
end;
theorem Th26:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
holds
0.R_VectorSpace_of_BoundedMultilinearOperators(X,Y)
= (the carrier of product X) --> 0.Y
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
A1: 0.R_VectorSpace_of_MultilinearOperators(X,Y)
= ((the carrier of product X) --> 0.Y) by Th18;
R_VectorSpace_of_BoundedMultilinearOperators(X,Y) is Subspace of
R_VectorSpace_of_MultilinearOperators(X,Y) by RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be object such that
A1: f in BoundedMultilinearOperators(X,Y);
func modetrans(f,X,Y) -> Lipschitzian MultilinearOperator of X,Y
equals
:Def11:
f;
coherence by A1,Def9;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let u be MultilinearOperator of X,Y;
func PreNorms(u) -> non empty Subset of REAL equals
{||.u.t .|| where t is VECTOR of product X :
for i be Element of dom X holds ||.t.i.|| <= 1 };
coherence
proof
A1: now
let x be object;
now
assume x in {||.u.t .|| where t is VECTOR of product X :
for i be Element of dom X holds ||.t.i.|| <= 1 };
then
ex t be VECTOR of product X
st x = ||.u.t .||
& for i be Element of dom X holds ||.t.i.|| <= 1;
hence x in REAL;
end;
hence x in {||.u.t .|| where t is VECTOR of product X :
for i be Element of dom X holds ||.t.i.|| <= 1 }
implies x in REAL;
end;
A2: product X = NORMSTR(# (product (carr X)),(zeros X),
[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
A3: dom X = dom carr X by LemmaX;
set x = 0.(product X);
reconsider s = x as Element of product carr X by A2;
for i be Element of dom X holds ||.x.i.|| <= 1
proof
let i be Element of dom X;
s.i = 0.(X.i) by A2,A3,PRVECT_1:def 14;
hence thesis;
end; then
||.u.x .|| in {||.u.t .|| where t is VECTOR of product X :
for i be Element of dom X holds ||.t.i.|| <= 1 };
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem
for X being RealNormSpace-Sequence,
s being Element of product X
ex F be FinSequence of REAL
st dom F = dom X
& for i be Element of dom X
holds F.i=||.s.i.||
proof
let X be RealNormSpace-Sequence,
s be Element of product X;
defpred P1[object, object] means
ex i be Element of dom X
st $1 = i & $2 = ||.s.i.||;
A5: for n being Nat st n in Seg len X holds
ex d being Element of REAL st P1[n,d]
proof
let n be Nat;
assume n in Seg len X; then
reconsider i = n as Element of dom X by FINSEQ_1:def 3;
reconsider d = ||.s.i.|| as Element of REAL;
take d;
thus P1[n,d];
end;
consider F being FinSequence of REAL such that
A6: len F = len X
& for n being Nat st n in Seg len X holds
P1[n,F /. n] from FINSEQ_4:sch 1(A5);
take F;
thus
A7: dom F = dom X by A6,FINSEQ_3:29;
thus for i be Element of dom X holds F.i=||.s.i.||
proof
let i be Element of dom X;
i in dom X; then
A8: i in Seg len X by FINSEQ_1:def 3;
reconsider n = i as Nat;
consider j be Element of dom X such that
A9: n = j & F/.n = ||.s.j.|| by A6,A8;
thus F.i = ||.s.i.|| by A7,A9,PARTFUN1:def 6;
end;
end;
theorem LM281:
for F be FinSequence of REAL
st for i be Element of dom F holds 0 <= F.i & F.i <= 1
holds 0 <= Product F & Product F <= 1
proof
let F be FinSequence of REAL;
assume
A1: for i be Element of dom F holds 0 <= F.i & F.i <= 1;
per cases;
suppose
ex i be Nat st i in dom F & F.i = 0;
hence 0 <= Product F & Product F <= 1 by RVSUM_1:103;
end;
suppose
A2: not ex i be Nat st i in dom F & F.i = 0;
A3: for k being Element of NAT st k in dom F holds F . k > 0
proof
let k be Element of NAT;
assume
A4: k in dom F;
F.k <> 0 by A2,A4;
hence F.k > 0 by A1,A4;
end;
hence 0 <= Product F by NAT_4:42;
1 is Element of REAL by XREAL_0:def 1; then
reconsider G = (len F) |-> 1 as FinSequence of REAL by FINSEQ_2:63;
A6: len G = len F by CARD_1:def 7;
for k being Element of NAT st k in dom F holds F.k <= G.k & F.k > 0
proof
let k being Element of NAT;
assume
A7: k in dom F;
A9: k in Seg len F by A7,FINSEQ_1:def 3;
F.k <= 1 by A1,A7;
hence F.k <= G.k by A9,FINSEQ_2:57;
thus thesis by A3,A7;
end; then
Product F <= Product G by A6,NAT_4:54;
hence Product F <= 1 by RVSUM_1:102;
end;
end;
theorem LM28:
for X being RealNormSpace-Sequence,
x being Point of product X
st ( for i be Element of dom X holds ||.x.i.|| <= 1 )
holds 0 <= NrProduct x & NrProduct x <= 1
proof
let X be RealNormSpace-Sequence,
x be Point of product X;
assume
A1: for i be Element of dom X holds ||.x.i.|| <= 1;
consider F be FinSequence of REAL such that
A2: dom F = dom X
& ( for i be Element of dom X holds F.i = ||.x.i.|| )
& NrProduct x = Product F by DefNrPro;
for i be Element of dom F holds 0 <= F.i & F.i <= 1
proof
let i be Element of dom F;
reconsider j = i as Element of dom X by A2;
A3: F.j = ||.x.j.|| by A2;
thus 0 <= F.i by A3;
thus F.i <= 1 by A1,A3;
end;
hence 0 <= NrProduct x & NrProduct x <= 1 by A2,LM281;
end;
LM31:
for F be FinSequence of REAL
st for i be Element of dom F holds F.i > 0
holds Product F > 0
proof
let F be FinSequence of REAL;
assume for i be Element of dom F holds F.i > 0; then
for j be Element of NAT st j in dom F holds F.j > 0;
hence Product F > 0 by NAT_4:42;
end;
theorem LM32:
for X being RealNormSpace-Sequence,
Y be RealNormSpace,
g be MultilinearOperator of X,Y,
t be Point of product X
st ex i be Element of dom X st t.i = 0.(X.i)
holds g.t = 0.Y
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace,
g be MultilinearOperator of X,Y,
t be Point of product X;
given i be Element of dom X such that
A2: t.i = 0.(X.i);
A6: (g * reproj(i,t)).( 0.(X.i) )
= g.(reproj(i,t).( 0.(X.i) )) by FUNCT_2:15
.= g.t by A2,Th4X;
g * reproj(i,t) is LinearOperator of X.i,Y by Def3;
hence g.t = 0.Y by A6,LOPBAN_7:3;
end;
theorem LM34:
for X being RealNormSpace-Sequence,
x be Point of product X
ex d be FinSequence of REAL
st dom d = dom X
& for i be Element of dom X holds d.i = ||.x.i.||"
proof
let X be RealNormSpace-Sequence,
x be Point of product X;
defpred P1[object, object] means
ex i be Element of dom X
st $1 = i & $2=||.x.i.||";
A4: for n being Nat st n in Seg len X holds
ex d being Element of REAL st P1[n,d]
proof
let n be Nat;
assume n in Seg len X; then
reconsider i = n as Element of dom X by FINSEQ_1:def 3;
reconsider d = ||.x.i.||" as Element of REAL by XREAL_0:def 1;
take d;
thus P1[n,d];
end;
consider F being FinSequence of REAL such that
A5: len F = len X
& for n being Nat st n in Seg len X holds
P1[n,F /. n] from FINSEQ_4:sch 1(A4);
take F;
thus
A6: dom F = dom X by A5,FINSEQ_3:29;
thus for i be Element of dom X holds F.i = ||.x.i.||"
proof
let i be Element of dom X;
i in dom X; then
A7: i in Seg len X by FINSEQ_1:def 3;
reconsider n = i as Nat;
consider j be Element of dom X such that
A8: n = j & F/.n = ||.x.j.||" by A5,A7;
thus F.i = ||.x.i.||" by A6,A8,PARTFUN1:def 6;
end;
end;
theorem LM33:
for X being RealNormSpace-Sequence,
s be Point of product X,
a be FinSequence of REAL
ex s1 be Point of product X
st for i be Element of dom X holds s1.i = (a/.i) * s.i
proof
let X be RealNormSpace-Sequence,
x be Point of product X,
a be FinSequence of REAL;
A4: dom carr X = dom X by LemmaX;
defpred P1[object, object] means
ex i be Element of dom X
st $1 = i & $2=a/.i * x.i;
A5: for n being Nat st n in Seg len X holds
ex d being object st P1[n,d]
proof
let n be Nat;
assume n in Seg len X; then
reconsider i=n as Element of dom X by FINSEQ_1:def 3;
reconsider d = a/.i * x.i as Element of X.i;
take d;
thus P1[n,d];
end;
consider F being FinSequence such that
A6: dom F = Seg len X
& for n being Nat st n in Seg len X holds
P1[n,F . n] from FINSEQ_1:sch 1(A5);
A7: dom F = dom carr X by A4,A6,FINSEQ_1:def 3;
for y being object st y in dom carr X holds F.y in (carr X).y
proof
let y be object;
assume
A8: y in dom carr X; then
reconsider n = y as Nat;
consider i be Element of dom X such that
A9: n = i & F.n = a/.i * x.i by A6,A7,A8;
F.n in the carrier of (X.i) by A9;
hence F.y in (carr X).y by A9,PRVECT_1:def 11;
end; then
reconsider F as Element of product carr X by A7,CARD_3:def 5;
reconsider F as Element of product X by EXTh10;
take F;
thus for i be Element of dom X holds F.i = a/.i * x.i
proof
let i be Element of dom X;
i in dom X; then
A10: i in Seg len X by FINSEQ_1:def 3;
set n = i;
consider j be Element of dom X such that
A11: n = j & F.n = a/.j * x.j by A6,A10;
thus F.i = a/.i* x.i by A11;
end;
end;
theorem LM35:
for X being RealNormSpace-Sequence,
Y being RealNormSpace,
g be MultilinearOperator of X,Y,
a be FinSequence of REAL
st dom a = dom X
holds
for t,t1 be Point of product X
st for i be Element of dom X holds t1.i= (a/.i) * t.i
holds g.t1 = (Product a) * g.t
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace,
g be MultilinearOperator of X,Y,
a be FinSequence of REAL;
assume
A1: dom a = dom X;
A4: dom carr X = dom X by LemmaX;
A5: product X = NORMSTR(# (product (carr X)),(zeros X),
[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
defpred P[Nat] means
for t,t1 be Point of product X,
b be FinSequence of REAL
st b = a | $1 & $1 <= len a
& ( for i be Element of dom X holds
( ( i in Seg $1 implies t1.i= (a/.i) * t.i )
& ( not i in Seg $1 implies t1.i= t.i )))
holds
g.t1 = (Product b) * g.t;
A6: P[0]
proof
let t,t1 be Point of product X,
b be FinSequence of REAL;
assume
A7: b = a | 0 & 0 <= len a
& for i be Element of dom X holds
( ( i in Seg 0 implies t1.i = (a/.i) * t.i )
& ( not i in Seg 0 implies t1.i = t.i ) );
A10: ex g being Function
st t1 = g
& dom g = dom carr X
& for y being object st y in dom carr X holds
g.y in (carr X).y by A5,CARD_3:def 5;
A11: ex g being Function
st t = g
& dom g = dom carr X
& for y being object st y in dom carr X holds
g.y in (carr X).y by A5,CARD_3:def 5;
t1 = t by A4,A7,A10,A11;
hence g.t1 = (Product b) * g.t by A7,RLVECT_1:def 8,RVSUM_1:94;
end;
A15: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A16: P[k];
let t,t1 be Point of product X, b be FinSequence of REAL;
assume
A17: b = a | (k+1) & (k+1) <= len a
& for i be Element of dom X holds
( ( i in Seg (k+1) implies t1.i = (a/.i) * t.i )
& ( not i in Seg (k+1) implies t1.i = t.i ) );
reconsider b2 = a | k as FinSequence of REAL;
A18: k <= k+1 by NAT_1:11;
1 <= k+1 <= len a by A17,NAT_1:11; then
B19: k+1 in Seg len a; then
A20: k+1 in dom a by FINSEQ_1:def 3;
A22: b2 = b|k by A17,FINSEQ_1:82,NAT_1:11;
A23: b = b2 ^ <*b.(k+1)*> by A17,A22,FINSEQ_1:59,FINSEQ_3:55
.= b2 ^ <*a.(k+1)*> by A17,FINSEQ_1:4,FUNCT_1:49
.= b2 ^ <*a/.(k+1)*> by A20,PARTFUN1:def 6;
defpred LP1[object] means $1 in Seg k;
deffunc F1(Element of dom X) = a/.$1 * t.$1;
deffunc F2(Element of dom X) = t.$1;
consider s2 be Function such that
A25: dom s2 = dom X
& for i being Element of dom X holds
( LP1[i] implies s2. i = F1(i) )
& ( not LP1[i] implies s2. i = F2(i) ) from PARTFUN1:sch 4;
for y being object st y in dom carr X holds s2.y in (carr X).y
proof
let y be object;
assume y in dom carr X; then
reconsider i = y as Element of dom X by LemmaX;
per cases;
suppose
LP1[i]; then
s2.y = a/.i * t.i by A25; then
s2.y in the carrier of (X.i);
hence s2.y in (carr X).y by PRVECT_1:def 11;
end;
suppose
not LP1[i]; then
s2.y = t.i by A25; then
s2.y in the carrier of (X.i);
hence s2.y in (carr X). y by PRVECT_1:def 11;
end;
end; then
reconsider s2 as Element of product carr X by A4,A25,CARD_3:def 5;
reconsider t2 = s2 as Point of product X by A5;
reconsider k1 = k+1 as Element of dom X by A1,B19,FINSEQ_1:def 3;
k + 0 < k +1 by XREAL_1:8; then
not k1 in Seg k by FINSEQ_1:1; then
A29: s2.k1 = t.k1 by A25;
A30: g * reproj(k1,t2) is LinearOperator of X.k1,Y by Def3;
set RK = reproj (k1,t2).( (a/.k1) * t.k1 );
A31: ex g being Function
st t1 = g
& dom g = dom carr X
& for y being object st y in dom carr X holds
g.y in (carr X).y by A5,CARD_3:def 5;
A32: ex g being Function
st RK = g
& dom g = dom carr X
& for y being object st y in dom carr X holds
g.y in (carr X).y by A5,CARD_3:def 5;
reconsider RK as Function;
for x be object st x in dom t1 holds t1.x = RK.x
proof
let x be object;
assume x in dom t1; then
reconsider i = x as Element of dom X by LemmaX,A31;
A37: ( i in Seg k implies s2.i = (a/.i) * t.i )
& ( not i in Seg k implies s2.i = t.i ) by A25;
per cases;
suppose
A40:i in Seg(k+1);
per cases;
suppose
A42: i = k+1; then
RK.i = (a/.k1) * t.k1 by Th3
.= t1.i by A17,A40,A42;
hence t1.x = RK.x;
end;
suppose
A43: i <> k+1; then
A44: RK.i = s2.i by Th4;
1 <= i <= k+1 by A40,FINSEQ_1:1; then
1 <= i & i < k+1 by A43,XXREAL_0:1; then
1 <= i <= k by NAT_1:13;
hence t1.x = RK.x by A17,A37,A40,A44;
end;
end;
suppose
A45: not i in Seg(k+1);
A46: 1 <= i <= len X by FINSEQ_3:25;
A48: k+1 < i by A45,A46; then
A49: RK.i = s2.i by Th4;
k <= k+1 by NAT_1:11; then
k < i by A48,XXREAL_0:2;
hence t1.x = RK.x by A17,A37,A45,A49,FINSEQ_1:1;
end;
end; then
A50: t1 = reproj (k1,t2).( (a/.k1) * t.k1 ) by A31,A32;
A53: g.t1 = ( g*reproj (k1,t2)).((a/.k1) * t.k1) by A50,FUNCT_2:15
.= (a/.k1) * ( g * reproj(k1,t2) ).(t.k1) by A30,LOPBAN_1:def 5
.= (a/.(k+1)) * ( g.((reproj (k1,t2)).(t.k1)) ) by FUNCT_2:15
.= (a/.(k+1)) * g.t2 by A29,Th4X;
thus g.t1
= (a/.(k+1)) * ((Product b2 ) * g.t) by A16,A17,A18,A25,A53,XXREAL_0:2
.= ((a/.(k+1)) * (Product b2 ))* g.t by RLVECT_1:def 7
.= (Product b) * g.t by A23,RVSUM_1:96;
end;
A54: for k be Nat holds P[k] from NAT_1:sch 2(A6,A15);
let t,t1 be Point of product X;
assume
A55: for i be Element of dom X holds t1.i = (a/.i) * t.i;
set b = a | len a;
A56: b = a & len a <= len a by FINSEQ_2:20;
for i be Element of dom X holds
( i in Seg len a implies t1.i = (a/.i) * t.i )
& ( not i in Seg len a implies t1.i = t.i )
proof
let i be Element of dom X;
thus i in Seg len a implies t1.i = (a/.i) * t.i by A55;
thus not i in Seg len a implies t1.i = t.i
proof
assume not i in Seg len a; then
not i in dom X by A1,FINSEQ_1:def 3;
hence t1.i = t.i;
end;
end;
hence g.t1 = (Product a) * g.t by A54,A56;
end;
LM36A:
for F,G be FinSequence of REAL
st len F = len G
& ( for i being Element of NAT st i in dom F holds G.i = (F.i)" )
holds Product G = (Product F)"
proof
let f1,f2 be FinSequence of REAL;
defpred P[Nat] means
for f1,f2 being FinSequence of REAL
st len f1 = len f2 & $1 = len f1
& (for k being Element of NAT st k in dom f1
holds f2.k = (f1.k)")
holds Product f2 = (Product f1)";
assume
A1: len f1 = len f2;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
for f1,f2 being FinSequence of REAL
st len f1 = len f2 & n+1 = len f1
& (for k being Element of NAT st k in dom f1 holds f2.k =(f1.k)" )
holds Product f2 = ( Product f1 )"
proof
let f1,f2 be FinSequence of REAL;
assume that
A4: len f1 = len f2 and
A5: n+1 = len f1;
consider g2 be FinSequence of REAL, r2 be Element of REAL such that
A6: f2 = g2^<*r2*> by A4,A5,FINSEQ_2:19;
len f2 = len g2 + len <* r2 *> by A6,FINSEQ_1:22; then
A7: n+1 = len g2 + 1 by A4,A5,FINSEQ_1:39;
A8: Product f2 = (Product g2) * r2 by A6,RVSUM_1:96;
consider g1 be FinSequence of REAL, r1 be Element of REAL such that
A9: f1 = g1^<*r1*> by A5,FINSEQ_2:19;
set k1 = len g1+1;
A10: Product f1 = (Product g1) * r1 by A9,RVSUM_1:96;
len f1 = len g1 + len <* r1 *> by A9,FINSEQ_1:22; then
A11: n+1 = len g1 + 1 by A5,FINSEQ_1:39;
assume
A12: for k being Element of NAT st k in dom f1 holds f2.k = (f1.k)";
A13: now
let k be Element of NAT;
A14: dom g1 c= dom f1 by A9,FINSEQ_1:26;
assume
A15: k in dom g1; then
k in Seg len g2 by A7,A11,FINSEQ_1:def 3; then
k in dom g2 by FINSEQ_1:def 3; then
A16: f2.k = g2.k by A6,FINSEQ_1:def 7;
f1.k = g1.k by A9,A15,FINSEQ_1:def 7;
hence g2.k = (g1.k)" by A12,A14,A15,A16;
end;
A17: Product g2 = ( Product g1) " by A3,A7,A11,A13;
n+1 >= 0+1 by XREAL_1:6; then
k1 in Seg (n+1) by A11; then
k1 in dom f1 by A5,FINSEQ_1:def 3; then
A19: f2.k1 = (f1.k1)" by A12;
r1 = f1.k1 & r2 = f2.k1 by A6,A7,A9,A11,FINSEQ_1:42;
hence Product f2 = (Product f1)" by A8,A10,A17,A19,XCMPLX_1:204;
end;
hence thesis;
end;
A21: P[0]
proof
let f1,f2 be FinSequence of REAL;
assume len f1 = len f2 & 0 = len f1
& (for k being Element of NAT st k in dom f1
holds f2.k = (f1.k)"); then
f1 = {} & f2 = {};
hence Product f2 = (Product f1)" by RVSUM_1:94;
end;
A25: for n being Nat holds P[n] from NAT_1:sch 2(A21,A2);
assume for k being Element of NAT st k in dom f1 holds f2.k = (f1.k)";
hence thesis by A1,A25;
end;
theorem LM36:
for F,G be FinSequence of REAL
st dom F = dom G
& ( for i being Element of dom F holds G.i = (F.i)" )
holds Product G = (Product F)"
proof
let F,G be FinSequence of REAL;
assume that
A1: dom F = dom G and
A2: for i being Element of dom F holds G.i = (F.i)";
A3: len F = len G by A1,FINSEQ_3:29;
for i being Element of NAT st i in dom F holds G.i = (F.i)" by A2;
hence thesis by A3,LM36A;
end;
theorem Th27:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for g be Lipschitzian MultilinearOperator of X,Y
holds PreNorms(g) is bounded_above
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let g be Lipschitzian MultilinearOperator of X,Y;
consider K be Real such that
A1: 0 <= K and
A2: for x being Point of product X
holds ||. g.x .|| <= K * NrProduct x by Def8;
take K;
let r be ExtReal;
assume r in PreNorms(g); then
consider t be VECTOR of product X such that
A3: r = ||. g.t .|| and
A4: for i be Element of dom X holds ||. t.i .|| <= 1;
A5: ||.g.t.|| <= K*NrProduct t by A2;
0 <= NrProduct t & NrProduct t <= 1 by A4,LM28; then
K * NrProduct t <= K * 1 by A1,XREAL_1:64;
hence r <=K by A3,A5,XXREAL_0:2;
end;
theorem
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for g be MultilinearOperator of X,Y
holds g is Lipschitzian iff PreNorms(g) is bounded_above
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let g be MultilinearOperator of X,Y;
now
reconsider K = upper_bound PreNorms(g) as Real;
assume
A1: PreNorms(g) is bounded_above;
A2: now
let t be VECTOR of product X;
consider F be FinSequence of REAL such that
A3: dom F = dom X
& ( for i be Element of dom X holds F.i = ||.t.i.|| )
& NrProduct t = Product F by DefNrPro;
now
per cases;
suppose
ex i be Element of dom X st t.i = 0.(X.i); then
consider i be Element of dom X such that
A6: t.i = 0.(X.i);
A7: F.i = ||.t.i.|| by A3;
F.i = 0 by A6,A7; then
A10: Product F = 0 by A3,RVSUM_1:103;
g.t = 0.Y by A6,LM32;
hence ||.g.t.|| <= K * NrProduct t by A3,A10;
end;
suppose
A11: not ex i be Element of dom X st t.i = 0.(X.i);
A12: for i be Element of dom F holds F.i > 0
proof
let i be Element of dom F;
reconsider j = i as Element of dom X by A3;
A13: F.j = ||. t.j .|| by A3;
t.j <> 0.(X.j) by A11; then
F.j <> 0 by A13,NORMSP_0:def 5;
hence thesis by A13;
end;
A15: 0 < Product F by A12,LM31;
consider d be FinSequence of REAL such that
A16: dom d = dom X
& for i be Element of dom X holds d.i= ||.t.i.||" by LM34;
consider t1 be Element of product X such that
A17: for i be Element of dom X holds t1.i= ( d/.i) * t.i
by LM33;
A18: (Product d) * g.t = g.t1 by A16,A17,LM35;
A22: for i be Element of dom F holds d.i = (F.i)"
proof
let i be Element of dom F;
reconsider j = i as Element of dom X by A3;
d.j = ||.t.j.||" by A16;
hence thesis by A3;
end;
A23: |. (Product d) .| * ||.g.t.|| = ||.g.t1.|| by A18,NORMSP_1:def 1;
|. (Product F)" .| = |. 1*(Product F)" .|
.= |. 1/(Product F) .| by XCMPLX_0:def 9
.= 1 / (Product F) by A15,ABSVALUE:def 1; then
A25: |. (Product d) .| * ||.g.t.||
= (1/(Product F)) * ||.g.t.|| by A3,A16,A22,LM36
.= ||.g.t.||/ Product F by XCMPLX_1:99;
A26: for i be Element of dom X holds ||.t1.i.|| <= 1
proof
let i be Element of dom X;
A27: d.i = ||.t.i.||" by A16;
A28: t1.i = (d/.i) * t.i by A17;
t.i <> 0.(X.i) by A11; then
A29: ||.t.i.|| <> 0 by NORMSP_0:def 5;
||.t1.i.|| = |.d/.i.| * ||.t.i.|| by A28,NORMSP_1:def 1
.= |. ||.t.i.||" .| * ||.t.i.|| by A16,A27,PARTFUN1:def 6
.= ||.t.i.||" * ||.t.i.|| by ABSVALUE:def 1
.= 1 by A29,XCMPLX_0:def 7;
hence thesis;
end;
||.g.t1.|| in {||.g.t .|| where t is VECTOR of product X :
for i be Element of dom X holds ||.t.i.|| <= 1 } by A26; then
||.g.t.|| / Product F <= K by A1,A23,A25,SEQ_4:def 1; then
||.g.t.|| / Product F * Product F <= K * Product F
by A15,XREAL_1:64;
hence ||.g.t.|| <= K * NrProduct t by A3,A15,XCMPLX_1:87;
end;
end;
hence ||.g.t .|| <= K *NrProduct t;
end;
take K;
0 <= K
proof
consider r0 be object such that
A30: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A30;
now
let r be Real;
assume r in PreNorms(g); then
ex t be VECTOR of product X st r = ||. g.t .||
& for i be Element of dom X holds ||.t.i.|| <= 1;
hence 0 <= r;
end; then
0 <= r0 by A30;
hence thesis by A1,A30,SEQ_4:def 1;
end;
hence g is Lipschitzian by A2;
end;
hence thesis by Th27;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
func BoundedMultilinearOperatorsNorm(X,Y)
-> Function of BoundedMultilinearOperators(X,Y),REAL means :Def13:
for x be object st x in BoundedMultilinearOperators(X,Y)
holds it.x = upper_bound PreNorms(modetrans(x,X,Y));
existence
proof
deffunc F(object) = upper_bound PreNorms(modetrans($1,X,Y));
A1: for z be object st z in BoundedMultilinearOperators(X,Y)
holds F(z) in REAL by XREAL_0:def 1;
thus ex f being Function of BoundedMultilinearOperators(X,Y),REAL
st for x being object st x in BoundedMultilinearOperators(X,Y)
holds f.x = F(x) from FUNCT_2:sch 2(A1);
end;
uniqueness
proof
let NORM1,NORM2 be Function of BoundedMultilinearOperators(X,Y),REAL
such that
A2: for x be object st x in BoundedMultilinearOperators(X,Y)
holds NORM1.x = upper_bound PreNorms(modetrans(x,X,Y)) and
A3: for x be object st x in BoundedMultilinearOperators(X,Y)
holds NORM2.x = upper_bound PreNorms(modetrans(x,X,Y));
A4: for z be object st z in BoundedMultilinearOperators(X,Y)
holds NORM1.z = NORM2.z
proof
let z be object; assume
A5: z in BoundedMultilinearOperators(X,Y); then
NORM1.z = upper_bound PreNorms(modetrans(z,X,Y)) by A2;
hence thesis by A3,A5;
end;
dom NORM1 = BoundedMultilinearOperators(X,Y) by FUNCT_2:def 1;
hence thesis by A4,FUNCT_2:def 1;
end;
end;
Th29:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f be Lipschitzian MultilinearOperator of X,Y
holds modetrans(f,X,Y) = f
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be Lipschitzian MultilinearOperator of X,Y;
f in BoundedMultilinearOperators(X,Y) by Def9;
hence thesis by Def11;
end;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be Lipschitzian MultilinearOperator of X,Y;
reduce modetrans(f,X,Y) to f;
reducibility by Th29;
end;
theorem Th30:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f be Lipschitzian MultilinearOperator of X,Y
holds BoundedMultilinearOperatorsNorm(X,Y).f = upper_bound PreNorms(f)
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be Lipschitzian MultilinearOperator of X,Y;
reconsider f9 = f as set;
f in BoundedMultilinearOperators(X,Y) by Def9;
hence BoundedMultilinearOperatorsNorm(X,Y).f
= upper_bound PreNorms(modetrans(f9,X,Y)) by Def13
.= upper_bound PreNorms(f);
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
func R_NormSpace_of_BoundedMultilinearOperators(X,Y)
-> non empty strict NORMSTR equals
NORMSTR(# BoundedMultilinearOperators(X,Y),
Zero_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Add_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Mult_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
BoundedMultilinearOperatorsNorm(X,Y) #);
coherence;
end;
theorem Th31:
for X being RealNormSpace-Sequence,
Y be RealNormSpace holds
(the carrier of product X) --> 0.Y
= 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y)
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
((the carrier of product X) --> 0.Y)
= 0.R_VectorSpace_of_BoundedMultilinearOperators(X,Y) by Th26
.= 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y);
hence thesis;
end;
theorem Th32:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f being Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
for g be Lipschitzian MultilinearOperator of X,Y st g = f
holds
for t be VECTOR of product X holds ||. g.t .|| <= ||.f.|| * NrProduct t
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y);
let g be Lipschitzian MultilinearOperator of X,Y such that
A1: g = f;
A2: PreNorms(g) is non empty bounded_above by Th27;
now
let t be VECTOR of product X;
consider F be FinSequence of REAL such that
A3: dom F = dom X
& ( for i be Element of dom X holds F.i = ||.t.i.|| )
& NrProduct t = Product F by DefNrPro;
now
per cases;
suppose
ex i be Element of dom X st t.i = 0.(X.i); then
consider i be Element of dom X such that
A7: t.i = 0.(X.i);
F.i = ||.0.(X.i).|| by A3,A7
.= 0; then
A9: Product F = 0 by A3,RVSUM_1:103;
g.t = 0.Y by A7,LM32;
hence ||.g.t.|| <= ||.f.|| * NrProduct t by A3,A9;
end;
suppose
A10: for i be Element of dom X holds t.i <> 0.(X.i);
for i be Element of dom F holds F.i > 0
proof
let i be Element of dom F;
reconsider j=i as Element of dom X by A3;
A12: F.j = ||.t.j.|| by A3;
t.j <> 0.(X.j) by A10; then
F.j <> 0 by A12,NORMSP_0:def 5;
hence thesis by A12;
end; then
A13: 0 < Product F by LM31;
consider d be FinSequence of REAL such that
A14: dom d = dom X
& for i be Element of dom X holds d.i= ||.t.i.||" by LM34;
consider t1 be Element of product X such that
A15: for i be Element of dom X holds t1.i= ( d/.i) * t.i
by LM33;
A16: for i be Element of dom X holds ||.t1.i.|| <= 1
proof
let i be Element of dom X;
A17: d.i= ||.t.i.||" by A14;
A18:t1.i= ( d/.i) * t.i by A15;
t.i <> 0.(X.i) by A10; then
A19: ||.t.i.|| <> 0 by NORMSP_0:def 5;
||.t1.i.|| = |.d/.i.| * ||.t.i.|| by A18,NORMSP_1:def 1
.= |. ||.t.i.||" .| * ||.t.i.|| by A14,A17,PARTFUN1:def 6
.= ||.t.i.||" * ||.t.i.|| by ABSVALUE:def 1
.= 1 by A19,XCMPLX_0:def 7;
hence thesis;
end;
A20: (Product d)* g.t = g.t1 by A14,A15,LM35;
A23: for i be Element of dom F holds d.i = (F.i)"
proof
let i be Element of dom F;
reconsider j=i as Element of dom X by A3;
d.i = ||.t.j.||" by A14;
hence thesis by A3;
end;
A24: |. (Product d) .| * ||.g.t.|| = ||.g.t1.||
by A20,NORMSP_1:def 1;
A25: |. (Product F)".| = |. 1*(Product F)".|
.= |. 1/(Product F) .| by XCMPLX_0:def 9
.= 1 / (Product F) by A13,ABSVALUE:def 1;
A26: |. (Product d) .| * ||.g.t.||
= (1/(Product F)) * ||.g.t.|| by A3,A14,A23,A25,LM36
.= ||.g.t.||/ Product F by XCMPLX_1:99;
||.g.t1.|| in {||.g.t .|| where t is VECTOR of product X :
for i be Element of dom X holds ||.t.i.|| <= 1 } by A16; then
||.g.t.||/ Product F <= upper_bound PreNorms(g)
by A2,A24,A26,SEQ_4:def 1; then
A28: ||.g.t.||/( Product F) <= ||.f.|| by A1,Th30;
||.g.t.|| / (Product F) * (Product F) =||.g.t.|| by A13,XCMPLX_1:87;
hence ||.g.t.|| <= ||.f.||*NrProduct t by A3,A28,XREAL_1:64;
end;
end;
hence ||.g.t.|| <= ||.f.||*NrProduct t;
end;
hence thesis;
end;
theorem Th33:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f being Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
holds 0 <= ||.f.||
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y);
reconsider g = f as Lipschitzian MultilinearOperator of X,Y by Def9;
consider r0 be object such that
A1: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A1;
A2: PreNorms(g) is non empty bounded_above by Th27;
A3: BoundedMultilinearOperatorsNorm(X,Y).f = upper_bound PreNorms(g)
by Th30;
now
let r be Real;
assume r in PreNorms(g); then
ex t be VECTOR of product X
st r = ||.g.t .||
& for i be Element of dom X holds ||.t.i.|| <= 1;
hence 0 <= r;
end; then
0 <= r0 by A1;
hence thesis by A1,A2,A3,SEQ_4:def 1;
end;
theorem Th34:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f being Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
st f = 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y)
holds 0 = ||.f.||
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be Point of
R_NormSpace_of_BoundedMultilinearOperators(X,Y) such that
A1: f = 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y);
reconsider g = f as Lipschitzian MultilinearOperator of X,Y by Def9;
set z = (the carrier of product X) --> 0.Y;
reconsider z as Function of the carrier of product X,the carrier of Y;
consider r0 be object such that
A2: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A2;
A3: (for s be Real st s in PreNorms(g) holds s <= 0)
implies upper_bound PreNorms(g) <= 0 by SEQ_4:45;
A4: PreNorms(g) is non empty bounded_above by Th27;
A5: z = g by A1,Th31;
A6: now
let r be Real;
assume r in PreNorms(g); then
consider t be VECTOR of product X such that
A7: r = ||. g.t .|| and
for i be Element of dom X holds ||.t.i.|| <= 1;
||.g.t.|| = ||.0.Y.|| by A5,FUNCOP_1:7
.= 0;
hence 0 <= r & r <=0 by A7;
end; then
0 <= r0 by A2; then
upper_bound PreNorms(g) = 0 by A6,A4,A2,A3,SEQ_4:def 1;
hence thesis by Th30;
end;
registration
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
cluster -> Function-like Relation-like for Element of
R_NormSpace_of_BoundedMultilinearOperators(X,Y);
coherence;
end;
definition
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f be Element of R_NormSpace_of_BoundedMultilinearOperators(X,Y);
let v be VECTOR of product X;
redefine func f.v -> VECTOR of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider f as MultilinearOperator of X,Y by Def9;
f.v is VECTOR of Y;
hence thesis;
end;
end;
theorem Th35:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f,g,h be Point of
R_NormSpace_of_BoundedMultilinearOperators(X,Y)
holds h = f+g iff for x be VECTOR of product X holds h.x = f.x + g.x
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y);
reconsider f1=f, g1=g, h1=h as VECTOR of
R_VectorSpace_of_BoundedMultilinearOperators(X,Y);
h = f+g iff h1 = f1+g1;
hence thesis by Th24;
end;
theorem Th36:
for X being RealNormSpace-Sequence,
Y be RealNormSpace
for f,h be Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
for a be Real
holds h = a * f iff for x be VECTOR of product X holds h.x = a * f.x
proof
let X be RealNormSpace-Sequence,
Y be RealNormSpace;
let f,h be Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y);
let a be Real;
reconsider f1 = f, h1 = h as VECTOR
of R_VectorSpace_of_BoundedMultilinearOperators(X,Y);
h = a * f iff h1 = a * f1;
hence thesis by Th25;
end;
theorem Th37:
for X being RealNormSpace-Sequence,Y be RealNormSpace
for f, g being Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
for a be Real holds
( ||.f.|| = 0 iff f = 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y) )
& ||.a*f.|| = |.a.| * ||.f.|| & ||.f+g.|| <= ||.f.|| + ||.g.||
proof
let X be RealNormSpace-Sequence,Y be RealNormSpace;
let f, g be Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y);
let a be Real;
A2: now
assume
A3: f = 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y);
thus ||.f.|| = 0
proof
reconsider g=f as Lipschitzian MultilinearOperator of X,Y by Def9;
set z = (the carrier of product X) --> 0.Y;
reconsider z as Function of the carrier of product X,the carrier of Y;
consider r0 be object such that
A4: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A4;
A5: (for s be Real st s in PreNorms(g) holds s <= 0)
implies upper_bound PreNorms(g) <= 0 by SEQ_4:45;
A6: PreNorms(g) is non empty bounded_above by Th27;
A7: z = g by A3,Th31;
A8: now
let r be Real;
assume r in PreNorms(g); then
consider t be VECTOR of product X such that
A9: r = ||.g.t .|| and
for i be Element of dom X holds ||.t.i.|| <= 1;
||.g.t.|| = ||.0.Y.|| by A7,FUNCOP_1:7
.= 0;
hence 0 <= r & r <=0 by A9;
end; then
0 <= r0 by A4; then
upper_bound PreNorms(g) = 0 by A4,A5,A6,A8,SEQ_4:def 1;
hence thesis by Th30;
end;
end;
A11: ||.f+g.|| <= ||.f.|| + ||.g.||
proof
reconsider f1=f, g1=g, h1=f+g as Lipschitzian MultilinearOperator of X,Y
by Def9;
A12: ( for s be Real st s in PreNorms(h1) holds s <= ||.f.|| + ||.g.||)
implies upper_bound PreNorms(h1) <= ||.f.|| + ||.g.|| by SEQ_4:45;
A13: now
let t be VECTOR of product X;
assume
A14: for i be Element of dom X holds ||.t.i.|| <= 1;
A15: 0 <= NrProduct t & NrProduct t <= 1 by A14,LM28;
0 <= ||.g.|| by Th33; then
A16: ||.g.|| * (NrProduct t) <= ||.g.|| * 1 by A15,XREAL_1:64;
0 <= ||.f.|| by Th33; then
||.f.|| * ( NrProduct t) <= ||.f.|| * 1 by A15,XREAL_1:64; then
A17: ||.f.|| * NrProduct t + ||.g.|| * NrProduct t
<= ||.f.|| * 1 + ||.g.|| * 1 by A16,XREAL_1:7;
A18: ||.f1.t+g1.t.|| <= ||.f1.t.|| + ||.g1.t.|| by NORMSP_1:def 1;
A19: ||.g1.t.|| <= ||.g.|| * NrProduct t by Th32;
||.f1.t.|| <= ||.f.|| * NrProduct t by Th32; then
||.f1.t.|| + ||.g1.t.||
<= ||.f.|| * NrProduct t + ||.g.|| * NrProduct t
by A19,XREAL_1:7; then
A20: ||.f1.t.|| + ||.g1.t.|| <= ||.f.|| + ||.g.|| by A17,XXREAL_0:2;
||.h1.t.||= ||.f1.t+g1.t.|| by Th35;
hence ||.h1.t.|| <= ||.f.|| + ||.g.|| by A18,A20,XXREAL_0:2;
end;
now
let r be Real;
assume r in PreNorms(h1); then
consider t be VECTOR of product X such that
A22: r = ||. h1.t .|| and
A23: for i be Element of dom X holds ||.t.i.|| <= 1;
thus r <= ||.f.|| + ||.g.|| by A13,A22,A23;
end;
hence thesis by A12,Th30;
end;
reconsider f1=f, h1=a*f as Lipschitzian MultilinearOperator of X,Y
by Def9;
A25: (for s be Real st s in PreNorms(h1) holds s <= |.a.|*||.f.||)
implies upper_bound PreNorms(h1) <= |.a.|*||.f.|| by SEQ_4:45;
A24: ||.a*f.|| = |.a.| * ||.f.||
proof
A26: now
A27: 0 <= ||.f.|| by Th33;
let t be VECTOR of product X;
assume
A28: for i be Element of dom X holds ||.t.i.|| <= 1;
NrProduct t <= 1 by A28,LM28; then
A29: ||.f.|| * (NrProduct t) <= ||.f.|| * 1 by A27,XREAL_1:64;
||.f1.t.|| <= ||.f.|| * NrProduct t by Th32; then
A30: ||.f1.t.|| <= ||.f.|| by A29,XXREAL_0:2;
A31: ||.a*f1.t.|| = |.a.| * ||.f1.t.|| by NORMSP_1:def 1;
A32: 0 <= |.a.| by COMPLEX1:46;
||.h1.t.||= ||.a*f1.t.|| by Th36;
hence ||.h1.t.|| <= |.a.| * ||.f.|| by A30,A31,A32,XREAL_1:64;
end;
A33: now
let r be Real;
assume r in PreNorms(h1); then
consider t be VECTOR of product X such that
A34: r = ||. h1.t .|| and
A35: for i be Element of dom X holds ||.t.i.|| <= 1;
thus r <= |.a.|*||.f.|| by A26,A34,A35;
end;
A36: now
per cases;
case
A37: a <> 0;
A38: now
A39: 0 <= ||.a*f.|| by Th33;
let t be VECTOR of product X;
assume for i be Element of dom X holds ||.t.i.|| <= 1; then
NrProduct t <= 1 by LM28; then
A41: ||.a*f.|| * (NrProduct t) <= ||.a*f.|| * 1
by A39,XREAL_1:64;
||.h1.t.||<= ||.a*f.|| * NrProduct t by Th32; then
A42: ||.h1.t.|| <= ||.a*f.|| by A41,XXREAL_0:2;
h1.t = a*f1.t by Th36; then
A43: a" * h1.t = (a"* a) * f1.t by RLVECT_1:def 7
.= 1 * f1.t by A37,XCMPLX_0:def 7
.= f1.t by RLVECT_1:def 8;
A44: |.a".| = |.1*a".|
.= |. 1/a.| by XCMPLX_0:def 9
.= 1 / |.a.| by ABSVALUE:7
.= 1 * |.a.|" by XCMPLX_0:def 9
.= |.a.|";
A45: 0 <= |.a".| by COMPLEX1:46;
||.a" * h1.t.|| = |.a".| * ||.h1.t.|| by NORMSP_1:def 1;
hence ||.f1.t.|| <= |.a.|" * ||.a * f.||
by A42,A43,A44,A45,XREAL_1:64;
end;
A46: now
let r be Real;
assume r in PreNorms(f1); then
consider t be VECTOR of product X such that
A47: r = ||. f1.t .|| and
A48: for i be Element of dom X holds ||.t.i.|| <= 1;
thus r <= |.a.|" * ||.a*f.|| by A38,A47,A48;
end;
A49: ( for s be Real st s in PreNorms(f1) holds
s <= |.a.|"* ||.a*f.|| )
implies upper_bound PreNorms(f1) <= |.a.|"*||.a*f.||
by SEQ_4:45;
A50: 0 <= |.a.| by COMPLEX1:46;
||.f.|| <= |.a.|" * ||.a*f.|| by A46,A49,Th30; then
|.a.| * ||.f.|| <= |.a.| * (|.a.|" * ||.a*f.||)
by A50,XREAL_1:64; then
A51: |.a.|*||.f.|| <= (|.a.|*|.a.|") * ||.a*f.||;
|.a.| <> 0 by A37,COMPLEX1:47; then
|.a.| * ||.f.|| <= 1 * ||.a*f.|| by A51,XCMPLX_0:def 7;
hence |.a.| * ||.f.|| <= ||.a*f.||;
end;
case
A52: a=0;
reconsider fz=f as VECTOR of
R_VectorSpace_of_BoundedMultilinearOperators(X,Y);
A53: a * f = a * fz
.= 0.R_VectorSpace_of_BoundedMultilinearOperators(X,Y)
by A52,RLVECT_1:10
.= 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y);
thus |.a.| * ||.f.|| = 0 * ||.f.|| by A52,ABSVALUE:2
.= ||.a*f.|| by A53,Th34;
end;
end;
||.a*f.|| <= |.a.| * ||.f.|| by A25,A33,Th30;
hence thesis by A36,XXREAL_0:1;
end;
now
reconsider g = f as Lipschitzian MultilinearOperator of X,Y by Def9;
set z = (the carrier of product X) --> 0.Y;
reconsider z as Function of the carrier of product X,the carrier of Y;
assume
A54: ||.f.|| = 0;
now
let t be VECTOR of product X;
||.g.t.|| <= ||.f.|| *NrProduct t by Th32; then
||.g.t.|| = 0 by A54;
hence g.t = 0.Y by NORMSP_0:def 5
.= z.t by FUNCOP_1:7;
end; then
g = z by FUNCT_2:63;
hence f = 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y) by Th31;
end;
hence thesis by A2,A11,A24;
end;
Th38:
for X being RealNormSpace-Sequence,Y be RealNormSpace holds
R_NormSpace_of_BoundedMultilinearOperators(X,Y) is
reflexive discerning RealNormSpace-like
proof
let X be RealNormSpace-Sequence,Y be RealNormSpace;
thus ||.0.R_NormSpace_of_BoundedMultilinearOperators(X,Y).|| = 0 by Th37;
for x, y being Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
for a be Real holds
( ||.x.|| = 0 iff x = 0.R_NormSpace_of_BoundedMultilinearOperators(X,Y) )
& ||.a*x.|| = |.a.| * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Th37;
hence thesis by NORMSP_1:def 1,NORMSP_0:def 5;
end;
theorem Th39:
for X being RealNormSpace-Sequence,Y be RealNormSpace
holds R_NormSpace_of_BoundedMultilinearOperators(X,Y) is RealNormSpace
proof
let X be RealNormSpace-Sequence,Y be RealNormSpace;
RLSStruct (# BoundedMultilinearOperators(X,Y),
Zero_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Add_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)),
Mult_(BoundedMultilinearOperators(X,Y),
R_VectorSpace_of_MultilinearOperators(X,Y)) #) is RealLinearSpace;
hence thesis by Th38,RSSPACE3:2;
end;
registration
let X be RealNormSpace-Sequence,Y be RealNormSpace;
cluster R_NormSpace_of_BoundedMultilinearOperators(X,Y) ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence by Th39;
end;
theorem
for X being RealNormSpace-Sequence,Y be RealNormSpace
for f,g,h be Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y)
holds h = f-g iff for x be VECTOR of product X holds h.x = f.x - g.x
proof
let X be RealNormSpace-Sequence,Y be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_BoundedMultilinearOperators(X,Y);
reconsider f9=f,g9=g,h9=h as Lipschitzian MultilinearOperator of X,Y
by Def9;
hereby
assume h = f-g; then
h+g = f-(g-g) by RLVECT_1:29; then
A1: h+g = f-0.R_NormSpace_of_BoundedMultilinearOperators(X,Y)
by RLVECT_1:15;
now
let x be VECTOR of product X;
f9.x = h9.x + g9.x by A1,Th35; then
f9.x - g9.x = h9.x + (g9.x - g9.x) by RLVECT_1:def 3; then
f9.x - g9.x = h9.x + 0.Y by RLVECT_1:15;
hence f9.x - g9.x = h9.x;
end;
hence for x be VECTOR of product X holds h.x = f.x - g.x;
end;
assume
A2: for x be VECTOR of product X holds h.x = f.x - g.x;
now
let x be VECTOR of product X;
h9.x = f9.x - g9.x by A2; then
h9.x + g9.x = f9.x - (g9.x - g9.x) by RLVECT_1:29;
then h9.x + g9.x = f9.x - 0.Y by RLVECT_1:15;
hence h9.x + g9.x = f9.x;
end; then
f = h+g by Th35; then
f-g = h+(g-g) by RLVECT_1:def 3; then
f-g = h+0.R_NormSpace_of_BoundedMultilinearOperators(X,Y) by RLVECT_1:15;
hence thesis;
end;