let F, G be PartFunc of REAL,REAL; :: thesis: for X being set st F is_convex_on X & G is_convex_on X holds
F + G is_convex_on X
let X be set ; :: thesis: ( F is_convex_on X & G is_convex_on X implies F + G is_convex_on X )
A1: dom (F + G) = (dom F) /\ (dom G) by VALUED_1:def 1;
assume A2: ( F is_convex_on X & G is_convex_on X ) ; :: thesis: F + G is_convex_on X
then ( X c= dom F & X c= dom G ) ;
hence A3: X c= dom (F + G) by A1, XBOOLE_1:19; :: according to RFUNCT_3:def 12 :: 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
(F + G) . ((p * r) + ((1 - p) * s)) <= (p * ((F + G) . r)) + ((1 - p) * ((F + G) . 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
(F + G) . ((p * r) + ((1 - p) * s)) <= (p * ((F + G) . r)) + ((1 - p) * ((F + G) . 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
(F + G) . ((p * r) + ((1 - p) * s)) <= (p * ((F + G) . r)) + ((1 - p) * ((F + G) . s))
let x, y be Real; :: thesis: ( x in X & y in X & (p * x) + ((1 - p) * y) in X implies (F + G) . ((p * x) + ((1 - p) * y)) <= (p * ((F + G) . x)) + ((1 - p) * ((F + G) . y)) )
assume that
A5: x in X and
A6: y in X and
A7: (p * x) + ((1 - p) * y) in X ; :: thesis: (F + G) . ((p * x) + ((1 - p) * y)) <= (p * ((F + G) . x)) + ((1 - p) * ((F + G) . y))
( F . ((p * x) + ((1 - p) * y)) <= (p * (F . x)) + ((1 - p) * (F . y)) & G . ((p * x) + ((1 - p) * y)) <= (p * (G . x)) + ((1 - p) * (G . y)) ) by A2, A4, A5, A6, A7;
then (F . ((p * x) + ((1 - p) * y))) + (G . ((p * x) + ((1 - p) * y))) <= ((p * (F . x)) + ((1 - p) * (F . y))) + ((p * (G . x)) + ((1 - p) * (G . y))) by XREAL_1:7;
then A8: (F + G) . ((p * x) + ((1 - p) * y)) <= ((p * (F . x)) + ((1 - p) * (F . y))) + ((p * (G . x)) + ((1 - p) * (G . y))) by A3, A7, VALUED_1:def 1;
((p * (F . x)) + ((1 - p) * (F . y))) + ((p * (G . x)) + ((1 - p) * (G . y))) = ((p * ((F . x) + (G . x))) + ((1 - p) * (F . y))) + ((1 - p) * (G . y))
.= ((p * ((F + G) . x)) + ((1 - p) * (F . y))) + ((1 - p) * (G . y)) by A3, A5, VALUED_1:def 1
.= (p * ((F + G) . x)) + ((1 - p) * ((F . y) + (G . y))) ;
hence (F + G) . ((p * x) + ((1 - p) * y)) <= (p * ((F + G) . x)) + ((1 - p) * ((F + G) . y)) by A3, A6, A8, VALUED_1:def 1; :: thesis: verum