let f be PartFunc of REAL,REAL; :: thesis: ( f is total & ( for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) implies f is_convex_on REAL )
assume f is total ; :: thesis: ( ex n being Element of NAT ex P, E, F being Element of n -tuples_on REAL st
( Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) & not f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) or f is_convex_on REAL )
then A1: REAL c= dom f by PARTFUN1:def 2;
( ( for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) implies f is_convex_on REAL )

proof

assume A2: for n being Element of NAT
for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) holds
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; :: thesis: f is_convex_on REAL
for p being Real st 0 <= p & p <= 1 holds
for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))

proof

let p be Real; :: thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) )
assume that
A3: 0 <= p and
A4: p <= 1 ; :: thesis: for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds
f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
let r, s be Real; :: thesis: ( r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL implies f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) )
assume that
r in REAL and
s in REAL and
(p * r) + ((1 - p) * s) in REAL ; :: thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s))
reconsider rr = r, ss = s, pp = p, mp = 1 - p as Element of REAL by XREAL_0:def 1;
( f . rr in REAL & f . ss in REAL ) by XREAL_0:def 1;
then reconsider P = <*pp,mp*>, E = <*rr,ss*>, F = <*(f . rr),(f . ss)*> as Element of 2 -tuples_on REAL by FINSEQ_2:101;
A5: for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) )

proof

A6: dom P = Seg (len P) by FINSEQ_1:def 3
.= Seg 2 by CARD_1:def 7 ;
let i be Element of NAT ; :: thesis: ( i in dom P implies ( P . i >= 0 & F . i = f . (E . i) ) )
assume A7: i in dom P ; :: thesis: ( P . i >= 0 & F . i = f . (E . i) )

now :: thesis: ( P . i >= 0 & F . i = f . (E . i) )

per cases ( i = 1 or i = 2 ) by A7, A6, FINSEQ_1:2, TARSKI:def 2;

suppose A8: i = 1 ; :: thesis: ( P . i >= 0 & F . i = f . (E . i) )

thus ( P . i >= 0 & F . i = f . (E . i) ) by A3, A8; :: thesis: verum

end;

suppose A9: i = 2 ; :: thesis: ( P . i >= 0 & F . i = f . (E . i) )

thus ( P . i >= 0 & F . i = f . (E . i) ) by A4, A9, XREAL_1:48; :: thesis: verum

end;

end;

end;

hence ( P . i >= 0 & F . i = f . (E . i) ) ; :: thesis: verum

end;

Sum P = p + (1 - p) by RVSUM_1:77
.= 1 ;
then A10: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A2, A5;
len P = 2 by FINSEQ_1:44
.= len E by FINSEQ_1:44 ;
then len (multreal .: (P,E)) = len P by FINSEQ_2:72;
then A12: len (mlt (P,E)) = 2 by FINSEQ_1:44;
A13: ( (mlt (P,E)) . 1 = (P . 1) * (E . 1) & (mlt (P,E)) . 2 = (P . 2) * (E . 2) ) by RVSUM_1:60;
mlt (P,E) = <*(p * r),((1 - p) * s)*> by A12, A13, FINSEQ_1:44;
then A14: Sum (mlt (P,E)) = (p * r) + ((1 - p) * s) by RVSUM_1:77;
A15: ( (mlt (P,F)) . 1 = (P . 1) * (F . 1) & (mlt (P,F)) . 2 = (P . 2) * (F . 2) ) by RVSUM_1:60;
len P = 2 by FINSEQ_1:44
.= len F by FINSEQ_1:44 ;
then len (multreal .: (P,F)) = len P by FINSEQ_2:72;
then A16: len (mlt (P,F)) = 2 by FINSEQ_1:44;
mlt (P,F) = <*(p * (f . r)),((1 - p) * (f . s))*> by A16, A15, FINSEQ_1:44;
hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A10, A14, RVSUM_1:77; :: thesis: verum

end;

hence f is_convex_on REAL by A1, RFUNCT_3:def 12; :: thesis: verum

end;

hence ( ex n being Element of NAT ex P, E, F being Element of n -tuples_on REAL st
( Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) & not f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) or f is_convex_on REAL ) ; :: thesis: verum