let X, Y, Z be RealNormSpace; for g being BilinearOperator of X,Y,Z holds
( g is Lipschitzian iff PreNorms g is bounded_above )
let g be BilinearOperator of X,Y,Z; ( g is Lipschitzian iff PreNorms g is bounded_above )
now ( PreNorms g is bounded_above implies ex K being Real st g is Lipschitzian )reconsider K =
upper_bound (PreNorms g) as
Real ;
assume A1:
PreNorms g is
bounded_above
;
ex K being Real st g is Lipschitzian A2:
now for t being VECTOR of X
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||let t be
VECTOR of
X;
for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||let s be
VECTOR of
Y;
||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||now ( ( ( t = 0. X or s = 0. Y ) & ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.|| ) or ( t <> 0. X & s <> 0. Y & ||.(g . (t,s)).|| <= K * (||.t.|| * ||.s.||) ) )per cases
( t = 0. X or s = 0. Y or ( t <> 0. X & s <> 0. Y ) )
;
case A5:
(
t <> 0. X &
s <> 0. Y )
;
||.(g . (t,s)).|| <= K * (||.t.|| * ||.s.||)reconsider t1 =
(||.t.|| ") * t as
VECTOR of
X ;
reconsider s1 =
(||.s.|| ") * s as
VECTOR of
Y ;
A6:
(
||.t.|| <> 0 &
||.s.|| <> 0 )
by A5, NORMSP_0:def 5;
then A7:
||.t.|| * ||.s.|| <> 0
by XCMPLX_1:6;
A8:
(||.(g . (t,s)).|| / (||.t.|| * ||.s.||)) * (||.t.|| * ||.s.||) =
(||.(g . (t,s)).|| * ((||.t.|| * ||.s.||) ")) * (||.t.|| * ||.s.||)
by XCMPLX_0:def 9
.=
||.(g . (t,s)).|| * (((||.t.|| * ||.s.||) ") * (||.t.|| * ||.s.||))
.=
||.(g . (t,s)).|| * 1
by A7, XCMPLX_0:def 7
.=
||.(g . (t,s)).||
;
A9:
|.(||.t.|| ").| =
|.(1 * (||.t.|| ")).|
.=
|.(1 / ||.t.||).|
by XCMPLX_0:def 9
.=
1
/ ||.t.||
by ABSVALUE:def 1
.=
1
* (||.t.|| ")
by XCMPLX_0:def 9
.=
||.t.|| "
;
A10:
|.(||.s.|| ").| =
|.(1 * (||.s.|| ")).|
.=
|.(1 / ||.s.||).|
by XCMPLX_0:def 9
.=
1
/ ||.s.||
by ABSVALUE:def 1
.=
1
* (||.s.|| ")
by XCMPLX_0:def 9
.=
||.s.|| "
;
A11:
|.((||.t.|| * ||.s.||) ").| =
|.((||.t.|| ") * (||.s.|| ")).|
by XCMPLX_1:204
.=
(||.t.|| ") * (||.s.|| ")
by A9, A10, COMPLEX1:65
.=
(||.t.|| * ||.s.||) "
by XCMPLX_1:204
;
A12:
||.t1.|| =
|.(||.t.|| ").| * ||.t.||
by NORMSP_1:def 1
.=
1
by A6, A9, XCMPLX_0:def 7
;
||.s1.|| =
|.(||.s.|| ").| * ||.s.||
by NORMSP_1:def 1
.=
1
by A6, A10, XCMPLX_0:def 7
;
then A13:
||.(g . (t1,s1)).|| in { ||.(g . (t,s)).|| where t is VECTOR of X, s is VECTOR of Y : ( ||.t.|| <= 1 & ||.s.|| <= 1 ) }
by A12;
||.(g . (t,s)).|| / (||.t.|| * ||.s.||) =
||.(g . (t,s)).|| * ((||.t.|| * ||.s.||) ")
by XCMPLX_0:def 9
.=
||.(((||.t.|| * ||.s.||) ") * (g . (t,s))).||
by A11, NORMSP_1:def 1
.=
||.(((||.t.|| ") * (||.s.|| ")) * (g . (t,s))).||
by XCMPLX_1:204
.=
||.((||.t.|| ") * ((||.s.|| ") * (g . (t,s)))).||
by RLVECT_1:def 7
.=
||.((||.t.|| ") * (g . (t,s1))).||
by LOPBAN_8:12
.=
||.(g . (t1,s1)).||
by LOPBAN_8:12
;
then
||.(g . (t,s)).|| / (||.t.|| * ||.s.||) <= K
by A1, A13, SEQ_4:def 1;
hence
||.(g . (t,s)).|| <= K * (||.t.|| * ||.s.||)
by A8, XREAL_1:64;
verum end; end; end; hence
||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||
;
verum end; take K =
K;
g is Lipschitzian
0 <= K
hence
g is
Lipschitzian
by A2;
verum end;
hence
( g is Lipschitzian iff PreNorms g is bounded_above )
; verum