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 by Def13; :: 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 A2: ( x1 in [.a,b.] & x2 in [.a,b.] & x3 in [.a,b.] & x1 < x2 & x2 < x3 ) ; :: thesis: ((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3)
then A3: ( 0 < x3 - x2 & x2 - x3 < 0 & 0 < x2 - x1 & x1 - x2 < 0 ) by XREAL_1:51, XREAL_1:52;
x1 < x3 by A2, XXREAL_0:2;
then A4: ( x1 - x3 < 0 & 0 <> x1 - x3 ) by XREAL_1:51;
set r = (x2 - x3) / (x1 - x3);
A5: ((x2 - x3) / (x1 - x3)) + ((x1 - x2) / (x1 - x3)) = ((x1 - x2) + (x2 - x3)) / (x1 - x3) by XCMPLX_1:63
.= 1 by A4, XCMPLX_1:60 ;
then A6: (((x2 - x3) / (x1 - x3)) * x1) + ((1 - ((x2 - x3) / (x1 - x3))) * x3) = ((x1 * (x2 - x3)) / (x1 - x3)) + (x3 * ((x1 - x2) / (x1 - x3))) by XCMPLX_1:75
.= ((x1 * (x2 - x3)) / (x1 - x3)) + ((x3 * (x1 - x2)) / (x1 - x3)) by XCMPLX_1:75
.= (((x2 * x1) - (x3 * x1)) + ((x1 - x2) * x3)) / (x1 - x3) by XCMPLX_1:63
.= (x2 * (x1 - x3)) / (x1 - x3)
.= x2 by A4, XCMPLX_1:90 ;
A7: 0 <= (x2 - x3) / (x1 - x3) by A3, A4;
(x1 - x2) / (x1 - x3) > 0 by A3, A4, XREAL_1:142;
then (x2 - x3) / (x1 - x3) <= 1 by A5, XREAL_1:31;
then A8: (((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, A6, A7, Def13;
A9: ((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)) ;
then ((x2 - x3) / (x1 - x3)) * ((f . x2) - (f . x1)) <= (1 - ((x2 - x3) / (x1 - x3))) * ((f . x3) - (f . x2)) by A8, A9, XREAL_1:23;
then - ((1 - ((x2 - x3) / (x1 - x3))) * ((f . x3) - (f . x2))) <= - (((x2 - x3) / (x1 - x3)) * ((f . x2) - (f . x1))) by XREAL_1:26;
then A10: (1 - ((x2 - x3) / (x1 - x3))) * (- ((f . x3) - (f . x2))) <= ((x2 - x3) / (x1 - x3)) * (- ((f . x2) - (f . x1))) ;
(x1 - x2) / (x1 - x3) = ((x1 - x3) " ) * (x1 - x2) by XCMPLX_0:def 9;
then (((x1 - x3) " ) * (x1 - x2)) * ((f . x2) - (f . x3)) <= (((x1 - x3) " ) * (x2 - x3)) * ((f . x1) - (f . x2)) by A5, A10, XCMPLX_0:def 9;
then A11: (x1 - x3) * ((((x1 - x3) " ) * (x2 - x3)) * ((f . x1) - (f . x2))) <= (x1 - x3) * ((((x1 - x3) " ) * (x1 - x2)) * ((f . x2) - (f . x3))) by A4, XREAL_1:67;
set u = (x2 - x3) * ((f . x1) - (f . x2));
set v = (x1 - x2) * ((f . x2) - (f . x3));
A12: (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 A4, XCMPLX_0:def 7
.= (x2 - x3) * ((f . x1) - (f . x2)) ;
(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 A4, XCMPLX_0:def 7
.= (x1 - x2) * ((f . x2) - (f . x3)) ;
hence ((f . x1) - (f . x2)) / (x1 - x2) <= ((f . x2) - (f . x3)) / (x2 - x3) by A3, A11, A12, XREAL_1:105; :: thesis: verum

end;

assume that
A13: [.a,b.] c= dom f and
A14: 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

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 A15: ( 0 <= p & 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))
then A16: 0 <= 1 - p by XREAL_1:50;
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);
A17: { s where s is Real : ( a <= s & s <= b ) } = [.a,b.] by RCOMP_1:def 1;
A18: (p * x) + ((1 - p) * x) = x ;
A19: (p * y) + ((1 - p) * y) = y ;
A20: (p * a) + ((1 - p) * a) = a ;
A21: (p * b) + ((1 - p) * b) = b ;
assume A22: ( x in [.a,b.] & y in [.a,b.] ) ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))
then ( ex t being Real st
( t = x & a <= t & t <= b ) & ex t being Real st
( t = y & a <= t & t <= b ) ) by A17;
then ( p * a <= p * x & (1 - p) * a <= (1 - p) * y & p * x <= p * b & (1 - p) * y <= (1 - p) * b ) by A15, A16, XREAL_1:66;
then ( a <= (p * x) + ((1 - p) * y) & (p * x) + ((1 - p) * y) <= b ) by A20, A21, XREAL_1:9;
then A23: (p * x) + ((1 - p) * y) in [.a,b.] by A17;

now

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 A24: x <> y ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))

now

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 A25: p <> 0 ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))

