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 S_{1}[ 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 S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by RVSUM_1:79;

for k being Nat holds S_{1}[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

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 S

( P . i >= 0 & F . i = f . (E . i) ) ) holds

f . (Sum (mlt (P,E))) <= Sum (mlt (P,F));

A2: for k being Nat st S

S

proof

A41:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[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 A7, FINSEQ_1:42

.= 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 A6, FINSEQ_1:42 ;

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

P1 . i >= 0 ;

end;assume A3: S

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 A7, FINSEQ_1:42

.= 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 A6, FINSEQ_1:42 ;

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

then A19:
for i being Element of NAT st i in dom P1 holds
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 A14, FINSEQ_1:def 3;

then A16: 1 <= i by FINSEQ_1:1;

i <= len P1 by A15, FINSEQ_1:1;

then A17: i <= k by CARD_1:def 7;

k <= k + 1 by NAT_1:11;

then i <= k + 1 by A17, XXREAL_0:2;

then i in Seg (k + 1) by A16, FINSEQ_1:1;

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 A10, A14, FINSEQ_1:def 7;

hence P1 . i >= 0 by A5, A18; :: thesis: verum

end;assume A14: i in dom P1 ; :: thesis: P1 . i >= 0

A15: i in Seg (len P1) by A14, FINSEQ_1:def 3;

then A16: 1 <= i by FINSEQ_1:1;

i <= len P1 by A15, FINSEQ_1:1;

then A17: i <= k by CARD_1:def 7;

k <= k + 1 by NAT_1:11;

then i <= k + 1 by A17, XXREAL_0:2;

then i in Seg (k + 1) by A16, FINSEQ_1:1;

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 A10, A14, FINSEQ_1:def 7;

hence P1 . i >= 0 by A5, A18; :: thesis: verum

P1 . i >= 0 ;

now :: thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))end;

hence
f . (Sum (mlt (P,E))) <= Sum (mlt (P,F))
; :: thesis: verumper cases
( Sum P1 = 0 or Sum P1 <> 0 )
;

end;

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 A19, Th3;

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 A21, Th5;

then A23: Sum (mlt (P1,F1)) = k * 0 by RVSUM_1:80;

Sum P = 0 + p1 by A10, A20, RVSUM_1:74;

hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A4, A12, A11, A9, A22, A23; :: thesis: verum

end;P1 . i = 0 by A19, Th3;

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 A21, Th5;

then A23: Sum (mlt (P1,F1)) = k * 0 by RVSUM_1:80;

Sum P = 0 + p1 by A10, A20, RVSUM_1:74;

hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A4, A12, A11, A9, A22, A23; :: thesis: verum

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

A25:
0 <= Sum P1
by A13, RVSUM_1:84;

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) )

.= ((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 A10, FINSEQ_2:16;

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 A4, A10, RVSUM_1:74;

then A37: p1 = 1 - (Sum P1) ;

Sum (((Sum P1) ") * P1) = ((Sum P1) ") * (Sum P1) by RVSUM_1:87

.= 1 by A24, XCMPLX_0:def 7 ;

then (Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1)))) <= (Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1)))) by A3, A25, A35, A26, XREAL_1:64;

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 A10, FINSEQ_1:42;

then Sum P1 <= 1 by A5, A37, A36, XREAL_1:49;

then f . (Sum (mlt (P,E))) <= ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) by A1, A34, A37, A25, RFUNCT_3:def 12, A39, A40;

then f . (Sum (mlt (P,E))) <= (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,F1)))) + (p1 * (f . e1)) by A38, XXREAL_0:2;

hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A11, A9, A24, XCMPLX_0:def 7; :: thesis: verum

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

A34: Sum (mlt (P,E)) =
(((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,E1)))) + (p1 * e1)
by A12, A24, XCMPLX_0:def 7
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 A27, FINSEQ_1:1;

k <= k + 1 by NAT_1:11;

then i <= k + 1 by A30, XXREAL_0:2;

then i in Seg (k + 1) by A31, FINSEQ_1:1;

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 A29, FINSEQ_1:def 3;

then ( (((Sum P1) ") * P1) . i = ((Sum P1) ") * (P1 . i) & P1 . i >= 0 ) by A13, RVSUM_1:45;

hence (((Sum P1) ") * P1) . i >= 0 by A25; :: thesis: F1 . i = f . (E1 . i)

i in Seg (len E1) by A28, CARD_1:def 7;

then i in dom E1 by FINSEQ_1:def 3;

then A33: E . i = E1 . i by A6, FINSEQ_1:def 7;

i in Seg (len F1) by A28, CARD_1:def 7;

then i in dom F1 by FINSEQ_1:def 3;

then F . i = F1 . i by A7, FINSEQ_1:def 7;

hence F1 . i = f . (E1 . i) by A5, A32, A33; :: thesis: verum

end;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 A27, FINSEQ_1:1;

k <= k + 1 by NAT_1:11;

then i <= k + 1 by A30, XXREAL_0:2;

then i in Seg (k + 1) by A31, FINSEQ_1:1;

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 A29, FINSEQ_1:def 3;

then ( (((Sum P1) ") * P1) . i = ((Sum P1) ") * (P1 . i) & P1 . i >= 0 ) by A13, RVSUM_1:45;

hence (((Sum P1) ") * P1) . i >= 0 by A25; :: thesis: F1 . i = f . (E1 . i)

i in Seg (len E1) by A28, CARD_1:def 7;

then i in dom E1 by FINSEQ_1:def 3;

then A33: E . i = E1 . i by A6, FINSEQ_1:def 7;

i in Seg (len F1) by A28, CARD_1:def 7;

then i in dom F1 by FINSEQ_1:def 3;

then F . i = F1 . i by A7, FINSEQ_1:def 7;

hence F1 . i = f . (E1 . i) by A5, A32, A33; :: thesis: verum

.= ((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 A10, FINSEQ_2:16;

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 A4, A10, RVSUM_1:74;

then A37: p1 = 1 - (Sum P1) ;

Sum (((Sum P1) ") * P1) = ((Sum P1) ") * (Sum P1) by RVSUM_1:87

.= 1 by A24, XCMPLX_0:def 7 ;

then (Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1)))) <= (Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1)))) by A3, A25, A35, A26, XREAL_1:64;

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 A10, FINSEQ_1:42;

then Sum P1 <= 1 by A5, A37, A36, XREAL_1:49;

then f . (Sum (mlt (P,E))) <= ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) by A1, A34, A37, A25, RFUNCT_3:def 12, A39, A40;

then f . (Sum (mlt (P,E))) <= (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,F1)))) + (p1 * (f . e1)) by A38, XXREAL_0:2;

hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A11, A9, A24, XCMPLX_0:def 7; :: thesis: verum

for k being Nat holds S

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