let X be RealLinearSpace; :: thesis:
let f be Function of the carrier of X, ExtREAL ; :: thesis:
assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis:
thus ( f is convex implies for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) :: thesis:

proof

assume A2: f is convex ; :: thesis:
let n be non empty Element of NAT ; :: thesis:
let p be FinSequence of REAL ; :: thesis:
let F be FinSequence of ExtREAL ; :: thesis:
let y, z be FinSequence of the carrier of X; :: thesis:
assume that
A3: ( len p = n & len F = n & len y = n & len z = n ) and
A4: Sum p = 1 and
A5: for i being Element of NAT st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; :: thesis:
A6: for i being Element of NAT st i in Seg n holds
0. < R_EAL (p . i)

proof

let i be Element of NAT ; :: thesis:
assume i in Seg n ; :: thesis:
then p . i > 0 by A5;
hence 0. < R_EAL (p . i) by MEASURE6:def 1; :: thesis:

end;

for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A5;
then A7: not -infty in rng F by A1, A3, Lm17;

per cases ;

suppose A8: for i being Element of NAT st i in Seg n holds
f . (y /. i) <> +infty ; :: thesis:

A9: for i being Element of NAT st i in Seg n holds
f . (y /. i) in REAL

proof

let i be Element of NAT ; :: thesis:
assume i in Seg n ; :: thesis:
then f . (y /. i) <> +infty by A8;
hence f . (y /. i) in REAL by A1, XXREAL_0:14; :: thesis:

end;

reconsider V = Prod_of_RLS X,RLS_Real as RealLinearSpace ;
defpred S₁[ set , set ] means $2 = [(y /. $1),(f . (y /. $1))];
A10: for i being Element of NAT st i in Seg n holds
ex v being Element of V st S₁[i,v]

proof

let i be Element of NAT ; :: thesis:
assume i in Seg n ; :: thesis:
then reconsider w = f . (y /. i) as Real by A9;
set v = [(y /. i),w];
reconsider v = [(y /. i),w] as Element of V ;
take v ; :: thesis:
thus S₁[i,v] ; :: thesis:

end;

consider g being FinSequence of the carrier of V such that
A11: dom g = Seg n and
A12: for i being Element of NAT st i in Seg n holds
S₁[i,g /. i] from POLYNOM2:sch 1(A10);
A13: len g = n by A11, FINSEQ_1:def 3;
deffunc H₁( Nat) -> Element of the carrier of V = (p . $1) * (g /. $1);
consider G being FinSequence of the carrier of V such that
A14: len G = n and
A15: for i being Nat st i in dom G holds
G . i = H₁(i) from FINSEQ_2:sch 1();
A16: dom G = Seg n by A14, FINSEQ_1:def 3;
reconsider M = epigraph f as Subset of V ;
A17: for i being Nat st i in Seg n holds
( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M )

proof

let i be Nat; :: thesis:
assume A18: i in Seg n ; :: thesis:
hence p . i > 0 by A5; :: thesis:
thus G . i = (p . i) * (g /. i) by A15, A18, A16; :: thesis:
reconsider w = f . (y /. i) as Real by A9, A18;
f . (y /. i) = R_EAL w by MEASURE6:def 1;
then [(y /. i),w] in { [x,a] where x is Element of X, a is Element of REAL : f . x <= R_EAL a } ;
hence g /. i in M by A12, A18; :: thesis:

end;

M is convex by A2, Def7;
then A19: Sum G in M by A3, A4, A13, A14, A17, Th12;
defpred S₂[ set , set ] means $2 = F . $1;
A20: for i being Element of NAT st i in Seg n holds
ex w being Element of RLS_Real st S₂[i,w]

proof

let i be Element of NAT ; :: thesis:
assume A21: i in Seg n ; :: thesis:
then A22: F . i = (R_EAL (p . i)) * (f . (y /. i)) by A5;
reconsider a = f . (y /. i) as Real by A9, A21;
F . i = (p . i) * a by A22, Lm15;
then reconsider w = F . i as Element of RLS_Real ;
take w ; :: thesis:
thus S₂[i,w] ; :: thesis:

end;

consider F1 being FinSequence of the carrier of RLS_Real such that
A23: dom F1 = Seg n and
A24: for i being Element of NAT st i in Seg n holds
S₂[i,F1 /. i] from POLYNOM2:sch 1(A20);
A25: for i being Element of NAT st i in Seg n holds
F1 . i = F . i

