let V be RealLinearSpace; for M being convex Subset of V
for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let M be convex Subset of V; for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let N be Subset of V; for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M
let L be Linear_Combination of N; ( L is convex & N c= M implies Sum L in M )
assume that
A1:
L is convex
and
A2:
N c= M
; Sum L in M
consider F being FinSequence of the carrier of V such that
A3:
F is one-to-one
and
A4:
rng F = Carrier L
and
A5:
ex f being FinSequence of REAL st
( len f = len F & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 ) ) )
by A1, CONVEX1:def 3;
consider f being FinSequence of REAL such that
A6:
len f = len F
and
A7:
Sum f = 1
and
A8:
for n being Nat st n in dom f holds
( f . n = L . (F . n) & f . n >= 0 )
by A5;
not Carrier L, {} are_equipotent
by A1, CARD_1:46, CONVEX1:21;
then A9:
card (Carrier L) <> card {}
by CARD_1:21;
then reconsider i = len F as non empty Element of NAT by A3, A4, FINSEQ_4:77;
A10:
len (L (#) F) = len F
by RLVECT_2:def 9;
defpred S1[ Nat] means (1 / (Sum (mid f,1,$1))) * (Sum (mid (L (#) F),1,$1)) in M;
A11:
len (L (#) F) = len F
by RLVECT_2:def 9;
A12:
for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non
empty Nat;
( S1[k] implies S1[k + 1] )
A13:
k >= 1
by NAT_1:14;
assume A14:
(1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k)) in M
;
S1[k + 1]
now per cases
( k >= len f or k < len f )
;
suppose A15:
k >= len f
;
S1[k + 1]A16:
mid (L (#) F),1,
(k + 1) =
(L (#) F) | (k + 1)
by FINSEQ_6:122, NAT_1:12
.=
L (#) F
by A6, A11, A15, FINSEQ_1:79, NAT_1:12
;
A17:
mid f,1,
k =
f | k
by FINSEQ_6:122, NAT_1:14
.=
f
by A15, FINSEQ_1:79
;
A18:
mid f,1,
(k + 1) =
f | (k + 1)
by FINSEQ_6:122, NAT_1:12
.=
f
by A15, FINSEQ_1:79, NAT_1:12
;
mid (L (#) F),1,
k =
(L (#) F) | k
by FINSEQ_6:122, NAT_1:14
.=
L (#) F
by A6, A11, A15, FINSEQ_1:79
;
hence
S1[
k + 1]
by A14, A17, A18, A16;
verum end; suppose A19:
k < len f
;
S1[k + 1]
mid f,1,
k = f | k
by FINSEQ_6:122, NAT_1:14;
then A20:
len (mid f,1,k) = k
by A19, FINSEQ_1:80;
A21:
ex
i being
Element of
NAT st
(
i in dom (mid f,1,k) &
0 < (mid f,1,k) . i )
proof
take
1
;
( 1 in dom (mid f,1,k) & 0 < (mid f,1,k) . 1 )
1
<= len f
by A19, NAT_1:14;
then A22:
1
in Seg (len f)
;
then
1
in dom f
by FINSEQ_1:def 3;
then A23:
(
f . 1
= L . (F . 1) &
f . 1
>= 0 )
by A8;
1
in dom F
by A6, A22, FINSEQ_1:def 3;
then
F . 1
in Carrier L
by A4, FUNCT_1:def 5;
then
F . 1
in { v where v is Element of V : L . v <> 0 }
by RLVECT_2:def 6;
then A24:
ex
v being
Element of
V st
(
v = F . 1 &
L . v <> 0 )
;
1
in Seg (len (mid f,1,k))
by A13, A20;
hence
( 1
in dom (mid f,1,k) &
0 < (mid f,1,k) . 1 )
by A13, A19, A23, A24, FINSEQ_1:def 3, FINSEQ_6:129;
verum
end; A25:
for
i being
Nat st
i in dom <*((mid f,1,(k + 1)) . (k + 1))*> holds
(mid f,1,(k + 1)) . ((len (mid f,1,k)) + i) = <*((mid f,1,(k + 1)) . (k + 1))*> . i
proof
let i be
Nat;
( i in dom <*((mid f,1,(k + 1)) . (k + 1))*> implies (mid f,1,(k + 1)) . ((len (mid f,1,k)) + i) = <*((mid f,1,(k + 1)) . (k + 1))*> . i )
assume
i in dom <*((mid f,1,(k + 1)) . (k + 1))*>
;
(mid f,1,(k + 1)) . ((len (mid f,1,k)) + i) = <*((mid f,1,(k + 1)) . (k + 1))*> . i
then
i in Seg 1
by FINSEQ_1:55;
then
i = 1
by FINSEQ_1:4, TARSKI:def 1;
hence
(mid f,1,(k + 1)) . ((len (mid f,1,k)) + i) = <*((mid f,1,(k + 1)) . (k + 1))*> . i
by A20, FINSEQ_1:57;
verum
end; A26:
mid f,1,
(k + 1) = f | (k + 1)
by FINSEQ_6:122, NAT_1:14;
set r1 =
Sum (mid f,1,k);
for
i being
Nat st
i in dom (mid f,1,k) holds
0 <= (mid f,1,k) . i
proof
let i be
Nat;
( i in dom (mid f,1,k) implies 0 <= (mid f,1,k) . i )
assume
i in dom (mid f,1,k)
;
0 <= (mid f,1,k) . i
then A27:
i in Seg k
by A20, FINSEQ_1:def 3;
then A28:
1
<= i
by FINSEQ_1:3;
A29:
i <= k
by A27, FINSEQ_1:3;
then
i <= len f
by A19, XXREAL_0:2;
then A30:
i in dom f
by A28, FINSEQ_3:27;
(mid f,1,k) . i = f . i
by A19, A28, A29, FINSEQ_6:129;
hence
0 <= (mid f,1,k) . i
by A8, A30;
verum
end; then A31:
Sum (mid f,1,k) > 0
by A21, RVSUM_1:115;
A32:
k + 1
<= len f
by A19, NAT_1:13;
then A33:
len (f | (k + 1)) = k + 1
by FINSEQ_1:80;
A34:
for
i being
Nat st
i in dom (mid f,1,k) holds
(mid f,1,(k + 1)) . i = (mid f,1,k) . i
proof
let i be
Nat;
( i in dom (mid f,1,k) implies (mid f,1,(k + 1)) . i = (mid f,1,k) . i )
A35:
mid f,1,
k = f | k
by FINSEQ_6:122, NAT_1:14;
assume A36:
i in dom (mid f,1,k)
;
(mid f,1,(k + 1)) . i = (mid f,1,k) . i
then A37:
i in Seg (len (f | k))
by A35, FINSEQ_1:def 3;
len (f | k) = k
by A19, FINSEQ_1:80;
then
i <= k
by A37, FINSEQ_1:3;
then A38:
i <= k + 1
by NAT_1:12;
(f | k) . i = (f | k) /. i
by A36, A35, PARTFUN1:def 8;
then A39:
(mid f,1,k) . i = f /. i
by A36, A35, FINSEQ_4:85;
(
i in NAT & 1
<= i )
by A37, FINSEQ_1:3;
then
i in Seg (k + 1)
by A38;
then A40:
i in dom (f | (k + 1))
by A33, FINSEQ_1:def 3;
then
(f | (k + 1)) . i = (f | (k + 1)) /. i
by PARTFUN1:def 8;
hence
(mid f,1,(k + 1)) . i = (mid f,1,k) . i
by A26, A39, A40, FINSEQ_4:85;
verum
end; A41:
k + 1
>= 1
by NAT_1:14;
then A42:
k + 1
in Seg (len f)
by A32;
then A43:
k + 1
in dom f
by FINSEQ_1:def 3;
A44:
k + 1
in dom F
by A6, A42, FINSEQ_1:def 3;
k + 1
in Seg (k + 1)
by A41;
then A45:
k + 1
in dom (f | (k + 1))
by A33, FINSEQ_1:def 3;
then
(f | (k + 1)) /. (k + 1) = f /. (k + 1)
by FINSEQ_4:85;
then
(mid f,1,(k + 1)) . (k + 1) = f /. (k + 1)
by A26, A45, PARTFUN1:def 8;
then (mid f,1,(k + 1)) . (k + 1) =
f . (k + 1)
by A43, PARTFUN1:def 8
.=
L . (F . (k + 1))
by A8, A43
;
then A46:
(mid f,1,(k + 1)) . (k + 1) = L . (F /. (k + 1))
by A44, PARTFUN1:def 8;
mid f,1,
(k + 1) = f | (k + 1)
by FINSEQ_6:122, NAT_1:14;
then
(
len <*((mid f,1,(k + 1)) . (k + 1))*> = 1 &
len (mid f,1,(k + 1)) = k + 1 )
by A32, FINSEQ_1:57, FINSEQ_1:80;
then
dom (mid f,1,(k + 1)) = Seg ((len (mid f,1,k)) + (len <*((mid f,1,(k + 1)) . (k + 1))*>))
by A20, FINSEQ_1:def 3;
then
mid f,1,
(k + 1) = (mid f,1,k) ^ <*((mid f,1,(k + 1)) . (k + 1))*>
by A34, A25, FINSEQ_1:def 7;
then A47:
Sum (mid f,1,(k + 1)) = (Sum (mid f,1,k)) + (L . (F /. (k + 1)))
by A46, RVSUM_1:104;
A48:
mid (L (#) F),1,
(k + 1) = (L (#) F) | (k + 1)
by FINSEQ_6:122, NAT_1:14;
set w2 =
F /. (k + 1);
set w1 =
Sum (mid (L (#) F),1,k);
set r2 =
L . (F /. (k + 1));
A49:
(1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)) = (Sum (mid f,1,k)) / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))
by XCMPLX_1:100;
A50:
(
F /. (k + 1) in M &
L . (F /. (k + 1)) > 0 )
proof
k + 1
in Seg (len f)
by A41, A32;
then
k + 1
in dom f
by FINSEQ_1:def 3;
then A51:
(
f . (k + 1) = L . (F . (k + 1)) &
f . (k + 1) >= 0 )
by A8;
k + 1
in Seg (len F)
by A6, A41, A32;
then A52:
k + 1
in dom F
by FINSEQ_1:def 3;
then
F /. (k + 1) = F . (k + 1)
by PARTFUN1:def 8;
then A53:
F /. (k + 1) in Carrier L
by A4, A52, FUNCT_1:def 5;
Carrier L c= N
by RLVECT_2:def 8;
hence
F /. (k + 1) in M
by A2, A53, TARSKI:def 3;
L . (F /. (k + 1)) > 0
F /. (k + 1) in { v where v is Element of V : L . v <> 0 }
by A53, RLVECT_2:def 6;
then
ex
v being
Element of
V st
(
v = F /. (k + 1) &
L . v <> 0 )
;
hence
L . (F /. (k + 1)) > 0
by A52, A51, PARTFUN1:def 8;
verum
end; then
(Sum (mid f,1,k)) + (L . (F /. (k + 1))) > Sum (mid f,1,k)
by XREAL_1:31;
then A54:
(1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)) < 1
by A31, A49, XREAL_1:191;
A55:
(Sum (mid f,1,k)) + (L . (F /. (k + 1))) > 0 + 0
by A31, A50, XREAL_1:10;
then
1
/ ((Sum (mid f,1,k)) + (L . (F /. (k + 1)))) > 0
by XREAL_1:141;
then A56:
0 < (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))
by A31, XREAL_1:131;
k + 1
<= len (L (#) F)
by A6, A32, RLVECT_2:def 9;
then A57:
k + 1
in dom (L (#) F)
by A41, FINSEQ_3:27;
A58:
k < len (L (#) F)
by A6, A19, RLVECT_2:def 9;
then A59:
k + 1
<= len (L (#) F)
by NAT_1:13;
then A60:
len ((L (#) F) | (k + 1)) = k + 1
by FINSEQ_1:80;
A61:
for
i being
Nat st
i in dom (mid (L (#) F),1,k) holds
(mid (L (#) F),1,(k + 1)) . i = (mid (L (#) F),1,k) . i
proof
let i be
Nat;
( i in dom (mid (L (#) F),1,k) implies (mid (L (#) F),1,(k + 1)) . i = (mid (L (#) F),1,k) . i )
A62:
mid (L (#) F),1,
k = (L (#) F) | k
by FINSEQ_6:122, NAT_1:14;
assume A63:
i in dom (mid (L (#) F),1,k)
;
(mid (L (#) F),1,(k + 1)) . i = (mid (L (#) F),1,k) . i
then A64:
i in Seg (len ((L (#) F) | k))
by A62, FINSEQ_1:def 3;
len ((L (#) F) | k) = k
by A58, FINSEQ_1:80;
then
i <= k
by A64, FINSEQ_1:3;
then A65:
i <= k + 1
by NAT_1:12;
((L (#) F) | k) . i = ((L (#) F) | k) /. i
by A63, A62, PARTFUN1:def 8;
then A66:
(mid (L (#) F),1,k) . i = (L (#) F) /. i
by A63, A62, FINSEQ_4:85;
(
i in NAT & 1
<= i )
by A64, FINSEQ_1:3;
then
i in Seg (k + 1)
by A65;
then A67:
i in dom ((L (#) F) | (k + 1))
by A60, FINSEQ_1:def 3;
then
((L (#) F) | (k + 1)) . i = ((L (#) F) | (k + 1)) /. i
by PARTFUN1:def 8;
hence
(mid (L (#) F),1,(k + 1)) . i = (mid (L (#) F),1,k) . i
by A48, A66, A67, FINSEQ_4:85;
verum
end;
k + 1
in Seg (k + 1)
by A41;
then A68:
k + 1
in dom ((L (#) F) | (k + 1))
by A60, FINSEQ_1:def 3;
then
((L (#) F) | (k + 1)) /. (k + 1) = (L (#) F) /. (k + 1)
by FINSEQ_4:85;
then
(mid (L (#) F),1,(k + 1)) . (k + 1) = (L (#) F) /. (k + 1)
by A48, A68, PARTFUN1:def 8;
then A69:
(mid (L (#) F),1,(k + 1)) . (k + 1) =
(L (#) F) . (k + 1)
by A57, PARTFUN1:def 8
.=
(L . (F /. (k + 1))) * (F /. (k + 1))
by A57, RLVECT_2:def 9
;
mid (L (#) F),1,
k = (L (#) F) | k
by FINSEQ_6:122, NAT_1:14;
then A70:
len (mid (L (#) F),1,k) = k
by A58, FINSEQ_1:80;
A71:
for
i being
Nat st
i in dom <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> holds
(mid (L (#) F),1,(k + 1)) . ((len (mid (L (#) F),1,k)) + i) = <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> . i
proof
let i be
Nat;
( i in dom <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> implies (mid (L (#) F),1,(k + 1)) . ((len (mid (L (#) F),1,k)) + i) = <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> . i )
assume
i in dom <*((mid (L (#) F),1,(k + 1)) . (k + 1))*>
;
(mid (L (#) F),1,(k + 1)) . ((len (mid (L (#) F),1,k)) + i) = <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> . i
then
i in Seg 1
by FINSEQ_1:55;
then
i = 1
by FINSEQ_1:4, TARSKI:def 1;
hence
(mid (L (#) F),1,(k + 1)) . ((len (mid (L (#) F),1,k)) + i) = <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> . i
by A70, FINSEQ_1:57;
verum
end;
(
len <*((mid (L (#) F),1,(k + 1)) . (k + 1))*> = 1 &
len (mid (L (#) F),1,(k + 1)) = k + 1 )
by A59, A48, FINSEQ_1:57, FINSEQ_1:80;
then
dom (mid (L (#) F),1,(k + 1)) = Seg ((len (mid (L (#) F),1,k)) + (len <*((mid (L (#) F),1,(k + 1)) . (k + 1))*>))
by A70, FINSEQ_1:def 3;
then
mid (L (#) F),1,
(k + 1) = (mid (L (#) F),1,k) ^ <*((mid (L (#) F),1,(k + 1)) . (k + 1))*>
by A61, A71, FINSEQ_1:def 7;
then A72:
(1 / (Sum (mid f,1,(k + 1)))) * (Sum (mid (L (#) F),1,(k + 1))) =
(1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((Sum (mid (L (#) F),1,k)) + ((L . (F /. (k + 1))) * (F /. (k + 1))))
by A47, A69, FVSUM_1:87
.=
(1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((1 * (Sum (mid (L (#) F),1,k))) + ((L . (F /. (k + 1))) * (F /. (k + 1))))
by RLVECT_1:def 11
.=
(1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((((Sum (mid f,1,k)) * (1 / (Sum (mid f,1,k)))) * (Sum (mid (L (#) F),1,k))) + ((L . (F /. (k + 1))) * (F /. (k + 1))))
by A31, XCMPLX_1:107
.=
(1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (((Sum (mid f,1,k)) * ((1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k)))) + ((L . (F /. (k + 1))) * (F /. (k + 1))))
by RLVECT_1:def 10
.=
((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((Sum (mid f,1,k)) * ((1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k))))) + ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1))))
by RLVECT_1:def 8
.=
(((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))) * ((1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k)))) + ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * ((L . (F /. (k + 1))) * (F /. (k + 1))))
by RLVECT_1:def 10
.=
(((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))) * ((1 / (Sum (mid f,1,k))) * (Sum (mid (L (#) F),1,k)))) + (((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (L . (F /. (k + 1)))) * (F /. (k + 1)))
by RLVECT_1:def 10
;
1
- ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k))) =
(((Sum (mid f,1,k)) + (L . (F /. (k + 1)))) * (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1)))))) - ((1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1))))) * (Sum (mid f,1,k)))
by A55, XCMPLX_1:107
.=
(((Sum (mid f,1,k)) + (L . (F /. (k + 1)))) - (Sum (mid f,1,k))) * (1 / ((Sum (mid f,1,k)) + (L . (F /. (k + 1)))))
;
hence
S1[
k + 1]
by A14, A50, A56, A54, A72, CONVEX1:def 2;
verum end;
hence
S1[
k + 1]
;
verum
end;
len F > 0
by A3, A4, A9, CARD_1:47, FINSEQ_4:77;
then A73:
len F >= 0 + 1
by NAT_1:13;
A74:
S1[1]
proof
mid f,1,1
= f | 1
by FINSEQ_6:122;
then A75:
len (mid f,1,1) = 1
by A6, A73, FINSEQ_1:80;
then
1
in dom (mid f,1,1)
by FINSEQ_3:27;
then reconsider m =
(mid f,1,1) . 1 as
Element of
REAL by PARTFUN1:27;
mid f,1,1
= <*((mid f,1,1) . 1)*>
by A75, FINSEQ_1:57;
then A76:
Sum (mid f,1,1) = m
by FINSOP_1:12;
Carrier L c= N
by RLVECT_2:def 8;
then A77:
Carrier L c= M
by A2, XBOOLE_1:1;
mid (L (#) F),1,1
= (L (#) F) | 1
by FINSEQ_6:122;
then
len (mid (L (#) F),1,1) = 1
by A73, A11, FINSEQ_1:80;
then A78:
mid (L (#) F),1,1
= <*((mid (L (#) F),1,1) . 1)*>
by FINSEQ_1:57;
A79:
1
in Seg (len (L (#) F))
by A73, A11;
then A80:
1
in dom F
by A11, FINSEQ_1:def 3;
then A81:
F /. 1
= F . 1
by PARTFUN1:def 8;
A82:
1
in dom (L (#) F)
by A79, FINSEQ_1:def 3;
A83:
F . 1
in rng F
by A80, FUNCT_1:def 5;
then
F . 1
in { v where v is Element of V : L . v <> 0 }
by A4, RLVECT_2:def 6;
then A84:
ex
v2 being
Element of
V st
(
F . 1
= v2 &
L . v2 <> 0 )
;
1
in dom f
by A6, A11, A79, FINSEQ_1:def 3;
then f . 1 =
L . (F . 1)
by A8
.=
L . (F /. 1)
by A80, PARTFUN1:def 8
;
then A85:
Sum (mid f,1,1) = L . (F /. 1)
by A6, A73, A76, FINSEQ_6:129;
(mid (L (#) F),1,1) . 1 =
(L (#) F) . 1
by A73, A11, FINSEQ_6:129
.=
(L . (F /. 1)) * (F /. 1)
by A82, RLVECT_2:def 9
;
then (1 / (Sum (mid f,1,1))) * (Sum (mid (L (#) F),1,1)) =
(1 / (Sum (mid f,1,1))) * ((L . (F /. 1)) * (F /. 1))
by A78, RLVECT_1:61
.=
((1 / (Sum (mid f,1,1))) * (L . (F /. 1))) * (F /. 1)
by RLVECT_1:def 10
.=
1
* (F /. 1)
by A81, A85, A84, XCMPLX_1:107
.=
F /. 1
by RLVECT_1:def 11
;
hence
S1[1]
by A4, A81, A83, A77;
verum
end;
for k being non empty Nat holds S1[k]
from NAT_1:sch 10(A74, A12);
then A86:
(1 / (Sum (mid f,1,i))) * (Sum (mid (L (#) F),1,i)) in M
;
Sum (mid f,1,(len f)) = 1
by A6, A7, A73, FINSEQ_6:126;
then (1 / (Sum (mid f,1,(len f)))) * (Sum (mid (L (#) F),1,(len (L (#) F)))) =
Sum (mid (L (#) F),1,(len (L (#) F)))
by RLVECT_1:def 11
.=
Sum (L (#) F)
by A73, A10, FINSEQ_6:126
;
hence
Sum L in M
by A3, A4, A6, A86, A10, RLVECT_2:def 10; verum