let X be RealLinearSpace; 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; ( 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 )
( ( 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
;
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;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
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
verumproof
let p be
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 Mlet y,
z be
FinSequence of the
carrier of
X;
( 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 )
;
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 FINSEQ_3:112, NAT_1:14;
p | n = p | (Seg n)
by FINSEQ_1:def 15;
then
p = (p | n) ^ <*(p . (n + 1))*>
by A4, FINSEQ_3:55;
then A11:
1
= (Sum (p | n)) + (p . (n + 1))
by A7, RVSUM_1:74;
A12:
0 + n <= 1
+ n
by XREAL_1:6;
then A13:
len (p | n) = n
by A4, FINSEQ_1:59;
then A14:
dom (p | n) = Seg n
by FINSEQ_1:def 3;
A15:
Seg n c= Seg (n + 1)
by A12, FINSEQ_1:5;
A16:
for
i being
Nat st
i in dom (p | n) holds
0 <= (p | n) . i
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 FINSEQ_2:sch 1();
A21:
len (y | n) = n
by A5, A12, FINSEQ_1:59;
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;
for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds
z9 . i = (1 / (1 - (p . (n + 1)))) * vlet v be
VECTOR of
X;
( 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
;
z9 . i = (1 / (1 - (p . (n + 1)))) * v
A26:
i in Seg n
by A19, A24, FINSEQ_1:def 3;
then A27:
(y | n) /. i = y /. i
by A22, FINSEQ_4:70;
A28:
i <= n
by A26, FINSEQ_1:1;
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 A20, A24
.=
((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 A28, FINSEQ_3:112
.=
(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
;
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 A11, A14, A16, A10, RVSUM_1:85;
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 A9, VALUED_1:def 5;
then A31:
len ((1 / (1 - (p . (n + 1)))) * (p | n)) = n
by A13, FINSEQ_1:6;
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 A8, A32, XREAL_1:44;
z | n = z | (Seg n)
by FINSEQ_1:def 15;
then A35:
z = (z | n) ^ <*(z . (n + 1))*>
by A6, FINSEQ_3:55;
z . (n + 1) = (p . (n + 1)) * (y /. (n + 1))
by A8, A32;
then A36:
Sum z =
(Sum (z | n)) + (Sum <*((p . (n + 1)) * (y /. (n + 1)))*>)
by A35, RLVECT_1:41
.=
(Sum (z | n)) + ((1 - (1 - (p . (n + 1)))) * (y /. (n + 1)))
by RLVECT_1:44
;
A37:
dom z9 = Seg n
by A19, FINSEQ_1:def 3;
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;
( 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
;
( ((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 A41, FINSEQ_3:112
;
A43:
Seg n c= Seg (n + 1)
by A12, FINSEQ_1:5;
then
p . i > 0
by A8, A40;
hence
((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0
by A39, A42;
( 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 A20, A37, A40;
(y | n) /. i in M
y /. i in M
by A8, A40, A43;
hence
(y | n) /. i in M
by A22, A40, FINSEQ_4:70;
verum
end;
len (z | n) = n
by A6, A12, FINSEQ_1:59;
then A44:
(1 - (p . (n + 1))) * (Sum z9) =
(1 - (p . (n + 1))) * ((1 / (1 - (p . (n + 1)))) * (Sum (z | n)))
by A19, A23, RLVECT_1:39
.=
((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))) * (Sum (z | n))
by RLVECT_1:def 7
.=
1
* (Sum (z | n))
by A30, XCMPLX_1:106
.=
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 A11, RVSUM_1:87
.=
1
by A30, XCMPLX_1:106
;
then
Sum z9 in M
by A3, A19, A31, A21, A38;
hence
Sum z in M
by A1, A33, A34, A30, A36, A44, CONVEX1:def 2;
verum
end;
end;
A45:
S1[1]
proof
let p be
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 Mlet y,
z be
FinSequence of the
carrier of
X;
( 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 )
;
Sum z in M
reconsider p1 =
p . 1 as
Element of
REAL by XREAL_0:def 1;
p = <*p1*>
by A46, FINSEQ_1:40;
then A50:
p . 1
= 1
by A48, FINSOP_1:11;
A51:
1
in Seg 1
by FINSEQ_1:2, TARSKI:def 1;
then
z . 1
= (p . 1) * (y /. 1)
by A49;
then A52:
z . 1
= y /. 1
by A50, RLVECT_1:def 8;
A53:
z = <*(z . 1)*>
by A47, FINSEQ_1:40;
y /. 1
in M
by A49, A51;
hence
Sum z in M
by A53, A52, RLVECT_1:44;
verum
end;
thus
for
n being non
zero Nat holds
S1[
n]
from NAT_1:sch 10(A45, A2); 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 )
verumproof
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
;
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;
for r being Real st 0 < r & r < 1 & x1 in M & x2 in M holds
(r * x1) + ((1 - r) * x2) in Mlet r be
Real;
( 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
;
(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;
( 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
;
( <*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 A60, FINSEQ_1:2, TARSKI:def 2;
suppose A61:
i = 1
;
( <*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 A61, FINSEQ_1:44;
hence
(
<*r,r1*> . i > 0 &
<*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) &
<*x1,x2*> /. i in M )
by A55, A57, A61, A62, FINSEQ_1:44;
verum end; suppose A63:
i = 2
;
( <*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 A63, FINSEQ_1:44;
hence
(
<*r,r1*> . i > 0 &
<*(r * x1),((1 - r) * x2)*> . i = (<*r,r1*> . i) * (<*x1,x2*> /. i) &
<*x1,x2*> /. i in M )
by A56, A58, A63, A64, FINSEQ_1:44, XREAL_1:50;
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;
verum
end;
hence
M is
convex
by CONVEX1:def 2;
verum
end;