let f, g be PartFunc of REAL,REAL; for X being set st f is_strictly_convex_on X & g is_convex_on X holds
f + g is_strictly_convex_on X
let X be set ; ( f is_strictly_convex_on X & g is_convex_on X implies f + g is_strictly_convex_on X )
assume A1:
( f is_strictly_convex_on X & g is_convex_on X )
; f + g is_strictly_convex_on X
then
( X c= dom f & X c= dom g )
by RFUNCT_3:def 12;
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;
( 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 )
;
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;
( 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
;
(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, RFUNCT_3:def 12;
hence
(f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s))
by A8, A9, XREAL_1:8;
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))
;
verum
end;
hence
f + g is_strictly_convex_on X
by A2; verum