let f be PartFunc of REAL,REAL; :: thesis: for X being set holds
( f is_strictly_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_strictly_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_strictly_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_strictly_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 & r <> s 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 & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) )
assume that
A4: 0 < p and
A5: p < 1 ; :: thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
A6: 1 - p > 0 by A5, XREAL_1:50;
for s, t being Real st s in X & t in X & (p * s) + ((1 - p) * t) in X & s <> t 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 & s <> t implies f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) )
assume that
A7: ( s in X & t in X & (p * s) + ((1 - p) * t) in X ) and
A8: s <> t ; :: 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 ( s < t or s > t ) by A8, XXREAL_0:1;

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

then A9: t - s > 0 by XREAL_1:50;
((p * s) + ((1 - p) * t)) - s = (1 - p) * (t - s) ;
then A10: ((p * s) + ((1 - p) * t)) - s > 0 by A6, A9, XREAL_1:129;
then A11: (p * s) + ((1 - p) * t) > s by XREAL_1:47;
A12: ( (((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 A13: t - ((p * s) + ((1 - p) * t)) > 0 by A4, A9, 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, A7, A11;
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 A13, A10, XREAL_1:102;
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 A12, XREAL_1:21;
then f . ((p * s) + ((1 - p) * t)) < ((((1 - p) * (f . t)) * (t - s)) + ((p * (f . s)) * (t - s))) / (t - s) by A9, XREAL_1:81;
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 A9, XCMPLX_1:89;
hence f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) by A9, XCMPLX_1:89; :: thesis: verum

end;

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

then A14: s - t > 0 by XREAL_1:50;
((p * s) + ((1 - p) * t)) - t = p * (s - t) ;
then A15: ((p * s) + ((1 - p) * t)) - t > 0 by A4, A14, XREAL_1:129;
then A16: (p * s) + ((1 - p) * t) > t by XREAL_1:47;
A17: ( (((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 A18: s - ((p * s) + ((1 - p) * t)) > 0 by A6, A14, 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, A7, A16;
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 A18, A15, XREAL_1:102;
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 A17, XREAL_1:21;
then f . ((p * s) + ((1 - p) * t)) < (((p * (f . s)) * (s - t)) + (((1 - p) * (f . t)) * (s - t))) / (s - t) by A14, XREAL_1:81;
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 A14, XCMPLX_1:89;
hence f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) by A14, 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;

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

end;

hence f is_strictly_convex_on X by A2; :: thesis: verum

end;

( f is_strictly_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 A19: f is_strictly_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
A20: ( a in X & b in X & r in X ) and
A21: a < r and
A22: 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 p = (b - r) / (b - a) as Real ;
reconsider aa = a, bb = b as Real ;
A23: ( b - r < b - a & 0 < b - r ) by A21, A22, XREAL_1:10, XREAL_1:50;
A24: p + ((r - a) / (b - a)) = ((b - r) + (r - a)) / (b - a) by XCMPLX_1:62
.= 1 by A23, 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 A23, XCMPLX_1:89;
( 0 < (b - r) / (b - a) & (bb - r) / (bb - aa) < 1 ) by A23, XREAL_1:139, XREAL_1:189;
then A26: f . r < (p * (f . a)) + ((1 - p) * (f . b)) by A19, A20, A21, A22, A25;
A27: 0 < r - a by A21, XREAL_1:50;
A28: ((p * (f . a)) + ((1 - p) * (f . b))) * (b - a) = (((b - a) * p) * (f . a)) + ((b - a) * ((1 - p) * (f . b)))
.= ((((b - a) * (b - r)) / (b - a)) * (f . a)) + (((b - a) * ((r - a) / (b - a))) * (f . b)) by A24, XCMPLX_1:74
.= ((((b - r) * (b - a)) / (b - a)) * (f . a)) + ((((b - a) * (r - a)) / (b - a)) * (f . b)) by XCMPLX_1:74
.= (((b - r) * ((b - a) / (b - a))) * (f . a)) + ((((b - a) * (r - a)) / (b - a)) * (f . b)) by XCMPLX_1:74
.= (((b - r) * 1) * (f . a)) + ((((r - a) * (b - a)) / (b - a)) * (f . b)) by A23, XCMPLX_1:60
.= ((b - r) * (f . a)) + (((r - a) * ((b - a) / (b - a))) * (f . b)) by XCMPLX_1:74
.= ((b - r) * (f . a)) + (((r - a) * 1) * (f . b)) by A23, XCMPLX_1:60 ;
then (f . r) * (b - a) < ((b - a) * (f . a)) + (((r - a) * (f . b)) - ((r - a) * (f . a))) by A23, A26, XREAL_1:68;
then ((f . r) * (b - a)) - ((b - a) * (f . a)) < ((r - a) * (f . b)) - ((r - a) * (f . a)) by XREAL_1:19;
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 A23, A27, XREAL_1:106; :: thesis: ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r)
(f . r) * (b - a) < (((r - b) * (f . b)) + ((b - r) * (f . a))) + ((b - a) * (f . b)) by A23, A26, A28, XREAL_1:68;
then ((f . r) * (b - a)) - (((r - b) * (f . b)) + ((b - r) * (f . a))) < (b - a) * (f . b) by XREAL_1:19;
then ((f . r) * (b - a)) + (- (((r - b) * (f . b)) + ((b - r) * (f . a)))) < (b - a) * (f . b) ;
then (- ((r - b) * (f . b))) - ((b - r) * (f . a)) < ((b - a) * (f . b)) - ((b - a) * (f . r)) by XREAL_1:20;
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 A23, XREAL_1:106; :: 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 A19; :: thesis: verum

end;

hence ( f is_strictly_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