let X be set ; :: thesis: for f being PartFunc of REAL ,REAL holds
( f is_strictly_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_strictly_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_strictly_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_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 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 & r <> s 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 & r <> s 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 & r <> s implies f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) )
assume that
A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) and
A6: r <> s ; :: 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

now

per cases ( 0 < p & p < 1 ) by A4;

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

then A8: 0 < 1 - p by XREAL_1:52;

now

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

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

set t = (p * r) + ((1 - p) * s);
A10: r - s > 0 by A9, XREAL_1:52;
A11: r - ((p * r) + ((1 - p) * s)) = (1 - p) * (r - s) ;
then r - ((p * r) + ((1 - p) * s)) > 0 by A8, A10, XREAL_1:131;
then A12: (p * r) + ((1 - p) * s) < r by XREAL_1:49;
A13: ((p * r) + ((1 - p) * s)) - s = p * (r - s) ;
then A14: (((p * r) + ((1 - p) * s)) - s) / (r - s) = p by A10, XCMPLX_1:90;
((p * r) + ((1 - p) * s)) - s > 0 by A7, A10, A13, XREAL_1:131;
then A15: s < (p * r) + ((1 - p) * s) by XREAL_1:49;
(r - ((p * r) + ((1 - p) * s))) / (r - s) = 1 - p by A10, A11, XCMPLX_1:90;
hence f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A15, A12, A14; :: thesis: verum

end;

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

set t = (p * r) + ((1 - p) * s);
A17: s - r > 0 by A16, XREAL_1:52;
A18: s - ((p * r) + ((1 - p) * s)) = p * (s - r) ;
then s - ((p * r) + ((1 - p) * s)) > 0 by A7, A17, XREAL_1:131;
then A19: (p * r) + ((1 - p) * s) < s by XREAL_1:49;
A20: ((p * r) + ((1 - p) * s)) - r = (1 - p) * (s - r) ;
then A21: (((p * r) + ((1 - p) * s)) - r) / (s - r) = 1 - p by A17, XCMPLX_1:90;
((p * r) + ((1 - p) * s)) - r > 0 by A8, A17, A20, XREAL_1:131;
then A22: r < (p * r) + ((1 - p) * s) by XREAL_1:49;
(s - ((p * r) + ((1 - p) * s))) / (s - r) = p by A17, A18, XCMPLX_1:90;
hence f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A22, A19, A21; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

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

end;

( f is_strictly_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 A23: f is_strictly_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
A24: ( a in X & b in X & c in X ) and
A25: ( 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);
A26: ( c - b < c - a & 0 < c - b ) by A25, XREAL_1:12, XREAL_1:52;
then A27: ( 0 < (c - b) / (c - a) & (c - b) / (c - a) < 1 ) by XREAL_1:141, XREAL_1:191;
A28: ((c - b) / (c - a)) + ((b - a) / (c - a)) = ((c - b) + (b - a)) / (c - a) by XCMPLX_1:63
.= 1 by A26, 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:75
.= ((a * (c - b)) / (c - a)) + ((c * (b - a)) / (c - a)) by XCMPLX_1:75
.= (((c * a) - (b * a)) + ((b - a) * c)) / (c - a) by XCMPLX_1:63
.= (b * (c - a)) / (c - a) ;
then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = b by A26, XCMPLX_1:90;
hence f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) by A23, A24, A25, A27, A28, Def1; :: 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 A23, Def1; :: thesis: verum

end;

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