let F be PartFunc of REAL,REAL; for X being set
for r being Real st F is_convex_on X holds
max+ (F - r) is_convex_on X
let X be set ; for r being Real st F is_convex_on X holds
max+ (F - r) is_convex_on X
let r be Real; ( F is_convex_on X implies max+ (F - r) is_convex_on X )
assume A1:
F is_convex_on X
; max+ (F - r) is_convex_on X
then A2:
X c= dom F
;
A3:
( dom F = dom (F - r) & dom (max+ (F - r)) = dom (F - r) )
by Def10, VALUED_1:3;
hence
X c= dom (max+ (F - r))
by A1; 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
(max+ (F - r)) . ((p * r) + ((1 - p) * s)) <= (p * ((max+ (F - r)) . r)) + ((1 - p) * ((max+ (F - r)) . 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
(max+ (F - r)) . ((p * r) + ((1 - p) * s)) <= (p * ((max+ (F - r)) . r)) + ((1 - p) * ((max+ (F - r)) . s)) )
assume that
A4:
0 <= p
and
A5:
p <= 1
; for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
(max+ (F - r)) . ((p * r) + ((1 - p) * s)) <= (p * ((max+ (F - r)) . r)) + ((1 - p) * ((max+ (F - r)) . s))
let x, y be Real; ( x in X & y in X & (p * x) + ((1 - p) * y) in X implies (max+ (F - r)) . ((p * x) + ((1 - p) * y)) <= (p * ((max+ (F - r)) . x)) + ((1 - p) * ((max+ (F - r)) . y)) )
assume that
A6:
x in X
and
A7:
y in X
and
A8:
(p * x) + ((1 - p) * y) in X
; (max+ (F - r)) . ((p * x) + ((1 - p) * y)) <= (p * ((max+ (F - r)) . x)) + ((1 - p) * ((max+ (F - r)) . y))
F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y))
by A1, A4, A5, A6, A7, A8;
then
(F . ((p * x) + ((1 - p) * y))) - r <= ((p * (F . x)) + ((1 - p) * (F . y))) - r
by XREAL_1:9;
then A9:
max+ ((F . ((p * x) + ((1 - p) * y))) - r) <= max ((((p * (F . x)) + ((1 - p) * (F . y))) - r),0)
by XXREAL_0:26;
0 + p <= 1
by A5;
then
0 <= 1 - p
by XREAL_1:19;
then A10:
max+ ((1 - p) * ((F - r) . y)) = (1 - p) * (max+ ((F - r) . y))
by Th4;
A11:
max+ ((p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))) <= (max+ (p * ((F - r) . x))) + (max+ ((1 - p) * ((F - r) . y)))
by Th5;
A12:
max+ (p * ((F - r) . x)) = p * (max+ ((F - r) . x))
by A4, Th4;
reconsider pc = (p * x) + ((1 - p) * y) as Element of REAL by XREAL_0:def 1;
reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;
((p * (F . x)) + ((1 - p) * (F . y))) - r =
(p * ((F . x) - r)) + ((1 - p) * ((F . y) - r))
.=
(p * ((F - r) . x)) + ((1 - p) * ((F . y) - r))
by A6, A2, VALUED_1:3
.=
(p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))
by A7, A2, VALUED_1:3
;
then
max+ ((F . ((p * x) + ((1 - p) * y))) - r) <= (p * (max+ ((F - r) . x))) + ((1 - p) * (max+ ((F - r) . y)))
by A9, A11, A12, A10, XXREAL_0:2;
then
max+ ((F - r) . pc) <= (p * (max+ ((F - r) . x))) + ((1 - p) * (max+ ((F - r) . y)))
by A8, A2, VALUED_1:3;
then
(max+ (F - r)) . pc <= (p * (max+ ((F - r) . x))) + ((1 - p) * (max+ ((F - r) . y)))
by A3, A8, A2, Def10;
then
(max+ (F - r)) . pc <= (p * ((max+ (F - r)) . x)) + ((1 - p) * (max+ ((F - r) . y)))
by A3, A6, A2, Def10;
hence
(max+ (F - r)) . ((p * x) + ((1 - p) * y)) <= (p * ((max+ (F - r)) . x)) + ((1 - p) * ((max+ (F - r)) . y))
by A3, A7, A2, Def10; verum