let X be RealLinearSpace; :: thesis: for M being Subset of X holds
( M is convex iff for n being non zero Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M )

let M be Subset of X; :: thesis: ( M is convex iff for n being non zero Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M )

thus ( M is convex implies for n being non zero Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M ) :: thesis: ( ( for n being non zero Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M ) implies M is convex )
proof
defpred S1[ Nat] means for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = \$1 & len y = \$1 & len z = \$1 & Sum p = 1 & ( for i being Nat st i in Seg \$1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M;
assume A1: M is convex ; :: thesis: for n being non zero Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M

A2: for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
thus for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M :: thesis: verum
proof
let p be FinSequence of REAL ; :: thesis: for y, z being FinSequence of the carrier of X st len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M

let y, z be FinSequence of the carrier of X; :: thesis: ( len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) implies Sum z in M )

assume that
A4: len p = n + 1 and
A5: len y = n + 1 and
A6: len z = n + 1 and
A7: Sum p = 1 and
A8: for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; :: thesis: Sum z in M
set q = 1 - (p . (n + 1));
A9: dom (p | n) = Seg (len (p | n)) by FINSEQ_1:def 3;
1 <= n + 1 by NAT_1:14;
then 1 in Seg (n + 1) by FINSEQ_1:1;
then p . 1 > 0 by A8;
then A10: (p | n) . 1 > 0 by ;
p | n = p | (Seg n) by FINSEQ_1:def 15;
then p = (p | n) ^ <*(p . (n + 1))*> by ;
then A11: 1 = (Sum (p | n)) + (p . (n + 1)) by ;
A12: 0 + n <= 1 + n by XREAL_1:6;
then A13: len (p | n) = n by ;
then A14: dom (p | n) = Seg n by FINSEQ_1:def 3;
A15: Seg n c= Seg (n + 1) by ;
A16: for i being Nat st i in dom (p | n) holds
0 <= (p | n) . i
proof
let i be Nat; :: thesis: ( i in dom (p | n) implies 0 <= (p | n) . i )
assume A17: i in dom (p | n) ; :: thesis: 0 <= (p | n) . i
then A18: i <= n by ;
p . i > 0 by A8, A14, A15, A17;
hence 0 <= (p | n) . i by ; :: thesis: verum
end;
set y9 = y | n;
set p9 = (1 / (1 - (p . (n + 1)))) * (p | n);
deffunc H1( Nat) -> Element of the carrier of X = (((1 / (1 - (p . (n + 1)))) * (p | n)) . \$1) * ((y | n) /. \$1);
consider z9 being FinSequence of the carrier of X such that
A19: len z9 = n and
A20: for i being Nat st i in dom z9 holds
z9 . i = H1(i) from A21: len (y | n) = n by ;
then A22: dom (y | n) = Seg n by FINSEQ_1:def 3;
A23: for i being Nat
for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds
z9 . i = (1 / (1 - (p . (n + 1)))) * v
proof
let i be Nat; :: thesis: for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds
z9 . i = (1 / (1 - (p . (n + 1)))) * v

