let X be set ; 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; ( 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))
;
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;
( 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 )
;
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;
( 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
;
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 f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))per cases
( 0 < p & p < 1 )
by A4;
suppose A7:
(
0 < p &
p < 1 )
;
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))then A8:
0 < 1
- p
by XREAL_1:50;
now f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))per cases
( r > s or r < s )
by A6, XXREAL_0:1;
suppose A9:
r > s
;
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:50;
A11:
r - ((p * r) + ((1 - p) * s)) = (1 - p) * (r - s)
;
then
r - ((p * r) + ((1 - p) * s)) > 0
by A8, A10, XREAL_1:129;
then A12:
(p * r) + ((1 - p) * s) < r
by XREAL_1:47;
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:89;
((p * r) + ((1 - p) * s)) - s > 0
by A7, A10, A13, XREAL_1:129;
then A15:
s < (p * r) + ((1 - p) * s)
by XREAL_1:47;
(r - ((p * r) + ((1 - p) * s))) / (r - s) = 1
- p
by A10, A11, XCMPLX_1:89;
hence
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
by A3, A5, A15, A12, A14;
verum end; suppose A16:
r < s
;
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:50;
A18:
s - ((p * r) + ((1 - p) * s)) = p * (s - r)
;
then
s - ((p * r) + ((1 - p) * s)) > 0
by A7, A17, XREAL_1:129;
then A19:
(p * r) + ((1 - p) * s) < s
by XREAL_1:47;
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:89;
((p * r) + ((1 - p) * s)) - r > 0
by A8, A17, A20, XREAL_1:129;
then A22:
r < (p * r) + ((1 - p) * s)
by XREAL_1:47;
(s - ((p * r) + ((1 - p) * s))) / (s - r) = p
by A17, A18, XCMPLX_1:89;
hence
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
by A3, A5, A22, A19, A21;
verum end; end; end; hence
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
;
verum end; end; end;
hence
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
;
verum
end;
hence
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
;
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))
;
verum
end;
hence
f is_strictly_convex_on X
by A2;
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
;
( 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;
( 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 )
;
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:10, XREAL_1:50;
then A27:
(
0 < (c - b) / (c - a) &
(c - b) / (c - a) < 1 )
by XREAL_1:139, XREAL_1:189;
A28:
((c - b) / (c - a)) + ((b - a) / (c - a)) =
((c - b) + (b - a)) / (c - a)
by XCMPLX_1:62
.=
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: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 A26, XCMPLX_1:89;
hence
f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c))
by A23, A24, A25, A27, A28;
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;
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; verum