let E, F, G be RealNormSpace; for f being Lipschitzian BilinearOperator of E,F,G ex K being Real st
( 0 <= K & ( for z being Point of [:E,F:] ex L being Lipschitzian LinearOperator of [:E,F:],G st
( ( for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= (K * ||.z.||) * ||.s.|| ) ) ) )
let f be Lipschitzian BilinearOperator of E,F,G; ex K being Real st
( 0 <= K & ( for z being Point of [:E,F:] ex L being Lipschitzian LinearOperator of [:E,F:],G st
( ( for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= (K * ||.z.||) * ||.s.|| ) ) ) )
consider K being Real such that
A1:
( 0 <= K & ( for x being VECTOR of E
for y being VECTOR of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) )
by LOPBAN_9:def 3;
set H = 2 * K;
take
2 * K
; ( 0 <= 2 * K & ( for z being Point of [:E,F:] ex L being Lipschitzian LinearOperator of [:E,F:],G st
( ( for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= ((2 * K) * ||.z.||) * ||.s.|| ) ) ) )
thus
0 <= 2 * K
by A1, XREAL_1:127; for z being Point of [:E,F:] ex L being Lipschitzian LinearOperator of [:E,F:],G st
( ( for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= ((2 * K) * ||.z.||) * ||.s.|| ) )
let z be Point of [:E,F:]; ex L being Lipschitzian LinearOperator of [:E,F:],G st
( ( for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= ((2 * K) * ||.z.||) * ||.s.|| ) )
deffunc H1( Element of E, Element of F) -> Element of the carrier of G = (f . ($1,(z `2))) + (f . ((z `1),$2));
consider L0 being Function of [: the carrier of E, the carrier of F:], the carrier of G such that
A2:
for x being Element of the carrier of E
for y being Element of the carrier of F holds L0 . (x,y) = H1(x,y)
from BINOP_1:sch 4();
reconsider L = L0 as Function of [:E,F:],G ;
for x, y being Element of [:E,F:] holds L . (x + y) = (L . x) + (L . y)
proof
let x,
y be
Element of
[:E,F:];
L . (x + y) = (L . x) + (L . y)
consider Ex being
Point of
E,
Fx being
Point of
F such that A3:
x = [Ex,Fx]
by PRVECT_3:18;
consider Ey being
Point of
E,
Fy being
Point of
F such that A4:
y = [Ey,Fy]
by PRVECT_3:18;
A5:
L . x =
L . (
Ex,
Fx)
by A3
.=
(f . (Ex,(z `2))) + (f . ((z `1),Fx))
by A2
;
A6:
L . y =
L . (
Ey,
Fy)
by A4
.=
(f . (Ey,(z `2))) + (f . ((z `1),Fy))
by A2
;
thus L . (x + y) =
L . (
(Ex + Ey),
(Fx + Fy))
by A3, A4, PRVECT_3:18
.=
(f . ((Ex + Ey),(z `2))) + (f . ((z `1),(Fx + Fy)))
by A2
.=
((f . (Ex,(z `2))) + (f . (Ey,(z `2)))) + (f . ((z `1),(Fx + Fy)))
by LOPBAN_8:12
.=
((f . (Ex,(z `2))) + (f . (Ey,(z `2)))) + ((f . ((z `1),Fx)) + (f . ((z `1),Fy)))
by LOPBAN_8:12
.=
(((f . (Ex,(z `2))) + (f . (Ey,(z `2)))) + (f . ((z `1),Fx))) + (f . ((z `1),Fy))
by RLVECT_1:def 3
.=
(((f . (Ex,(z `2))) + (f . ((z `1),Fx))) + (f . (Ey,(z `2)))) + (f . ((z `1),Fy))
by RLVECT_1:def 3
.=
(L . x) + (L . y)
by A5, A6, RLVECT_1:def 3
;
verum
end;
then A7:
L is additive
;
for x being VECTOR of [:E,F:]
for a being Real holds L . (a * x) = a * (L . x)
proof
let x be
VECTOR of
[:E,F:];
for a being Real holds L . (a * x) = a * (L . x)let a be
Real;
L . (a * x) = a * (L . x)
consider Ex being
Point of
E,
Fx being
Point of
F such that A8:
x = [Ex,Fx]
by PRVECT_3:18;
A9:
L . x =
L . (
Ex,
Fx)
by A8
.=
(f . (Ex,(z `2))) + (f . ((z `1),Fx))
by A2
;
thus L . (a * x) =
L . (
(a * Ex),
(a * Fx))
by A8, PRVECT_3:18
.=
(f . ((a * Ex),(z `2))) + (f . ((z `1),(a * Fx)))
by A2
.=
(a * (f . (Ex,(z `2)))) + (f . ((z `1),(a * Fx)))
by LOPBAN_8:12
.=
(a * (f . (Ex,(z `2)))) + (a * (f . ((z `1),Fx)))
by LOPBAN_8:12
.=
a * (L . x)
by A9, RLVECT_1:def 5
;
verum
end;
then reconsider L = L as LinearOperator of [:E,F:],G by LOPBAN_1:def 5, A7;
set K1 = (2 * K) * ||.z.||;
0 <= ||.(z `2).||
by NORMSP_1:4;
then A10:
0 <= K * ||.(z `2).||
by A1, XREAL_1:127;
0 <= ||.(z `1).||
by NORMSP_1:4;
then A11:
0 <= K * ||.(z `1).||
by A1, XREAL_1:127;
0 <= ||.z.||
by NORMSP_1:4;
then
0 <= K * ||.z.||
by A1, XREAL_1:127;
then A13:
0 <= 2 * (K * ||.z.||)
by XREAL_1:127;
A14:
for w being VECTOR of [:E,F:] holds ||.(L . w).|| <= ((2 * K) * ||.z.||) * ||.w.||
proof
let w be
Element of
[:E,F:];
||.(L . w).|| <= ((2 * K) * ||.z.||) * ||.w.||
consider x being
Point of
E,
y being
Point of
F such that A15:
w = [x,y]
by PRVECT_3:18;
L . w =
L0 . (
x,
y)
by A15
.=
(f . (x,(z `2))) + (f . ((z `1),y))
by A2
;
then A16:
||.(L . w).|| <= ||.(f . (x,(z `2))).|| + ||.(f . ((z `1),y)).||
by NORMSP_1:def 1;
A17:
||.(f . (x,(z `2))).|| <= (K * ||.x.||) * ||.(z `2).||
by A1;
||.(f . ((z `1),y)).|| <= (K * ||.(z `1).||) * ||.y.||
by A1;
then
||.(f . (x,(z `2))).|| + ||.(f . ((z `1),y)).|| <= ((K * ||.x.||) * ||.(z `2).||) + ((K * ||.(z `1).||) * ||.y.||)
by A17, XREAL_1:7;
then A18:
||.(L . w).|| <= ((K * ||.(z `2).||) * ||.x.||) + ((K * ||.(z `1).||) * ||.y.||)
by A16, XXREAL_0:2;
A19:
(K * ||.(z `2).||) * ||.x.|| <= (K * ||.(z `2).||) * ||.w.||
by A10, A15, LOPBAN_7:15, XREAL_1:64;
(K * ||.(z `1).||) * ||.y.|| <= (K * ||.(z `1).||) * ||.w.||
by A11, A15, LOPBAN_7:15, XREAL_1:64;
then
((K * ||.(z `2).||) * ||.x.||) + ((K * ||.(z `1).||) * ||.y.||) <= ((K * ||.(z `2).||) * ||.w.||) + ((K * ||.(z `1).||) * ||.w.||)
by A19, XREAL_1:7;
then A20:
||.(L . w).|| <= ((K * ||.(z `2).||) + (K * ||.(z `1).||)) * ||.w.||
by A18, XXREAL_0:2;
consider x1 being
Point of
E,
y1 being
Point of
F such that A21:
z = [x1,y1]
by PRVECT_3:18;
A22:
K * ||.(z `1).|| <= K * ||.z.||
by A1, A21, LOPBAN_7:15, XREAL_1:64;
K * ||.(z `2).|| <= K * ||.z.||
by A1, A21, LOPBAN_7:15, XREAL_1:64;
then A23:
(K * ||.(z `2).||) + (K * ||.(z `1).||) <= (K * ||.z.||) + (K * ||.z.||)
by A22, XREAL_1:7;
0 <= ||.w.||
by NORMSP_1:4;
then
((K * ||.(z `2).||) + (K * ||.(z `1).||)) * ||.w.|| <= ((2 * K) * ||.z.||) * ||.w.||
by A23, XREAL_1:64;
hence
||.(L . w).|| <= ((2 * K) * ||.z.||) * ||.w.||
by A20, XXREAL_0:2;
verum
end;
then reconsider L = L as Lipschitzian LinearOperator of [:E,F:],G by A13, LOPBAN_1:def 8;
take
L
; ( ( for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= ((2 * K) * ||.z.||) * ||.s.|| ) )
thus
( ( for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= ((2 * K) * ||.z.||) * ||.s.|| ) )
by A2, A14; verum