let v be VECTOR of X; :: thesis: ( i in dom z9 & v = (z | n) . i implies z9 . i = (1 / (1 - (p . (n + 1)))) * v )
assume that
A24: i in dom z9 and
A25: v = (z | n) . i ; :: thesis: z9 . i = (1 / (1 - (p . (n + 1)))) * v
A26: i in Seg n by ;
then A27: (y | n) /. i = y /. i by ;
A28: i <= n by ;
then A29: (z | n) . i = z . i by FINSEQ_3:112;
z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by
.= ((1 / (1 - (p . (n + 1)))) * ((p | n) . i)) * ((y | n) /. i) by RVSUM_1:44
.= ((1 / (1 - (p . (n + 1)))) * (p . i)) * ((y | n) /. i) by
.= (1 / (1 - (p . (n + 1)))) * ((p . i) * ((y | n) /. i)) by RLVECT_1:def 7
.= (1 / (1 - (p . (n + 1)))) * v by A8, A15, A25, A26, A29, A27 ;
hence z9 . i = (1 / (1 - (p . (n + 1)))) * v ; :: thesis: verum
end;
1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then A30: 1 - (p . (n + 1)) > 0 by ;
dom ((1 / (1 - (p . (n + 1)))) * (p | n)) = Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) by FINSEQ_1:def 3;
then Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) = Seg (len (p | n)) by ;
then A31: len ((1 / (1 - (p . (n + 1)))) * (p | n)) = n by ;
A32: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A33: y /. (n + 1) in M by A8;
A34: 1 - (p . (n + 1)) < 1 by ;
z | n = z | (Seg n) by FINSEQ_1:def 15;
then A35: z = (z | n) ^ <*(z . (n + 1))*> by ;
z . (n + 1) = (p . (n + 1)) * (y /. (n + 1)) by ;
then A36: Sum z = (Sum (z | n)) + (Sum <*((p . (n + 1)) * (y /. (n + 1)))*>) by
.= (Sum (z | n)) + ((1 - (1 - (p . (n + 1)))) * (y /. (n + 1))) by RLVECT_1:44 ;
A37: dom z9 = Seg n by ;
A38: for i being Nat st i in Seg n holds
( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )
proof
(1 - (p . (n + 1))) " > 0 by A30;
then A39: 1 / (1 - (p . (n + 1))) > 0 by XCMPLX_1:215;
let i be Nat; :: thesis: ( i in Seg n implies ( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M ) )
assume A40: i in Seg n ; :: thesis: ( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )
then A41: i <= n by FINSEQ_1:1;
A42: ((1 / (1 - (p . (n + 1)))) * (p | n)) . i = (1 / (1 - (p . (n + 1)))) * ((p | n) . i) by RVSUM_1:44
.= (1 / (1 - (p . (n + 1)))) * (p . i) by ;
A43: Seg n c= Seg (n + 1) by ;
then p . i > 0 by ;
hence ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 by ; :: thesis: ( z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )
thus z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by ; :: thesis: (y | n) /. i in M
y /. i in M by A8, A40, A43;
hence (y | n) /. i in M by ; :: thesis: verum
end;
len (z | n) = n by ;
then A44: (1 - (p . (n + 1))) * (Sum z9) = (1 - (p . (n + 1))) * ((1 / (1 - (p . (n + 1)))) * (Sum (z | n))) by
.= ((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))) * (Sum (z | n)) by RLVECT_1:def 7
.= 1 * (Sum (z | n)) by
.= Sum (z | n) by RLVECT_1:def 8 ;
Sum ((1 / (1 - (p . (n + 1)))) * (p | n)) = (1 / (1 - (p . (n + 1)))) * (1 - (p . (n + 1))) by
.= 1 by ;
then Sum z9 in M by A3, A19, A31, A21, A38;
hence Sum z in M by ; :: thesis: verum
end;
end;
A45: S1[1]
proof
let p be FinSequence of REAL ; :: thesis: for y, z being FinSequence of the carrier of X st len p = 1 & len y = 1 & len z = 1 & Sum p = 1 & ( for i being Nat st i in Seg 1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M

let y, z be FinSequence of the carrier of X; :: thesis: ( len p = 1 & len y = 1 & len z = 1 & Sum p = 1 & ( for i being Nat st i in Seg 1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) implies Sum z in M )

assume that
A46: len p = 1 and
len y = 1 and
A47: len z = 1 and
A48: Sum p = 1 and
A49: for i being Nat st i in Seg 1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; :: thesis: Sum z in M
reconsider p1 = p . 1 as Element of REAL by XREAL_0:def 1;
p = <*p1*> by ;
then A50: p . 1 = 1 by ;
A51: 1 in Seg 1 by ;
then z . 1 = (p . 1) * (y /. 1) by A49;
then A52: z . 1 = y /. 1 by ;
A53: z = <*(z . 1)*> by ;
y /. 1 in M by ;
hence Sum z in M by ; :: thesis: verum
end;
thus for n being non zero Nat holds S1[n] from :: thesis: verum
end;
thus ( ( for n being non zero Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M ) implies M is convex ) :: thesis: verum
proof
assume A54: for n being non zero Nat
for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M ; :: thesis: M is convex
for x1, x2 being VECTOR of X
for r being Real st 0 < r & r < 1 & x1 in M & x2 in M holds
(r * x1) + ((1 - r) * x2) in M
proof
let x1, x2 be VECTOR of X; :: thesis: for r being Real st 0 < r & r < 1 & x1 in M & x2 in M holds
(r * x1) + ((1 - r) * x2) in M

let r be Real; :: thesis: ( 0 < r & r < 1 & x1 in M & x2 in M implies (r * x1) + ((1 - r) * x2) in M )
assume that
A55: 0 < r and
A56: r < 1 and
A57: x1 in M and
A58: x2 in M ; :: thesis: (r * x1) + ((1 - r) * x2) in M
set z = <*(r * x1),((1 - r) * x2)*>;
set y = <*x1,x2*>;
reconsider r = r as Element of REAL by XREAL_0:def 1;
reconsider r1 = 1 - r as Element of REAL by XREAL_0:def 1;
set p = <*r,r1*>;
A59: for i being Nat st i in Seg 2 holds
( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )
proof
let i be Nat; :: thesis: ( i in Seg 2 implies ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) )
assume A60: i in Seg 2 ; :: thesis: ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )
per cases ( i = 1 or i = 2 ) by ;
suppose A61: i = 1 ; :: thesis: ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )
then A62: <*x1,x2*> /. i = x1 by FINSEQ_4:17;
<*r,r1*> . i = r by ;
hence ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by ; :: thesis: verum
end;
suppose A63: i = 2 ; :: thesis: ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )
then A64: <*x1,x2*> /. i = x2 by FINSEQ_4:17;
<*r,r1*> . i = 1 - r by ;
hence ( <*r,r1*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by ; :: thesis: verum
end;
end;
end;
A65: len <*x1,x2*> = 2 by FINSEQ_1:44;
A66: Sum <*r,r1*> = r + (1 - r) by RVSUM_1:77
.= 1 ;
A67: len <*(r * x1),((1 - r) * x2)*> = 2 by FINSEQ_1:44;
len <*r,r1*> = 2 by FINSEQ_1:44;
then Sum <*(r * x1),((1 - r) * x2)*> in M by A54, A65, A67, A66, A59;
hence (r * x1) + ((1 - r) * x2) in M by RLVECT_1:45; :: thesis: verum
end;
hence M is convex by CONVEX1:def 2; :: thesis: verum
end;