now

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 A15, XXREAL_0:1;
then A26: 0 < 1 - p by XREAL_1:52;

now

per cases ( x < y or y < x ) by A24, XXREAL_0:1;

case A27: x < y ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))

then p * x < p * y by A15, A25, XREAL_1:70;
then A28: (p * x) + ((1 - p) * y) < y by A19, XREAL_1:10;
then A29: ((p * x) + ((1 - p) * y)) - y < 0 by XREAL_1:51;
(1 - p) * x < (1 - p) * y by A26, A27, XREAL_1:70;
then A30: x < (p * x) + ((1 - p) * y) by A18, XREAL_1:10;
then A31: x - ((p * x) + ((1 - p) * y)) < 0 by XREAL_1:51;
A32: ( x - y < 0 & x - y <> 0 ) by A27, XREAL_1:51;
((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 A14, A22, A23, A28, A30;
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 A29, A31, XREAL_1:109;
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 A32, XREAL_1:75;
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 A32, XCMPLX_1:90;
then ((f . ((p * x) + ((1 - p) * y))) * (1 - p)) - ((f . y) * (1 - p)) <= ((f . x) * p) - ((f . ((p * x) + ((1 - p) * y))) * p) by A32, XCMPLX_1:90;
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:21;
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:22; :: thesis: verum

end;

case A33: y < x ; :: thesis: f . ((p * x) + ((1 - p) * y)) <= (p * (f . x)) + ((1 - p) * (f . y))

then p * y < p * x by A15, A25, XREAL_1:70;
then A34: y < (p * x) + ((1 - p) * y) by A19, XREAL_1:10;
then A35: y - ((p * x) + ((1 - p) * y)) < 0 by XREAL_1:51;
(1 - p) * y < (1 - p) * x by A26, A33, XREAL_1:70;
then A36: (p * x) + ((1 - p) * y) < x by A18, XREAL_1:10;
then A37: ((p * x) + ((1 - p) * y)) - x < 0 by XREAL_1:51;
A38: ( y - x < 0 & y - x <> 0 ) by A33, XREAL_1:51;
((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 A14, A22, A23, A34, A36;
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 A35, A37, XREAL_1:109;
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 A38, XREAL_1:75;
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 A38, XCMPLX_1:90;
then ((f . ((p * x) + ((1 - p) * y))) * p) - ((f . x) * p) <= ((f . y) * (1 - p)) - ((f . ((p * x) + ((1 - p) * y))) * (1 - p)) by A38, XCMPLX_1:90;
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:21;
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:22; :: 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 A13, Th55; :: thesis: verum