let f be PartFunc of REAL ,REAL ; :: thesis: for X being set holds
( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) )
let X be set ; :: thesis: ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) )
A1: ( f is_convex_on X implies ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) )

proof

assume A2: f is_convex_on X ; :: thesis: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) )
( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) )

proof

thus X c= dom f by A2, RFUNCT_3:def 13; :: thesis: for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) )
for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) )

proof

let a, b, r be Real; :: thesis: ( a in X & b in X & r in X & a < r & r < b implies ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) )
assume A3: ( a in X & b in X & r in X & a < r & r < b ) ; :: thesis: ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) )
then A4: ( b - r < b - a & 0 < b - r & 0 < r - a ) by XREAL_1:12, XREAL_1:52;
then A5: ( 0 < (b - r) / (b - a) & (b - r) / (b - a) < 1 ) by XREAL_1:141, XREAL_1:191;
set p = (b - r) / (b - a);
A6: ( 1 - ((b - r) / (b - a)) = (r - a) / (b - a) & (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = r )

proof

A7: ((b - r) / (b - a)) + ((r - a) / (b - a)) = ((b - r) + (r - a)) / (b - a) by XCMPLX_1:63
.= 1 by A4, XCMPLX_1:60 ;
hence 1 - ((b - r) / (b - a)) = (r - a) / (b - a) ; :: thesis: (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = r
(((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = ((a * (b - r)) / (b - a)) + (b * ((r - a) / (b - a))) by A7, XCMPLX_1:75
.= ((a * (b - r)) / (b - a)) + ((b * (r - a)) / (b - a)) by XCMPLX_1:75
.= (((b * a) - (r * a)) + ((r - a) * b)) / (b - a) by XCMPLX_1:63
.= (r * (b - a)) / (b - a) ;
hence (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = r by A4, XCMPLX_1:90; :: thesis: verum

end;

then A8: f . ((((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b)) <= (((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b)) by A2, A3, A5, RFUNCT_3:def 13;
A9: (b - a) * ((((b - r) / (b - a)) * (f . a)) + (((r - a) / (b - a)) * (f . b))) = (((b - a) * ((b - r) / (b - a))) * (f . a)) + ((b - a) * (((r - a) / (b - a)) * (f . b)))
.= ((b - r) * (f . a)) + (((b - a) * ((r - a) / (b - a))) * (f . b)) by A4, XCMPLX_1:88
.= ((b - r) * (f . a)) + ((r - a) * (f . b)) by A4, XCMPLX_1:88 ;
then (b - a) * (f . r) <= ((b - a) * (f . a)) + (((r - a) * (f . b)) - ((r - a) * (f . a))) by A4, A6, A8, XREAL_1:66;
then ((b - a) * (f . r)) - ((b - a) * (f . a)) <= ((r - a) * (f . b)) - ((r - a) * (f . a)) by XREAL_1:22;
then (b - a) * ((f . r) - (f . a)) <= (r - a) * ((f . b) - (f . a)) ;
hence ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) by A4, XREAL_1:104; :: thesis: ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r)
(b - a) * (f . r) <= ((b - a) * (f . b)) - (((b - r) * (f . b)) - ((b - r) * (f . a))) by A4, A6, A8, A9, XREAL_1:66;
then (((b - r) * (f . b)) - ((b - r) * (f . a))) + ((b - a) * (f . r)) <= (b - a) * (f . b) by XREAL_1:21;
then ((b - r) * (f . b)) - ((b - r) * (f . a)) <= ((b - a) * (f . b)) - ((b - a) * (f . r)) by XREAL_1:21;
then (b - r) * ((f . b) - (f . a)) <= (b - a) * ((f . b) - (f . r)) ;
hence ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) by A4, XREAL_1:104; :: thesis: verum

end;

hence for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ; :: thesis: verum

end;

hence ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ; :: thesis: verum

end;

( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) implies f is_convex_on X )

proof

assume A10: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ; :: thesis: f is_convex_on X
for p being Real st 0 <= p & p <= 1 holds
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))

proof

let p be Real; :: thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) )
assume A11: ( 0 <= p & p <= 1 ) ; :: thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
for s, t being Real st s in X & t in X & (p * s) + ((1 - p) * t) in X holds
f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))

proof

let s, t be Real; :: thesis: ( s in X & t in X & (p * s) + ((1 - p) * t) in X implies f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) )
assume A12: ( s in X & t in X & (p * s) + ((1 - p) * t) in X ) ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))

now

per cases ( p = 0 or p = 1 or ( 0 < p & p < 1 ) ) by A11, XXREAL_0:1;

