let f be Function of REAL,REAL; :: thesis: for a, b, c, d, r, s being Real st ( for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ) holds
f is Lipschitzian
let a, b, c, d, r, s be Real; :: thesis: ( ( for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ) implies f is Lipschitzian )
assume A1: for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ; :: thesis: f is Lipschitzian
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
per cases ( c = 0 or c <> 0 ) ;
suppose C1: c = 0 ; :: thesis: 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).| ) )
take 1 ; :: thesis: ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
proof
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1
.= |.((max (r,(min (s,((0 * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((0 * (sin ((a * x2) + b))) + d)))))).| by C1, A1
.= 0 by COMPLEX1:44 ;
hence |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| by COMPLEX1:46; :: thesis: verum
end;
hence ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum
end;
suppose A3: c <> 0 ; :: thesis: 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).| ) )
per cases ( a = 0 or a <> 0 ) ;
suppose A0: a = 0 ; :: thesis: 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).| ) )
take 1 ; :: thesis: ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
proof
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| )
|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1
.= |.((max (r,(min (s,((c * (sin ((0 * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((0 * x2) + b))) + d)))))).| by A0, A1
.= 0 by COMPLEX1:44 ;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) by COMPLEX1:46; :: thesis: verum
end;
hence ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum
end;
suppose A2: a <> 0 ; :: thesis: 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).| ) )
take |.a.| * |.c.| ; :: thesis: ( 0 < |.a.| * |.c.| & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| ) )
A5: ( |.c.| > 0 & |.a.| > 0 ) by A2, A3, COMPLEX1:47;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).|
proof
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).|
A9: |.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1
.= |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((a * x2) + b))) + d)))))).| by A1 ;
A7: |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((a * x2) + b))) + d)))))).| <= |.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| by LeMM01;
A8: |.c.| * |.(((a * x1) + b) - ((a * x2) + b)).| = |.c.| * |.(a * (x1 - x2)).|
.= |.c.| * (|.a.| * |.(x1 - x2).|) by COMPLEX1:65 ;
A6: ( |.(c * ((sin ((a * x1) + b)) - (sin ((a * x2) + b)))).| = |.c.| * |.((sin ((a * x1) + b)) - (sin ((a * x2) + b))).| & |.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| = |.(c * ((sin ((a * x1) + b)) - (sin ((a * x2) + b)))).| ) by COMPLEX1:65;
|.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| <= |.c.| * |.(((a * x1) + b) - ((a * x2) + b)).| by XREAL_1:64, A5, A6, LmSin2;
hence |.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| by A9, A8, A7, XXREAL_0:2; :: thesis: verum
end;
hence ( 0 < |.a.| * |.c.| & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| ) ) by A5; :: thesis: verum
end;
end;
end;
end;
end;
hence f is Lipschitzian ; :: thesis: verum