Copyright (c) 2003 Association of Mizar Users
environ
vocabulary RLVECT_1, FUNCT_1, PROB_2, ARYTM_1, RELAT_1, BHSP_1, FINSEQ_1,
BOOLE, JORDAN1, SETFAM_1, CONNSP_3, ARYTM_3, RLSUB_1, CONVEX1, FINSEQ_4,
SEQ_1, CARD_1, RLVECT_2, JORDAN3, TARSKI, FUNCT_2, RFINSEQ, FINSET_1,
CONVEX2;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
FINSEQ_1, RELAT_1, FUNCT_1, FINSET_1, CARD_1, NAT_1, SETFAM_1, STRUCT_0,
FUNCT_2, RLVECT_1, RLSUB_1, RLSUB_2, FINSEQ_4, RLVECT_2, RVSUM_1, BHSP_1,
RUSUB_4, CONVEX1, TOPREAL1, JORDAN3, RFINSEQ;
constructors REAL_1, SEQ_1, RUSUB_5, FINSEQ_4, CONVEX1, JORDAN3, NAT_1,
MONOID_0, WELLORD2, TOPREAL1, MATRIX_2, RFINSEQ, RLSUB_2, MEMBERED;
clusters RELSET_1, FINSEQ_1, ARYTM_3, STRUCT_0, RLVECT_1, SEQ_1, RUSUB_4,
CONVEX1, BINARITH, XREAL_0, MEMBERED;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, CONVEX1;
theorems BHSP_1, RLVECT_1, RVSUM_1, FUNCT_1, FINSEQ_1, TARSKI, ZFMISC_1,
REAL_1, XBOOLE_0, REAL_2, SETFAM_1, AXIOMS, RLSUB_1, RUSUB_4, XBOOLE_1,
RLVECT_2, CARD_1, FINSEQ_3, FINSEQ_4, ENUMSET1, CONVEX1, PARTFUN1,
JORDAN3, RLSUB_2, FUNCT_2, BINARITH, NAT_1, TOPREAL1, FVSUM_1, RFINSEQ,
SQUARE_1, FINSET_1, VECTSP_9, PRALG_3, BAGORDER, EUCLID_2, INTEGRA5,
XCMPLX_1;
schemes BINARITH, RLVECT_4, XBOOLE_0, FINSEQ_1, FUNCT_1;
begin :: Convex Combination on Convex Family
theorem
for V being non empty RLSStruct, M,N being convex Subset of V holds
M /\ N is convex
proof
let V be non empty RLSStruct;
let M,N be convex Subset of V;
let x,y be VECTOR of V;
let r be Real;
assume
A1: 0 < r & r < 1 & x in M /\ N & y in M /\ N;
then x in M & x in N & y in M & y in N by XBOOLE_0:def 3;
then r * x + (1-r) * y in M & r * x + (1-r) * y in N by A1,CONVEX1:def 2;
hence thesis by XBOOLE_0:def 3;
end;
theorem
for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V,
F being FinSequence of the carrier of V, B being FinSequence of REAL st
M = {u where u is VECTOR of V :
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u .|. v <= B.i}
holds M is convex
proof
let V be RealUnitarySpace-like (non empty UNITSTR);
let M be Subset of V;
let F be FinSequence of the carrier of V;
let B be FinSequence of REAL;
assume
A1:M = {u where u is VECTOR of V:
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u.|.v <= B.i};
let u1,v1 be VECTOR of V;
let r be Real;
assume that
A2: 0 < r & r < 1 and
A3: u1 in M & v1 in M;
consider u' be VECTOR of V such that
A4: u1 = u' and
A5: for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u'.|.v <= B.i by A1,A3;
consider v' be VECTOR of V such that
A6: v1 = v' and
A7: for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & v'.|.v <= B.i by A1,A3;
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & (r*u1 + (1-r)*v1).|.v <= B.i
proof
let i be Nat;
assume
A8: i in (dom F /\ dom B);
then i in dom B by XBOOLE_0:def 3;
then reconsider b = B.i as Real by PARTFUN1:27;
consider x being VECTOR of V such that
A9: x = F.i & u'.|. x <= b by A5,A8;
consider y being VECTOR of V such that
A10: y = F.i & v'.|. y <= b by A7,A8;
take v = x;
A11: r*(u1.|.v) <= r*b by A2,A4,A9,AXIOMS:25;
0 + r < 1 by A2;
then 1 - r > 0 by REAL_1:86;
then A12: (1-r)*(v1.|.v) <= (1-r)*b by A6,A9,A10,AXIOMS:25;
(r*u1 + (1-r)*v1).|.v = (r*u1).|.v + ((1-r)*v1).|.v by BHSP_1:def 2
.= r*(u1.|.v) + ((1-r)*v1).|.v by BHSP_1:def 2
.= r*(u1.|.v) + (1-r)*(v1.|.v) by BHSP_1:def 2;
then (r*u1 + (1-r)*v1).|.v <= r * b + (1-r)*(v1.|.v) by A11,AXIOMS:24;
then (r*u1 + (1-r)*v1).|.v - r * b <= (1-r)*(v1.|.v) by REAL_1:86;
then (r*u1 + (1-r)*v1).|.v - r * b <= (1-r)*b by A12,AXIOMS:22;
then (r*u1 + (1-r)*v1).|.v <= r * b + (1-r)*b by REAL_1:86;
then (r*u1 + (1-r)*v1).|.v <= (r+(1-r))*b by XCMPLX_1:8;
then (r*u1 + (1-r)*v1).|.v <= (1+r-r)*b by XCMPLX_1:29;
then (r*u1 + (1-r)*v1).|.v <= 1*b by XCMPLX_1:26;
hence thesis by A9;
end;
hence r*u1 + (1-r)*v1 in M by A1;
end;
theorem
for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V,
F being FinSequence of the carrier of V, B being FinSequence of REAL st
M = {u where u is VECTOR of V :
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u .|. v < B.i}
holds M is convex
proof
let V be RealUnitarySpace-like (non empty UNITSTR);
let M be Subset of V;
let F be FinSequence of the carrier of V;
let B be FinSequence of REAL;
assume
A1:M = {u where u is VECTOR of V:
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u.|.v < B.i};
let u1,v1 be VECTOR of V;
let r be Real;
assume that
A2: 0 < r & r < 1 and
A3: u1 in M & v1 in M;
consider u' be VECTOR of V such that
A4: u1 = u' and
A5: for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u'.|.v < B.i by A1,A3;
consider v' be VECTOR of V such that
A6: v1 = v' and
A7: for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & v'.|.v < B.i by A1,A3;
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & (r*u1 + (1-r)*v1).|.v < B.i
proof
let i be Nat;
assume
A8: i in (dom F /\ dom B);
then i in dom B by XBOOLE_0:def 3;
then reconsider b = B.i as Real by PARTFUN1:27;
consider x being VECTOR of V such that
A9: x = F.i & u'.|. x < b by A5,A8;
consider y being VECTOR of V such that
A10: y = F.i & v'.|. y < b by A7,A8;
take v = x;
A11: r*(u1.|.v) < r*b by A2,A4,A9,REAL_1:70;
0 + r < 1 by A2;
then 1 - r > 0 by REAL_1:86;
then A12: (1-r)*(v1.|.v) <= (1-r)*b by A6,A9,A10,AXIOMS:25;
(r*u1 + (1-r)*v1).|.v = (r*u1).|.v + ((1-r)*v1).|.v by BHSP_1:def 2
.= r*(u1.|.v) + ((1-r)*v1).|.v by BHSP_1:def 2
.= r*(u1.|.v) + (1-r)*(v1.|.v) by BHSP_1:def 2;
then (r*u1 + (1-r)*v1).|.v < r * b + (1-r)*(v1.|.v) by A11,REAL_1:67;
then (r*u1 + (1-r)*v1).|.v - r * b < (1-r)*(v1.|.v) by REAL_1:84;
then (r*u1 + (1-r)*v1).|.v - r * b < (1-r)*b by A12,AXIOMS:22;
then (r*u1 + (1-r)*v1).|.v < r * b + (1-r)*b by REAL_1:84;
then (r*u1 + (1-r)*v1).|.v < (r+(1-r))*b by XCMPLX_1:8;
then (r*u1 + (1-r)*v1).|.v < (1+r-r)*b by XCMPLX_1:29;
then (r*u1 + (1-r)*v1).|.v < 1*b by XCMPLX_1:26;
hence thesis by A9;
end;
hence r*u1 + (1-r)*v1 in M by A1;
end;
theorem
for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V,
F being FinSequence of the carrier of V, B being FinSequence of REAL st
M = {u where u is VECTOR of V :
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u .|. v >= B.i}
holds M is convex
proof
let V be RealUnitarySpace-like (non empty UNITSTR);
let M be Subset of V;
let F be FinSequence of the carrier of V;
let B be FinSequence of REAL;
assume
A1:M = {u where u is VECTOR of V:
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u.|.v >= B.i};
let u1,v1 be VECTOR of V;
let r be Real;
assume that
A2: 0 < r & r < 1 and
A3: u1 in M & v1 in M;
consider u' be VECTOR of V such that
A4: u1 = u' and
A5: for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u'.|.v >= B.i by A1,A3;
consider v' be VECTOR of V such that
A6: v1 = v' and
A7: for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & v'.|.v >= B.i by A1,A3;
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & (r*u1 + (1-r)*v1).|.v >= B.i
proof
let i be Nat;
assume
A8: i in (dom F /\ dom B);
then i in dom B by XBOOLE_0:def 3;
then reconsider b = B.i as Real by PARTFUN1:27;
consider x being VECTOR of V such that
A9: x = F.i & u'.|. x >= b by A5,A8;
consider y being VECTOR of V such that
A10: y = F.i & v'.|. y >= b by A7,A8;
take v = x;
A11: r*(u1.|.v) >= r*b by A2,A4,A9,AXIOMS:25;
0 + r < 1 by A2;
then 1 - r > 0 by REAL_1:86;
then A12: (1-r)*(v1.|.v) >= (1-r)*b by A6,A9,A10,AXIOMS:25;
(r*u1 + (1-r)*v1).|.v = (r*u1).|.v + ((1-r)*v1).|.v by BHSP_1:def 2
.= r*(u1.|.v) + ((1-r)*v1).|.v by BHSP_1:def 2
.= r*(u1.|.v) + (1-r)*(v1.|.v) by BHSP_1:def 2;
then (r*u1 + (1-r)*v1).|.v >= r * b + (1-r)*(v1.|.v) by A11,AXIOMS:24;
then (r*u1 + (1-r)*v1).|.v - r * b >= (1-r)*(v1.|.v) by REAL_1:84;
then (r*u1 + (1-r)*v1).|.v - r * b >= (1-r)*b by A12,AXIOMS:22;
then (r*u1 + (1-r)*v1).|.v >= r * b + (1-r)*b by REAL_1:84;
then (r*u1 + (1-r)*v1).|.v >= (r+(1-r))*b by XCMPLX_1:8;
then (r*u1 + (1-r)*v1).|.v >= (1+r-r)*b by XCMPLX_1:29;
then (r*u1 + (1-r)*v1).|.v >= 1*b by XCMPLX_1:26;
hence thesis by A9;
end;
hence r*u1 + (1-r)*v1 in M by A1;
end;
theorem
for V being RealUnitarySpace-like (non empty UNITSTR), M being Subset of V,
F being FinSequence of the carrier of V, B being FinSequence of REAL st
M = {u where u is VECTOR of V :
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u .|. v > B.i}
holds M is convex
proof
let V be RealUnitarySpace-like (non empty UNITSTR);
let M be Subset of V;
let F be FinSequence of the carrier of V;
let B be FinSequence of REAL;
assume
A1:M = {u where u is VECTOR of V:
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u.|.v > B.i};
let u1,v1 be VECTOR of V;
let r be Real;
assume that
A2: 0 < r & r < 1 and
A3: u1 in M & v1 in M;
consider u' be VECTOR of V such that
A4: u1 = u' and
A5: for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & u'.|.v > B.i by A1,A3;
consider v' be VECTOR of V such that
A6: v1 = v' and
A7: for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & v'.|.v > B.i by A1,A3;
for i being Nat st i in (dom F /\ dom B) holds
ex v being VECTOR of V st v = F.i & (r*u1 + (1-r)*v1).|.v > B.i
proof
let i be Nat;
assume
A8: i in (dom F /\ dom B);
then i in dom B by XBOOLE_0:def 3;
then reconsider b = B.i as Real by PARTFUN1:27;
consider x being VECTOR of V such that
A9: x = F.i & u'.|. x > b by A5,A8;
consider y being VECTOR of V such that
A10: y = F.i & v'.|. y > b by A7,A8;
take v = x;
A11: r*(u1.|.v) > r*b by A2,A4,A9,REAL_1:70;
0 + r < 1 by A2;
then 1 - r > 0 by REAL_1:86;
then A12: (1-r)*(v1.|.v) >= (1-r)*b by A6,A9,A10,AXIOMS:25;
(r*u1 + (1-r)*v1).|.v = (r*u1).|.v + ((1-r)*v1).|.v by BHSP_1:def 2
.= r*(u1.|.v) + ((1-r)*v1).|.v by BHSP_1:def 2
.= r*(u1.|.v) + (1-r)*(v1.|.v) by BHSP_1:def 2;
then (r*u1 + (1-r)*v1).|.v > r * b + (1-r)*(v1.|.v) by A11,REAL_1:67;
then (r*u1 + (1-r)*v1).|.v - r * b > (1-r)*(v1.|.v) by REAL_1:86;
then (r*u1 + (1-r)*v1).|.v - r * b > (1-r)*b by A12,AXIOMS:22;
then (r*u1 + (1-r)*v1).|.v > r * b + (1-r)*b by REAL_1:86;
then (r*u1 + (1-r)*v1).|.v > (r+(1-r))*b by XCMPLX_1:8;
then (r*u1 + (1-r)*v1).|.v > (1+r-r)*b by XCMPLX_1:29;
then (r*u1 + (1-r)*v1).|.v > 1*b by XCMPLX_1:26;
hence thesis by A9;
end;
hence r*u1 + (1-r)*v1 in M by A1;
end;
Lm1:
for V being RealLinearSpace, M being convex Subset of V holds
for N being Subset of V, L being Linear_Combination of N st
L is convex & N c= M holds Sum(L) in M
proof
let V be RealLinearSpace;
let M be convex Subset of V;
let N be Subset of V;
let L be Linear_Combination of N;
assume that
A1:L is convex and
A2:N c= 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;
A9:len F >= 1
proof
Carrier(L) <> {} by A1,CONVEX1:21;
then not (Carrier(L),{} are_equipotent) by CARD_1:46;
then card(Carrier(L)) <> card {} by CARD_1:21;
then len F <> card {} by A3,A4,FINSEQ_4:77;
then len F > 0 by CARD_1:78,NAT_1:19;
then len F >= 0 + 1 by NAT_1:38;
hence thesis;
end;
then len F in Seg len F by FINSEQ_1:3;
then reconsider i = len F as non empty Nat by BINARITH:5;
defpred P[Nat] means
(1/Sum(mid(f,1,$1)))*Sum(mid(L(#)F,1,$1)) in M;
A10:len (L(#)F) = len F by RLVECT_2:def 9;
A11:P[1]
proof
mid(f,1,1) = f|1 by JORDAN3:25;
then A12: len(mid(f,1,1)) = 1 by A6,A9,TOPREAL1:3;
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 A12,FINSEQ_1:57;
then A13: Sum(mid(f,1,1)) = m by RVSUM_1:103;
mid(L(#)F,1,1) = (L(#)F)|1 by JORDAN3:25;
then A14: len(mid(L(#)F,1,1)) = 1 by A9,A10,TOPREAL1:3;
1 in Seg len (L(#)F) by A9,A10,FINSEQ_1:3;
then A15: 1 in dom (L(#)F) & 1 in dom F & 1 in dom f by A6,A10,FINSEQ_1:def 3;
then A16: F/.1 = F.1 by FINSEQ_4:def 4;
A17: mid(L(#)F,1,1).1 = (L(#)F).1 by A9,A10,JORDAN3:32
.=L.(F/.1)*F/.1 by A15,RLVECT_2:def 9;
f.1 = L.(F.1) by A8,A15 .= L.(F/.1) by A15,FINSEQ_4:def 4;
then A18: Sum(mid(f,1,1)) = L.(F/.1) by A6,A9,A13,JORDAN3:32;
A19: F.1 in rng F by A15,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 consider v2 being Element of V such that
A20: F.1 = v2 & L.v2 <> 0;
mid(L(#)F,1,1) = <* mid(L(#)F,1,1).1 *> by A14,FINSEQ_1:57;
then A21: (1/Sum(mid(f,1,1)))*Sum(mid(L(#)F,1,1))
= (1/Sum(mid(f,1,1))) * (L.(F/.1) * F/.1) by A17,RLVECT_1:61
.= ((1/Sum(mid(f,1,1))) * L.(F/.1)) * F/.1 by RLVECT_1:def 9
.= 1 * F/.1 by A16,A18,A20,XCMPLX_1:107
.= F/.1 by RLVECT_1:def 9;
Carrier(L) c= N by RLVECT_2:def 8;
then Carrier(L) c= M by A2,XBOOLE_1:1;
hence thesis by A4,A16,A19,A21;
end;
A22:for k being non empty Nat st P[k] holds P[k+1]
proof
let k be non empty Nat;
assume
A23: (1/Sum(mid(f,1,k)))*Sum(mid(L(#)F,1,k)) in M;
A24: k >= 1 by RLVECT_1:99;
now per cases;
suppose
A25: k >= len f;
A26: mid(f,1,k) = f|k by A24,JORDAN3:25 .= f by A25,TOPREAL1:2;
A27: mid(L(#)F,1,k) = (L(#)F)|k by A24,JORDAN3:25 .= L(#)F
by A6,A10,A25,TOPREAL1:2;
A28: k+1 >= 1 & k+1 >= len f & k+1 >= len (L(#)F)
by A6,A10,A25,NAT_1:37;
then A29: mid(f,1,k+1) = f|(k+1) by JORDAN3:25 .= f by A28,TOPREAL1:2;
mid(L(#)F,1,k+1) = (L(#)F)|(k+1) by A28,JORDAN3:25
.= L(#)F by A28,TOPREAL1:2;
hence thesis by A23,A26,A27,A29;
suppose
A30: k < len f;
then A31: k+1 >= 1 & k+1 <= len f by A24,NAT_1:38;
mid(f,1,k) = f|k by A24,JORDAN3:25;
then A32: len mid(f,1,k) = k by A30,TOPREAL1:3;
A33: len <* mid(f,1,k+1).(k+1) *> = 1 by FINSEQ_1:57;
mid(f,1,k+1) = f|(k+1) by A31,JORDAN3:25;
then len mid(f,1,k+1) = k+1 by A31,TOPREAL1:3;
then A34: dom mid(f,1,k+1) = Seg (len mid(f,1,k) + len <* mid(f,1,k+1).(k+1)
*>)
by A32,A33,FINSEQ_1:def 3;
A35: mid(f,1,k+1) = f|(k+1) by A31,JORDAN3:25;
A36: len (f|(k+1)) = k+1 by A31,TOPREAL1:3;
A37: 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;
assume
A38: i in dom mid(f,1,k);
A39: mid(f,1,k) = f|k by A24,JORDAN3:25;
then (f|k).i = (f|k)/.i by A38,FINSEQ_4:def 4;
then A40: mid(f,1,k).i = f/.i by A38,A39,TOPREAL1:1;
A41: i in Seg len(f|k) by A38,A39,FINSEQ_1:def 3;
len(f|k) = k by A30,TOPREAL1:3;
then 1 <= i & i <= k by A41,FINSEQ_1:3;
then 1 <= i & i <= k+1 by NAT_1:37;
then i in Seg (k+1) by FINSEQ_1:3;
then A42: i in dom (f|(k+1)) by A36,FINSEQ_1:def 3;
then (f|(k+1)).i = (f|(k+1))/.i by FINSEQ_4:def 4;
hence thesis by A35,A40,A42,TOPREAL1:1;
end;
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;
assume
i in dom <* mid(f,1,k+1).(k+1) *>;
then i in Seg 1 by FINSEQ_1:55;
then i = 1 by FINSEQ_1:4,TARSKI:def 1;
hence thesis by A32,FINSEQ_1:57;
end;
then A43: mid(f,1,k+1)=mid(f,1,k)^<* mid(f,1,k+1).(k+1) *>
by A34,A37,FINSEQ_1:def 7;
k+1 in Seg (k+1) by A31,FINSEQ_1:3;
then A44: k+1 in dom (f|(k+1)) by A36,FINSEQ_1:def 3;
then (f|(k+1))/.(k+1) = f/.(k+1) by TOPREAL1:1;
then A45: mid(f,1,k+1).(k+1) = f/.(k+1) by A35,A44,FINSEQ_4:def 4;
A46: k+1 in Seg len f by A31,FINSEQ_1:3;
then A47: k+1 in dom f by FINSEQ_1:def 3;
then A48: mid(f,1,k+1).(k+1) = f.(k+1) by A45,FINSEQ_4:def 4
.= L.(F.(k+1)) by A8,A47;
k+1 in dom F by A6,A46,FINSEQ_1:def 3;
then mid(f,1,k+1).(k+1) = L.(F/.(k+1)) by A48,FINSEQ_4:def 4;
then A49: Sum(mid(f,1,k+1)) = Sum(mid(f,1,k)) + L.(F/.(k+1)) by A43,RVSUM_1:
104;
A50: k < len (L(#)F) by A6,A30,RLVECT_2:def 9;
then A51: k+1 >= 1 & k+1 <= len (L(#)F) by A24,NAT_1:38;
mid(L(#)F,1,k) = (L(#)F)|k by A24,JORDAN3:25;
then A52: len mid(L(#)F,1,k) = k by A50,TOPREAL1:3;
A53: len <* mid(L(#)F,1,k+1).(k+1) *> = 1 by FINSEQ_1:57;
A54: mid(L(#)F,1,k+1) = (L(#)F)|(k+1) by A51,JORDAN3:25;
then len mid(L(#)F,1,k+1) = k+1 by A51,TOPREAL1:3;
then A55: dom mid(L(#)F,1,k+1)
= Seg (len mid(L(#)F,1,k) + len <* mid(L(#)F,1,k+1).(k+1) *>)
by A52,A53,FINSEQ_1:def 3;
A56: len ((L(#)F)|(k+1)) = k+1 by A51,TOPREAL1:3;
A57: 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;
assume
A58: i in dom mid(L(#)F,1,k);
A59: mid(L(#)F,1,k) = (L(#)F)|k by A24,JORDAN3:25;
then ((L(#)F)|k).i = ((L(#)F)|k)/.i by A58,FINSEQ_4:def 4;
then A60: mid(L(#)F,1,k).i = (L(#)F)/.i by A58,A59,TOPREAL1:1;
A61: i in Seg len((L(#)F)|k) by A58,A59,FINSEQ_1:def 3;
len((L(#)F)|k) = k by A50,TOPREAL1:3;
then 1 <= i & i <= k by A61,FINSEQ_1:3;
then 1 <= i & i <= k+1 by NAT_1:37;
then i in Seg (k+1) by FINSEQ_1:3;
then A62: i in dom ((L(#)F)|(k+1)) by A56,FINSEQ_1:def 3;
then ((L(#)F)|(k+1)).i = ((L(#)F)|(k+1))/.i by FINSEQ_4:def 4;
hence thesis by A54,A60,A62,TOPREAL1:1;
end;
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;
assume
i in dom <* mid(L(#)F,1,k+1).(k+1) *>;
then i in Seg 1 by FINSEQ_1:55;
then i = 1 by FINSEQ_1:4,TARSKI:def 1;
hence thesis by A52,FINSEQ_1:57;
end;
then A63: mid(L(#)F,1,k+1) = mid(L(#)F,1,k)^<* mid(L(#)F,1,k+1).(k+1) *>
by A55,A57,FINSEQ_1:def 7;
k+1 in Seg (k+1) by A31,FINSEQ_1:3;
then A64: k+1 in dom ((L(#)F)|(k+1)) by A56,FINSEQ_1:def 3;
then ((L(#)F)|(k+1))/.(k+1) = (L(#)F)/.(k+1) by TOPREAL1:1;
then A65: mid((L(#)F),1,k+1).(k+1) = (L(#)F)/.(k+1) by A54,A64,FINSEQ_4:def 4
;
k+1 <= len (L(#)F) by A6,A31,RLVECT_2:def 9;
then A66: k+1 in dom (L(#)F) by A31,FINSEQ_3:27;
then A67: mid((L(#)F),1,k+1).(k+1) = (L(#)F).(k+1) by A65,FINSEQ_4:def 4
.= L.(F/.(k+1)) * F/.(k+1) by A66,RLVECT_2:def 9;
set r1 = Sum(mid(f,1,k));
set r2 = L.(F/.(k+1));
set w1 = Sum(mid(L(#)F,1,k));
set w2 = F/.(k+1);
A68: for i being Nat st i in dom mid(f,1,k) holds 0 <= mid(f,1,k).i
proof
let i be Nat;
assume i in dom mid(f,1,k);
then i in Seg k by A32,FINSEQ_1:def 3;
then A69: 1 <= i & i <= k by FINSEQ_1:3;
then A70: mid(f,1,k).i = f.i by A30,JORDAN3:32;
1 <= i & i <= len f by A30,A69,AXIOMS:22;
then i in dom f by FINSEQ_3:27;
hence thesis by A8,A70;
end;
ex i being Nat st i in dom mid(f,1,k) & 0 < mid(f,1,k).i
proof
A71: 1 in Seg len mid(f,1,k) by A24,A32,FINSEQ_1:3;
1 <= len f by A24,A30,AXIOMS:22;
then A72: 1 in Seg len f by FINSEQ_1:3;
then 1 in dom f by FINSEQ_1:def 3;
then A73: f.1 = L.(F.1) & f.1 >= 0 by A8;
1 in dom F by A6,A72,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 consider v being Element of V such that
A74: v = F.1 & L.v <> 0;
take 1;
thus thesis by A24,A30,A71,A73,A74,FINSEQ_1:def 3,JORDAN3:32;
end;
then A75: r1 > 0 by A68,RVSUM_1:115;
A76: w2 in M & r2 > 0
proof
k+1 in Seg len F by A6,A31,FINSEQ_1:3;
then A77: k+1 in dom F by FINSEQ_1:def 3;
then w2 = F.(k+1) by FINSEQ_4:def 4;
then A78: w2 in Carrier(L) by A4,A77,FUNCT_1:def 5;
Carrier(L) c= N by RLVECT_2:def 8;
hence w2 in M by A2,A78,TARSKI:def 3;
w2 in {v where v is Element of V : L.v <> 0}
by A78,RLVECT_2:def 6;
then consider v being Element of V such that
A79: v = w2 & L.v <> 0;
k+1 in Seg len f by A31,FINSEQ_1:3;
then k+1 in dom f by FINSEQ_1:def 3;
then f.(k+1) = L.(F.(k+1)) & f.(k+1) >= 0 by A8;
hence r2 > 0 by A77,A79,FINSEQ_4:def 4;
end;
then A80: r1+r2 > 0+0 by A75,REAL_1:67;
A81: 0 < (1/(r1+r2))*r1 & (1/(r1+r2))*r1 < 1
proof
1/(r1+r2) > 0 by A80,REAL_2:127;
hence (1/(r1+r2))*r1 > 0 by A75,REAL_2:122;
A82: r1+r2 > r1 by A76,REAL_1:69;
(1/(r1+r2))*r1 = r1/(r1+r2) by XCMPLX_1:100;
hence (1/(r1+r2))*r1 < 1 by A75,A82,REAL_2:142;
end;
A83: (1/(r1+r2))*r2 = 1 - (1/(r1+r2))*r1
proof
1 - (1/(r1+r2))*r1 = (r1+r2)*(1/(r1+r2)) - (1/(r1+r2))*r1
by A80,XCMPLX_1:107
.= (r1+r2-r1)*(1/(r1+r2)) by XCMPLX_1:40;
hence thesis by XCMPLX_1:26;
end;
(1/Sum(mid(f,1,k+1)))*Sum(mid(L(#)F,1,k+1))
= (1/(r1+r2))*(w1+r2*w2) by A49,A63,A67,FVSUM_1:87
.= (1/(r1+r2))*(1 * w1 + r2 * w2) by RLVECT_1:def 9
.= (1/(r1+r2))*((r1 * (1/r1)) * w1 + r2 * w2) by A75,XCMPLX_1:107
.= (1/(r1+r2))*(r1 * ((1/r1)*w1) + r2 * w2) by RLVECT_1:def 9
.= (1/(r1+r2))*(r1 * ((1/r1)*w1))
+(1/(r1+r2))*(r2 * w2) by RLVECT_1:def 9
.= (1/(r1+r2))*r1 * ((1/r1)*w1)
+(1/(r1+r2))*(r2 * w2) by RLVECT_1:def 9
.= (1/(r1+r2))*r1 * ((1/r1)*w1)
+(1/(r1+r2))*r2 * w2 by RLVECT_1:def 9;
hence thesis by A23,A76,A81,A83,CONVEX1:def 2;
end;
hence thesis;
end;
for k being non empty Nat holds P[k] from Ind_from_1(A11,A22);
then A84:(1/Sum(mid(f,1,i)))*Sum(mid(L(#)F,1,i)) in M;
A85:len (L (#) F) = len F by RLVECT_2:def 9;
Sum(mid(f,1,len f)) = 1 by A6,A7,A9,JORDAN3:29;
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 9
.= Sum(L (#) F) by A9,A85,JORDAN3:29;
hence thesis by A3,A4,A6,A84,A85,RLVECT_2:def 10;
end;
Lm2:
for V being RealLinearSpace, M being Subset of V st
for N being Subset of V, L being Linear_Combination of N st
L is convex & N c= M holds Sum(L) in M
holds M is convex
proof
let V be RealLinearSpace;
let M be Subset of V;
assume
A1:for N being Subset of V, L being Linear_Combination of N st
L is convex & N c= M holds Sum(L) in M;
let u,v be VECTOR of V;
let r be Real;
assume that
A2: 0 < r and
A3: r < 1 and
A4: u in M and
A5: v in M;
set N = {u,v};
A6: N c= M by A4,A5,ZFMISC_1:38;
reconsider N as Subset of V;
now per cases;
suppose A7:u <> v;
consider L being Linear_Combination of {u,v} such that
A8: L.u = r & L.v = (1-r) from LinCEx2(A7);
reconsider L as Linear_Combination of N;
A9: Sum(L)=r*u + (1-r)*v by A7,A8,RLVECT_2:51;
L is convex
proof
ex F being FinSequence of the carrier of V st
(F is one-to-one & rng F = Carrier L &
(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)))
proof
A10: Carrier L c= {u,v} by RLVECT_2:def 8;
u in {w where w is Element of V : L.w <> 0}
by A2,A8;
then A11: u in Carrier L by RLVECT_2:def 6;
r-r < 1-r by A3,REAL_1:54;
then A12: 0 < 1-r by XCMPLX_1:14;
then v in {w where w is Element of V : L.w <> 0}
by A8;
then v in Carrier L by RLVECT_2:def 6;
then A13: {u,v} c= Carrier L by A11,ZFMISC_1:38;
<*u,v*> = <*u*>^<*v*> by FINSEQ_1:def 9;
then A14: rng <*u,v*> = rng <*u*> \/ rng <*v*> by FINSEQ_1:44
.= {u} \/ rng <*v*> by FINSEQ_1:55
.= {u} \/ {v} by FINSEQ_1:55
.= {u,v} by ENUMSET1:41
.= Carrier L by A10,A13,XBOOLE_0:def 10;
A15: ex f being FinSequence of REAL st len f = len <*u,v*> & Sum(f) = 1 &
(for n being Nat st n in dom f holds f.n = L.(<*u,v*>.n) & f.n >= 0)
proof
A16: len <*r,1-r*> = 2 by FINSEQ_1:61 .= len <*u,v*> by FINSEQ_1:61;
A17: Sum(<*r,1-r*>) = r + (1-r) by RVSUM_1:107
.= r + 1 - r by XCMPLX_1:29 .= 1 by XCMPLX_1:26;
A18: for n being Nat st n in dom <*r,1-r*>
holds <*r,1-r*>.n = L.(<*u,v*>.n) & <*r,1-r*>.n >= 0
proof
let n be Nat;
assume n in dom <*r,1-r*>;
then n in Seg len <*r,1-r*> by FINSEQ_1:def 3;
then A19: n in {1,2} by FINSEQ_1:4,61;
now per cases by A19,TARSKI:def 2;
suppose
A20: n = 1;
then L.(<*u,v*>.n) = r by A8,FINSEQ_1:61;
hence thesis by A2,A20,FINSEQ_1:61;
suppose
A21: n = 2;
then L.(<*u,v*>.n) = 1-r by A8,FINSEQ_1:61;
hence thesis by A12,A21,FINSEQ_1:61;
end;
hence thesis;
end;
take <*r,1-r*>;
thus thesis by A16,A17,A18;
end;
take <*u,v*>;
thus thesis by A7,A14,A15,FINSEQ_3:103;
end;
hence thesis by CONVEX1:def 3;
end;
hence thesis by A1,A6,A9;
suppose A22:u = v;
consider L being Linear_Combination of {u} such that
A23: L.u = 1 from LinCEx1;
reconsider L as Linear_Combination of N by A22,ENUMSET1:69;
L is convex
proof
ex F being FinSequence of the carrier of V st
(F is one-to-one & rng F = Carrier L &
(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)))
proof
A24: Carrier L c= {u,v} by RLVECT_2:def 8;
u in {w where w is Element of V : L.w <> 0}
by A23;
then A25: u in Carrier L by RLVECT_2:def 6;
v in {w where w is Element of V : L.w <> 0}
by A22,A23;
then v in Carrier L by RLVECT_2:def 6;
then {u,v} c= Carrier L by A25,ZFMISC_1:38;
then Carrier L = {u,v} by A24,XBOOLE_0:def 10;
then A26: Carrier L = {u} by A22,ENUMSET1:69;
A27: ex f being FinSequence of REAL st len f = len <*u*> & Sum(f) = 1 &
for n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
proof
reconsider f = <*1*> as FinSequence of REAL;
A28: len <*1*> = 1 by FINSEQ_1:56 .= len <*u*> by FINSEQ_1:56;
A29: for n being Nat st n in dom f holds f.n = L.(<*u*>.n) &
f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in {1} by FINSEQ_1:4,55;
then A30: n = 1 by TARSKI:def 1;
then A31: f.n = 1 by FINSEQ_1:57
.= L.(<*u*>.n) by A23,A30,FINSEQ_1:57;
f.n = 1 by A30,FINSEQ_1:57;
hence thesis by A31;
end;
take f;
thus thesis by A28,A29,RVSUM_1:103;
end;
take <*u*>;
thus thesis by A26,A27,FINSEQ_1:55,FINSEQ_3:102;
end;
hence thesis by CONVEX1:def 3;
end;
then A32: Sum(L) in M by A1,A6;
r*u + (1-r)*v = (r+(1-r))*u by A22,RLVECT_1:def 9
.= (r+1-r)*u by XCMPLX_1:29
.= (r-r+1)*u by XCMPLX_1:29
.= (0+1)*u by XCMPLX_1:14;
hence thesis by A23,A32,RLVECT_2:50;
end;
hence thesis;
end;
theorem
for V being RealLinearSpace, M being Subset of V holds
(for N being Subset of V, L being Linear_Combination of N st
L is convex & N c= M holds Sum(L) in M)
iff M is convex by Lm1,Lm2;
definition let V be RealLinearSpace, M be Subset of V;
defpred P[set] means $1 is Linear_Combination of M;
func LinComb(M) -> set means
for L being set holds
L in it iff L is Linear_Combination of M;
existence
proof
consider A being set such that
A1: for x being set holds
x in A iff x in Funcs(the carrier of V, REAL) & P[x] from Separation;
take A;
let L be set;
thus L in A implies L is Linear_Combination of M by A1;
assume L is Linear_Combination of M;
hence thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
end;
end;
Lm3:
for V being RealLinearSpace holds
ex L be Linear_Combination of V st L is convex
proof
let V be RealLinearSpace;
consider u being Element of V;
consider L being Linear_Combination of {u} such that
A1:L.u = 1 from LinCEx1;
reconsider L as Linear_Combination of V;
A2: L is convex
proof
A3: Carrier L c= {u} by RLVECT_2:def 8;
u in {w where w is Element of V : L.w <> 0}
by A1;
then u in Carrier L by RLVECT_2:def 6;
then {u} c= Carrier L by ZFMISC_1:37;
then A4: Carrier L = {u} by A3,XBOOLE_0:def 10;
A5: ex f being FinSequence of REAL st len f = len <*u*> & Sum(f) = 1 &
for n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
proof
reconsider f = <*1*> as FinSequence of REAL;
A6: len <*1*> = 1 by FINSEQ_1:56 .= len <*u*> by FINSEQ_1:56;
A7: for n being Nat st n in dom f holds f.n = L.(<*u*>.n) &
f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in {1} by FINSEQ_1:4,55;
then A8: n = 1 by TARSKI:def 1;
then A9: f.n = L.u by A1,FINSEQ_1:57
.= L.(<*u*>.n) by A8,FINSEQ_1:57;
f.n = 1 by A8,FINSEQ_1:57;
hence thesis by A9;
end;
take f;
thus thesis by A6,A7,RVSUM_1:103;
end;
take <*u*>;
thus thesis by A4,A5,FINSEQ_1:55,FINSEQ_3:102;
end;
take L;
thus thesis by A2;
end;
definition let V be RealLinearSpace;
cluster convex Linear_Combination of V;
existence by Lm3;
end;
definition let V be RealLinearSpace;
mode Convex_Combination of V is convex Linear_Combination of V;
end;
Lm4:
for V being RealLinearSpace, M being non empty Subset of V holds
ex L being Linear_Combination of M st L is convex
proof
let V be RealLinearSpace;
let M be non empty Subset of V;
consider u being set such that
A1:u in M by XBOOLE_0:def 1;
reconsider u as Element of V by A1;
consider L being Linear_Combination of {u} such that
A2:L.u = 1 from LinCEx1;
{u} c= M by A1,ZFMISC_1:37;
then reconsider L as Linear_Combination of M by RLVECT_2:33;
A3: L is convex
proof
A4: Carrier L c= {u} by RLVECT_2:def 8;
u in {w where w is Element of V : L.w <> 0}
by A2;
then u in Carrier L by RLVECT_2:def 6;
then {u} c= Carrier L by ZFMISC_1:37;
then A5: Carrier L = {u} by A4,XBOOLE_0:def 10;
A6: ex f being FinSequence of REAL st len f = len <*u*> & Sum(f) = 1 &
for n being Nat st n in dom f holds f.n = L.(<*u*>.n) & f.n >= 0
proof
reconsider f = <*1*> as FinSequence of REAL;
A7: len <*1*> = 1 by FINSEQ_1:56 .= len <*u*> by FINSEQ_1:56;
A8: for n being Nat st n in dom f holds f.n = L.(<*u*>.n) &
f.n >= 0
proof
let n be Nat;
assume n in dom f;
then n in {1} by FINSEQ_1:4,55;
then A9: n = 1 by TARSKI:def 1;
then A10: f.n = L.u by A2,FINSEQ_1:57
.= L.(<*u*>.n) by A9,FINSEQ_1:57;
f.n = 1 by A9,FINSEQ_1:57;
hence thesis by A10;
end;
take f;
thus thesis by A7,A8,RVSUM_1:103;
end;
take <*u*>;
thus thesis by A5,A6,FINSEQ_1:55,FINSEQ_3:102;
end;
take L;
thus thesis by A3;
end;
definition let V be RealLinearSpace, M be non empty Subset of V;
cluster convex Linear_Combination of M;
existence by Lm4;
end;
definition let V be RealLinearSpace, M be non empty Subset of V;
mode Convex_Combination of M is convex Linear_Combination of M;
end;
Lm5:
for V being RealLinearSpace, W1,W2 being Subspace of V holds
Up(W1+W2) = Up(W1) + Up(W2)
proof
let V be RealLinearSpace;
let W1,W2 being Subspace of V;
A1:Up(W1+W2) = the carrier of W1+W2 by RUSUB_4:def 6
.= {v + u where v,u is VECTOR of V : v in W1 & u in W2} by RLSUB_2:def 1;
for x being set st x in Up(W1+W2) holds x in Up(W1) + Up(W2)
proof
let x be set;
assume x in Up(W1+W2);
then consider v,u being VECTOR of V such that
A2: x = v + u & v in W1 & u in W2 by A1;
v in the carrier of W1 & u in the carrier of W2 by A2,RLVECT_1:def 1;
then v in Up(W1) & u in Up(W2) by RUSUB_4:def 6;
then x in {u' + v' where u',v' is Element of V:
u' in Up(W1) & v' in Up(W2)} by A2;
hence thesis by RUSUB_4:def 10;
end;
then A3:Up(W1+W2) c= Up(W1) + Up(W2) by TARSKI:def 3;
for x being set st x in Up(W1) + Up(W2) holds x in Up(W1+W2)
proof
let x be set;
assume x in Up(W1) + Up(W2);
then x in {u + v where u,v is Element of V:
u in Up(W1) & v in Up(W2)} by RUSUB_4:def 10;
then consider u,v being Element of V such that
A4: x = u + v & u in Up(W1) & v in Up(W2);
u in the carrier of W1 & v in the carrier of W2 by A4,RUSUB_4:def 6;
then u in W1 & v in W2 by RLVECT_1:def 1;
hence thesis by A1,A4;
end;
then Up(W1) + Up(W2) c= Up(W1+W2) by TARSKI:def 3;
hence thesis by A3,XBOOLE_0:def 10;
end;
Lm6:
for V being RealLinearSpace, W1,W2 being Subspace of V holds
Up(W1 /\ W2) = Up(W1) /\ Up(W2)
proof
let V be RealLinearSpace;
let W1,W2 be Subspace of V;
A1:Up(W1 /\ W2) = the carrier of W1 /\ W2 by RUSUB_4:def 6
.= (the carrier of W1) /\ (the carrier of W2) by RLSUB_2:def 2;
for x being set st x in Up(W1 /\ W2) holds x in Up(W1) /\ Up(W2)
proof
let x be set;
assume x in Up(W1 /\ W2);
then x in the carrier of W1 & x in the carrier of W2 by A1,XBOOLE_0:def 3
;
then x in Up(W1) & x in Up(W2) by RUSUB_4:def 6;
hence thesis by XBOOLE_0:def 3;
end;
then A2:Up(W1 /\ W2) c= Up(W1) /\ Up(W2) by TARSKI:def 3;
for x being set st x in Up(W1) /\ Up(W2) holds x in Up(W1 /\ W2)
proof
let x be set;
assume x in Up(W1) /\ Up(W2);
then x in Up(W1) & x in Up(W2) by XBOOLE_0:def 3;
then x in the carrier of W1 & x in the carrier of W2 by RUSUB_4:def 6;
hence thesis by A1,XBOOLE_0:def 3;
end;
then Up(W1) /\ Up(W2) c= Up(W1 /\ W2) by TARSKI:def 3;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th7:
for V being RealLinearSpace, M be Subset of V holds
Convex-Family M <> {}
proof
let V be RealLinearSpace;
let M be Subset of V;
A1:Up((Omega).V) is convex by CONVEX1:9;
M c= Up((Omega).V)
proof
let x be set;
assume x in M;
then reconsider x as Element of V;
x in the carrier of (the RLSStruct of V);
then x in the carrier of (Omega).V by RLSUB_1:def 4;
hence thesis by RUSUB_4:def 6;
end;
hence thesis by A1,CONVEX1:def 4;
end;
theorem
for V being RealLinearSpace, M being Subset of V holds M c= conv(M)
proof
let V be RealLinearSpace;
let M be Subset of V;
let v be set;
assume
A1: v in M;
A2: Convex-Family M <> {} by Th7;
for Y being set holds
Y in Convex-Family M implies v in Y
proof
let Y be set;
assume
A3: Y in Convex-Family M;
then reconsider Y as Subset of V;
Y is convex & M c= Y by A3,CONVEX1:def 4;
hence thesis by A1;
end;
then v in meet(Convex-Family M) by A2,SETFAM_1:def 1;
hence thesis by CONVEX1:def 5;
end;
Lm7:
for V being RealLinearSpace, L1, L2 being Convex_Combination of V,
a,b being Real st a * b > 0 holds
Carrier(a*L1 + b*L2) = Carrier(a * L1) \/ Carrier(b * L2)
proof
let V be RealLinearSpace;
let L1, L2 be Convex_Combination of V;
let a,b be Real;
assume a * b > 0;
then A1:not (a>=0 & b<=0 or a<=0 & b>=0) by REAL_2:123;
then A2: Carrier(L1) = Carrier(a * L1) &
Carrier(L2) = Carrier(b * L2) by RLVECT_2:65;
for x being set st x in Carrier(a * L1) \/ Carrier(b * L2) holds
x in Carrier(a*L1 + b*L2)
proof
let x be set;
assume
A3: x in Carrier(a * L1) \/ Carrier(b * L2);
now per cases by A3,XBOOLE_0:def 2;
suppose
A4: x in Carrier(a * L1);
then x in {v where v is Element of V : (a * L1).v <> 0}
by RLVECT_2:def 6;
then consider v being Element of V such that
A5: v = x & (a * L1).v <> 0;
A6: L1.v > 0 by A2,A4,A5,CONVEX1:22;
v in Carrier(a*L1 + b*L2)
proof
now per cases;
suppose v in Carrier(L2);
then A7: L2.v > 0 by CONVEX1:22;
now per cases by A1;
suppose a > 0 & b > 0;
then a*L1.v > 0 & b*L2.v > 0 by A6,A7,SQUARE_1:21;
then A8: (a*L1).v > 0 & (b*L2).v > 0 by RLVECT_2:def 13;
then (a*L1).v + (b*L2).v > (a*L1).v by REAL_1:69;
then (a*L1).v + (b*L2).v > 0 by A8,AXIOMS:22;
then (a*L1 + b*L2).v > 0 by RLVECT_2:def 12;
hence thesis by RLVECT_2:28;
suppose a < 0 & b < 0;
then a*L1.v < 0 & b*L2.v < 0 by A6,A7,SQUARE_1:24;
then A9: (a*L1).v < 0 & (b*L2).v < 0 by RLVECT_2:def 13;
then (a*L1).v + (b*L2).v < (b*L2).v by REAL_2:173;
then (a*L1).v + (b*L2).v < 0 by A9,AXIOMS:22;
then (a*L1 + b*L2).v < 0 by RLVECT_2:def 12;
hence thesis by RLVECT_2:28;
end;
hence thesis;
suppose not v in Carrier(L2);
then L2.v = 0 by RLVECT_2:28;
then b*L2.v = 0;
then (b*L2).v = 0 by RLVECT_2:def 13;
then (a*L1).v + (b*L2).v = (a*L1).v;
then (a*L1 + b*L2).v <> 0 by A5,RLVECT_2:def 12;
hence thesis by RLVECT_2:28;
end;
hence thesis;
end;
hence thesis by A5;
suppose
A10: x in Carrier(b * L2);
then x in {v where v is Element of V : (b * L2).v <> 0}
by RLVECT_2:def 6;
then consider v being Element of V such that
A11: v = x & (b * L2).v <> 0;
A12: L2.v > 0 by A2,A10,A11,CONVEX1:22;
v in Carrier(a*L1 + b*L2)
proof
now per cases;
suppose v in Carrier(L1);
then A13: L1.v > 0 by CONVEX1:22;
now per cases by A1;
suppose a > 0 & b > 0;
then a*L1.v > 0 & b*L2.v > 0 by A12,A13,SQUARE_1:21;
then A14: (a*L1).v > 0 & (b*L2).v > 0 by RLVECT_2:def 13;
then (a*L1).v + (b*L2).v > (a*L1).v by REAL_1:69;
then (a*L1).v + (b*L2).v > 0 by A14,AXIOMS:22;
then (a*L1 + b*L2).v > 0 by RLVECT_2:def 12;
hence thesis by RLVECT_2:28;
suppose a < 0 & b < 0;
then a*L1.v < 0 & b*L2.v < 0 by A12,A13,SQUARE_1:24;
then A15: (a*L1).v < 0 & (b*L2).v < 0 by RLVECT_2:def 13;
then (a*L1).v + (b*L2).v < (b*L2).v by REAL_2:173;
then (a*L1).v + (b*L2).v < 0 by A15,AXIOMS:22;
then (a*L1 + b*L2).v < 0 by RLVECT_2:def 12;
hence thesis by RLVECT_2:28;
end;
hence thesis;
suppose not v in Carrier(L1);
then L1.v = 0 by RLVECT_2:28;
then a*L1.v = 0;
then (a*L1).v = 0 by RLVECT_2:def 13;
then (a*L1).v + (b*L2).v = (b*L2).v;
then (a*L1 + b*L2).v <> 0 by A11,RLVECT_2:def 12;
hence thesis by RLVECT_2:28;
end;
hence thesis;
end;
hence thesis by A11;
end;
hence thesis;
end;
then A16:Carrier(a * L1) \/ Carrier(b * L2) c= Carrier(a*L1 + b*L2) by TARSKI:
def 3;
Carrier(a*L1 + b*L2) c= Carrier(a*L1) \/ Carrier(b*L2) by RLVECT_2:58;
hence thesis by A16,XBOOLE_0:def 10;
end;
Lm8:
for F,G being Function st F,G are_fiberwise_equipotent
for x1,x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1,z2 being set st
z1 in dom G & z2 in dom G & z1 <> z2 & F.x1 = G.z1 & F.x2 = G.z2
proof
let F,G be Function;
assume
A1:F,G are_fiberwise_equipotent;
let x1,x2 be set;
assume that
A2:x1 in dom F and
A3:x2 in dom F and
A4:x1 <> x2;
consider H being Function such that
A5:dom H = dom F & rng H = dom G & H is one-to-one & F = G*H by A1,RFINSEQ:3;
A6:H.x1 in dom G & H.x2 in dom G by A2,A3,A5,FUNCT_1:12;
A7:H.x1 <> H.x2 by A2,A3,A4,A5,FUNCT_1:def 8;
F.x1 = G.(H.x1) & F.x2 = G.(H.x2) by A2,A3,A5,FUNCT_1:22;
hence thesis by A6,A7;
end;
Lm9:
for V being RealLinearSpace, L being Linear_Combination of V,
A being Subset of V st A c= Carrier(L) holds
ex L1 being Linear_Combination of V st Carrier(L1) = A
proof
let V be RealLinearSpace;
let L be Linear_Combination of V;
let A be Subset of V;
assume
A1:A c= Carrier(L);
consider F being Function such that
A2:L = F & dom F = the carrier of V & rng F c= REAL by FUNCT_2:def 2;
defpred P[set,set] means
($1 in A implies $2 = F.$1) & (not $1 in A implies $2 = 0);
A3:for x,y1,y2 being set st x in the carrier of V & P[x,y1] & P[x,y2]
holds y1 = y2;
A4:for x being set st x in the carrier of V
ex y being set st P[x,y]
proof
let x be set;
assume x in the carrier of V;
now per cases;
suppose x in A;
hence thesis;
suppose not x in A;
hence thesis;
end;
hence thesis;
end;
consider L1 being Function such that
A5:dom L1 = the carrier of V &
for x being set st x in the carrier of V holds P[x,L1.x] from FuncEx(A3,A4);
for y being set st y in rng L1 holds y in REAL
proof
let y be set;
assume y in rng L1;
then consider x being set such that
A6: x in dom L1 & y = L1.x by FUNCT_1:def 5;
reconsider x as Element of V by A5,A6;
now per cases;
suppose x in A;
then A7: y = F.x by A5,A6;
F.x in rng F by A2,FUNCT_1:12;
hence thesis by A2,A7;
suppose not x in A;
then L1.x = 0 by A5;
hence thesis by A6;
end;
hence thesis;
end;
then rng L1 c= REAL by TARSKI:def 3;
then A8:L1 is Element of Funcs(the carrier of V, REAL)
by A5,FUNCT_2:def 2;
reconsider A as finite Subset of V by A1,FINSET_1:13;
for v being Element of V st not v in A holds
L1.v = 0 by A5;
then reconsider L1 as Linear_Combination of V by A8,RLVECT_2:def 5;
for v being set st v in A holds v in Carrier(L1)
proof
let v be set;
assume
A9: v in A;
then reconsider v as Element of V;
A10: L1.v = F.v by A5,A9;
L.v <> 0 by A1,A9,RLVECT_2:28;
hence thesis by A2,A10,RLVECT_2:28;
end;
then A11:A c= Carrier(L1) by TARSKI:def 3;
for v being set st v in Carrier(L1) holds v in A
proof
let v be set;
assume
A12: v in Carrier(L1);
then reconsider v as Element of V;
L1.v <> 0 by A12,RLVECT_2:28;
hence thesis by A5;
end;
then A13:Carrier(L1) c= A by TARSKI:def 3;
take L1;
thus thesis by A11,A13,XBOOLE_0:def 10;
end;
theorem Th9:
for V being RealLinearSpace, L1,L2 being Convex_Combination of V,
r being Real st 0 < r & r < 1 holds
r*L1 + (1-r)*L2 is Convex_Combination of V
proof
let V be RealLinearSpace;
let L1,L2 be Convex_Combination of V;
let r be Real;
assume
A1:0 < r & r < 1;
then r - r < 1 - r by REAL_1:54;
then A2:0 < 1 - r by XCMPLX_1:14;
then A3:r*(1-r) > 0 by A1,REAL_2:122;
consider F1 being FinSequence of the carrier of V such that
A4:F1 is one-to-one & rng F1 = Carrier(L1) &
(ex f being FinSequence of REAL st len f = len F1 & Sum(f) = 1 &
(for n being Nat st n in dom f holds f.n = L1.(F1.n) & f.n >= 0))
by CONVEX1:def 3;
consider f1 being FinSequence of REAL such that
A5:len f1 = len F1 & Sum(f1) = 1 &
(for n being Nat st n in dom f1 holds f1.n = L1.(F1.n) & f1.n >= 0)
by A4;
consider F2 being FinSequence of the carrier of V such that
A6:F2 is one-to-one & rng F2 = Carrier(L2) &
(ex f being FinSequence of REAL st len f = len F2 & Sum(f) = 1 &
(for n being Nat st n in dom f holds f.n = L2.(F2.n) & f.n >= 0))
by CONVEX1:def 3;
consider f2 being FinSequence of REAL such that
A7:len f2 = len F2 & Sum(f2) = 1 &
(for n being Nat st n in dom f2 holds f2.n = L2.(F2.n) & f2.n >= 0)
by A6;
set L = r*L1 + (1-r)*L2;
A8:Carrier(r*L1) = Carrier(L1) & Carrier((1-r)*L2) = Carrier(L2)
by A1,A2,RLVECT_2:65;
A9:Carrier(L) = Carrier(r*L1) \/ Carrier((1-r)*L2) by A3,Lm7;
set Top = Carrier(L) \ Carrier((1-r)*L2);
set Mid = Carrier(r*L1) /\ Carrier((1-r)*L2);
set Btm = Carrier(L) \ Carrier(r*L1);
Top c= Carrier(L) by XBOOLE_1:36;
then consider Lt being Linear_Combination of V such that
A10:Carrier(Lt) = Top by Lm9;
Mid c= Carrier(L) by A9,XBOOLE_1:29;
then consider Lm being Linear_Combination of V such that
A11:Carrier(Lm) = Mid by Lm9;
Btm c= Carrier(L) by XBOOLE_1:36;
then consider Lb being Linear_Combination of V such that
A12:Carrier(Lb) = Btm by Lm9;
consider Ft being FinSequence of the carrier of V such that
A13:Ft is one-to-one & rng Ft = Carrier(Lt) & Sum(Lt) = Sum(Lt (#) Ft)
by RLVECT_2:def 10;
consider Fm being FinSequence of the carrier of V such that
A14:Fm is one-to-one & rng Fm = Carrier(Lm) & Sum(Lm) = Sum(Lm (#) Fm)
by RLVECT_2:def 10;
consider Fb being FinSequence of the carrier of V such that
A15:Fb is one-to-one & rng Fb = Carrier(Lb) & Sum(Lb) = Sum(Lb (#) Fb)
by RLVECT_2:def 10;
deffunc F(set) = L1.(Ft.$1);
consider ft being FinSequence such that
A16:len ft = len Ft &
for j being Nat st j in Seg (len Ft) holds ft.j = F(j) from SeqLambda;
rng ft c= REAL
proof
let y be set;
assume y in rng ft;
then consider x being set such that
A17: x in dom ft & ft.x = y by FUNCT_1:def 5;
Seg len ft c= NAT;
then dom ft c= NAT by FINSEQ_1:def 3;
then reconsider x as Nat by A17;
A18: x in Seg len Ft by A16,A17,FINSEQ_1:def 3;
then x in dom Ft by FINSEQ_1:def 3;
then Ft.x in rng Ft & rng Ft c= the carrier of V
by FINSEQ_1:def 4,FUNCT_1:12;
then reconsider Ftx = Ft.x as Element of V;
A19: ft.x = L1.(Ft.x) by A16,A18;
consider L1f being Function such that
A20: L1 = L1f & dom L1f = the carrier of V & rng L1f c= REAL
by FUNCT_2:def 2;
Ftx in dom L1f by A20;
then ft.x in rng L1f by A19,A20,FUNCT_1:12;
hence thesis by A17,A20;
end;
then reconsider ft as FinSequence of REAL by FINSEQ_1:def 4;
deffunc F(set) = L1.(Fm.$1);
consider fm1 being FinSequence such that
A21:len fm1 = len Fm &
for j being Nat st j in Seg (len Fm) holds fm1.j = F(j) from SeqLambda;
rng fm1 c= REAL
proof
let y be set;
assume y in rng fm1;
then consider x being set such that
A22: x in dom fm1 & fm1.x = y by FUNCT_1:def 5;
Seg len fm1 c= NAT;
then dom fm1 c= NAT by FINSEQ_1:def 3;
then reconsider x as Nat by A22;
A23: x in Seg len Fm by A21,A22,FINSEQ_1:def 3;
then x in dom Fm by FINSEQ_1:def 3;
then Fm.x in rng Fm & rng Fm c= the carrier of V
by FINSEQ_1:def 4,FUNCT_1:12;
then reconsider Fmx = Fm.x as Element of V;
A24: fm1.x = L1.(Fm.x) by A21,A23;
consider L1f being Function such that
A25: L1 = L1f & dom L1f = the carrier of V & rng L1f c= REAL
by FUNCT_2:def 2;
Fmx in dom L1f by A25;
then fm1.x in rng L1f by A24,A25,FUNCT_1:12;
hence thesis by A22,A25;
end;
then reconsider fm1 as FinSequence of REAL by FINSEQ_1:def 4;
deffunc F(set) = L2.(Fm.$1);
consider fm2 being FinSequence such that
A26:len fm2 = len Fm &
for j being Nat st j in Seg (len Fm) holds fm2.j = F(j) from SeqLambda;
rng fm2 c= REAL
proof
let y be set;
assume y in rng fm2;
then consider x being set such that
A27: x in dom fm2 & fm2.x = y by FUNCT_1:def 5;
Seg len fm2 c= NAT;
then dom fm2 c= NAT by FINSEQ_1:def 3;
then reconsider x as Nat by A27;
A28: x in Seg len Fm by A26,A27,FINSEQ_1:def 3;
then x in dom Fm by FINSEQ_1:def 3;
then Fm.x in rng Fm & rng Fm c= the carrier of V
by FINSEQ_1:def 4,FUNCT_1:12;
then reconsider Fmx = Fm.x as Element of V;
A29: fm2.x = L2.(Fm.x) by A26,A28;
consider L2f being Function such that
A30: L2 = L2f & dom L2f = the carrier of V & rng L2f c= REAL
by FUNCT_2:def 2;
Fmx in dom L2f by A30;
then fm2.x in rng L2f by A29,A30,FUNCT_1:12;
hence thesis by A27,A30;
end;
then reconsider fm2 as FinSequence of REAL by FINSEQ_1:def 4;
deffunc F(set) = L2.(Fb.$1);
consider fb being FinSequence such that
A31:len fb = len Fb &
for j being Nat st j in Seg (len Fb) holds fb.j = F(j) from SeqLambda;
rng fb c= REAL
proof
let y be set;
assume y in rng fb;
then consider x being set such that
A32: x in dom fb & fb.x = y by FUNCT_1:def 5;
Seg len fb c= NAT;
then dom fb c= NAT by FINSEQ_1:def 3;
then reconsider x as Nat by A32;
A33: x in Seg len Fb by A31,A32,FINSEQ_1:def 3;
then x in dom Fb by FINSEQ_1:def 3;
then Fb.x in rng Fb & rng Fb c= the carrier of V
by FINSEQ_1:def 4,FUNCT_1:12;
then reconsider Fbx = Fb.x as Element of V;
A34: fb.x = L2.(Fb.x) by A31,A33;
consider L2f being Function such that
A35: L2 = L2f & dom L2f = the carrier of V & rng L2f c= REAL
by FUNCT_2:def 2;
Fbx in dom L2f by A35;
then fb.x in rng L2f by A34,A35,FUNCT_1:12;
hence thesis by A32,A35;
end;
then reconsider fb as FinSequence of REAL by FINSEQ_1:def 4;
Carrier(r*L1) /\ Carrier((1-r)*L2) c= Carrier((1-r)*L2) by XBOOLE_1:17;
then A36:rng Ft misses rng Fm by A10,A11,A13,A14,XBOOLE_1:85;
Carrier(r*L1) /\ Carrier((1-r)*L2) c= Carrier(r*L1) by XBOOLE_1:17;
then A37:rng Fm misses rng Fb by A11,A12,A14,A15,XBOOLE_1:85;
A38:F1, Ft^Fm are_fiberwise_equipotent
proof
A39: Ft^Fm is one-to-one by A13,A14,A36,FINSEQ_3:98;
rng (Ft^Fm) = rng Ft \/ rng Fm by FINSEQ_1:44
.= ((Carrier(L1) \/ Carrier(L2)) \ Carrier(L2))
\/ (Carrier(L1) /\ Carrier(L2)) by A3,A8,A10,A11,A13,A14,Lm7
.= ( Carrier(L1) \ Carrier(L2) ) \/ ( Carrier(L2) \ Carrier(L2) )
\/ (Carrier(L1) /\ Carrier(L2)) by XBOOLE_1:42
.= ( Carrier(L1) \ Carrier(L2) ) \/ {}
\/ (Carrier(L1) /\ Carrier(L2)) by XBOOLE_1:37
.= Carrier(L1) \ (Carrier(L2) \ Carrier(L2)) by XBOOLE_1:52
.= Carrier(L1) \ {} by XBOOLE_1:37
.= rng F1 by A4;
hence thesis by A4,A39,VECTSP_9:4;
end;
f1, ft^fm1 are_fiberwise_equipotent
proof
A40: dom L1 = the carrier of V by PRALG_3:4;
A41: for x being set holds x in dom f1 iff x in dom F1 & F1.x in dom L1
proof
let x be set;
A42: now assume x in dom f1;
then x in Seg len F1 by A5,FINSEQ_1:def 3;
hence x in dom F1 by FINSEQ_1:def 3;
then F1.x in rng F1 by FUNCT_1:12;
hence F1.x in dom L1 by A4,A40;
end;
now assume x in dom F1 & F1.x in dom L1;
then x in Seg len F1 by FINSEQ_1:def 3;
hence x in dom f1 by A5,FINSEQ_1:def 3;
end;
hence thesis by A42;
end;
for x being set st x in dom f1 holds f1.x = L1.(F1.x)
proof
let x be set;
assume
A43: x in dom f1;
Seg len f1 c= NAT;
then dom f1 c= NAT by FINSEQ_1:def 3;
then reconsider n = x as Nat by A43;
f1.n = L1.(F1.n) by A5,A43;
hence f1.x = L1.(F1.x);
end;
then A44: f1 = L1*F1 by A41,FUNCT_1:20;
A45: rng (Ft^Fm) = Carrier(Lt) \/ Carrier(Lm) by A13,A14,FINSEQ_1:44;
A46: for x being set holds
x in dom (ft^fm1) iff x in dom(Ft^Fm) & (Ft^Fm).x in dom L1
proof
let x be set;
A47: len (ft^fm1) = len ft + len fm1 by FINSEQ_1:35
.= len (Ft^Fm) by A16,A21,FINSEQ_1:35;
A48: dom(ft^fm1) = Seg len(ft^fm1) by FINSEQ_1:def 3
.= dom (Ft^Fm) by A47,FINSEQ_1:def 3;
x in dom (ft^fm1) implies (Ft^Fm).x in dom L1
proof
assume x in dom (ft^fm1);
then (Ft^Fm).x in rng (Ft^Fm) by A48,FUNCT_1:12;
then A49: (Ft^Fm).x in Carrier(Lt) \/ Carrier(Lm) by A13,A14,FINSEQ_1:44;
dom L1 = the carrier of V by PRALG_3:4;
hence thesis by A49;
end;
hence thesis by A48;
end;
for x being set st x in dom(ft^fm1) holds (ft^fm1).x = L1.((Ft^Fm).x)
proof
let x be set;
assume
A50: x in dom (ft^fm1);
Seg len (ft^fm1) c= NAT;
then dom (ft^fm1) c= NAT by FINSEQ_1:def 3;
then reconsider n = x as Nat by A50;
now per cases by A50,FINSEQ_1:38;
suppose
A51: n in dom ft;
then A52: n in Seg len Ft by A16,FINSEQ_1:def 3;
then ft.n = L1.(Ft.n) by A16;
then A53: (ft^fm1).n = L1.(Ft.n) by A51,FINSEQ_1:def 7;
n in dom Ft by A52,FINSEQ_1:def 3;
hence thesis by A53,FINSEQ_1:def 7;
suppose ex m being Nat st m in dom fm1 & n = len ft + m;
then consider m being Nat such that
A54: m in dom fm1 & n = len ft + m;
A55: m in Seg len Fm by A21,A54,FINSEQ_1:def 3;
A56: (ft^fm1).n = fm1.m by A54,FINSEQ_1:def 7
.= L1.(Fm.m) by A21,A55;
m in dom Fm & n = len Ft + m by A16,A54,A55,FINSEQ_1:def 3;
hence thesis by A56,FINSEQ_1:def 7;
end;
hence thesis;
end;
then A57: (ft^fm1) = L1*(Ft^Fm) by A46,FUNCT_1:20;
dom F1 = dom (Ft^Fm) by A38,RFINSEQ:16;
hence thesis by A4,A38,A40,A44,A45,A57,BAGORDER:4;
end;
then A58:Sum(f1) = Sum(ft^fm1) by RFINSEQ:22;
A59:F2, Fm^Fb are_fiberwise_equipotent
proof
A60: Fm^Fb is one-to-one by A14,A15,A37,FINSEQ_3:98;
rng (Fm^Fb) = (Carrier(L) \ Carrier(r*L1))
\/ (Carrier(r*L1) /\ Carrier((1-r)*L2)) by A11,A12,A14,A15,FINSEQ_1:44
.= ((Carrier(L1) \/ Carrier(L2)) \ Carrier(L1))
\/ (Carrier(L1) /\ Carrier(L2)) by A3,A8,Lm7
.= ( Carrier(L1) \ Carrier(L1) ) \/ ( Carrier(L2) \ Carrier(L1) )
\/ (Carrier(L1) /\ Carrier(L2)) by XBOOLE_1:42
.= ( Carrier(L2) \ Carrier(L1) ) \/ {}
\/ (Carrier(L1) /\ Carrier(L2)) by XBOOLE_1:37
.= Carrier(L2) \ (Carrier(L1) \ Carrier(L1)) by XBOOLE_1:52
.= Carrier(L2) \ {} by XBOOLE_1:37
.= rng F2 by A6;
hence thesis by A6,A60,VECTSP_9:4;
end;
f2, fm2^fb are_fiberwise_equipotent
proof
A61: dom L2 = the carrier of V by PRALG_3:4;
A62: for x being set holds x in dom f2 iff x in dom F2 & F2.x in dom L2
proof
let x be set;
A63: now assume
x in dom f2;
then x in Seg len F2 by A7,FINSEQ_1:def 3;
hence x in dom F2 by FINSEQ_1:def 3;
then F2.x in rng F2 by FUNCT_1:12;
hence F2.x in dom L2 by A6,A61;
end;
now assume x in dom F2 & F2.x in dom L2;
then x in Seg len F2 by FINSEQ_1:def 3;
hence x in dom f2 by A7,FINSEQ_1:def 3;
end;
hence thesis by A63;
end;
for x being set st x in dom f2 holds f2.x = L2.(F2.x)
proof
let x be set;
assume
A64: x in dom f2;
Seg len f2 c= NAT;
then dom f2 c= NAT by FINSEQ_1:def 3;
then reconsider n = x as Nat by A64;
f2.n = L2.(F2.n) by A7,A64;
hence f2.x = L2.(F2.x);
end;
then A65: f2 = L2*F2 by A62,FUNCT_1:20;
A66: rng (Fm^Fb) = Carrier(Lm) \/ Carrier(Lb) by A14,A15,FINSEQ_1:44;
A67: for x being set holds
x in dom (fm2^fb) iff x in dom(Fm^Fb) & (Fm^Fb).x in dom L2
proof
let x be set;
A68: len (fm2^fb) = len fm2 + len fb by FINSEQ_1:35
.= len (Fm^Fb) by A26,A31,FINSEQ_1:35;
A69: dom(fm2^fb) = Seg len(fm2^fb) by FINSEQ_1:def 3
.= dom (Fm^Fb) by A68,FINSEQ_1:def 3;
x in dom (fm2^fb) implies (Fm^Fb).x in dom L2
proof
assume x in dom (fm2^fb);
then (Fm^Fb).x in rng (Fm^Fb) by A69,FUNCT_1:12;
then A70: (Fm^Fb).x in Carrier(Lm) \/ Carrier(Lb) by A14,A15,FINSEQ_1:44;
dom L2 = the carrier of V by PRALG_3:4;
hence thesis by A70;
end;
hence thesis by A69;
end;
for x being set st x in dom(fm2^fb) holds (fm2^fb).x = L2.((Fm^Fb).x)
proof
let x be set;
assume
A71: x in dom (fm2^fb);
Seg len (fm2^fb) c= NAT;
then dom (fm2^fb) c= NAT by FINSEQ_1:def 3;
then reconsider n = x as Nat by A71;
now per cases by A71,FINSEQ_1:38;
suppose
A72: n in dom fm2;
then A73: n in Seg len Fm by A26,FINSEQ_1:def 3;
then fm2.n = L2.(Fm.n) by A26;
then A74: (fm2^fb).n = L2.(Fm.n) by A72,FINSEQ_1:def 7;
n in dom Fm by A73,FINSEQ_1:def 3;
hence thesis by A74,FINSEQ_1:def 7;
suppose ex m being Nat st m in dom fb & n = len fm2 + m;
then consider m being Nat such that
A75: m in dom fb & n = len fm2 + m;
A76: m in Seg len Fb by A31,A75,FINSEQ_1:def 3;
A77: (fm2^fb).n = fb.m by A75,FINSEQ_1:def 7
.= L2.(Fb.m) by A31,A76;
m in dom Fb & n = len Fm + m by A26,A75,A76,FINSEQ_1:def 3;
hence thesis by A77,FINSEQ_1:def 7;
end;
hence thesis;
end;
then A78: (fm2^fb) = L2*(Fm^Fb) by A67,FUNCT_1:20;
dom F2 = dom (Fm^Fb) by A59,RFINSEQ:16;
hence thesis by A6,A59,A61,A65,A66,A78,BAGORDER:4;
end;
then A79:Sum(f2) = Sum(fm2^fb) by RFINSEQ:22;
set F = Ft^Fm^Fb;
set f = (r*ft)^(r*fm1 + (1-r)*fm2)^((1-r)*fb);
A80:rng (Ft^Fm) = Carrier(L1) by A4,A38,RFINSEQ:1;
A81:rng Fb = Carrier(L) \ Carrier(L1) by A1,A12,A15,RLVECT_2:65;
then A82:rng (Ft^Fm) misses rng Fb by A80,XBOOLE_1:79;
Ft^Fm is one-to-one by A13,A14,A36,FINSEQ_3:98;
then A83:F is one-to-one by A15,A82,FINSEQ_3:98;
A84:Carrier(L1) c= Carrier(L) by A8,A9,XBOOLE_1:7;
A85:rng F = Carrier(L1) \/ (Carrier(L) \ Carrier(L1)) by A80,A81,FINSEQ_1:44
.= Carrier(L1) \/ Carrier(L) by XBOOLE_1:39
.= Carrier(L) by A84,XBOOLE_1:12;
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
proof
A86: len (r*fm1) = len fm1 by EUCLID_2:8
.= len ((1-r)*fm2) by A21,A26,EUCLID_2:8;
len f = len ((r*ft)^(r*fm1 + (1-r)*fm2)) + len((1-r)*fb) by FINSEQ_1:35
.= len(r*ft) + len(r*fm1 + (1-r)*fm2) + len((1-r)*fb) by FINSEQ_1:35
.= len ft + len(r*fm1 + (1-r)*fm2) + len((1-r)*fb) by EUCLID_2:8
.= len ft + len(r*fm1 + (1-r)*fm2) + len fb by EUCLID_2:8
.= len ft + len (r*fm1) + len fb by A86,INTEGRA5:2
.= len Ft + len Fm + len Fb by A16,A21,A31,EUCLID_2:8
.= len (Ft^Fm) + len Fb by FINSEQ_1:35;
hence len f = len F by FINSEQ_1:35;
Sum(f) = Sum((r*ft)^(r*fm1 + (1-r)*fm2)) + Sum((1-r)*fb) by RVSUM_1:105
.= Sum(r*ft) + Sum(r*fm1 + (1-r)*fm2) + Sum((1-r)*fb) by RVSUM_1:105
.= r*Sum(ft) + Sum(r*fm1 + (1-r)*fm2) + Sum((1-r)*fb) by RVSUM_1:117
.= r*Sum(ft) + Sum(r*fm1 + (1-r)*fm2) + (1-r)*Sum(fb) by RVSUM_1:117
.= r*Sum(ft) + ( Sum(r*fm1) + Sum((1-r)*fm2) ) + (1-r)*Sum(fb)
by A86,INTEGRA5:2
.= r*Sum(ft)+( r*Sum(fm1) + Sum((1-r)*fm2) )+(1-r)*Sum(fb) by RVSUM_1:117
.= r*Sum(ft)+( r*Sum(fm1) + (1-r)*Sum(fm2) )+(1-r)*Sum(fb) by RVSUM_1:117
.= r*Sum(ft)+ r*Sum(fm1) + (1-r)*Sum(fm2) +(1-r)*Sum(fb) by XCMPLX_1:1
.= r*(Sum(ft)+Sum(fm1)) + (1-r)*Sum(fm2) +(1-r)*Sum(fb) by XCMPLX_1:8
.= r*(Sum(ft)+Sum(fm1)) + ((1-r)*Sum(fm2) +(1-r)*Sum(fb)) by XCMPLX_1:1
.= r*(Sum(ft)+Sum(fm1)) + (1-r)*(Sum(fm2)+Sum(fb)) by XCMPLX_1:8
.= r*(Sum(ft^fm1)) + (1-r)*(Sum(fm2)+Sum(fb)) by RVSUM_1:105
.= r*1 + (1-r)*1 by A5,A7,A58,A79,RVSUM_1:105
.= r + 1 - r by XCMPLX_1:29
.= r - r + 1 by XCMPLX_1:29
.= 0 + 1 by XCMPLX_1:14;
hence Sum(f) = 1;
for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0
proof
let n be Nat;
assume
A87: n in dom f;
now per cases by A87,FINSEQ_1:38;
suppose
A88: n in dom ((r*ft)^(r*fm1 + (1-r)*fm2));
then A89: f.n = ((r*ft)^(r*fm1 + (1-r)*fm2)).n by FINSEQ_1:def 7;
now per cases by A88,FINSEQ_1:38;
suppose
A90: n in dom(r*ft);
then n in dom ft by RVSUM_1:65;
then A91: n in Seg len Ft by A16,FINSEQ_1:def 3;
A92: f.n = (r*ft).n by A89,A90,FINSEQ_1:def 7
.= r*(ft.n) by RVSUM_1:66
.= r*(L1.(Ft.n)) by A16,A91;
A93: n in dom Ft by A91,FINSEQ_1:def 3;
then A94: Ft.n in rng Ft by FUNCT_1:12;
A95: Ft.n in Carrier(Lt) by A13,A93,FUNCT_1:12;
then reconsider Ftn = Ft.n as Element of V;
Ft.n in Carrier(L) & not Ft.n in Carrier(L2)
by A8,A10,A95,XBOOLE_0:def 4;
then L2.(Ftn) = 0 by RLVECT_2:28;
then (1-r)*L2.(Ftn) = 0;
then ((1-r)*L2).(Ftn) = 0 by RLVECT_2:def 13;
then A96: f.n = (r*L1).(Ftn) + ((1-r)*L2).(Ftn) by A92,RLVECT_2:def 13
.= (r*L1 + (1-r)*L2).(Ft.n) by RLVECT_2:def 12;
len((r*ft)^(r*fm1+(1-r)*fm2))
= len(r*ft) + len(r*fm1 + (1-r)*fm2) by FINSEQ_1:35
.= len ft + len(r*fm1 + (1-r)*fm2) by EUCLID_2:8
.= len ft + len (r*fm1) by A86,INTEGRA5:2
.= len Ft + len Fm by A16,A21,EUCLID_2:8
.= len (Ft^Fm) by FINSEQ_1:35;
then n in Seg len(Ft^Fm) by A88,FINSEQ_1:def 3;
then n in dom (Ft^Fm) by FINSEQ_1:def 3;
then (Ft^Fm).n = F.n by FINSEQ_1:def 7;
hence f.n = L.(F.n) by A93,A96,FINSEQ_1:def 7;
rng Ft c= rng (Ft^Fm) by FINSEQ_1:42;
then Ft.n in rng (Ft^Fm) by A94;
then Ft.n in rng F1 by A38,RFINSEQ:1;
then consider m' being set such that
A97: m' in dom F1 & F1.m' = Ft.n by FUNCT_1:def 5;
Seg len F1 c= NAT;
then dom F1 c= NAT by FINSEQ_1:def 3;
then reconsider m' as Nat by A97;
m' in Seg len f1 by A5,A97,FINSEQ_1:def 3;
then m' in dom f1 by FINSEQ_1:def 3;
then f1.m' = L1.(F1.m') & f1.m' >= 0 by A5;
hence f.n >= 0 by A1,A92,A97,SQUARE_1:19;
suppose
ex k being Nat st k in dom(r*fm1 + (1-r)*fm2) &
n = len(r*ft) + k;
then consider m being Nat such that
A98: m in dom(r*fm1 + (1-r)*fm2) & n=len(r*ft)+m;
len (r*fm1) = len fm1 by EUCLID_2:8
.= len ((1-r)*fm2) by A21,A26,EUCLID_2:8;
then len (r*fm1 + (1-r)*fm2) = len (r*fm1) by INTEGRA5:2
.= len fm1 by EUCLID_2:8;
then A99: m in Seg len Fm by A21,A98,FINSEQ_1:def 3;
A100: f.n = (r*fm1 + (1-r)*fm2).m by A89,A98,FINSEQ_1:def 7
.= (r*fm1).m + ((1-r)*fm2).m by A98,RVSUM_1:26
.= r*(fm1.m) + ((1-r)*fm2).m by RVSUM_1:66
.= r*(fm1.m) + (1-r)*(fm2.m) by RVSUM_1:66
.= r*(L1.(Fm.m)) + (1-r)*(fm2.m) by A21,A99
.= r*(L1.(Fm.m)) + (1-r)*(L2.(Fm.m)) by A26,A99;
A101: m in dom Fm by A99,FINSEQ_1:def 3;
then A102: Fm.m in rng Fm by FUNCT_1:12;
then reconsider Fmm = Fm.m as Element of V by A14;
r*(L1.(Fmm)) = (r*L1).(Fm.m) &
(1-r)*(L2.(Fmm)) = ((1-r)*L2).(Fm.m) by RLVECT_2:def 13;
then A103: f.n = (r*L1 + (1-r)*L2).(Fm.m) by A100,RLVECT_2:def 12;
len((r*ft)^(r*fm1+(1-r)*fm2))
= len(r*ft) + len(r*fm1 + (1-r)*fm2) by FINSEQ_1:35
.= len ft + len(r*fm1 + (1-r)*fm2) by EUCLID_2:8
.= len ft + len (r*fm1) by A86,INTEGRA5:2
.= len Ft + len Fm by A16,A21,EUCLID_2:8
.= len (Ft^Fm) by FINSEQ_1:35;
then n in Seg len(Ft^Fm) by A88,FINSEQ_1:def 3;
then n in dom (Ft^Fm) by FINSEQ_1:def 3;
then A104: (Ft^Fm).n = F.n by FINSEQ_1:def 7;
len(r*ft) = len Ft by A16,EUCLID_2:8;
hence f.n = L.(F.n) by A98,A101,A103,A104,FINSEQ_1:def 7;
rng Fm c= rng (Ft^Fm) by FINSEQ_1:43;
then Fm.m in rng (Ft^Fm) by A102;
then Fm.m in rng F1 by A38,RFINSEQ:1;
then consider m' being set such that
A105: m' in dom F1 & F1.m' = Fm.m by FUNCT_1:def 5;
Seg len F1 c= NAT;
then dom F1 c= NAT by FINSEQ_1:def 3;
then reconsider m' as Nat by A105;
m' in Seg len F1 by A105,FINSEQ_1:def 3;
then m' in dom f1 by A5,FINSEQ_1:def 3;
then f1.m' = L1.(F1.m') & f1.m' >= 0 by A5;
then A106: r*L1.(Fm.m) >= 0 by A1,A105,SQUARE_1:19;
rng Fm c= rng (Fm^Fb) by FINSEQ_1:42;
then Fm.m in rng (Fm^Fb) by A102;
then Fm.m in rng F2 by A59,RFINSEQ:1;
then consider m' being set such that
A107: m' in dom F2 & F2.m' = Fm.m by FUNCT_1:def 5;
Seg len F2 c= NAT;
then dom F2 c= NAT by FINSEQ_1:def 3;
then reconsider m' as Nat by A107;
m' in Seg len F2 by A107,FINSEQ_1:def 3;
then m' in dom f2 by A7,FINSEQ_1:def 3;
then f2.m' = L2.(F2.m') & f2.m' >= 0 by A7;
then (1-r)*L2.(Fm.m) >= 0 by A2,A107,SQUARE_1:19;
then r*(L1.(Fm.m)) + (1-r)*(L2.(Fm.m)) >= 0 + 0 by A106,REAL_1:55;
hence f.n >= 0 by A100;
end;
hence thesis;
suppose ex m being Nat st m in dom((1-r)*fb) &
n = len ((r*ft)^(r*fm1 + (1-r)*fm2)) + m;
then consider m being Nat such that
A108: m in dom((1-r)*fb) & n=len((r*ft)^(r*fm1+(1-r)*fm2))+m;
m in dom fb by A108,RVSUM_1:65;
then A109: m in Seg len Fb by A31,FINSEQ_1:def 3;
A110: f.n = ((1-r)*fb).m by A108,FINSEQ_1:def 7
.= (1-r)*(fb.m) by RVSUM_1:66
.= (1-r)*(L2.(Fb.m)) by A31,A109;
A111: m in dom Fb by A109,FINSEQ_1:def 3;
then A112: Fb.m in rng Fb by FUNCT_1:12;
then reconsider Fbm = Fb.m as Element of V by A15;
Fb.m in Carrier(L) & not Fb.m in Carrier(L1)
by A8,A12,A15,A112,XBOOLE_0:def 4;
then L1.(Fbm) = 0 by RLVECT_2:28;
then r*L1.(Fbm) = 0;
then (r*L1).(Fbm) = 0 by RLVECT_2:def 13;
then A113: f.n = (r*L1).(Fbm) + ((1-r)*L2).(Fbm) by A110,RLVECT_2:def 13
.= (r*L1 + (1-r)*L2).(Fb.m) by RLVECT_2:def 12;
len((r*ft)^(r*fm1+(1-r)*fm2))
= len(r*ft) + len(r*fm1 + (1-r)*fm2) by FINSEQ_1:35
.= len ft + len(r*fm1 + (1-r)*fm2) by EUCLID_2:8
.= len ft + len (r*fm1) by A86,INTEGRA5:2
.= len Ft + len Fm by A16,A21,EUCLID_2:8
.= len (Ft^Fm) by FINSEQ_1:35;
hence f.n = L.(F.n) by A108,A111,A113,FINSEQ_1:def 7;
rng Fb c= rng (Fm^Fb) by FINSEQ_1:43;
then Fb.m in rng (Fm^Fb) by A112;
then Fb.m in rng F2 by A59,RFINSEQ:1;
then consider m' being set such that
A114: m' in dom F2 & F2.m' = Fb.m by FUNCT_1:def 5;
Seg len F2 c= NAT;
then dom F2 c= NAT by FINSEQ_1:def 3;
then reconsider m' as Nat by A114;
m' in Seg len F2 by A114,FINSEQ_1:def 3;
then m' in dom f2 by A7,FINSEQ_1:def 3;
then f2.m' = L2.(F2.m') & f2.m' >= 0 by A7;
hence f.n >= 0 by A2,A110,A114,SQUARE_1:19;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A83,A85,CONVEX1:def 3;
end;
theorem
for V being RealLinearSpace, M being non empty Subset of V,
L1,L2 being Convex_Combination of M,
r being Real st 0 < r & r < 1 holds
r*L1 + (1-r)*L2 is Convex_Combination of M
proof
let V be RealLinearSpace;
let M be non empty Subset of V;
let L1,L2 be Convex_Combination of M;
let r be Real;
assume
A1:0 < r & r < 1;
A2:r*L1 is Linear_Combination of M by RLVECT_2:67;
(1-r)*L2 is Linear_Combination of M by RLVECT_2:67;
hence thesis by A1,A2,Th9,RLVECT_2:59;
end;
theorem
for V being RealLinearSpace holds
ex L being Linear_Combination of V st L is convex by Lm3;
theorem
for V being RealLinearSpace, M being non empty Subset of V holds
ex L being Linear_Combination of M st L is convex by Lm4;
begin :: Miscellaneous
theorem
for V being RealLinearSpace, W1,W2 being Subspace of V holds
Up(W1+W2) = Up(W1) + Up(W2) by Lm5;
theorem
for V being RealLinearSpace, W1,W2 being Subspace of V holds
Up(W1 /\ W2) = Up(W1) /\ Up(W2) by Lm6;
theorem
for V being RealLinearSpace, L1, L2 being Convex_Combination of V,
a,b being Real st a * b > 0 holds
Carrier(a*L1 + b*L2) = Carrier(a * L1) \/ Carrier(b * L2) by Lm7;
theorem
for F,G being Function st F,G are_fiberwise_equipotent
for x1,x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1,z2 being set st
z1 in dom G & z2 in dom G & z1 <> z2 & F.x1 = G.z1 & F.x2 = G.z2 by Lm8;
theorem
for V being RealLinearSpace, L being Linear_Combination of V,
A being Subset of V st A c= Carrier(L) holds
ex L1 being Linear_Combination of V st Carrier(L1) = A by Lm9;