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:137;
consider F1 being Element of k -tuples_on REAL , f1 being Real such that
A8: F = F1 ^ <*f1*> by FINSEQ_2:137;
(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 A9: (len F1) + 1 in dom P by FINSEQ_1:def 3;
A10: f1 = F . ((len F1) + 1) by A8, FINSEQ_1:59
.= f . (E . ((len F1) + 1)) by A6, A9
.= f . (E . (k + 1)) by FINSEQ_1:def 18
.= f . (E . ((len E1) + 1)) by FINSEQ_1:def 18
.= f . e1 by A7, FINSEQ_1:59 ;
consider P1 being Element of k -tuples_on REAL , p1 being Real such that
A11: P = P1 ^ <*p1*> by FINSEQ_2:137;
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:104;
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:104;
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:3;
i <= len P1 by A16, FINSEQ_1:3;
then A18: i <= k by FINSEQ_1:def 18;
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:3;
then i in Seg (len P) by FINSEQ_1:def 18;
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:110;
mlt P1,F1 = k |-> 0 by A22, Th5;
then A24: Sum (mlt P1,F1) = k * 0 by RVSUM_1:110;
Sum P = 0 + p1 by A11, A21, RVSUM_1:104;
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:114;
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 FINSEQ_1:def 18;
then A30: i in Seg (len P1) by FINSEQ_1:def 18;
then i <= len P1 by FINSEQ_1:3;
then A31: i <= k by FINSEQ_1:def 18;
A32: 1 <= i by A28, FINSEQ_1:3;
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:3;
then i in Seg (len P) by FINSEQ_1:def 18;
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:67;
hence (((Sum P1) " ) * P1) . i >= 0 by A26; :: thesis: F1 . i = f . (E1 . i)
i in Seg (len E1) by A29, FINSEQ_1:def 18;
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, FINSEQ_1:def 18;
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:117
.= ((Sum P1) * (Sum (mlt (((Sum P1) " ) * P1),E1))) + (p1 * e1) by FINSEQOP:27 ;
A36: ((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 ;
(len P1) + 1 = len P by A11, 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;
(Sum P1) + p1 = 1 by A5, A11, RVSUM_1:104;
then A38: p1 = 1 - (Sum P1) ;
Sum (((Sum P1) " ) * P1) = ((Sum P1) " ) * (Sum P1) by RVSUM_1:117
.= 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:66;
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:8;
P . ((len P1) + 1) = p1 by A11, FINSEQ_1:59;
then Sum P1 <= 1 by A6, A38, A37, XREAL_1:51;
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 13;
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:109;
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 4;
( ( 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:121;
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 FINSEQ_1:def 18 ;
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:4, TARSKI:def 2;

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

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

end;

hence f is_convex_on REAL by A41, RFUNCT_3:def 13; :: 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