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

proof

assume A2: f is convex ; :: thesis:
let n be non zero 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 and
A4: len F = n and
A5: len y = n and
A6: len z = n and
A7: Sum p = 1 and
A8: 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:
consider s being Permutation of (dom p), k being Element of NAT such that
A9: for i being Element of NAT st i in dom p holds
( i in Seg k iff p . (s . i) <> 0 ) by Lm14;
A10: dom p = Seg n by A3, FINSEQ_1:def 3;
then reconsider s1 = s as FinSequence of Seg n by FINSEQ_2:25;
A11: dom F = Seg n by A4, FINSEQ_1:def 3;
then A12: F is Function of (Seg n),ExtREAL by FINSEQ_2:26;
then reconsider F9 = F * s1 as FinSequence of ExtREAL by FINSEQ_2:32;
A13: F9 = (F9 | k) ^ (F9 /^ k) by RFINSEQ:8;
A14: for i being Element of NAT st 1 <= i & i <= n - k holds
( i + k in Seg n & p . (s . (i + k)) = 0 )

proof

let i be Element of NAT ; :: thesis:
assume that
A15: 1 <= i and
A16: i <= n - k ; :: thesis:
i <= i + k by INT_1:6;
then A17: 1 <= i + k by A15, XXREAL_0:2;
0 + k < i + k by A15, XREAL_1:6;
then A18: not i + k in Seg k by FINSEQ_1:1;
A19: i + k <= (n - k) + k by A16, XREAL_1:6;
then i + k in dom p by A10, A17, FINSEQ_1:1;
hence ( i + k in Seg n & p . (s . (i + k)) = 0 ) by A9, A19, A17, A18, FINSEQ_1:1; :: thesis:

end;

A20: dom z = Seg n by A6, FINSEQ_1:def 3;
then A21: z is Function of (Seg n), the carrier of X by FINSEQ_2:26;
then reconsider z9 = z * s1 as FinSequence of the carrier of X by FINSEQ_2:32;
dom s = Seg n by A10, FUNCT_2:def 1;
then A22: len s1 = n by FINSEQ_1:def 3;
then A23: len z9 = n by A21, FINSEQ_2:33;
A24: Sum (z9 /^ k) = 0. X

proof

per cases ;

suppose k >= n ; :: thesis:

then z9 /^ k = <*> the carrier of X by A23, FINSEQ_5:32;
hence Sum (z9 /^ k) = 0. X by RLVECT_1:43; :: thesis:

end;

suppose A25: k < n ; :: thesis:

for w being object st w in rng (z9 /^ k) holds
w in {(0. X)}

proof

reconsider k1 = n - k as Element of NAT by A25, INT_1:5;
let w be object ; :: thesis:
assume w in rng (z9 /^ k) ; :: thesis:
then consider i being object such that
A26: i in dom (z9 /^ k) and
A27: (z9 /^ k) . i = w by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A26;
len (z9 /^ k) = k1 by A23, A25, RFINSEQ:def 1;
then A28: i in Seg k1 by A26, FINSEQ_1:def 3;
then A29: 1 <= i by FINSEQ_1:1;
A30: i <= n - k by A28, FINSEQ_1:1;
then s . (i + k) in Seg n by A10, A14, A29, FUNCT_2:5;
then z . (s . (i + k)) = (p . (s . (i + k))) * (y /. (s . (i + k))) by A8;
then A31: z . (s . (i + k)) = 0. X by A14, A29, A30, RLVECT_1:10;
i + k in Seg n by A14, A29, A30;
then i + k in dom z9 by A23, FINSEQ_1:def 3;
then z9 . (i + k) = 0. X by A31, FUNCT_1:12;
then w = 0. X by A23, A25, A26, A27, RFINSEQ:def 1;
hence w in {(0. X)} by TARSKI:def 1; :: thesis:

end;

then rng (z9 /^ k) c= {(0. X)} by TARSKI:def 3;
hence Sum (z9 /^ k) = 0. X by Lm11; :: thesis:

end;

A32: p is Function of (Seg n),REAL by A10, FINSEQ_2:26;
then reconsider p9 = p * s1 as FinSequence of REAL by FINSEQ_2:32;
set k9 = min (k,n);
reconsider k9 = min (k,n) as Element of NAT ;
p9 = (p9 | k) ^ (p9 /^ k) by RFINSEQ:8;
then A33: Sum p9 = (Sum (p9 | k)) + (Sum (p9 /^ k)) by RVSUM_1:75;
A34: len F9 = n by A22, A12, FINSEQ_2:33;
A35: Sum (F9 /^ k) = 0.

proof

per cases ;

suppose k >= n ; :: thesis:

