let F be PartFunc of REAL,REAL; :: thesis: for X being set st X c= dom F holds
0 (#) F is_convex_on X
let X be set ; :: thesis: ( X c= dom F implies 0 (#) F is_convex_on X )
assume A1: X c= dom F ; :: thesis: 0 (#) F is_convex_on X
hence X c= dom (0 (#) F) by VALUED_1:def 5; :: 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
(0 (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((0 (#) F) . r)) + ((1 - p) * ((0 (#) F) . 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
(0 (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((0 (#) F) . r)) + ((1 - p) * ((0 (#) F) . s)) )
assume that
0 <= p and
p <= 1 ; :: thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds
(0 (#) F) . ((p * r) + ((1 - p) * s)) <= (p * ((0 (#) F) . r)) + ((1 - p) * ((0 (#) F) . s))
let x, y be Real; :: thesis: ( x in X & y in X & (p * x) + ((1 - p) * y) in X implies (0 (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((0 (#) F) . x)) + ((1 - p) * ((0 (#) F) . y)) )
assume that
A2: x in X and
A3: y in X and
A4: (p * x) + ((1 - p) * y) in X ; :: thesis: (0 (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((0 (#) F) . x)) + ((1 - p) * ((0 (#) F) . y))
A5: dom F = dom (0 (#) F) by VALUED_1:def 5;
then A6: (0 (#) F) . ((p * x) + ((1 - p) * y)) = 0 * (F . ((p * x) + ((1 - p) * y))) by A1, A4, VALUED_1:def 5
.= 0 ;
(p * ((0 (#) F) . x)) + ((1 - p) * ((0 (#) F) . y)) = (p * (0 * (F . x))) + ((1 - p) * ((0 (#) F) . y)) by A1, A5, A2, VALUED_1:def 5
.= (p * 0) + ((1 - p) * (0 * (F . y))) by A1, A5, A3, VALUED_1:def 5
.= 0 + 0 ;
hence (0 (#) F) . ((p * x) + ((1 - p) * y)) <= (p * ((0 (#) F) . x)) + ((1 - p) * ((0 (#) F) . y)) by A6; :: thesis: verum