let a, b be Real; :: thesis: for F being PartFunc of REAL,REAL holds
( F is_convex_on [.a,b.] iff ( [.a,b.] c= dom F & ( for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds
((F . x1) - (F . x2)) / (x1 - x2) <= ((F . x2) - (F . x3)) / (x2 - x3) ) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds
((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3) ) ) )
thus ( f is_convex_on [.a,b.] implies ( [.a,b.] c= dom f & ( for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds
((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3) ) ) ) :: thesis: ( [.a,b.] c= dom f & ( for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds
((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3) ) implies f is_convex_on [.a,b.] )
proof
assume A1: f is_convex_on [.a,b.] ; :: thesis: ( [.a,b.] c= dom f & ( for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds
((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3) ) )
hence [.a,b.] c= dom f ; :: thesis: for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds
((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3)
let x1, x2, x3 be Real; :: thesis: ( x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 implies ((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3) )
assume that
A2: ( x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] ) and
A3: x1 < x2 and
A4: x2 < x3 ; :: thesis: ((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3)
A5: x2 - x3 < 0 by A4, XREAL_1:49;
set r = (x2 - x3) / (x1 - x3);
A6: ( ((x2 - x3) / (x1 - x3)) * ((f . x2) - (f . x1)) = (((x2 - x3) / (x1 - x3)) * (f . x2)) - (((x2 - x3) / (x1 - x3)) * (f . x1)) & (1 - ((x2 - x3) / (x1 - x3))) * ((f . x3) - (f . x2)) = ((1 - ((x2 - x3) / (x1 - x3))) * (f . x3)) - ((1 - ((x2 - x3) / (x1 - x3))) * (f . x2)) ) ;
A7: (x1 - x2) / (x1 - x3) = ((x1 - x3) ") * (x1 - x2) by XCMPLX_0:def 9;
x1 < x3 by A3, A4, XXREAL_0:2;
then A8: x1 - x3 < 0 by XREAL_1:49;
A9: ((x2 - x3) / (x1 - x3)) + ((x1 - x2) / (x1 - x3)) = ((x1 - x2) + (x2 - x3)) / (x1 - x3) by XCMPLX_1:62
.= 1 by A8, XCMPLX_1:60 ;
then A10: (((x2 - x3) / (x1 - x3)) * x1) + ((1 - ((x2 - x3) / (x1 - x3))) * x3) = ((x1 * (x2 - x3)) / (x1 - x3)) + (x3 * ((x1 - x2) / (x1 - x3))) by XCMPLX_1:74
.= ((x1 * (x2 - x3)) / (x1 - x3)) + ((x3 * (x1 - x2)) / (x1 - x3)) by XCMPLX_1:74
.= (((x2 * x1) - (x3 * x1)) + ((x1 - x2) * x3)) / (x1 - x3) by XCMPLX_1:62
.= (x2 * (x1 - x3)) / (x1 - x3)
.= x2 by A8, XCMPLX_1:89 ;
A11: x1 - x2 < 0 by A3, XREAL_1:49;
then (x2 - x3) / (x1 - x3) <= 1 by A8, A9, XREAL_1:29, XREAL_1:140;
then (((x2 - x3) / (x1 - x3)) * (f . x2)) + ((1 - ((x2 - x3) / (x1 - x3))) * (f . x2)) <= (((x2 - x3) / (x1 - x3)) * (f . x1)) + ((1 - ((x2 - x3) / (x1 - x3))) * (f . x3)) by A1, A2, A5, A8, A10;
then ((x2 - x3) / (x1 - x3)) * ((f . x2) - (f . x1)) <= (1 - ((x2 - x3) / (x1 - x3))) * ((f . x3) - (f . x2)) by A6, XREAL_1:21;
then - ((1 - ((x2 - x3) / (x1 - x3))) * ((f . x3) - (f . x2))) <= - (((x2 - x3) / (x1 - x3)) * ((f . x2) - (f . x1))) by XREAL_1:24;
then (1 - ((x2 - x3) / (x1 - x3))) * (- ((f . x3) - (f . x2))) <= ((x2 - x3) / (x1 - x3)) * (- ((f . x2) - (f . x1))) ;
then (((x1 - x3) ") * (x1 - x2)) * ((f . x2) - (f . x3)) <= (((x1 - x3) ") * (x2 - x3)) * ((f . x1) - (f . x2)) by A9, A7, XCMPLX_0:def 9;
then A12: (x1 - x3) * ((((x1 - x3) ") * (x2 - x3)) * ((f . x1) - (f . x2))) <= (x1 - x3) * ((((x1 - x3) ") * (x1 - x2)) * ((f . x2) - (f . x3))) by A8, XREAL_1:65;
set v = (x1 - x2) * ((f . x2) - (f . x3));
set u = (x2 - x3) * ((f . x1) - (f . x2));
A13: (x1 - x3) * ((((x1 - x3) ") * (x1 - x2)) * ((f . x2) - (f . x3))) = ((x1 - x3) * ((x1 - x3) ")) * ((x1 - x2) * ((f . x2) - (f . x3)))
.= 1 * ((x1 - x2) * ((f . x2) - (f . x3))) by A8, XCMPLX_0:def 7
.= (x1 - x2) * ((f . x2) - (f . x3)) ;
(x1 - x3) * ((((x1 - x3) ") * (x2 - x3)) * ((f . x1) - (f . x2))) = ((x1 - x3) * ((x1 - x3) ")) * ((x2 - x3) * ((f . x1) - (f . x2)))
.= 1 * ((x2 - x3) * ((f . x1) - (f . x2))) by A8, XCMPLX_0:def 7
.= (x2 - x3) * ((f . x1) - (f . x2)) ;
hence ((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3) by A5, A11, A12, A13, XREAL_1:103; :: thesis: verum
end;
assume that
A14: [.a,b.] c= dom f and
A15: for x1, x2, x3 being Real st x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 holds
((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3) ; :: thesis: f is_convex_on [.a,b.]
now :: thesis: for p being Real st 0 <= p & p <= 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] holds
f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
let p be Real; :: thesis: ( 0 <= p & p <= 1 implies for x, y being Real st x in [.a,b.] & y in [.a,b.] holds
f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) )
assume that
A16: 0 <= p and
A17: p <= 1 ; :: thesis: for x, y being Real st x in [.a,b.] & y in [.a,b.] holds
f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
A18: 0 <= 1 - p by A17, XREAL_1:48;
let x, y be Real; :: thesis: ( x in [.a,b.] & y in [.a,b.] implies f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) )
set r = (p * x) + ((1 - p) * y);
assume that
A19: x in [.a,b.] and
A20: y in [.a,b.] ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
A21: (p * y) + ((1 - p) * y) = y ;
A22: { s where s is Real : ( a <= s & s <= b ) } = [.a,b.] by RCOMP_1:def 1;
then A23: ex t being Real st
( t = y & a <= t & t <= b ) by A20;
then A24: (1 - p) * y <= (1 - p) * b by A18, XREAL_1:64;
A25: ex t being Real st
( t = x & a <= t & t <= b ) by A22, A19;
then ( (p * b) + ((1 - p) * b) = b & p * x <= p * b ) by A16, XREAL_1:64;
then A26: (p * x) + ((1 - p) * y) <= b by A24, XREAL_1:7;
A27: (1 - p) * a <= (1 - p) * y by A18, A23, XREAL_1:64;
( (p * a) + ((1 - p) * a) = a & p * a <= p * x ) by A16, A25, XREAL_1:64;
then a <= (p * x) + ((1 - p) * y) by A27, XREAL_1:7;
then A28: (p * x) + ((1 - p) * y) in [.a,b.] by A22, A26;
A29: (p * x) + ((1 - p) * x) = x ;
now :: thesis: ( ( x = y & f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ) or ( x <> y & f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ) )
per cases ( x = y or x <> y ) ;
case x = y ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ; :: thesis: verum
end;
case A30: x <> y ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
now :: thesis: ( ( p = 0 & f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ) or ( p <> 0 & f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ) )
per cases ( p = 0 or p <> 0 ) ;
case p = 0 ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ; :: thesis: verum
end;
case A31: p <> 0 ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
now :: thesis: ( ( p = 1 & f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ) or ( p <> 1 & f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ) )
per cases ( p = 1 or p <> 1 ) ;
case p = 1 ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ; :: thesis: verum
end;
case p <> 1 ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
then p < 1 by A17, XXREAL_0:1;
then A32: 0 < 1 - p by XREAL_1:50;
now :: thesis: ( ( x < y & f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ) or ( y < x & f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ) )
per cases ( x < y or y < x ) by A30, XXREAL_0:1;
case A33: x < y ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
then (1 - p) * x < (1 - p) * y by A32, XREAL_1:68;
then A34: x < (p * x) + ((1 - p) * y) by A29, XREAL_1:8;
then A35: x - ((p * x) + ((1 - p) * y)) < 0 by XREAL_1:49;
p * x < p * y by A16, A31, A33, XREAL_1:68;
then A36: (p * x) + ((1 - p) * y) < y by A21, XREAL_1:8;
then A37: ((p * x) + ((1 - p) * y)) - y < 0 by XREAL_1:49;
A38: x - y < 0 by A33, XREAL_1:49;
((f . x) - (f . ((p * x) + ((1 - p) * y)))) / (x - ((p * x) + ((1 - p) * y))) <= ((f . ((p * x) + ((1 - p) * y))) - (f . y)) / (((p * x) + ((1 - p) * y)) - y) by A15, A19, A20, A28, A36, A34;
then ((f . x) - (f . ((p * x) + ((1 - p) * y)))) * (p * (x - y)) <= ((f . ((p * x) + ((1 - p) * y))) - (f . y)) * ((1 - p) * (x - y)) by A37, A35, XREAL_1:107;
then ((((f . x) - (f . ((p * x) + ((1 - p) * y)))) * p) * (x - y)) / (x - y) >= ((((f . ((p * x) + ((1 - p) * y))) - (f . y)) * (1 - p)) * (x - y)) / (x - y) by A38, XREAL_1:73;
then ((((f . ((p * x) + ((1 - p) * y))) - (f . y)) * (1 - p)) * (x - y)) / (x - y) <= ((f . x) - (f . ((p * x) + ((1 - p) * y)))) * p by A38, XCMPLX_1:89;
then ((f . ((p * x) + ((1 - p) * y))) * (1 - p)) - ((f . y) * (1 - p)) <= ((f . x) * p) - ((f . ((p * x) + ((1 - p) * y))) * p) by A38, XCMPLX_1:89;
then ((f . ((p * x) + ((1 - p) * y))) * p) + (((f . ((p * x) + ((1 - p) * y))) * (1 - p)) - ((f . y) * (1 - p))) <= (f . x) * p by XREAL_1:19;
then (((f . ((p * x) + ((1 - p) * y))) * p) + ((f . ((p * x) + ((1 - p) * y))) * (1 - p))) - ((f . y) * (1 - p)) <= (f . x) * p ;
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) by XREAL_1:20; :: thesis: verum
end;
case A39: y < x ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
then (1 - p) * y < (1 - p) * x by A32, XREAL_1:68;
then A40: (p * x) + ((1 - p) * y) < x by A29, XREAL_1:8;
then A41: ((p * x) + ((1 - p) * y)) - x < 0 by XREAL_1:49;
p * y < p * x by A16, A31, A39, XREAL_1:68;
then A42: y < (p * x) + ((1 - p) * y) by A21, XREAL_1:8;
then A43: y - ((p * x) + ((1 - p) * y)) < 0 by XREAL_1:49;
A44: y - x < 0 by A39, XREAL_1:49;
((f . y) - (f . ((p * x) + ((1 - p) * y)))) / (y - ((p * x) + ((1 - p) * y))) <= ((f . ((p * x) + ((1 - p) * y))) - (f . x)) / (((p * x) + ((1 - p) * y)) - x) by A15, A19, A20, A28, A42, A40;
then ((f . y) - (f . ((p * x) + ((1 - p) * y)))) * ((1 - p) * (y - x)) <= ((f . ((p * x) + ((1 - p) * y))) - (f . x)) * (p * (y - x)) by A43, A41, XREAL_1:107;
then ((((f . y) - (f . ((p * x) + ((1 - p) * y)))) * (1 - p)) * (y - x)) / (y - x) >= ((((f . ((p * x) + ((1 - p) * y))) - (f . x)) * p) * (y - x)) / (y - x) by A44, XREAL_1:73;
then ((((f . ((p * x) + ((1 - p) * y))) - (f . x)) * p) * (y - x)) / (y - x) <= ((f . y) - (f . ((p * x) + ((1 - p) * y)))) * (1 - p) by A44, XCMPLX_1:89;
then ((f . ((p * x) + ((1 - p) * y))) * p) - ((f . x) * p) <= ((f . y) * (1 - p)) - ((f . ((p * x) + ((1 - p) * y))) * (1 - p)) by A44, XCMPLX_1:89;
then (((f . ((p * x) + ((1 - p) * y))) * p) - ((f . x) * p)) + ((f . ((p * x) + ((1 - p) * y))) * (1 - p)) <= (f . y) * (1 - p) by XREAL_1:19;
then (((f . ((p * x) + ((1 - p) * y))) * p) + ((f . ((p * x) + ((1 - p) * y))) * (1 - p))) - ((f . x) * p) <= (f . y) * (1 - p) ;
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) by XREAL_1:20; :: thesis: verum
end;
end;
end;
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ; :: thesis: verum
end;
end;
end;
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ; :: thesis: verum
end;
end;
end;
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ; :: thesis: verum
end;
end;
end;
hence f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y)) ; :: thesis: verum
end;
hence f is_convex_on [.a,b.] by A14; :: thesis: verum