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: ( 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 that
A2: X c= dom f and
A3: 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 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 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 A5: ( 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 :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
per cases ( p = 0 or p = 1 or ( 0 < p & p < 1 ) ) by A4, 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 A6: ( 0 < p & p < 1 ) ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
then A7: 1 - p > 0 by XREAL_1:50;
now :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
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 A8: t - s > 0 by XREAL_1:50;
((p * s) + ((1 - p) * t)) - s = (1 - p) * (t - s) ;
then A9: ((p * s) + ((1 - p) * t)) - s > 0 by A7, A8, XREAL_1:129;
then A10: (p * s) + ((1 - p) * t) > s by XREAL_1:47;
A11: ( (((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))))) ) ;
t - ((p * s) + ((1 - p) * t)) = p * (t - s) ;
then A12: t - ((p * s) + ((1 - p) * t)) > 0 by A6, A8, XREAL_1:129;
then (p * s) + ((1 - p) * t) < t by XREAL_1:47;
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 A3, A5, A10;
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 ((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 A12, A9, XREAL_1:106;
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 A11, XREAL_1:21;
then f . ((p * s) + ((1 - p) * t)) <= ((((1 - p) * (f . t)) * (t - s)) + ((p * (f . s)) * (t - s))) / (t - s) by A8, XREAL_1:77;
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:62;
then f . ((p * s) + ((1 - p) * t)) <= ((1 - p) * (f . t)) + (((p * (f . s)) * (t - s)) / (t - s)) by A8, XCMPLX_1:89;
hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) by A8, XCMPLX_1:89; :: thesis: verum
end;
suppose s > t ; :: thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t))
then A13: s - t > 0 by XREAL_1:50;
((p * s) + ((1 - p) * t)) - t = p * (s - t) ;
then A14: ((p * s) + ((1 - p) * t)) - t > 0 by A6, A13, XREAL_1:129;
then A15: (p * s) + ((1 - p) * t) > t by XREAL_1:47;
A16: ( (((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))))) ) ;
s - ((p * s) + ((1 - p) * t)) = (1 - p) * (s - t) ;
then A17: s - ((p * s) + ((1 - p) * t)) > 0 by A7, A13, XREAL_1:129;
then (p * s) + ((1 - p) * t) < s by XREAL_1:47;
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 A3, A5, A15;
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 ((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 A17, A14, XREAL_1:106;
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 A16, XREAL_1:21;
then f . ((p * s) + ((1 - p) * t)) <= (((p * (f . s)) * (s - t)) + (((1 - p) * (f . t)) * (s - t))) / (s - t) by A13, XREAL_1:77;
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:62;
then f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by A13, XCMPLX_1:89;
hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) by A13, XCMPLX_1:89; :: 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 A2, RFUNCT_3:def 12; :: thesis: verum
end;
( 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 A18: 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) ) ) )
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 that
A19: ( a in X & b in X & r in X ) and
A20: a < r and
A21: 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) )
reconsider aa = a, bb = b as Real ;
A22: ( b - r < b - a & 0 < b - r ) by A20, A21, XREAL_1:10, XREAL_1:50;
reconsider p = (b - r) / (b - a) as Real ;
A23: 0 < r - a by A20, XREAL_1:50;
A24: p + ((r - a) / (b - a)) = ((b - r) + (r - a)) / (b - a) by XCMPLX_1:62
.= 1 by A22, XCMPLX_1:60 ;
then (p * a) + ((1 - p) * b) = ((a * (b - r)) / (b - a)) + (b * ((r - a) / (b - a))) by XCMPLX_1:74
.= ((a * (b - r)) / (b - a)) + ((b * (r - a)) / (b - a)) by XCMPLX_1:74
.= (((b * a) - (r * a)) + ((r - a) * b)) / (b - a) by XCMPLX_1:62
.= (r * (b - a)) / (b - a) ;
then A25: (p * a) + ((1 - p) * b) = r by A22, XCMPLX_1:89;
A26: (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 A22, XCMPLX_1:87
.= ((b - r) * (f . a)) + ((r - a) * (f . b)) by A22, XCMPLX_1:87 ;
(bb - r) / (bb - aa) < 1 by A22, XREAL_1:189;
then A27: f . ((p * a) + ((1 - p) * b)) <= (p * (f . a)) + ((1 - p) * (f . b)) by A18, A19, A22, A25, RFUNCT_3:def 12;
then (b - a) * (f . r) <= ((b - a) * (f . a)) + (((r - a) * (f . b)) - ((r - a) * (f . a))) by A22, A24, A25, A26, XREAL_1:64;
then ((b - a) * (f . r)) - ((b - a) * (f . a)) <= ((r - a) * (f . b)) - ((r - a) * (f . a)) by XREAL_1:20;
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 A22, A23, XREAL_1:102; :: 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 A22, A24, A25, A27, A26, XREAL_1:64;
then (((b - r) * (f . b)) - ((b - r) * (f . a))) + ((b - a) * (f . r)) <= (b - a) * (f . b) by XREAL_1:19;
then ((b - r) * (f . b)) - ((b - r) * (f . a)) <= ((b - a) * (f . b)) - ((b - a) * (f . r)) by XREAL_1:19;
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 A22, XREAL_1:102; :: 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) ) ) ) by A18, RFUNCT_3:def 12; :: 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