proof

let i be Element of NAT ; :: thesis:
assume A26: i in Seg n ; :: thesis:
then F1 /. i = F1 . i by A23, PARTFUN1:def 8;
hence F1 . i = F . i by A24, A26; :: thesis:

end;

A27: len F1 = n by A23, FINSEQ_1:def 3;
for i being Element of NAT st i in Seg n holds
G . i = [(z . i),(F1 . i)]

proof

let i be Element of NAT ; :: thesis:
assume A28: i in Seg n ; :: thesis:
then reconsider a = f . (y /. i) as Real by A9;
g /. i = [(y /. i),a] by A12, A28;
then (p . i) * (g /. i) = [((p . i) * (y /. i)),((p . i) * a)] by Lm1;
then G . i = [((p . i) * (y /. i)),((p . i) * a)] by A15, A28, A16;
then A29: G . i = [(z . i),((p . i) * a)] by A5, A28;
F . i = (R_EAL (p . i)) * (f . (y /. i)) by A5, A28;
then F . i = (p . i) * a by Lm15;
hence G . i = [(z . i),(F1 . i)] by A25, A28, A29; :: thesis:

end;

then Sum G = [(Sum z),(Sum F1)] by A3, A14, A27, Th3;
then [(Sum z),(Sum F)] in M by A3, A19, A25, A27, Lm8;
then consider x being Element of X, w being Element of REAL such that
A30: [(Sum z),(Sum F)] = [x,w] and
A31: f . x <= R_EAL w ;
( x = Sum z & w = Sum F ) by A30, ZFMISC_1:33;
hence f . (Sum z) <= Sum F by A31, MEASURE6:def 1; :: thesis:

end;

suppose ex i being Element of NAT st
( i in Seg n & f . (y /. i) = +infty ) ; :: thesis:

then consider i being Element of NAT such that
A32: i in Seg n and
A33: f . (y /. i) = +infty ;
A34: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A5, A32;
A35: i in dom F by A3, A32, FINSEQ_1:def 3;
0. < R_EAL (p . i) by A6, A32;
then F . i = +infty by A33, A34, EXTREAL1:def 1;
then Sum F = +infty by A7, A35, Lm6, FUNCT_1:12;
hence f . (Sum z) <= Sum F by XXREAL_0:4; :: thesis:

end;

thus ( ( for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex ) :: thesis:

proof

assume A36: for n being non empty Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ; :: thesis:
for x1, x2 being VECTOR of X
for q being Real st 0 < q & q < 1 holds
f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2))

proof

let x1, x2 be VECTOR of X; :: thesis:
let q be Real; :: thesis:
assume A37: ( 0 < q & q < 1 ) ; :: thesis:
reconsider p = <*q,(1 - q)*> as FinSequence of REAL ;
reconsider y = <*x1,x2*> as FinSequence of the carrier of X ;
reconsider z = <*(q * x1),((1 - q) * x2)*> as FinSequence of the carrier of X ;
reconsider F = <*((R_EAL q) * (f . x1)),((R_EAL (1 - q)) * (f . x2))*> as FinSequence of ExtREAL ;
set n = 2;
A38: ( len p = 2 & len F = 2 & len y = 2 & len z = 2 ) by FINSEQ_1:61;
A39: Sum p = q + (1 - q) by RVSUM_1:107
.= 1 ;
A40: for i being Element of NAT st i in Seg 2 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) )

proof

let i be Element of NAT ; :: thesis:
assume A41: i in Seg 2 ; :: thesis:

per cases by A41, FINSEQ_1:4, TARSKI:def 2;

suppose i = 1 ; :: thesis:

then ( p . i = q & y /. i = x1 & z . i = q * x1 & F . i = (R_EAL q) * (f . x1) ) by FINSEQ_1:61, FINSEQ_4:26;
hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A37; :: thesis:

end;

suppose i = 2 ; :: thesis:

then ( p . i = 1 - q & y /. i = x2 & z . i = (1 - q) * x2 & F . i = (R_EAL (1 - q)) * (f . x2) ) by FINSEQ_1:61, FINSEQ_4:26;
hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A37, XREAL_1:52; :: thesis:

end;

( Sum z = (q * x1) + ((1 - q) * x2) & Sum F = ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) ) by Th6, RLVECT_1:62;
hence f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) by A36, A38, A39, A40; :: thesis:

end;

hence f is convex by A1, Th9; :: thesis:

end;