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 )

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

( 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

thus
( ( for n being non zero Element of NAT
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 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 )

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

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.

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 15;

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

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 15;

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

hence f . (Sum z) <= Sum F by A1, A2, A65, A63, A61, A69, A50, A45, A71, Th8; :: thesis: verum

end;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 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

A20:
dom z = Seg n
by A6, FINSEQ_1:def 3;
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 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: verum

end;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 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: verum

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
end;

A32:
p is Function of (Seg n),REAL
by A10, FINSEQ_2:26;per cases
( k >= n or k < n )
;

end;

suppose
k >= n
; :: thesis: Sum (z9 /^ k) = 0. X

then
z9 /^ k = <*> the carrier of X
by A23, FINSEQ_5:32;

hence Sum (z9 /^ k) = 0. X by RLVECT_1:43; :: thesis: verum

end;hence Sum (z9 /^ k) = 0. X by RLVECT_1:43; :: thesis: verum

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)}

hence Sum (z9 /^ k) = 0. X by Lm11; :: thesis: verum

end;w in {(0. X)}

proof

then
rng (z9 /^ k) c= {(0. X)}
by TARSKI:def 3;
reconsider k1 = n - k as Element of NAT by A25, INT_1:5;

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

end;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 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: verum

hence Sum (z9 /^ k) = 0. X by Lm11; :: thesis: verum

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
end;

A44:
F9 | k = F9 | (Seg k)
by FINSEQ_1:def 15;per cases
( k >= n or k < n )
;

end;

suppose A36:
k < n
; :: thesis: Sum (F9 /^ k) = 0.

for w being object st w in rng (F9 /^ k) holds

w in {0.}

hence Sum (F9 /^ k) = 0. by Lm9; :: thesis: verum

end;w in {0.}

proof

then
rng (F9 /^ k) c= {0.}
by TARSKI:def 3;
reconsider k1 = n - k as Element of NAT by A36, INT_1:5;

let w be object ; :: thesis: ( w in rng (F9 /^ k) implies w in {0.} )

assume w in rng (F9 /^ k) ; :: thesis: w in {0.}

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

end;let w be object ; :: thesis: ( w in rng (F9 /^ k) implies w in {0.} )

assume w in rng (F9 /^ k) ; :: thesis: w in {0.}

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

hence Sum (F9 /^ k) = 0. by Lm9; :: thesis: verum

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 15;

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
end;

A60:
p9 | k = p9 | (Seg k)
by FINSEQ_1:def 15;per cases
( k >= n or k < n )
;

end;

suppose A53:
k < n
; :: thesis: Sum (p9 /^ k) = 0

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

w in {0}

hence Sum (p9 /^ k) = 0 by Lm10; :: thesis: verum

end;w in {0}

proof

then
rng (p9 /^ k) c= {0}
by TARSKI:def 3;
reconsider k1 = n - k as Element of NAT by A53, INT_1:5;

let w be object ; :: thesis: ( w in rng (p9 /^ k) implies w in {0} )

assume w in rng (p9 /^ k) ; :: thesis: w in {0}

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

end;let w be object ; :: thesis: ( w in rng (p9 /^ k) implies w in {0} )

assume w in rng (p9 /^ k) ; :: thesis: w in {0}

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

hence Sum (p9 /^ k) = 0 by Lm10; :: thesis: verum

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 15;

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

Sum (p9 | k) = 1
by A7, A33, A52, A70, RFINSEQ:9;
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 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: verum

end;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 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: verum

hence f . (Sum z) <= Sum F by A1, A2, A65, A63, A61, A69, A50, A45, A71, Th8; :: thesis: verum

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

end;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

hence
f is convex
by A1, Th8; :: thesis: verum
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;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