hence Sum (F9 /^ k) = 0. by A34, EXTREAL1:7, FINSEQ_5:32; :: thesis:

end;

suppose A36: k < n ; :: thesis:

for w being object st w in rng (F9 /^ k) holds
w in {0.}

proof

reconsider k1 = n - k as Element of NAT by A36, INT_1:5;
let w be object ; :: thesis:
assume w in rng (F9 /^ k) ; :: thesis:
then consider i being object such that
A37: i in dom (F9 /^ k) and
A38: (F9 /^ k) . i = w by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A37;
len (F9 /^ k) = k1 by A34, A36, RFINSEQ:def 1;
then A39: i in Seg k1 by A37, FINSEQ_1:def 3;
then A40: 1 <= i by FINSEQ_1:1;
A41: i <= n - k by A39, FINSEQ_1:1;
then A42: p . (s . (i + k)) = 0 by A14, A40;
i + k in Seg n by A14, A40, A41;
then A43: i + k in dom F9 by A34, FINSEQ_1:def 3;
s . (i + k) in Seg n by A10, A14, A40, A41, FUNCT_2:5;
then F . (s . (i + k)) = 0 * (f . (y /. (s . (i + k)))) by A8, A42;
then F9 . (i + k) = 0. by A43, FUNCT_1:12;
then w = 0. by A34, A36, A37, A38, RFINSEQ:def 1;
hence w in {0.} by TARSKI:def 1; :: thesis:

end;

then rng (F9 /^ k) c= {0.} by TARSKI:def 3;
hence Sum (F9 /^ k) = 0. by Lm9; :: thesis:

end;

A44: F9 | k = F9 | (Seg k) by FINSEQ_1:def 16;
then A45: len (F9 | k) = k9 by A34, FINSEQ_2:21;
for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (p . i) * (f . (y /. i)) ) by A8;
then A46: not -infty in rng F by A1, A4, Lm13;
then not -infty in rng F9 by FUNCT_1:14;
then A47: not -infty in (rng (F9 | k)) \/ (rng (F9 /^ k)) by A13, FINSEQ_1:31;
then A48: not -infty in rng (F9 /^ k) by XBOOLE_0:def 3;
A49: z9 | k = z9 | (Seg k) by FINSEQ_1:def 16;
then A50: len (z9 | k) = k9 by A23, FINSEQ_2:21;
A51: len p9 = n by A22, A32, FINSEQ_2:33;
A52: Sum (p9 /^ k) = 0

proof

per cases ;

suppose k >= n ; :: thesis:

hence Sum (p9 /^ k) = 0 by A51, FINSEQ_5:32, RVSUM_1:72; :: thesis:

end;

suppose A53: k < n ; :: thesis:

for w being object st w in rng (p9 /^ k) holds
w in {0}

proof

reconsider k1 = n - k as Element of NAT by A53, INT_1:5;
let w be object ; :: thesis:
assume w in rng (p9 /^ k) ; :: thesis:
then consider i being object such that
A54: i in dom (p9 /^ k) and
A55: (p9 /^ k) . i = w by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A54;
len (p9 /^ k) = k1 by A51, A53, RFINSEQ:def 1;
then A56: i in Seg k1 by A54, FINSEQ_1:def 3;
then A57: 1 <= i by FINSEQ_1:1;
A58: i <= n - k by A56, FINSEQ_1:1;
then i + k in Seg n by A14, A57;
then A59: i + k in dom p9 by A51, FINSEQ_1:def 3;
p . (s . (i + k)) = 0 by A14, A57, A58;
then p9 . (i + k) = 0 by A59, FUNCT_1:12;
then w = 0 by A51, A53, A54, A55, RFINSEQ:def 1;
hence w in {0} by TARSKI:def 1; :: thesis:

end;

then rng (p9 /^ k) c= {0} by TARSKI:def 3;
hence Sum (p9 /^ k) = 0 by Lm10; :: thesis:

end;

