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 )

( 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

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

hence
( ex n being Element of NAT ex P, E, F being Element of n -tuples_on REAL st
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))

end;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

hence
f is_convex_on REAL
by A1, RFUNCT_3:def 12; :: thesis: verum
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) )

.= 1 ;

then A10: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A2, A5;

A11: ( P . 1 = p & P . 2 = 1 - p ) by FINSEQ_1:44;

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;

( E . 1 = r & E . 2 = s ) by FINSEQ_1:44;

then mlt (P,E) = <*(p * r),((1 - p) * s)*> by A11, 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;

( F . 1 = f . r & F . 2 = f . s ) by FINSEQ_1:44;

then mlt (P,F) = <*(p * (f . r)),((1 - p) * (f . s))*> by A11, 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;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

Sum P =
p + (1 - p)
by RVSUM_1:77
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) )

end;.= 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) )

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

.= 1 ;

then A10: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A2, A5;

A11: ( P . 1 = p & P . 2 = 1 - p ) by FINSEQ_1:44;

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;

( E . 1 = r & E . 2 = s ) by FINSEQ_1:44;

then mlt (P,E) = <*(p * r),((1 - p) * s)*> by A11, 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;

( F . 1 = f . r & F . 2 = f . s ) by FINSEQ_1:44;

then mlt (P,F) = <*(p * (f . r)),((1 - p) * (f . s))*> by A11, 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

( 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