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: ( 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 A2: 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) ) ) )
( 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

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 . r < (((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b)) by A2, A3, A5, Def1;
A9: ((((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b))) * (b - a) = (((b - a) * ((b - r) / (b - a))) * (f . a)) + ((b - a) * ((1 - ((b - r) / (b - a))) * (f . b)))
.= ((((b - a) * (b - r)) / (b - a)) * (f . a)) + (((b - a) * ((r - a) / (b - a))) * (f . b)) by A6, XCMPLX_1:75
.= ((((b - r) * (b - a)) / (b - a)) * (f . a)) + ((((b - a) * (r - a)) / (b - a)) * (f . b)) by XCMPLX_1:75
.= (((b - r) * ((b - a) / (b - a))) * (f . a)) + ((((b - a) * (r - a)) / (b - a)) * (f . b)) by XCMPLX_1:75
.= (((b - r) * 1) * (f . a)) + ((((r - a) * (b - a)) / (b - a)) * (f . b)) by A4, XCMPLX_1:60
.= ((b - r) * (f . a)) + (((r - a) * ((b - a) / (b - a))) * (f . b)) by XCMPLX_1:75
.= ((b - r) * (f . a)) + (((r - a) * 1) * (f . b)) by A4, XCMPLX_1:60 ;
then (f . r) * (b - a) < ((b - a) * (f . a)) + (((r - a) * (f . b)) - ((r - a) * (f . a))) by A4, A8, XREAL_1:70;
then ((f . r) * (b - a)) - ((b - a) * (f . a)) < ((r - a) * (f . b)) - ((r - a) * (f . a)) by XREAL_1:21;
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:108; :: 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 A4, A8, A9, XREAL_1:70;
then ((f . r) * (b - a)) - (((r - b) * (f . b)) + ((b - r) * (f . a))) < (b - a) * (f . b) by XREAL_1:21;
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:22;
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:108; :: 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 A2, Def1; :: 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_strictly_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_strictly_convex_on X
f is_strictly_convex_on X

proof

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 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 & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
then A12: 1 - p > 0 by XREAL_1:52;
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 A13: ( s in X & t in X & (p * s) + ((1 - p) * t) in X & s <> t ) ; :: thesis: f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t))

now

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

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

then A14: t - s > 0 by XREAL_1:52;
t - ((p * s) + ((1 - p) * t)) = p * (t - s) ;
then A15: t - ((p * s) + ((1 - p) * t)) > 0 by A11, A14, XREAL_1:131;
then A16: (p * s) + ((1 - p) * t) < t by XREAL_1:49;
((p * s) + ((1 - p) * t)) - s = (1 - p) * (t - s) ;
then A17: ((p * s) + ((1 - p) * t)) - s > 0 by A12, A14, 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, A13, A16;
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 A18: ((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 A15, A17, XREAL_1:104;
A19: (((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 A18, A19, XREAL_1:23;
then f . ((p * s) + ((1 - p) * t)) < ((((1 - p) * (f . t)) * (t - s)) + ((p * (f . s)) * (t - s))) / (t - s) by A14, XREAL_1:83;
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 A14, XCMPLX_1:90;
hence f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) by A14, XCMPLX_1:90; :: thesis: verum

end;

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

then A20: s - t > 0 by XREAL_1:52;
s - ((p * s) + ((1 - p) * t)) = (1 - p) * (s - t) ;
then A21: s - ((p * s) + ((1 - p) * t)) > 0 by A12, A20, XREAL_1:131;
then A22: (p * s) + ((1 - p) * t) < s by XREAL_1:49;
((p * s) + ((1 - p) * t)) - t = p * (s - t) ;
then A23: ((p * s) + ((1 - p) * t)) - t > 0 by A11, A20, 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, A13, A22;
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 A24: ((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 A21, A23, XREAL_1:104;
A25: (((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 A24, A25, XREAL_1:23;
then f . ((p * s) + ((1 - p) * t)) < (((p * (f . s)) * (s - t)) + (((1 - p) * (f . t)) * (s - t))) / (s - t) by A20, XREAL_1:83;
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 A20, XCMPLX_1:90;
hence f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) by A20, 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;

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 A10, Def1; :: thesis: verum

end;

hence f is_strictly_convex_on X ; :: 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