let X be RealLinearSpace; :: thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds
( f is convex iff for n being non zero 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )

let f be Function of the carrier of X,ExtREAL; :: thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for n being non zero 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) )

assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis: ( f is convex iff for n being non zero 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )

thus ( f is convex implies for n being non zero 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) :: thesis: ( ( for n being non zero 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex )
proof
assume A2: f is convex ; :: thesis: for n being non zero 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F

let n be non zero Element of NAT ; :: thesis: 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F

let p be FinSequence of REAL ; :: thesis: 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F

let F be FinSequence of ExtREAL ; :: thesis: 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F

let y, z be FinSequence of the carrier of X; :: thesis: ( 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 = (p . i) * (f . (y /. i)) ) ) implies f . (Sum z) <= Sum F )

assume that
A3: len p = n and
A4: len F = n and
len y = n and
A5: len z = n and
A6: Sum p = 1 and
A7: for i being Element of NAT st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) ; :: thesis: f . (Sum z) <= Sum F
for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (p . i) * (f . (y /. i)) ) by A7;
then A8: not -infty in rng F by A1, A4, Lm13;
per cases ( for i being Element of NAT st i in Seg n holds
f . (y /. i) <> +infty or ex i being Element of NAT st
( i in Seg n & f . (y /. i) = +infty ) )
;
suppose A9: for i being Element of NAT st i in Seg n holds
f . (y /. i) <> +infty ; :: thesis: f . (Sum z) <= Sum F
defpred S1[ set , set ] means \$2 = [(y /. \$1),(f . (y /. \$1))];
reconsider V = Prod_of_RLS (X,RLS_Real) as RealLinearSpace ;
A10: 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: ( i in Seg n implies f . (y /. i) in REAL )
assume i in Seg n ; :: thesis: f . (y /. i) in REAL
then f . (y /. i) <> +infty by A9;
hence f . (y /. i) in REAL by ; :: thesis: verum
end;
A11: for i being Nat st i in Seg n holds
ex v being Element of V st S1[i,v]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex v being Element of V st S1[i,v] )
assume i in Seg n ; :: thesis: ex v being Element of V st S1[i,v]
then reconsider w = f . (y /. i) as Element of REAL by A10;
set v = [(y /. i),w];
reconsider v = [(y /. i),w] as Element of V ;
take v ; :: thesis: S1[i,v]
thus S1[i,v] ; :: thesis: verum
end;
consider g being FinSequence of the carrier of V such that
A12: dom g = Seg n and
A13: for i being Nat st i in Seg n holds
S1[i,g /. i] from A14: len g = n by ;
defpred S2[ set , set ] means \$2 = F . \$1;
A15: for i being Nat st i in Seg n holds
ex w being Element of RLS_Real st S2[i,w]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex w being Element of RLS_Real st S2[i,w] )
assume A16: i in Seg n ; :: thesis: ex w being Element of RLS_Real st S2[i,w]
then reconsider a = f . (y /. i) as Element of REAL by A10;
F . i = (p . i) * (f . (y /. i)) by ;
then F . i = (p . i) * a by EXTREAL1:1;
then reconsider w = F . i as Element of RLS_Real by XREAL_0:def 1;
take w ; :: thesis: S2[i,w]
thus S2[i,w] ; :: thesis: verum
end;
consider F1 being FinSequence of the carrier of RLS_Real such that
A17: dom F1 = Seg n and
A18: for i being Nat st i in Seg n holds
S2[i,F1 /. i] from A19: len F1 = n by ;
reconsider M = epigraph f as Subset of V ;
deffunc H1( Nat) -> Element of the carrier of V = (p . \$1) * (g /. \$1);
consider G being FinSequence of the carrier of V such that
A20: len G = n and
A21: for i being Nat st i in dom G holds
G . i = H1(i) from A22: dom G = Seg n by ;
A23: 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: ( i in Seg n implies ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M ) )
assume A24: i in Seg n ; :: thesis: ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M )
hence p . i > 0 by A7; :: thesis: ( G . i = (p . i) * (g /. i) & g /. i in M )
thus G . i = (p . i) * (g /. i) by ; :: thesis: g /. i in M
reconsider w = f . (y /. i) as Element of REAL by ;
[(y /. i),w] in { [x,a] where x is Element of X, a is Element of REAL : f . x <= a } ;
hence g /. i in M by ; :: thesis: verum
end;
M is convex by A2;
then A25: Sum G in M by A3, A6, A14, A20, A23, Th7;
A26: for i being Element of NAT st i in Seg n holds
F1 . i = F . i
proof
let i be Element of NAT ; :: thesis: ( i in Seg n implies F1 . i = F . i )
assume A27: i in Seg n ; :: thesis: F1 . i = F . i
then F1 /. i = F1 . i by ;
hence F1 . i = F . i by ; :: thesis: verum
end;
for i being Nat st i in Seg n holds
G . i = [(z . i),(F1 . i)]
proof
let i be Nat; :: thesis: ( i in Seg n implies G . i = [(z . i),(F1 . i)] )
assume A28: i in Seg n ; :: thesis: G . i = [(z . i),(F1 . i)]
then reconsider a = f . (y /. i) as Element of REAL by A10;
g /. i = [(y /. i),a] by ;
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 ;
then A29: G . i = [(z . i),((p . i) * a)] by ;
F . i = (p . i) * (f . (y /. i)) by ;
then F . i = (p . i) * a by EXTREAL1:1;
hence G . i = [(z . i),(F1 . i)] by ; :: thesis: verum
end;
then Sum G = [(Sum z),(Sum F1)] by A5, A20, A19, Th3;
then [(Sum z),(Sum F)] in M by A4, A25, A26, A19, 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 <= w ;
x = Sum z by ;
hence f . (Sum z) <= Sum F by ; :: thesis: verum
end;
suppose ex i being Element of NAT st
( i in Seg n & f . (y /. i) = +infty ) ; :: thesis: f . (Sum z) <= Sum F
then consider i being Element of NAT such that
A32: i in Seg n and
A33: f . (y /. i) = +infty ;
A34: F . i = (p . i) * (f . (y /. i)) by ;
A35: i in dom F by ;
p . i > 0 by ;
then F . i = +infty by ;
then Sum F = +infty by ;
hence f . (Sum z) <= Sum F by XXREAL_0:4; :: thesis: verum
end;
end;
end;
thus ( ( for n being non zero 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex ) :: thesis: verum
proof
assume A36: for n being non zero 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 = (p . i) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ; :: thesis: f is convex
for x1, x2 being VECTOR of X
for q being Real st 0 < q & q < 1 holds
f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2))
proof
set n = 2;
let x1, x2 be VECTOR of X; :: thesis: for q being Real st 0 < q & q < 1 holds
f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2))

