let a, b be Real; for f being PartFunc of REAL,REAL holds
( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) )
let f be PartFunc of REAL,REAL; ( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) )
set ab = { r where r is Real : ( a <= r & r <= b ) } ;
A1:
[.a,b.] = { r where r is Real : ( a <= r & r <= b ) }
by RCOMP_1:def 1;
thus
( f is_strictly_convex_on [.a,b.] implies ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) ) )
( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) implies f is_strictly_convex_on [.a,b.] )proof
assume A2:
f is_strictly_convex_on [.a,b.]
;
( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) )
hence
[.a,b.] c= dom f
;
for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
let p be
Real;
( 0 < p & p < 1 implies for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that A3:
0 < p
and A4:
p < 1
;
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
A5:
0 <= 1
- p
by A4, XREAL_1:48;
A6:
(p * b) + ((1 - p) * b) = b
;
A7:
(p * a) + ((1 - p) * a) = a
;
let x,
y be
Real;
( x in [.a,b.] & y in [.a,b.] & x <> y implies f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that A8:
x in [.a,b.]
and A9:
y in [.a,b.]
and A10:
x <> y
;
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
A11:
ex
r2 being
Real st
(
r2 = y &
a <= r2 &
r2 <= b )
by A1, A9;
then A12:
(1 - p) * y <= (1 - p) * b
by A5, XREAL_1:64;
A13:
ex
r1 being
Real st
(
r1 = x &
a <= r1 &
r1 <= b )
by A1, A8;
then
p * x <= p * b
by A3, XREAL_1:64;
then A14:
(p * x) + ((1 - p) * y) <= b
by A12, A6, XREAL_1:7;
A15:
(1 - p) * a <= (1 - p) * y
by A5, A11, XREAL_1:64;
p * a <= p * x
by A3, A13, XREAL_1:64;
then
a <= (p * x) + ((1 - p) * y)
by A15, A7, XREAL_1:7;
then
(p * x) + ((1 - p) * y) in { r where r is Real : ( a <= r & r <= b ) }
by A14;
hence
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
by A1, A2, A3, A4, A8, A9, A10;
verum
end;
assume that
A16:
[.a,b.] c= dom f
and
A17:
for p being Real st 0 < p & p < 1 holds
for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y))
; f is_strictly_convex_on [.a,b.]
thus
[.a,b.] c= dom f
by A16; RFUNCT_4:def 1 for p being Real st 0 < p & p < 1 holds
for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
let p be Real; ( 0 < p & p < 1 implies for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) )
assume A18:
( 0 < p & p < 1 )
; for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
let x, y be Real; ( x in [.a,b.] & y in [.a,b.] & (p * x) + ((1 - p) * y) in [.a,b.] & x <> y implies f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
assume that
A19:
( x in [.a,b.] & y in [.a,b.] )
and
(p * x) + ((1 - p) * y) in [.a,b.]
; ( not x <> y or f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
thus
( not x <> y or f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) )
by A17, A18, A19; verum