let f be PartFunc of REAL,REAL; :: thesis: ( f is total implies ( ( 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)) ) iff f is_convex_on REAL ) )
A1: ( f is_convex_on REAL implies 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)) )

proof

assume A2: f is_convex_on REAL ; :: thesis: 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))
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))

proof

defpred S₁[ Element of NAT ] means for P, E, F being Element of $1 -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));
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: for P, E, F being Element of k -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: S₁[k + 1]
for P, E, F being Element of (k + 1) -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))

proof

let P, E, F be Element of (k + 1) -tuples_on REAL; :: thesis: ( Sum P = 1 & ( for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ) implies f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) )
assume that
A5: Sum P = 1 and
A6: for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) ) ; :: thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
consider E1 being Element of k -tuples_on REAL, e1 being Real such that
A7: E = E1 ^ <*e1*> by FINSEQ_2:117;
consider F1 being Element of k -tuples_on REAL, f1 being Real such that
A8: F = F1 ^ <*f1*> by FINSEQ_2:117;
(len F1) + 1 = k + 1 by CARD_1:def 7
.= len P by CARD_1:def 7 ;
then (len F1) + 1 in Seg (len P) by FINSEQ_1:4;
then A9: (len F1) + 1 in dom P by FINSEQ_1:def 3;
A10: f1 = F . ((len F1) + 1) by A8, FINSEQ_1:42
.= f . (E . ((len F1) + 1)) by A6, A9
.= f . (E . (k + 1)) by CARD_1:def 7
.= f . (E . ((len E1) + 1)) by CARD_1:def 7
.= f . e1 by A7, FINSEQ_1:42 ;
consider P1 being Element of k -tuples_on REAL, p1 being Real such that
A11: P = P1 ^ <*p1*> by FINSEQ_2:117;
mlt (P,F) = (mlt (P1,F1)) ^ <*(p1 * f1)*> by A11, A8, Th2;
then A12: Sum (mlt (P,F)) = (1 * (Sum (mlt (P1,F1)))) + (p1 * f1) by RVSUM_1:74;
mlt (P,E) = (mlt (P1,E1)) ^ <*(p1 * e1)*> by A11, A7, Th2;
then A13: Sum (mlt (P,E)) = (1 * (Sum (mlt (P1,E1)))) + (p1 * e1) by RVSUM_1:74;
A14: for i being Nat st i in dom P1 holds
P1 . i >= 0

proof

let i be Nat; :: thesis: ( i in dom P1 implies P1 . i >= 0 )
assume A15: i in dom P1 ; :: thesis: P1 . i >= 0
A16: i in Seg (len P1) by A15, FINSEQ_1:def 3;
then A17: 1 <= i by FINSEQ_1:1;
i <= len P1 by A16, FINSEQ_1:1;
then A18: i <= k by CARD_1:def 7;
k <= k + 1 by NAT_1:11;
then i <= k + 1 by A18, XXREAL_0:2;
then i in Seg (k + 1) by A17, FINSEQ_1:1;
then i in Seg (len P) by CARD_1:def 7;
then A19: i in dom P by FINSEQ_1:def 3;
P1 . i = P . i by A11, A15, FINSEQ_1:def 7;
hence P1 . i >= 0 by A6, A19; :: thesis: verum

end;

then A20: for i being Element of NAT st i in dom P1 holds
P1 . i >= 0 ;

now

per cases ( Sum P1 = 0 or Sum P1 <> 0 ) ;

suppose A21: Sum P1 = 0 ; :: thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))

then for i being Element of NAT st i in dom P1 holds
P1 . i = 0 by A20, Th3;
then A22: P1 = k |-> 0 by Th4;
then mlt (P1,E1) = k |-> 0 by Th5;
then A23: Sum (mlt (P1,E1)) = k * 0 by RVSUM_1:80;
mlt (P1,F1) = k |-> 0 by A22, Th5;
then A24: Sum (mlt (P1,F1)) = k * 0 by RVSUM_1:80;
Sum P = 0 + p1 by A11, A21, RVSUM_1:74;
hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A5, A13, A12, A10, A23, A24; :: thesis: verum

end;

suppose A25: Sum P1 <> 0 ; :: thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))

