let F be PartFunc of REAL,REAL; for X being set
for r being Real st 0 < r holds
( F is_convex_on X iff r (#) F is_convex_on X )
let X be set ; for r being Real st 0 < r holds
( F is_convex_on X iff r (#) F is_convex_on X )
let r be Real; ( 0 < r implies ( F is_convex_on X iff r (#) F is_convex_on X ) )
assume A1:
0 < r
; ( F is_convex_on X iff r (#) F is_convex_on X )
A2:
dom F = dom (r (#) F)
by VALUED_1:def 5;
thus
( F is_convex_on X implies r (#) F is_convex_on X )
( r (#) F is_convex_on X implies F is_convex_on X )proof
assume A3:
F is_convex_on X
;
r (#) F is_convex_on X
then A4:
X c= dom F
;
thus
X c= dom (r (#) F)
by A2, A3;
RFUNCT_3:def 12 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 holds
(r (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((r (#) F) . r)) + ((1 - p) * ((r (#) F) . s))
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 holds
(r (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((r (#) F) . r)) + ((1 - p) * ((r (#) F) . s)) )
assume A5:
(
0 <= p &
p <= 1 )
;
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
(r (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((r (#) F) . r)) + ((1 - p) * ((r (#) F) . s))
let x,
y be
Real;
( x in X & y in X & (p * x) + ((1 - p) * y) in X implies (r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y)) )
assume that A6:
x in X
and A7:
y in X
and A8:
(p * x) + ((1 - p) * y) in X
;
(r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y))
F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y))
by A3, A5, A6, A7, A8;
then
r * (F . ((p * x) + ((1 - p) * y))) <= r * ((p * (F . x)) + ((1 - p) * (F . y)))
by A1, XREAL_1:64;
then
(r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * (r * (F . x))) + (((1 - p) * r) * (F . y))
by A2, A4, A8, VALUED_1:def 5;
then
(r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * (r * (F . y)))
by A2, A4, A6, VALUED_1:def 5;
hence
(r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y))
by A2, A4, A7, VALUED_1:def 5;
verum
end;
assume A9:
r (#) F is_convex_on X
; F is_convex_on X
then A10:
X c= dom (r (#) F)
;
hence
X c= dom F
by VALUED_1:def 5; RFUNCT_3:def 12 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 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 X & s in X & (p * r) + ((1 - p) * s) in X holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) )
assume A11:
( 0 <= p & p <= 1 )
; for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s))
let x, y be Real; ( x in X & y in X & (p * x) + ((1 - p) * y) in X implies F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) )
assume that
A12:
x in X
and
A13:
y in X
and
A14:
(p * x) + ((1 - p) * y) in X
; F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y))
(r (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y))
by A9, A11, A12, A13, A14;
then
r * (F . ((p * x) + ((1 - p) * y))) <= (p * ((r (#) F) . x)) + ((1 - p) * ((r (#) F) . y))
by A10, A14, VALUED_1:def 5;
then
r * (F . ((p * x) + ((1 - p) * y))) <= (p * (r * (F . x))) + ((1 - p) * ((r (#) F) . y))
by A10, A12, VALUED_1:def 5;
then
r * (F . ((p * x) + ((1 - p) * y))) <= (p * (r * (F . x))) + ((1 - p) * (r * (F . y)))
by A10, A13, VALUED_1:def 5;
then
(r * (F . ((p * x) + ((1 - p) * y)))) / r <= (r * ((p * (F . x)) + ((1 - p) * (F . y)))) / r
by A1, XREAL_1:72;
then
F . ((p * x) + ((1 - p) * y)) <= (r * ((p * (F . x)) + ((1 - p) * (F . y)))) / r
by A1, XCMPLX_1:89;
hence
F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y))
by A1, XCMPLX_1:89; verum