let f, g be PartFunc of REAL,REAL; :: thesis: for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X holds
f + g is_strictly_convex_on X
let X be set ; :: thesis: ( f is_strictly_convex_on X & g is_strictly_convex_on X implies f + g is_strictly_convex_on X )
assume A1: ( f is_strictly_convex_on X & g is_strictly_convex_on X ) ; :: thesis: f + g is_strictly_convex_on X
then ( X c= dom f & X c= dom g ) ;
then X c= (dom f) /\ (dom g) by XBOOLE_1:19;
then A2: X c= dom (f + g) by VALUED_1:def 1;
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 & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
proof
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 & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) )
assume A3: ( 0 < p & p < 1 ) ; :: thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
proof
let r, s be Real; :: thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) )
assume that
A4: r in X and
A5: s in X and
A6: (p * r) + ((1 - p) * s) in X and
A7: r <> s ; :: thesis: (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
A8: ( (f + g) . ((p * r) + ((1 - p) * s)) = (f . ((p * r) + ((1 - p) * s))) + (g . ((p * r) + ((1 - p) * s))) & (f + g) . r = (f . r) + (g . r) ) by A2, A4, A6, VALUED_1:def 1;
A9: ( ((p * (f . r)) + ((1 - p) * (f . s))) + ((p * (g . r)) + ((1 - p) * (g . s))) = (p * ((f . r) + (g . r))) + ((1 - p) * ((f . s) + (g . s))) & (f + g) . s = (f . s) + (g . s) ) by A2, A5, VALUED_1:def 1;
( f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) & g . ((p * r) + ((1 - p) * s)) < (p * (g . r)) + ((1 - p) * (g . s)) ) by A1, A3, A4, A5, A6, A7;
hence (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) by A8, A9, XREAL_1:8; :: thesis: verum
end;
hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ; :: thesis: verum
end;
hence f + g is_strictly_convex_on X by A2; :: thesis: verum