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 ) )
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 A1: REAL c= dom f by PARTFUN1:def 4;
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) ) implies f is_convex_on REAL )

proof

assume A3: 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 A4: ( 0 <= p & 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 ( r in REAL & s in REAL & (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:121;
A5: Sum P = p + (1 - p) by RVSUM_1:107
.= 1 ;
for i being Element of NAT st i in dom P holds
( P . i >= 0 & F . i = f . (E . i) )

proof

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

now

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

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

then ( E . i = r & P . i = p & F . i = f . r ) by FINSEQ_1:61;
hence ( P . i >= 0 & F . i = f . (E . i) ) by A4; :: thesis: verum

end;

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

then ( E . i = s & P . i = 1 - p & F . i = f . s ) by FINSEQ_1:61;
hence ( P . i >= 0 & F . i = f . (E . i) ) by A4, XREAL_1:50; :: thesis: verum

end;

end;

end;

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

end;

then A8: f . (Sum (mlt P,E)) <= Sum (mlt P,F) by A3, A5;
A9: ( P . 1 = p & P . 2 = 1 - p & E . 1 = r & E . 2 = s & F . 1 = f . r & F . 2 = f . s ) by FINSEQ_1:61;
len P = 2 by FINSEQ_1:61
.= len E by FINSEQ_1:61 ;
then len (multreal .: P,E) = len P by FINSEQ_2:86;
then A10: len (mlt P,E) = 2 by FINSEQ_1:61;
( (mlt P,E) . 1 = (P . 1) * (E . 1) & (mlt P,E) . 2 = (P . 2) * (E . 2) ) by RVSUM_1:87;
then mlt P,E = <*(p * r),((1 - p) * s)*> by A9, A10, FINSEQ_1:61;
then A11: Sum (mlt P,E) = (p * r) + ((1 - p) * s) by RVSUM_1:107;
len P = 2 by FINSEQ_1:61
.= len F by FINSEQ_1:61 ;
then len (multreal .: P,F) = len P by FINSEQ_2:86;
then A12: len (mlt P,F) = 2 by FINSEQ_1:61;
( (mlt P,F) . 1 = (P . 1) * (F . 1) & (mlt P,F) . 2 = (P . 2) * (F . 2) ) by RVSUM_1:87;
then mlt P,F = <*(p * (f . r)),((1 - p) * (f . s))*> by A9, A12, FINSEQ_1:61;
hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A8, A11, RVSUM_1:107; :: thesis: verum

end;

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

end;

( 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 A13: 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);
A14: S₁[ 0 ] by RVSUM_1:109;
A15: 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 A16: 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 A17: ( Sum P = 1 & ( 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 P1 being Element of k -tuples_on REAL , p1 being Real such that
A18: P = P1 ^ <*p1*> by FINSEQ_2:137;
consider E1 being Element of k -tuples_on REAL , e1 being Real such that
A19: E = E1 ^ <*e1*> by FINSEQ_2:137;
consider F1 being Element of k -tuples_on REAL , f1 being Real such that
A20: F = F1 ^ <*f1*> by FINSEQ_2:137;
mlt P,E = (mlt P1,E1) ^ <*(p1 * e1)*> by A18, A19, Th2;
then A21: Sum (mlt P,E) = (1 * (Sum (mlt P1,E1))) + (p1 * e1) by RVSUM_1:104;
mlt P,F = (mlt P1,F1) ^ <*(p1 * f1)*> by A18, A20, Th2;
then A22: Sum (mlt P,F) = (1 * (Sum (mlt P1,F1))) + (p1 * f1) by RVSUM_1:104;
(len F1) + 1 = k + 1 by FINSEQ_1:def 18
.= len P by FINSEQ_1:def 18 ;
then (len F1) + 1 in Seg (len P) by FINSEQ_1:6;
then A23: (len F1) + 1 in dom P by FINSEQ_1:def 3;
A24: f1 = F . ((len F1) + 1) by A20, FINSEQ_1:59
.= f . (E . ((len F1) + 1)) by A17, A23
.= f . (E . (k + 1)) by FINSEQ_1:def 18
.= f . (E . ((len E1) + 1)) by FINSEQ_1:def 18
.= f . e1 by A19, FINSEQ_1:59 ;
A25: 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 A26: i in dom P1 ; :: thesis: P1 . i >= 0
i in Seg (len P1) by A26, FINSEQ_1:def 3;
then ( 1 <= i & i <= len P1 ) by FINSEQ_1:3;
then ( 1 <= i & i <= k & k <= k + 1 ) by FINSEQ_1:def 18, NAT_1:11;
then ( 1 <= i & i <= k + 1 ) by XXREAL_0:2;
then i in Seg (k + 1) by FINSEQ_1:3;
then i in Seg (len P) by FINSEQ_1:def 18;
then A27: i in dom P by FINSEQ_1:def 3;
P1 . i = P . i by A18, A26, FINSEQ_1:def 7;
hence P1 . i >= 0 by A17, A27; :: thesis: verum

end;

then A28: 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 A29: 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 A28, Th3;
then A30: P1 = k |-> 0 by Th4;
then mlt P1,E1 = k |-> 0 by Th5;
then A31: Sum (mlt P1,E1) = k * 0 by RVSUM_1:110;
A32: Sum P = 0 + p1 by A18, A29, RVSUM_1:104;
mlt P1,F1 = k |-> 0 by A30, Th5;
then Sum (mlt P1,F1) = k * 0 by RVSUM_1:110;
hence f . (Sum (mlt P,E)) <= Sum (mlt P,F) by A17, A21, A22, A24, A31, A32; :: thesis: verum

end;

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

then A34: Sum (mlt P,E) = (((Sum P1) * ((Sum P1) " )) * (Sum (mlt P1,E1))) + (p1 * e1) by A21, 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:117
.= ((Sum P1) * (Sum (mlt (((Sum P1) " ) * P1),E1))) + (p1 * e1) by FINSEQOP:27 ;
(Sum P1) + p1 = 1 by A17, A18, RVSUM_1:104;
then A35: p1 = 1 - (Sum P1) ;
A36: ( 0 <= Sum P1 & Sum P1 <= 1 )

proof

thus 0 <= Sum P1 by A25, RVSUM_1:114; :: thesis: Sum P1 <= 1
(len P1) + 1 = len P by A18, FINSEQ_2:19;
then (len P1) + 1 in Seg (len P) by FINSEQ_1:6;
then A37: (len P1) + 1 in dom P by FINSEQ_1:def 3;
P . ((len P1) + 1) = p1 by A18, FINSEQ_1:59;
then p1 >= 0 by A17, A37;
hence Sum P1 <= 1 by A35, XREAL_1:51; :: thesis: verum

end;

then A38: f . (Sum (mlt P,E)) <= ((Sum P1) * (f . (Sum (mlt (((Sum P1) " ) * P1),E1)))) + (p1 * (f . e1)) by A13, A34, A35, RFUNCT_3:def 13;
f . (Sum (mlt (((Sum P1) " ) * P1),E1)) <= ((Sum P1) " ) * (Sum (mlt P1,F1))

proof

A39: ((Sum P1) " ) * (Sum (mlt P1,F1)) = Sum (((Sum P1) " ) * (mlt P1,F1)) by RVSUM_1:117
.= Sum (mlt (((Sum P1) " ) * P1),F1) by FINSEQOP:27 ;
A40: Sum (((Sum P1) " ) * P1) = ((Sum P1) " ) * (Sum P1) by RVSUM_1:117
.= 1 by A33, XCMPLX_0:def 7 ;
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 A41: i in dom (((Sum P1) " ) * P1) ; :: thesis: ( (((Sum P1) " ) * P1) . i >= 0 & F1 . i = f . (E1 . i) )
i in Seg (len (((Sum P1) " ) * P1)) by A41, FINSEQ_1:def 3;
then A42: i in Seg k by FINSEQ_1:def 18;
A43: (((Sum P1) " ) * P1) . i = ((Sum P1) " ) * (P1 . i) by RVSUM_1:67;
A44: (Sum P1) " > 0 by A33, A36;
A45: i in Seg (len P1) by A42, FINSEQ_1:def 18;
then i in dom P1 by FINSEQ_1:def 3;
then P1 . i >= 0 by A25;
hence (((Sum P1) " ) * P1) . i >= 0 by A43, A44; :: thesis: F1 . i = f . (E1 . i)
( i in Seg (len F1) & i in Seg (len E1) ) by A42, FINSEQ_1:def 18;
then A46: ( i in dom F1 & i in dom E1 ) by FINSEQ_1:def 3;
( 1 <= i & i <= len P1 ) by A45, FINSEQ_1:3;
then ( 1 <= i & i <= k & k <= k + 1 ) by FINSEQ_1:def 18, NAT_1:11;
then ( 1 <= i & i <= k + 1 ) by XXREAL_0:2;
then i in Seg (k + 1) by FINSEQ_1:3;
then i in Seg (len P) by FINSEQ_1:def 18;
then A47: i in dom P by FINSEQ_1:def 3;
( F . i = F1 . i & E . i = E1 . i ) by A19, A20, A46, FINSEQ_1:def 7;
hence F1 . i = f . (E1 . i) by A17, A47; :: thesis: verum

end;

hence f . (Sum (mlt (((Sum P1) " ) * P1),E1)) <= ((Sum P1) " ) * (Sum (mlt P1,F1)) by A16, A39, A40; :: thesis: verum

end;

then (Sum P1) * (f . (Sum (mlt (((Sum P1) " ) * P1),E1))) <= (Sum P1) * (((Sum P1) " ) * (Sum (mlt P1,F1))) by A36, XREAL_1:66;
then ((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:8;
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 A22, A24, A33, 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;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A14, A15);
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;

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 A2; :: thesis: verum