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

proof

assume that
A2: X c= dom f and
A3: for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ; :: 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 A4: ( 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 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 r, s be Real; :: thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X implies f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) )
assume A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) ; :: thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))

proof

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

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

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

end;

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

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

end;

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

then A7: 0 < 1 - p by XREAL_1:50;

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

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

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

end;

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

set t = (p * r) + ((1 - p) * s);
A9: r - s > 0 by A8, XREAL_1:50;
A10: r - ((p * r) + ((1 - p) * s)) = (1 - p) * (r - s) ;
then r - ((p * r) + ((1 - p) * s)) > 0 by A7, A9, XREAL_1:129;
then A11: (p * r) + ((1 - p) * s) < r by XREAL_1:47;
A12: ((p * r) + ((1 - p) * s)) - s = p * (r - s) ;
then A13: (((p * r) + ((1 - p) * s)) - s) / (r - s) = p by A9, XCMPLX_1:89;
((p * r) + ((1 - p) * s)) - s > 0 by A6, A9, A12, XREAL_1:129;
then A14: s < (p * r) + ((1 - p) * s) by XREAL_1:47;
(r - ((p * r) + ((1 - p) * s))) / (r - s) = 1 - p by A9, A10, XCMPLX_1:89;
hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A14, A11, A13; :: thesis: verum

end;

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

set t = (p * r) + ((1 - p) * s);
A16: s - r > 0 by A15, XREAL_1:50;
A17: s - ((p * r) + ((1 - p) * s)) = p * (s - r) ;
then s - ((p * r) + ((1 - p) * s)) > 0 by A6, A16, XREAL_1:129;
then A18: (p * r) + ((1 - p) * s) < s by XREAL_1:47;
A19: ((p * r) + ((1 - p) * s)) - r = (1 - p) * (s - r) ;
then A20: (((p * r) + ((1 - p) * s)) - r) / (s - r) = 1 - p by A16, XCMPLX_1:89;
((p * r) + ((1 - p) * s)) - r > 0 by A7, A16, A19, XREAL_1:129;
then A21: r < (p * r) + ((1 - p) * s) by XREAL_1:47;
(s - ((p * r) + ((1 - p) * s))) / (s - r) = p by A16, A17, XCMPLX_1:89;
hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A21, A18, A20; :: thesis: verum

end;

end;

end;

end;

end;

hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; :: 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 A2, RFUNCT_3:def 12; :: thesis: verum

end;

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

proof

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

proof

let a, b, c be Real; :: thesis: ( a in X & b in X & c in X & a < b & b < c implies f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) )
assume that
A23: ( a in X & b in X & c in X ) and
A24: ( a < b & b < c ) ; :: thesis: f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c))
set p = (c - b) / (c - a);
A25: ( c - b < c - a & 0 < c - b ) by A24, XREAL_1:10, XREAL_1:50;
then A26: (c - b) / (c - a) < 1 by XREAL_1:189;
A27: ((c - b) / (c - a)) + ((b - a) / (c - a)) = ((c - b) + (b - a)) / (c - a) by XCMPLX_1:62
.= 1 by A25, XCMPLX_1:60 ;
then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = ((a * (c - b)) / (c - a)) + (c * ((b - a) / (c - a))) by XCMPLX_1:74
.= ((a * (c - b)) / (c - a)) + ((c * (b - a)) / (c - a)) by XCMPLX_1:74
.= (((c * a) - (b * a)) + ((b - a) * c)) / (c - a) by XCMPLX_1:62
.= (b * (c - a)) / (c - a) ;
then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = b by A25, XCMPLX_1:89;
hence f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) by A22, A23, A25, A26, A27, RFUNCT_3:def 12; :: thesis: verum

end;

hence ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds
f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) by A22, RFUNCT_3:def 12; :: thesis: verum

end;

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