suppose p = 0 ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))

hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; :: thesis: verum

end;

suppose p = 1 ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))

hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; :: thesis: verum

end;

suppose A13: ( 0 < p & p < 1 ) ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))

then A14: 1 - p > 0 by XREAL_1:52;

now

per cases ( s = t or s < t or s > t ) by XXREAL_0:1;

suppose s = t ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))

hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; :: thesis: verum

end;

suppose s < t ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))

then A15: t - s > 0 by XREAL_1:52;
t - ((p * s) + ((1 - p) * t)) = p * (t - s) ;
then A16: t - ((p * s) + ((1 - p) * t)) > 0 by A13, A15, XREAL_1:131;
then A17: (p * s) + ((1 - p) * t) < t by XREAL_1:49;
((p * s) + ((1 - p) * t)) - s = (1 - p) * (t - s) ;
then A18: ((p * s) + ((1 - p) * t)) - s > 0 by A14, A15, XREAL_1:131;
then (p * s) + ((1 - p) * t) > s by XREAL_1:49;
then ( ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) <= ((f . t) - (f . s)) / (t - s) & ((f . t) - (f . s)) / (t - s) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) ) by A10, A12, A17;
then ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) by XXREAL_0:2;
then A19: ((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - ((p * s) + ((1 - p) * t))) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - s) by A16, A18, XREAL_1:108;
A20: (((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - s)) * p = (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) - (p * ((t - s) * (f . s))) ;
(((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (t - s)) * (1 - p) = ((1 - p) * ((t - s) * (f . t))) - ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) ;
then (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) + ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) <= ((1 - p) * ((t - s) * (f . t))) + (p * ((t - s) * (f . s))) by A19, A20, XREAL_1:23;
then f . ((p * s) + ((1 - p) * t)) <= ((((1 - p) * (f . t)) * (t - s)) + ((p * (f . s)) * (t - s))) / (t - s) by A15, XREAL_1:79;
then f . ((p * s) + ((1 - p) * t)) <= ((((1 - p) * (f . t)) * (t - s)) / (t - s)) + (((p * (f . s)) * (t - s)) / (t - s)) by XCMPLX_1:63;
then f . ((p * s) + ((1 - p) * t)) <= ((1 - p) * (f . t)) + (((p * (f . s)) * (t - s)) / (t - s)) by A15, XCMPLX_1:90;
hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) by A15, XCMPLX_1:90; :: thesis: verum

end;

suppose s > t ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))

then A21: s - t > 0 by XREAL_1:52;
s - ((p * s) + ((1 - p) * t)) = (1 - p) * (s - t) ;
then A22: s - ((p * s) + ((1 - p) * t)) > 0 by A14, A21, XREAL_1:131;
then A23: (p * s) + ((1 - p) * t) < s by XREAL_1:49;
((p * s) + ((1 - p) * t)) - t = p * (s - t) ;
then A24: ((p * s) + ((1 - p) * t)) - t > 0 by A13, A21, XREAL_1:131;
then (p * s) + ((1 - p) * t) > t by XREAL_1:49;
then ( ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) <= ((f . s) - (f . t)) / (s - t) & ((f . s) - (f . t)) / (s - t) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) ) by A10, A12, A23;
then ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) by XXREAL_0:2;
then A25: ((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - ((p * s) + ((1 - p) * t))) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - t) by A22, A24, XREAL_1:108;
A26: (((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - t)) * (1 - p) = ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) - ((1 - p) * ((s - t) * (f . t))) ;
(((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (s - t)) * p = (p * ((s - t) * (f . s))) - (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) ;
then ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) + (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) <= (p * ((s - t) * (f . s))) + ((1 - p) * ((s - t) * (f . t))) by A25, A26, XREAL_1:23;
then f . ((p * s) + ((1 - p) * t)) <= (((p * (f . s)) * (s - t)) + (((1 - p) * (f . t)) * (s - t))) / (s - t) by A21, XREAL_1:79;
then f . ((p * s) + ((1 - p) * t)) <= (((p * (f . s)) * (s - t)) / (s - t)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by XCMPLX_1:63;
then f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by A21, XCMPLX_1:90;
hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) by A21, XCMPLX_1:90; :: thesis: verum

end;

end;

end;

hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; :: thesis: verum

end;

end;

end;

hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; :: thesis: verum

end;

hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; :: thesis: verum

end;

hence f is_convex_on X by A10, RFUNCT_3:def 13; :: thesis: verum

end;

hence ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds
( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ) by A1; :: thesis: verum