let f be PartFunc of REAL,REAL; :: thesis: ( 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)) )

assume A1: 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))

defpred S1[ 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));
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
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
A4: Sum P = 1 and
A5: 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 Element of REAL such that
A6: E = E1 ^ <*e1*> by FINSEQ_2:117;
consider F1 being Element of k -tuples_on REAL, f1 being Element of REAL such that
A7: 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 A8: (len F1) + 1 in dom P by FINSEQ_1:def 3;
A9: f1 = F . ((len F1) + 1) by
.= f . (E . ((len F1) + 1)) by A5, A8
.= f . (E . (k + 1)) by CARD_1:def 7
.= f . (E . ((len E1) + 1)) by CARD_1:def 7
.= f . e1 by ;
consider P1 being Element of k -tuples_on REAL, p1 being Element of REAL such that
A10: P = P1 ^ <*p1*> by FINSEQ_2:117;
reconsider SP = (Sum P1) " as Element of REAL by XREAL_0:def 1;
mlt (P,F) = (mlt (P1,F1)) ^ <*(p1 * f1)*> by A10, A7, Th2;
then A11: Sum (mlt (P,F)) = (1 * (Sum (mlt (P1,F1)))) + (p1 * f1) by RVSUM_1:74;
mlt (P,E) = (mlt (P1,E1)) ^ <*(p1 * e1)*> by A10, A6, Th2;
then A12: Sum (mlt (P,E)) = (1 * (Sum (mlt (P1,E1)))) + (p1 * e1) by RVSUM_1:74;
A13: 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 A14: i in dom P1 ; :: thesis: P1 . i >= 0
A15: i in Seg (len P1) by ;
then A16: 1 <= i by FINSEQ_1:1;
i <= len P1 by ;
then A17: i <= k by CARD_1:def 7;
k <= k + 1 by NAT_1:11;
then i <= k + 1 by ;
then i in Seg (k + 1) by ;
then i in Seg (len P) by CARD_1:def 7;
then A18: i in dom P by FINSEQ_1:def 3;
P1 . i = P . i by ;
hence P1 . i >= 0 by ; :: thesis: verum
end;
then A19: for i being Element of NAT st i in dom P1 holds
P1 . i >= 0 ;
now :: thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
per cases ( Sum P1 = 0 or Sum P1 <> 0 ) ;
suppose A20: 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 ;
then A21: P1 = k |-> 0 by Th4;
then mlt (P1,E1) = k |-> 0 by Th5;
then A22: Sum (mlt (P1,E1)) = k * 0 by RVSUM_1:80;
mlt (P1,F1) = k |-> 0 by ;
then A23: Sum (mlt (P1,F1)) = k * 0 by RVSUM_1:80;
Sum P = 0 + p1 by ;
hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A4, A12, A11, A9, A22, A23; :: thesis: verum
end;
suppose A24: Sum P1 <> 0 ; :: thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
A25: 0 <= Sum P1 by ;
A26: 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 A27: i in Seg (len (((Sum P1) ") * P1)) by FINSEQ_1:def 3;
then A28: i in Seg k by CARD_1:def 7;
then A29: i in Seg (len P1) by CARD_1:def 7;
then i <= len P1 by FINSEQ_1:1;
then A30: i <= k by CARD_1:def 7;
A31: 1 <= i by ;
k <= k + 1 by NAT_1:11;
then i <= k + 1 by ;
then i in Seg (k + 1) by ;
then i in Seg (len P) by CARD_1:def 7;
then A32: i in dom P by FINSEQ_1:def 3;
i in dom P1 by ;
then ( (((Sum P1) ") * P1) . i = ((Sum P1) ") * (P1 . i) & P1 . i >= 0 ) by ;
hence (((Sum P1) ") * P1) . i >= 0 by A25; :: thesis: F1 . i = f . (E1 . i)
i in Seg (len E1) by ;
then i in dom E1 by FINSEQ_1:def 3;
then A33: E . i = E1 . i by ;
i in Seg (len F1) by ;
then i in dom F1 by FINSEQ_1:def 3;
then F . i = F1 . i by ;
hence F1 . i = f . (E1 . i) by A5, A32, A33; :: thesis: verum
end;
A34: Sum (mlt (P,E)) = (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,E1)))) + (p1 * e1) by
.= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,E1))))) + (p1 * e1)
.= ((Sum P1) * (Sum (SP * (mlt (P1,E1))))) + (p1 * e1) by RVSUM_1:87
.= ((Sum P1) * (Sum (mlt ((SP * P1),E1)))) + (p1 * e1) by FINSEQOP:26 ;
A35: ((Sum P1) ") * (Sum (mlt (P1,F1))) = Sum (SP * (mlt (P1,F1))) by RVSUM_1:87
.= Sum (mlt ((SP * P1),F1)) by FINSEQOP:26 ;
(len P1) + 1 = len P by ;
then (len P1) + 1 in Seg (len P) by FINSEQ_1:4;
then A36: (len P1) + 1 in dom P by FINSEQ_1:def 3;
(Sum P1) + p1 = 1 by ;
then A37: p1 = 1 - (Sum P1) ;
Sum (((Sum P1) ") * P1) = ((Sum P1) ") * (Sum P1) by RVSUM_1:87
.= 1 by ;
then (Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1)))) <= (Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1)))) by ;
then A38: ((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;
A39: Sum (mlt ((SP * P1),E1)) in REAL by XREAL_0:def 1;
A40: ((Sum P1) * (Sum (mlt ((SP * P1),E1)))) + (p1 * e1) in REAL by XREAL_0:def 1;
P . ((len P1) + 1) = p1 by ;
then Sum P1 <= 1 by ;
then f . (Sum (mlt (P,E))) <= ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) by ;
then f . (Sum (mlt (P,E))) <= (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,F1)))) + (p1 * (f . e1)) by ;
hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by ; :: thesis: verum
end;
end;
end;
hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; :: thesis: verum
end;
A41: S1[ 0 ] by RVSUM_1:79;
for k being Nat holds S1[k] from NAT_1:sch 2(A41, A2);
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