let q be Real; :: thesis: ( 0 < q & q < 1 implies f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2)) )
assume that
A37: 0 < q and
A38: q < 1 ; :: thesis: f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2))
reconsider q1 = q * (f . x1), q2 = (1 - q) * (f . x2) as R_eal by XXREAL_0:def 1;
reconsider F = <*q1,q2*> as FinSequence of ExtREAL ;
reconsider z = <*(q * x1),((1 - q) * x2)*> as FinSequence of the carrier of X ;
reconsider y = <*x1,x2*> as FinSequence of the carrier of X ;
reconsider q = q as Element of REAL by XREAL_0:def 1;
reconsider q1 = 1 - q as Element of REAL by XREAL_0:def 1;
reconsider p = <*q,q1*> as FinSequence of REAL ;
A39: for i being Element of NAT st i in Seg 2 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )
proof
let i be Element of NAT ; :: thesis: ( i in Seg 2 implies ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) )
assume A40: i in Seg 2 ; :: thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )
per cases ( i = 1 or i = 2 ) by ;
suppose A41: i = 1 ; :: thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )
then A42: y /. i = x1 by FINSEQ_4:17;
p . i = q by ;
hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) by ; :: thesis: verum
end;
suppose A43: i = 2 ; :: thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) )
then A44: y /. i = x2 by FINSEQ_4:17;
p . i = 1 - q by ;
hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (p . i) * (f . (y /. i)) ) by ; :: thesis: verum
end;
end;
end;
A45: len p = 2 by FINSEQ_1:44;
A46: Sum p = q + (1 - q) by RVSUM_1:77
.= 1 ;
A47: len z = 2 by FINSEQ_1:44;
A48: Sum z = (q * x1) + ((1 - q) * x2) by RLVECT_1:45;
A49: len y = 2 by FINSEQ_1:44;
A50: len F = 2 by FINSEQ_1:44;
Sum F = (q * (f . x1)) + ((1 - q) * (f . x2)) by EXTREAL1:9;
hence f . ((q * x1) + ((1 - q) * x2)) <= (q * (f . x1)) + ((1 - q) * (f . x2)) by A36, A45, A50, A49, A47, A46, A39, A48; :: thesis: verum
end;
hence f is convex by ; :: thesis: verum
end;