let F be PartFunc of REAL , REAL ; :: thesis: 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 ; :: thesis: for r being Real st F is_convex_on X holds
max+ (F - r) is_convex_on X
let r be Real; :: thesis: ( F is_convex_on X implies max+ (F - r) is_convex_on X )
assume A1: F is_convex_on X ; :: thesis: max+ (F - r) is_convex_on X
A2: dom F = dom (F - r) by VALUED_1:3;
A3: dom (max+ (F - r)) = dom (F - r) by Def10;
hence X c= dom (max+ (F - r)) by A1, A2, Def13; :: according to RFUNCT_3:def 13 :: thesis: 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; :: 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 holds
(max+ (F - r)) . ((p * r) + ((1 - p) * s)) <= (p * ((max+ (F - r)) . r)) + ((1 - p) * ((max+ (F - r)) . 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 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; :: thesis: ( 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 A5: ( x in X & y in X & (p * x) + ((1 - p) * y) in X ) ; :: thesis: (max+ (F - r)) . ((p * x) + ((1 - p) * y)) <= (p * ((max+ (F - r)) . x)) + ((1 - p) * ((max+ (F - r)) . y))
then F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) by A1, A4, Def13;
then (F . ((p * x) + ((1 - p) * y))) - r <= ((p * (F . x)) + ((1 - p) * (F . y))) - r by XREAL_1:11;
then A6: max+ ((F . ((p * x) + ((1 - p) * y))) - r) <= max (((p * (F . x)) + ((1 - p) * (F . y))) - r),0 by XXREAL_0:26;
A7: X c= dom F by A1, Def13;
A8: ((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 A5, A7, VALUED_1:3
.= (p * ((F - r) . x)) + ((1 - p) * ((F - r) . y)) by A5, A7, VALUED_1:3 ;
A9: max+ ((p * ((F - r) . x)) + ((1 - p) * ((F - r) . y))) <= (max+ (p * ((F - r) . x))) + (max+ ((1 - p) * ((F - r) . y))) by Th5;
0 + p <= 1 by A4;
then 0 <= 1 - p by XREAL_1:21;
then ( max+ (p * ((F - r) . x)) = p * (max+ ((F - r) . x)) & max+ ((1 - p) * ((F - r) . y)) = (1 - p) * (max+ ((F - r) . y)) ) by A4, Th4;
then max+ ((F . ((p * x) + ((1 - p) * y))) - r) <= (p * (max+ ((F - r) . x))) + ((1 - p) * (max+ ((F - r) . y))) by A6, A8, A9, XXREAL_0:2;
then max+ ((F - r) . ((p * x) + ((1 - p) * y))) <= (p * (max+ ((F - r) . x))) + ((1 - p) * (max+ ((F - r) . y))) by A5, A7, VALUED_1:3;
then (max+ (F - r)) . ((p * x) + ((1 - p) * y)) <= (p * (max+ ((F - r) . x))) + ((1 - p) * (max+ ((F - r) . y))) by A2, A3, A5, A7, Def10;
then (max+ (F - r)) . ((p * x) + ((1 - p) * y)) <= (p * ((max+ (F - r)) . x)) + ((1 - p) * (max+ ((F - r) . y))) by A2, A3, A5, A7, Def10;
hence (max+ (F - r)) . ((p * x) + ((1 - p) * y)) <= (p * ((max+ (F - r)) . x)) + ((1 - p) * ((max+ (F - r)) . y)) by A2, A3, A5, A7, Def10; :: thesis: verum