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
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: f . (Sum z) <= Sum F
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 ;
then reconsider s1 = s as FinSequence of Seg n by FINSEQ_2:25;
A11: dom F = Seg n by ;
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: ( 1 <= i & i <= n - k implies ( i + k in Seg n & p . (s . (i + k)) = 0 ) )
assume that
A15: 1 <= i and
A16: i <= n - k ; :: thesis: ( i + k in Seg n & p . (s . (i + k)) = 0 )
i <= i + k by INT_1:6;
then A17: 1 <= i + k by ;
0 + k < i + k by ;
then A18: not i + k in Seg k by FINSEQ_1:1;
A19: i + k <= (n - k) + k by ;
then i + k in dom p by ;
hence ( i + k in Seg n & p . (s . (i + k)) = 0 ) by ; :: thesis: verum
end;
A20: dom z = Seg n by ;
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 ;
then A22: len s1 = n by FINSEQ_1:def 3;
then A23: len z9 = n by ;
A24: Sum (z9 /^ k) = 0. X
proof
per cases ( k >= n or k < n ) ;
suppose k >= n ; :: thesis: Sum (z9 /^ k) = 0. X
then z9 /^ k = <*> the carrier of X by ;
hence Sum (z9 /^ k) = 0. X by RLVECT_1:43; :: thesis: verum
end;
suppose A25: k < n ; :: thesis: Sum (z9 /^ k) = 0. X
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 ;
let w be object ; :: thesis: ( w in rng (z9 /^ k) implies w in {(0. X)} )
assume w in rng (z9 /^ k) ; :: thesis: w in {(0. X)}
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 ;
then A28: i in Seg k1 by ;
then A29: 1 <= i by FINSEQ_1:1;
A30: i <= n - k by ;
then s . (i + k) in Seg n by ;
then z . (s . (i + k)) = (p . (s . (i + k))) * (y /. (s . (i + k))) by A8;
then A31: z . (s . (i + k)) = 0. X by ;
i + k in Seg n by ;
then i + k in dom z9 by ;
then z9 . (i + k) = 0. X by ;
then w = 0. X by ;
hence w in {(0. X)} by TARSKI:def 1; :: thesis: verum
end;
then rng (z9 /^ k) c= {(0. X)} by TARSKI:def 3;
hence Sum (z9 /^ k) = 0. X by Lm11; :: thesis: verum
end;
end;
end;
A32: p is Function of (Seg n),REAL by ;
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 ;
A35: Sum (F9 /^ k) = 0.
proof
per cases ( k >= n or k < n ) ;
suppose k >= n ; :: thesis: Sum (F9 /^ k) = 0.
hence Sum (F9 /^ k) = 0. by ; :: thesis: verum
end;
suppose A36: k < n ; :: thesis: Sum (F9 /^ k) = 0.
for w being object st w in rng (F9 /^ k) holds
w in
proof
reconsider k1 = n - k as Element of NAT by ;
let w be object ; :: thesis: ( w in rng (F9 /^ k) implies w in )
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 ;
then A39: i in Seg k1 by ;
then A40: 1 <= i by FINSEQ_1:1;
A41: i <= n - k by ;
then A42: p . (s . (i + k)) = 0 by ;
i + k in Seg n by ;
then A43: i + k in dom F9 by ;
s . (i + k) in Seg n by ;
then F . (s . (i + k)) = 0 * (f . (y /. (s . (i + k)))) by ;
then F9 . (i + k) = 0. by ;
then w = 0. by ;
hence w in by TARSKI:def 1; :: thesis: verum
end;
then rng (F9 /^ k) c= by TARSKI:def 3;
hence Sum (F9 /^ k) = 0. by Lm9; :: thesis: verum
end;
end;
end;
A44: F9 | k = F9 | (Seg k) by FINSEQ_1:def 15;
then A45: len (F9 | k) = k9 by ;
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 ;
then A48: not -infty in rng (F9 /^ k) by XBOOLE_0:def 3;
A49: z9 | k = z9 | (Seg k) by FINSEQ_1:def 15;
then A50: len (z9 | k) = k9 by ;
A51: len p9 = n by ;
A52: Sum (p9 /^ k) = 0
proof
per cases ( k >= n or k < n ) ;
suppose k >= n ; :: thesis: Sum (p9 /^ k) = 0
hence Sum (p9 /^ k) = 0 by ; :: thesis: verum
end;
suppose A53: k < n ; :: thesis: Sum (p9 /^ k) = 0
for w being object st w in rng (p9 /^ k) holds
w in
proof
reconsider k1 = n - k as Element of NAT by ;
let w be object ; :: thesis: ( w in rng (p9 /^ k) implies w in )
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 ;
then A56: i in Seg k1 by ;
then A57: 1 <= i by FINSEQ_1:1;
A58: i <= n - k by ;
then i + k in Seg n by ;
then A59: i + k in dom p9 by ;
p . (s . (i + k)) = 0 by ;
then p9 . (i + k) = 0 by ;
then w = 0 by ;
hence w in by TARSKI:def 1; :: thesis: verum
end;
then rng (p9 /^ k) c= by TARSKI:def 3;
hence Sum (p9 /^ k) = 0 by Lm10; :: thesis: verum
end;
end;
end;
A60: p9 | k = p9 | (Seg k) by FINSEQ_1:def 15;
then A61: len (p9 | k) = k9 by ;
not -infty in rng (F9 | k) by ;
then A62: Sum F9 = (Sum (F9 | k)) + (Sum (F9 /^ k)) by ;
Sum F9 = Sum F by ;
then A63: Sum (F9 | k) = Sum F by ;
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 ;
then A65: Sum (z9 | k) = Sum z by ;
A66: dom y = Seg n by ;
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 15;
len y9 = n by ;
then A69: len (y9 | k) = k9 by ;
A70: p9,p are_fiberwise_equipotent by RFINSEQ:4;
then p9 | k <> {} by ;
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: ( i in Seg k9 implies ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = ((p9 | k) . i) * (f . ((y9 | k) /. i)) ) )
assume A72: i in Seg k9 ; :: thesis: ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = ((p9 | k) . i) * (f . ((y9 | k) /. i)) )
then A73: i in dom (p9 | k) by ;
then A74: (p9 | k) /. i = p9 /. i by FINSEQ_4:70;
dom (p9 | k) = (dom p9) /\ (Seg k) by ;
then A75: i in dom p9 by ;
then A76: p9 . i = p . (s . i) by FUNCT_1:12;
p9 /. i = p9 . i by ;
then A77: (p9 | k) . i = p . (s . i) by ;
A78: i in dom (y9 | k) by ;
then A79: (y9 | k) /. i = y9 /. i by FINSEQ_4:70;
dom (y9 | k) = (dom y9) /\ (Seg k) by ;
then A80: i in dom y9 by ;
then A81: y9 . i = y . (s . i) by FUNCT_1:12;
A82: i in dom (F9 | k) by ;
then A83: (F9 | k) /. i = F9 /. i by FINSEQ_4:70;
dom (F9 | k) = (dom F9) /\ (Seg k) by ;
then A84: i in dom F9 by ;
then A85: F9 . i = F . (s . i) by FUNCT_1:12;
F9 /. i = F9 . i by ;
then A86: (F9 | k) . i = F . (s . i) by ;
A87: i in dom (z9 | k) by ;
then A88: (z9 | k) /. i = z9 /. i by FINSEQ_4:70;
dom (z9 | k) = (dom z9) /\ (Seg k) by ;
then A89: i in dom z9 by ;
then A90: z9 . i = z . (s . i) by FUNCT_1:12;
z9 /. i = z9 . i by ;
then A91: (z9 | k) . i = z . (s . i) by ;
A92: i in Seg n by ;
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 ;
then A94: (y9 | k) /. i = y /. (s . i) by ;
s . i in Seg n by ;
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: verum
end;
Sum (p9 | k) = 1 by ;
hence f . (Sum z) <= Sum F by A1, A2, A65, A63, A61, A69, A50, A45, A71, Th8; :: thesis: verum
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 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: f is convex
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: 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
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: f . (Sum z) <= Sum F
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: verum
end;
hence f is convex by ; :: thesis: verum
end;