A60: p9 | k = p9 | (Seg k) by FINSEQ_1:def 16;
then A61: len (p9 | k) = k9 by A51, FINSEQ_2:21;
not -infty in rng (F9 | k) by A47, XBOOLE_0:def 3;
then A62: Sum F9 = (Sum (F9 | k)) + (Sum (F9 /^ k)) by A13, A48, EXTREAL1:10;
Sum F9 = Sum F by A10, A11, A46, EXTREAL1:11;
then A63: Sum (F9 | k) = Sum F by A62, A35, XXREAL_3:4;
z9 = (z9 | k) ^ (z9 /^ k) by RFINSEQ:8;
then A64: Sum z9 = (Sum (z9 | k)) + (Sum (z9 /^ k)) by RLVECT_1:41;
Sum z9 = Sum z by A10, A20, RLVECT_2:7;
then A65: Sum (z9 | k) = Sum z by A64, A24;
A66: dom y = Seg n by A5, FINSEQ_1:def 3;
then A67: y is Function of (Seg n), the carrier of X by FINSEQ_2:26;
then reconsider y9 = y * s1 as FinSequence of the carrier of X by FINSEQ_2:32;
A68: y9 | k = y9 | (Seg k) by FINSEQ_1:def 16;
len y9 = n by A22, A67, FINSEQ_2:33;
then A69: len (y9 | k) = k9 by A68, FINSEQ_2:21;
A70: p9,p are_fiberwise_equipotent by RFINSEQ:4;
then p9 | k <> {} by A7, A33, A52, RFINSEQ:9, RVSUM_1:72;
then reconsider k9 = k9 as non zero Element of NAT by A61;
A71: for i being Element of NAT st i in Seg k9 holds
( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = ((p9 | k) . i) * (f . ((y9 | k) /. i)) )

proof

let i be Element of NAT ; :: thesis:
assume A72: i in Seg k9 ; :: thesis:
then A73: i in dom (p9 | k) by A61, FINSEQ_1:def 3;
then A74: (p9 | k) /. i = p9 /. i by FINSEQ_4:70;
dom (p9 | k) = (dom p9) /\ (Seg k) by A60, RELAT_1:61;
then A75: i in dom p9 by A73, XBOOLE_0:def 4;
then A76: p9 . i = p . (s . i) by FUNCT_1:12;
p9 /. i = p9 . i by A75, PARTFUN1:def 6;
then A77: (p9 | k) . i = p . (s . i) by A73, A74, A76, PARTFUN1:def 6;
A78: i in dom (y9 | k) by A69, A72, FINSEQ_1:def 3;
then A79: (y9 | k) /. i = y9 /. i by FINSEQ_4:70;
dom (y9 | k) = (dom y9) /\ (Seg k) by A68, RELAT_1:61;
then A80: i in dom y9 by A78, XBOOLE_0:def 4;
then A81: y9 . i = y . (s . i) by FUNCT_1:12;
A82: i in dom (F9 | k) by A45, A72, FINSEQ_1:def 3;
then A83: (F9 | k) /. i = F9 /. i by FINSEQ_4:70;
dom (F9 | k) = (dom F9) /\ (Seg k) by A44, RELAT_1:61;
then A84: i in dom F9 by A82, XBOOLE_0:def 4;
then A85: F9 . i = F . (s . i) by FUNCT_1:12;
F9 /. i = F9 . i by A84, PARTFUN1:def 6;
then A86: (F9 | k) . i = F . (s . i) by A82, A83, A85, PARTFUN1:def 6;
A87: i in dom (z9 | k) by A50, A72, FINSEQ_1:def 3;
then A88: (z9 | k) /. i = z9 /. i by FINSEQ_4:70;
dom (z9 | k) = (dom z9) /\ (Seg k) by A49, RELAT_1:61;
then A89: i in dom z9 by A87, XBOOLE_0:def 4;
then A90: z9 . i = z . (s . i) by FUNCT_1:12;
z9 /. i = z9 . i by A89, PARTFUN1:def 6;
then A91: (z9 | k) . i = z . (s . i) by A87, A88, A90, PARTFUN1:def 6;
A92: i in Seg n by A51, A75, FINSEQ_1:def 3;
k9 <= k by XXREAL_0:17;
then Seg k9 c= Seg k by FINSEQ_1:5;
then A93: p . (s . i) <> 0 by A9, A10, A72, A92;
y9 /. i = y9 . i by A80, PARTFUN1:def 6;
then A94: (y9 | k) /. i = y /. (s . i) by A10, A66, A79, A81, A92, FUNCT_2:5, PARTFUN1:def 6;
s . i in Seg n by A10, A92, FUNCT_2:5;
hence ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = ((p9 | k) . i) * (f . ((y9 | k) /. i)) ) by A8, A77, A94, A91, A86, A93; :: thesis:

end;

Sum (p9 | k) = 1 by A7, A33, A52, A70, RFINSEQ:9;
hence f . (Sum z) <= Sum F by A1, A2, A65, A63, A61, A69, A50, A45, A71, Th8; :: thesis:

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:

proof

assume A95: 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

proof

let n be non zero 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
A96: len p = n and
A97: len F = n and
A98: len y = n and
A99: len z = n and
A100: Sum p = 1 and
A101: 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:
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)) ) by A101;
hence f . (Sum z) <= Sum F by A95, A96, A97, A98, A99, A100; :: thesis:

end;

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

end;