let X, Y, Z be RealNormSpace; :: thesis: 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; :: thesis: ( g is Lipschitzian iff PreNorms g is bounded_above )

( g is Lipschitzian iff PreNorms g is bounded_above )

let g be BilinearOperator of X,Y,Z; :: thesis: ( g is Lipschitzian iff PreNorms g is bounded_above )

now :: thesis: ( PreNorms g is bounded_above implies ex K being Real st g is Lipschitzian )

hence
( g is Lipschitzian iff PreNorms g is bounded_above )
; :: thesis: verumreconsider K = upper_bound (PreNorms g) as Real ;

assume A1: PreNorms g is bounded_above ; :: thesis: ex K being Real st g is Lipschitzian

0 <= K

end;assume A1: PreNorms g is bounded_above ; :: thesis: ex K being Real st g is Lipschitzian

A2: now :: thesis: for t being VECTOR of X

for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

take K = K; :: thesis: g is Lipschitzian for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

let t be VECTOR of X; :: thesis: for s being VECTOR of Y holds ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

let s be VECTOR of Y; :: thesis: ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

end;let s be VECTOR of Y; :: thesis: ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

now :: thesis: ( ( ( 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.||) ) )end;

hence
||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||
; :: thesis: verumper cases
( t = 0. X or s = 0. Y or ( t <> 0. X & s <> 0. Y ) )
;

end;

case A3:
( t = 0. X or s = 0. Y )
; :: thesis: ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.||

then A4:
( ||.t.|| = 0 or ||.s.|| = 0 )
;

( t = 0 * t or s = 0 * s ) by A3;

then g . (t,s) = 0 * (g . (t,s)) by LOPBAN_8:12

.= 0. Z by RLVECT_1:10 ;

hence ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.|| by A4; :: thesis: verum

end;( t = 0 * t or s = 0 * s ) by A3;

then g . (t,s) = 0 * (g . (t,s)) by LOPBAN_8:12

.= 0. Z by RLVECT_1:10 ;

hence ||.(g . (t,s)).|| <= (K * ||.t.||) * ||.s.|| by A4; :: thesis: verum

case A5:
( t <> 0. X & s <> 0. Y )
; :: thesis: ||.(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; :: thesis: verum

end;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; :: thesis: verum

0 <= K

proof

hence
g is Lipschitzian
by A2; :: thesis: verum
consider r0 being object such that

A14: r0 in PreNorms g by XBOOLE_0:def 1;

reconsider r0 = r0 as Real by A14;

hence 0 <= K by A1, A14, SEQ_4:def 1; :: thesis: verum

end;A14: r0 in PreNorms g by XBOOLE_0:def 1;

reconsider r0 = r0 as Real by A14;

now :: thesis: for r being Real st r in PreNorms g holds

0 <= r

then
0 <= r0
by A14;0 <= r

let r be Real; :: thesis: ( r in PreNorms g implies 0 <= r )

assume r in PreNorms g ; :: thesis: 0 <= r

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(g . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

hence 0 <= r ; :: thesis: verum

end;assume r in PreNorms g ; :: thesis: 0 <= r

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(g . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

hence 0 <= r ; :: thesis: verum

hence 0 <= K by A1, A14, SEQ_4:def 1; :: thesis: verum