let X, Y be RealNormSpace; :: thesis: for f being LinearOperator of X,Y holds
( f is Lipschitzian iff f is_continuous_on the carrier of X )
let f be LinearOperator of X,Y; :: thesis: ( f is Lipschitzian iff f is_continuous_on the carrier of X )
hereby :: thesis: ( f is_continuous_on the carrier of X implies f is Lipschitzian )
assume A1: f is Lipschitzian ; :: thesis: f is_continuous_on the carrier of X
A2: dom f = the carrier of X by FUNCT_2:def 1;
consider K being Real such that
A3: ( 0 <= K & ( for x being VECTOR of X holds ||.(f . x).|| <= K * ||.x.|| ) ) by A1;
now :: thesis: for x, y being Point of X st x in the carrier of X & y in the carrier of X holds
||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).||
let x, y be Point of X; :: thesis: ( x in the carrier of X & y in the carrier of X implies ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| )
assume ( x in the carrier of X & y in the carrier of X ) ; :: thesis: ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).||
(f /. x) - (f /. y) = (f . x) + ((- 1) * (f . y)) by RLVECT_1:16;
then (f /. x) - (f /. y) = (f . x) + (f . ((- 1) * y)) by LOPBAN_1:def 5;
then (f /. x) - (f /. y) = f . (x + ((- 1) * y)) by VECTSP_1:def 20;
then A4: (f /. x) - (f /. y) = f . (x + (- y)) by RLVECT_1:16;
||.((f /. x) - (f /. y)).|| <= (K * ||.(x - y).||) + ||.(x - y).|| by A3, A4, XREAL_1:38;
hence ||.((f /. x) - (f /. y)).|| <= (K + 1) * ||.(x - y).|| ; :: thesis: verum
end;
hence f is_continuous_on the carrier of X by NFCONT_1:45, A2, A3, NFCONT_1:def 9; :: thesis: verum
end;
assume A5: f is_continuous_on the carrier of X ; :: thesis: f is Lipschitzian
A6: dom f = the carrier of X by FUNCT_2:def 1;
f | the carrier of X = f ;
then f is_continuous_in 0. X by A5, NFCONT_1:def 7;
then consider s being Real such that
A7: ( 0 < s & ( for x1 being Point of X st x1 in dom f & ||.(x1 - (0. X)).|| < s holds
||.((f /. x1) - (f /. (0. X))).|| < 1 ) ) by NFCONT_1:7;
set r1 = 2 / s;
now :: thesis: for x1 being VECTOR of X holds ||.(f . x1).|| <= (2 / s) * ||.x1.||
let x1 be VECTOR of X; :: thesis: ||.(f . b1).|| <= (2 / s) * ||.b1.||
A8: 0. Y = f /. (0. X) by Th3;
per cases ( x1 = 0. X or x1 <> 0. X ) ;
suppose x1 = 0. X ; :: thesis: ||.(f . b1).|| <= (2 / s) * ||.b1.||
hence ||.(f . x1).|| <= (2 / s) * ||.x1.|| by A7, A8; :: thesis: verum
end;
suppose A9: x1 <> 0. X ; :: thesis: ||.(f . b1).|| <= (2 / s) * ||.b1.||
then A10: ||.x1.|| <> 0 by NORMSP_0:def 5;
set r3 = (s / 2) / ||.x1.||;
0 < s / 2 by A7, XREAL_1:215;
then A11: 0 < (s / 2) / ||.x1.|| by A10, XREAL_1:139;
set x2 = ((s / 2) / ||.x1.||) * x1;
A12: 1 / ((s / 2) / ||.x1.||) = ||.x1.|| / (s / 2) by XCMPLX_1:57
.= ||.x1.|| * (2 / s) by XCMPLX_1:79 ;
||.(((s / 2) / ||.x1.||) * x1).|| = |.((s / 2) / ||.x1.||).| * ||.x1.|| by NORMSP_1:def 1
.= ((s / 2) / ||.x1.||) * ||.x1.|| by A7, ABSVALUE:def 1
.= s / 2 by A9, NORMSP_0:def 5, XCMPLX_1:87 ;
then ||.(((s / 2) / ||.x1.||) * x1).|| < s by A7, XREAL_1:216;
then ||.((((s / 2) / ||.x1.||) * x1) - (0. X)).|| < s by RLVECT_1:13;
then A13: ||.((f /. (((s / 2) / ||.x1.||) * x1)) - (f /. (0. X))).|| < 1 by A6, A7;
||.(f /. (((s / 2) / ||.x1.||) * x1)).|| = ||.(((s / 2) / ||.x1.||) * (f . x1)).|| by LOPBAN_1:def 5
.= |.((s / 2) / ||.x1.||).| * ||.(f . x1).|| by NORMSP_1:def 1
.= ((s / 2) / ||.x1.||) * ||.(f . x1).|| by A7, ABSVALUE:def 1 ;
then ((s / 2) / ||.x1.||) * ||.(f . x1).|| < 1 by A13, A8, RLVECT_1:13;
hence ||.(f . x1).|| <= (2 / s) * ||.x1.|| by A12, A11, XREAL_1:81; :: thesis: verum
end;
end;
end;
hence f is Lipschitzian by A7; :: thesis: verum