let a, b, p, q be Real; :: thesis: for f being Function of REAL,REAL st a > 0 & p > 0 & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) holds
f is Lipschitzian
let f be Function of REAL,REAL; :: thesis: ( a > 0 & p > 0 & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) implies f is Lipschitzian )
assume AP: ( a > 0 & p > 0 ) ; :: thesis: ( not f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) or f is Lipschitzian )
assume FF: f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) ; :: thesis: f is Lipschitzian
set fa = (AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[;
set fp = (AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[;
set f1 = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[);
Dfp: dom ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) = [.((q - b) / (a + p)),+infty.[ by FUNCT_2:def 1;
ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )
proof
take max (((a + p) + a),((a + p) + p)) ; :: thesis: ( 0 < max (((a + p) + a),((a + p) + p)) & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| ) )
( 0 + a < (p + a) + a & (a + p) + a <= max (((a + p) + a),((a + p) + p)) ) by XREAL_1:6, AP, XXREAL_0:25;
then a <= max (((a + p) + a),((a + p) + p)) by XXREAL_0:2;
then AA: |.a.| <= max (((a + p) + a),((a + p) + p)) by ABSVALUE:def 1, AP;
PP0: - (- p) = |.(- p).| by ABSVALUE:def 1, AP;
( 0 + p < (p + a) + p & (a + p) + p <= max (((a + p) + a),((a + p) + p)) ) by XREAL_1:6, AP, XXREAL_0:25;
then PP: |.(- p).| <= max (((a + p) + a),((a + p) + p)) by XXREAL_0:2, PP0;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).|
proof
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| )
A3: |.(x1 - x2).| >= 0 by COMPLEX1:46;
per cases ( x1 < (q - b) / (a + p) or x1 >= (q - b) / (a + p) ) ;
suppose B1: x1 < (q - b) / (a + p) ; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| )
then B12: f . x1 = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) . x1 by FUNCT_4:11, Dfp, XXREAL_1:236, FF
.= (AffineMap (a,b)) . x1 by FUNCT_1:49, B1, XXREAL_1:233 ;
per cases ( x2 < (q - b) / (a + p) or x2 >= (q - b) / (a + p) ) ;
suppose C1: x2 < (q - b) / (a + p) ; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| )
C13: f . x2 = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) . x2 by FUNCT_4:11, Dfp, XXREAL_1:236, C1, FF
.= (AffineMap (a,b)) . x2 by FUNCT_1:49, C1, XXREAL_1:233 ;
|.((f . x1) - (f . x2)).| = |.(((a * x1) + b) - ((AffineMap (a,b)) . x2)).| by FCONT_1:def 4, C13, B12
.= |.(((a * x1) + b) - ((a * x2) + b)).| by FCONT_1:def 4
.= |.(a * (x1 - x2)).|
.= |.a.| * |.(x1 - x2).| by COMPLEX1:65 ;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| ) by AA, A3, XREAL_1:64; :: thesis: verum
end;
suppose C2: x2 >= (q - b) / (a + p) ; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| )
then x2 in [.((q - b) / (a + p)),+infty.[ by XXREAL_1:236;
then C22: x2 in dom ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) by FUNCT_2:def 1;
C23: f . x2 = ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) . x2 by FUNCT_4:13, C22, FF
.= (AffineMap ((- p),q)) . x2 by FUNCT_1:49, C2, XXREAL_1:236 ;
C24: |.((f . x1) - (f . x2)).| = |.(((AffineMap (a,b)) . x1) - (f . x2)).| by B12
.= |.(((a * x1) + b) - ((AffineMap ((- p),q)) . x2)).| by FCONT_1:def 4, C23
.= |.(((a * x1) + b) - (((- p) * x2) + q)).| by FCONT_1:def 4
.= |.((((a + p) * x2) - (q - b)) + (a * (x1 - x2))).| ;
x2 * (a + p) >= ((q - b) / (a + p)) * (a + p) by XREAL_1:64, AP, C2;
then q - b <= (a + p) * x2 by XCMPLX_1:87, AP;
then C25: ((a + p) * x2) - (q - b) >= 0 by XREAL_1:48;
x1 * (a + p) < ((q - b) / (a + p)) * (a + p) by XREAL_1:68, AP, B1;
then C28: (a + p) * x1 < q - b by XCMPLX_1:87, AP;
then - ((a + p) * x1) > - (q - b) by XREAL_1:24;
then (- ((a + p) * x1)) + ((a + p) * x2) > (- (q - b)) + ((a + p) * x2) by XREAL_1:6;
then |.(((a + p) * x2) - (q - b)).| <= |.(((a + p) * x2) - ((a + p) * x1)).| by C25, ABS1;
then C30X: |.(((a + p) * x2) - (q - b)).| + |.(a * (x1 - x2)).| <= |.((a + p) * (x2 - x1)).| + |.(a * (x1 - x2)).| by XREAL_1:6;
C299: |.((((a + p) * x2) - (q - b)) + (a * (x1 - x2))).| <= |.(((a + p) * x2) - (q - b)).| + |.(a * (x1 - x2)).| by COMPLEX1:56;
|.((a + p) * (x2 - x1)).| + |.(a * (x1 - x2)).| = (|.(a + p).| * |.(x2 - x1).|) + |.(a * (x1 - x2)).| by COMPLEX1:65
.= (|.(a + p).| * |.(x2 - x1).|) + (|.a.| * |.(x1 - x2).|) by COMPLEX1:65
.= (|.(a + p).| * |.(x1 - x2).|) + (|.a.| * |.(x1 - x2).|) by COMPLEX1:60
.= ((a + p) * |.(x1 - x2).|) + (|.a.| * |.(x1 - x2).|) by ABSVALUE:def 1, AP
.= ((a + p) * |.(x1 - x2).|) + (a * |.(x1 - x2).|) by ABSVALUE:def 1, AP
.= ((a + p) + a) * |.(x1 - x2).| ;
then C30: |.((f . x1) - (f . x2)).| <= ((a + p) + a) * |.(x1 - x2).| by C24, C299, C30X, XXREAL_0:2;
( (a + p) + a <= max (((a + p) + a),((a + p) + p)) & |.(x1 - x2).| >= 0 ) by XXREAL_0:25, COMPLEX1:46;
then ((a + p) + a) * |.(x1 - x2).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| by XREAL_1:64;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| ) by C30, XXREAL_0:2; :: thesis: verum
end;
end;
end;
suppose B2: x1 >= (q - b) / (a + p) ; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| )
then x1 in [.((q - b) / (a + p)),+infty.[ by XXREAL_1:236;
then B22: x1 in dom ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) by FUNCT_2:def 1;
B23: f . x1 = ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) . x1 by FUNCT_4:13, B22, FF
.= (AffineMap ((- p),q)) . x1 by FUNCT_1:49, B2, XXREAL_1:236 ;
per cases ( x2 < (q - b) / (a + p) or x2 >= (q - b) / (a + p) ) ;
suppose D1: x2 < (q - b) / (a + p) ; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| )
D4: f . x2 = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) . x2 by FUNCT_4:11, Dfp, XXREAL_1:236, D1, FF
.= (AffineMap (a,b)) . x2 by FUNCT_1:49, D1, XXREAL_1:233 ;
D5: |.((f . x1) - (f . x2)).| = |.((((- p) * x1) + q) - ((AffineMap (a,b)) . x2)).| by FCONT_1:def 4, D4, B23
.= |.((((- p) * x1) + q) - ((a * x2) + b)).| by FCONT_1:def 4
.= |.(((q - b) - ((a + p) * x2)) + ((- p) * (x1 - x2))).| ;
x1 * (a + p) >= ((q - b) / (a + p)) * (a + p) by XREAL_1:64, AP, B2;
then D27: q - b <= (a + p) * x1 by XCMPLX_1:87, AP;
x2 * (a + p) < ((q - b) / (a + p)) * (a + p) by XREAL_1:68, AP, D1;
then D28: (a + p) * x2 < q - b by XCMPLX_1:87, AP;
then D25: (q - b) - ((a + p) * x2) >= 0 by XREAL_1:48;
(q - b) - ((a + p) * x2) <= ((a + p) * x1) - ((a + p) * x2) by XREAL_1:9, D27;
then |.((a + p) * (x1 - x2)).| >= |.((q - b) - ((a + p) * x2)).| by D25, ABS1;
then D30: |.((a + p) * (x1 - x2)).| + |.((- p) * (x1 - x2)).| >= |.((q - b) - ((a + p) * x2)).| + |.((- p) * (x1 - x2)).| by XREAL_1:6;
X29: |.(((q - b) - ((a + p) * x2)) + ((- p) * (x1 - x2))).| <= |.((q - b) - ((a + p) * x2)).| + |.((- p) * (x1 - x2)).| by COMPLEX1:56;
|.((a + p) * (x1 - x2)).| + |.((- p) * (x1 - x2)).| = (|.(a + p).| * |.(x1 - x2).|) + |.((- p) * (x1 - x2)).| by COMPLEX1:65
.= (|.(a + p).| * |.(x1 - x2).|) + (|.(- p).| * |.(x1 - x2).|) by COMPLEX1:65
.= ((a + p) * |.(x1 - x2).|) + (|.(- p).| * |.(x1 - x2).|) by ABSVALUE:def 1, AP
.= ((a + p) * |.(x1 - x2).|) + ((- (- p)) * |.(x1 - x2).|) by ABSVALUE:def 1, AP
.= ((a + p) + p) * |.(x1 - x2).| ;
then D31: |.((f . x1) - (f . x2)).| <= ((a + p) + p) * |.(x1 - x2).| by D5, X29, D30, XXREAL_0:2;
( (a + p) + p <= max (((a + p) + a),((a + p) + p)) & |.(x1 - x2).| >= 0 ) by XXREAL_0:25, COMPLEX1:46;
then ((a + p) + p) * |.(x1 - x2).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| by XREAL_1:64;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| ) by D31, XXREAL_0:2; :: thesis: verum
end;
suppose E1: x2 >= (q - b) / (a + p) ; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| )
then x2 in [.((q - b) / (a + p)),+infty.[ by XXREAL_1:236;
then E3: x2 in dom ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) by FUNCT_2:def 1;
E4: f . x2 = ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) . x2 by FUNCT_4:13, E3, FF
.= (AffineMap ((- p),q)) . x2 by FUNCT_1:49, E1, XXREAL_1:236 ;
|.((f . x1) - (f . x2)).| = |.((((- p) * x1) + q) - ((AffineMap ((- p),q)) . x2)).| by FCONT_1:def 4, E4, B23
.= |.((((- p) * x1) + q) - (((- p) * x2) + q)).| by FCONT_1:def 4
.= |.((- p) * (x1 - x2)).|
.= |.(- p).| * |.(x1 - x2).| by COMPLEX1:65 ;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| ) by PP, A3, XREAL_1:64; :: thesis: verum
end;
end;
end;
end;
end;
hence ( 0 < max (((a + p) + a),((a + p) + p)) & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= (max (((a + p) + a),((a + p) + p))) * |.(x1 - x2).| ) ) by XXREAL_0:def 10, AP; :: thesis: verum
end;
hence f is Lipschitzian ; :: thesis: verum