let E, F, G be RealNormSpace; for u being Lipschitzian BilinearOperator of E,F,G holds u * ((IsoCPNrSP (E,F)) ") is Lipschitzian MultilinearOperator of <*E,F*>,G
let u be Lipschitzian BilinearOperator of E,F,G; u * ((IsoCPNrSP (E,F)) ") is Lipschitzian MultilinearOperator of <*E,F*>,G
reconsider M = u * ((IsoCPNrSP (E,F)) ") as Function of (product <*E,F*>),G ;
A1: dom <*E,F*> =
Seg (len <*E,F*>)
by FINSEQ_1:def 3
.=
{1,2}
by FINSEQ_1:2, FINSEQ_1:44
;
then reconsider i1 = 1, i2 = 2 as Element of dom <*E,F*> by TARSKI:def 2;
for i being Element of dom <*E,F*>
for s being Element of (product <*E,F*>) holds M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),G
proof
let i be
Element of
dom <*E,F*>;
for s being Element of (product <*E,F*>) holds M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),Glet s be
Element of
(product <*E,F*>);
M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),G
consider x being
Point of
E,
y being
Point of
F such that A3:
s = <*x,y*>
by PRVECT_3:19;
len s = 2
by A3, FINSEQ_1:44;
then A5:
dom s = {1,2}
by FINSEQ_1:2, FINSEQ_1:def 3;
per cases
( i = 1 or i = 2 )
by A1, TARSKI:def 2;
suppose A6:
i = 1
;
M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),Gthen A7:
<*E,F*> . i = E
;
then reconsider L =
M * (reproj (i,s)) as
Function of
E,
G ;
A8:
dom (reproj (i,s)) =
the
carrier of
(<*E,F*> . i)
by FUNCT_2:def 1
.=
the
carrier of
E
by A6
;
A9:
for
z being
Point of
E holds
(reproj (i,s)) . z = <*z,y*>
proof
let x1 be
Point of
E;
(reproj (i,s)) . x1 = <*x1,y*>
A10:
len (s +* (i,x1)) = 2
by LemmaA;
A11:
(s +* (i,x1)) . 1
= x1
by A1, A5, A6, FUNCT_7:31;
A12:
(s +* (i,x1)) . 2 =
s . 2
by A6, FUNCT_7:32
.=
y
by A3
;
thus (reproj (i,s)) . x1 =
s +* (
i,
x1)
by A7, NDIFF_5:def 4
.=
<*x1,y*>
by A10, A11, A12, FINSEQ_1:44
;
verum
end; A14:
for
x1,
x2 being
Point of
E holds
L . (x1 + x2) = (L . x1) + (L . x2)
proof
let x1,
x2 be
Point of
E;
L . (x1 + x2) = (L . x1) + (L . x2)
reconsider x1y =
<*x1,y*>,
x2y =
<*x2,y*>,
x12y =
<*(x1 + x2),y*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
A18:
L . x1 =
M . ((reproj (i,s)) . x1)
by A8, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*x1,y*>
by A9
.=
u . (((IsoCPNrSP (E,F)) ") . x1y)
by FUNCT_2:15
.=
u . (
x1,
y)
by NDIFF_7:18
;
A19:
L . x2 =
M . ((reproj (i,s)) . x2)
by A8, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*x2,y*>
by A9
.=
u . (((IsoCPNrSP (E,F)) ") . x2y)
by FUNCT_2:15
.=
u . (
x2,
y)
by NDIFF_7:18
;
L . (x1 + x2) =
M . ((reproj (i,s)) . (x1 + x2))
by A8, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*(x1 + x2),y*>
by A9
.=
u . (((IsoCPNrSP (E,F)) ") . x12y)
by FUNCT_2:15
.=
u . (
(x1 + x2),
y)
by NDIFF_7:18
;
hence
L . (x1 + x2) = (L . x1) + (L . x2)
by A18, A19, LOPBAN_8:12;
verum
end;
for
x1 being
Point of
E for
a being
Real holds
L . (a * x1) = a * (L . x1)
proof
let x1 be
Point of
E;
for a being Real holds L . (a * x1) = a * (L . x1)let a be
Real;
L . (a * x1) = a * (L . x1)
reconsider ax1y =
<*(a * x1),y*>,
x1y =
<*x1,y*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
A23:
L . x1 =
M . ((reproj (i,s)) . x1)
by A8, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*x1,y*>
by A9
.=
u . (((IsoCPNrSP (E,F)) ") . x1y)
by FUNCT_2:15
.=
u . (
x1,
y)
by NDIFF_7:18
;
L . (a * x1) =
M . ((reproj (i,s)) . (a * x1))
by A8, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*(a * x1),y*>
by A9
.=
u . (((IsoCPNrSP (E,F)) ") . ax1y)
by FUNCT_2:15
.=
u . (
(a * x1),
y)
by NDIFF_7:18
;
hence
L . (a * x1) = a * (L . x1)
by A23, LOPBAN_8:12;
verum
end; hence
M * (reproj (i,s)) is
LinearOperator of
(<*E,F*> . i),
G
by A7, A14, LOPBAN_1:def 5, VECTSP_1:def 20;
verum end; suppose A25:
i = 2
;
M * (reproj (i,s)) is LinearOperator of (<*E,F*> . i),Gthen A26:
<*E,F*> . i = F
;
then reconsider L =
M * (reproj (i,s)) as
Function of
F,
G ;
A27:
dom (reproj (i,s)) =
the
carrier of
(<*E,F*> . i)
by FUNCT_2:def 1
.=
the
carrier of
F
by A25
;
A28:
for
z being
Point of
F holds
(reproj (i,s)) . z = <*x,z*>
proof
let y1 be
Point of
F;
(reproj (i,s)) . y1 = <*x,y1*>
A29:
len (s +* (i,y1)) = 2
by LemmaA;
A30:
(s +* (i,y1)) . 2
= y1
by A1, A5, A25, FUNCT_7:31;
A31:
(s +* (i,y1)) . 1 =
s . 1
by A25, FUNCT_7:32
.=
x
by A3
;
thus (reproj (i,s)) . y1 =
s +* (
i,
y1)
by A26, NDIFF_5:def 4
.=
<*x,y1*>
by A29, A30, A31, FINSEQ_1:44
;
verum
end; A33:
for
y1,
y2 being
Point of
F holds
L . (y1 + y2) = (L . y1) + (L . y2)
proof
let y1,
y2 be
Point of
F;
L . (y1 + y2) = (L . y1) + (L . y2)
reconsider y1y =
<*x,y1*>,
y2y =
<*x,y2*>,
y12y =
<*x,(y1 + y2)*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
A37:
L . y1 =
M . ((reproj (i,s)) . y1)
by A27, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*x,y1*>
by A28
.=
u . (((IsoCPNrSP (E,F)) ") . y1y)
by FUNCT_2:15
.=
u . (
x,
y1)
by NDIFF_7:18
;
A38:
L . y2 =
M . ((reproj (i,s)) . y2)
by A27, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*x,y2*>
by A28
.=
u . (((IsoCPNrSP (E,F)) ") . y2y)
by FUNCT_2:15
.=
u . (
x,
y2)
by NDIFF_7:18
;
L . (y1 + y2) =
M . ((reproj (i,s)) . (y1 + y2))
by A27, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*x,(y1 + y2)*>
by A28
.=
u . (((IsoCPNrSP (E,F)) ") . y12y)
by FUNCT_2:15
.=
u . (
x,
(y1 + y2))
by NDIFF_7:18
;
hence
L . (y1 + y2) = (L . y1) + (L . y2)
by A37, A38, LOPBAN_8:12;
verum
end;
for
y1 being
Point of
F for
a being
Real holds
L . (a * y1) = a * (L . y1)
proof
let y1 be
Point of
F;
for a being Real holds L . (a * y1) = a * (L . y1)let a be
Real;
L . (a * y1) = a * (L . y1)
reconsider ax1y =
<*x,(a * y1)*>,
x1y =
<*x,y1*> as
Point of
(product <*E,F*>) by PRVECT_3:19;
A42:
L . y1 =
M . ((reproj (i,s)) . y1)
by A27, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*x,y1*>
by A28
.=
u . (((IsoCPNrSP (E,F)) ") . x1y)
by FUNCT_2:15
.=
u . (
x,
y1)
by NDIFF_7:18
;
L . (a * y1) =
M . ((reproj (i,s)) . (a * y1))
by A27, FUNCT_1:13
.=
(u * ((IsoCPNrSP (E,F)) ")) . <*x,(a * y1)*>
by A28
.=
u . (((IsoCPNrSP (E,F)) ") . ax1y)
by FUNCT_2:15
.=
u . (
x,
(a * y1))
by NDIFF_7:18
;
hence
L . (a * y1) = a * (L . y1)
by A42, LOPBAN_8:12;
verum
end; hence
M * (reproj (i,s)) is
LinearOperator of
(<*E,F*> . i),
G
by A26, A33, LOPBAN_1:def 5, VECTSP_1:def 20;
verum end;
end;
then reconsider M = M as MultilinearOperator of <*E,F*>,G by LOPBAN10:def 6;
ex K being Real st
( 0 <= K & ( for s being Point of (product <*E,F*>) holds ||.(M . s).|| <= K * (NrProduct s) ) )
proof
consider K being
Real such that A44:
(
0 <= K & ( for
x being
Point of
E for
y being
Point of
F holds
||.(u . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) )
by LOPBAN_9:def 3;
take
K
;
( 0 <= K & ( for s being Point of (product <*E,F*>) holds ||.(M . s).|| <= K * (NrProduct s) ) )
thus
0 <= K
by A44;
for s being Point of (product <*E,F*>) holds ||.(M . s).|| <= K * (NrProduct s)
let xy be
Point of
(product <*E,F*>);
||.(M . xy).|| <= K * (NrProduct xy)
consider x being
Point of
E,
y being
Point of
F such that A45:
xy = <*x,y*>
by PRVECT_3:19;
A46:
M . xy =
u . (((IsoCPNrSP (E,F)) ") . xy)
by FUNCT_2:15
.=
u . (
x,
y)
by A45, NDIFF_7:18
;
consider Nx being
FinSequence of
REAL such that A47:
(
dom Nx = dom <*E,F*> & ( for
i being
Element of
dom <*E,F*> holds
Nx . i = ||.(xy . i).|| ) &
NrProduct xy = Product Nx )
by LOPBAN10:def 9;
dom Nx =
Seg (len <*E,F*>)
by A47, FINSEQ_1:def 3
.=
Seg 2
by FINSEQ_1:44
;
then A48:
len Nx = 2
by FINSEQ_1:def 3;
A50:
Nx . 1 =
||.(xy . i1).||
by A47
.=
||.x.||
by A45
;
Nx . 2 =
||.(xy . i2).||
by A47
.=
||.y.||
by A45
;
then
Nx = <*||.x.||,||.y.||*>
by A48, A50, FINSEQ_1:44;
then A51:
NrProduct xy = ||.x.|| * ||.y.||
by A47, RVSUM_1:99;
||.(u . (x,y)).|| <= (K * ||.x.||) * ||.y.||
by A44;
hence
||.(M . xy).|| <= K * (NrProduct xy)
by A46, A51;
verum
end;
hence
u * ((IsoCPNrSP (E,F)) ") is Lipschitzian MultilinearOperator of <*E,F*>,G
by LOPBAN10:def 10; verum