A26: 0 <= Sum P1 by A14, RVSUM_1:84;
A27: for i being Element of NAT st i in dom (((Sum P1) ") * P1) holds
( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) )

proof

let i be Element of NAT ; :: thesis: ( i in dom (((Sum P1) ") * P1) implies ( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) ) )
assume i in dom (((Sum P1) ") * P1) ; :: thesis: ( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) )
then A28: i in Seg (len (((Sum P1) ") * P1)) by FINSEQ_1:def 3;
then A29: i in Seg k by CARD_1:def 7;
then A30: i in Seg (len P1) by CARD_1:def 7;
then i <= len P1 by FINSEQ_1:1;
then A31: i <= k by CARD_1:def 7;
A32: 1 <= i by A28, FINSEQ_1:1;
k <= k + 1 by NAT_1:11;
then i <= k + 1 by A31, XXREAL_0:2;
then i in Seg (k + 1) by A32, FINSEQ_1:1;
then i in Seg (len P) by CARD_1:def 7;
then A33: i in dom P by FINSEQ_1:def 3;
i in dom P1 by A30, FINSEQ_1:def 3;
then ( (((Sum P1) ") * P1) . i = ((Sum P1) ") * (P1 . i) & P1 . i >= 0 ) by A14, RVSUM_1:45;
hence (((Sum P1) ") * P1) . i >= 0 by A26; :: thesis: F1 . i = f . (E1 . i)
i in Seg (len E1) by A29, CARD_1:def 7;
then i in dom E1 by FINSEQ_1:def 3;
then A34: E . i = E1 . i by A7, FINSEQ_1:def 7;
i in Seg (len F1) by A29, CARD_1:def 7;
then i in dom F1 by FINSEQ_1:def 3;
then F . i = F1 . i by A8, FINSEQ_1:def 7;
hence F1 . i = f . (E1 . i) by A6, A33, A34; :: thesis: verum

end;

A35: Sum (mlt (P,E)) = (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,E1)))) + (p1 * e1) by A13, A25, XCMPLX_0:def 7
.= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,E1))))) + (p1 * e1)
.= ((Sum P1) * (Sum (((Sum P1) ") * (mlt (P1,E1))))) + (p1 * e1) by RVSUM_1:87
.= ((Sum P1) * (Sum (mlt ((((Sum P1) ") * P1),E1)))) + (p1 * e1) by FINSEQOP:26 ;
A36: ((Sum P1) ") * (Sum (mlt (P1,F1))) = Sum (((Sum P1) ") * (mlt (P1,F1))) by RVSUM_1:87
.= Sum (mlt ((((Sum P1) ") * P1),F1)) by FINSEQOP:26 ;
(len P1) + 1 = len P by A11, FINSEQ_2:16;
then (len P1) + 1 in Seg (len P) by FINSEQ_1:4;
then A37: (len P1) + 1 in dom P by FINSEQ_1:def 3;
(Sum P1) + p1 = 1 by A5, A11, RVSUM_1:74;
then A38: p1 = 1 - (Sum P1) ;
Sum (((Sum P1) ") * P1) = ((Sum P1) ") * (Sum P1) by RVSUM_1:87
.= 1 by A25, XCMPLX_0:def 7 ;
then (Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1)))) <= (Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1)))) by A4, A26, A36, A27, XREAL_1:64;
then A39: ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) <= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1))))) + (p1 * (f . e1)) by XREAL_1:6;
P . ((len P1) + 1) = p1 by A11, FINSEQ_1:42;
then Sum P1 <= 1 by A6, A38, A37, XREAL_1:49;
then f . (Sum (mlt (P,E))) <= ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) by A2, A35, A38, A26, RFUNCT_3:def 12;
then f . (Sum (mlt (P,E))) <= (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,F1)))) + (p1 * (f . e1)) by A39, XXREAL_0:2;
hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A12, A10, A25, XCMPLX_0:def 7; :: thesis: verum

end;

end;

end;

hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A40: S₁[ 0 ] by RVSUM_1:79;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A40, A3);
hence 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: verum

end;

hence 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: verum

end;

assume f is total ; :: thesis: ( ( 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)) ) iff f is_convex_on REAL )
then A41: 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 A42: 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
A43: 0 <= p and
A44: 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 P = <*p,(1 - p)*>, E = <*r,s*>, F = <*(f . r),(f . s)*> as Element of 2 -tuples_on REAL by FINSEQ_2:101;
A45: for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) )

proof

A46: 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 A47: i in dom P ; :: thesis: ( P . i >= 0 & F . i = f . (E . i) )

now

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

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

then E . i = r by FINSEQ_1:44;
hence ( P . i >= 0 & F . i = f . (E . i) ) by A43, A48, FINSEQ_1:44; :: thesis: verum

end;

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

then ( E . i = s & P . i = 1 - p ) by FINSEQ_1:44;
hence ( P . i >= 0 & F . i = f . (E . i) ) by A44, A49, FINSEQ_1:44, 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 A50: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A42, A45;
A51: ( 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 A52: len (mlt (P,E)) = 2 by FINSEQ_1:44;
A53: ( (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 A51, A52, A53, FINSEQ_1:44;
then A54: Sum (mlt (P,E)) = (p * r) + ((1 - p) * s) by RVSUM_1:77;
A55: ( (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 A56: 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 A51, A56, A55, FINSEQ_1:44;
hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A50, A54, RVSUM_1:77; :: thesis: verum

end;

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

end;

hence ( ( 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)) ) iff f is_convex_on REAL ) by A1; :: thesis: verum