:: Some Properties for Convex Combinations
:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003-2011 Association of Mizar Users


begin

reconsider rr = 1 as Real ;

set ff = <*rr*>;

theorem :: CONVEX2:1
for V being non empty RLSStruct
for M, N being convex Subset of V holds M /\ N is convex ;

theorem :: CONVEX2:2
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of 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 end;

theorem :: CONVEX2:3
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of 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 end;

theorem :: CONVEX2:4
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of 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 end;

theorem :: CONVEX2:5
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of 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 end;

Lm1: for V being 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
proof end;

Lm2: for V being RealLinearSpace
for M being Subset of V st ( 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 ) holds
M is convex
proof end;

theorem :: CONVEX2:6
for V being RealLinearSpace
for M being Subset of V holds
( ( 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 ) iff M is convex ) by Lm1, Lm2;

definition
let V be RealLinearSpace;
let M be Subset of V;
defpred S1[ set ] means $1 is Linear_Combination of M;
func LinComb M -> set means :: CONVEX2:def 1
for L being set holds
( L in it iff L is Linear_Combination of M );
existence
ex b1 being set st
for L being set holds
( L in b1 iff L is Linear_Combination of M )
proof end;
uniqueness
for b1, b2 being set st ( for L being set holds
( L in b1 iff L is Linear_Combination of M ) ) & ( for L being set holds
( L in b2 iff L is Linear_Combination of M ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines LinComb CONVEX2:def 1 :
for V being RealLinearSpace
for M being Subset of V
for b3 being set holds
( b3 = LinComb M iff for L being set holds
( L in b3 iff L is Linear_Combination of M ) );

Lm3: for V being RealLinearSpace ex L being Linear_Combination of V st L is convex
proof end;

registration
let V be RealLinearSpace;
cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V119() V120() V121() convex Linear_Combination of V;
existence
ex b1 being Linear_Combination of V st b1 is convex
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
for M being non empty Subset of V ex L being Linear_Combination of M st L is convex
proof end;

registration
let V be RealLinearSpace;
let M be non empty Subset of V;
cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V119() V120() V121() convex Linear_Combination of M;
existence
ex b1 being Linear_Combination of M st b1 is convex
by Lm4;
end;

definition
let V be RealLinearSpace;
let M be non empty Subset of V;
mode Convex_Combination of M is convex Linear_Combination of M;
end;

Lm5: for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2)
proof end;

Lm6: for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2)
proof end;

theorem :: CONVEX2:7
for V being RealLinearSpace
for M being Subset of V holds Convex-Family M <> {} ;

Lm7: for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))
proof end;

Lm8: for F, G being Function st F,G are_fiberwise_equipotent holds
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 end;

Lm9: for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A
proof end;

theorem :: CONVEX2:8
canceled;

theorem Th9: :: CONVEX2:9
for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V
proof end;

theorem :: CONVEX2:10
for V being RealLinearSpace
for M being non empty Subset of V
for L1, L2 being Convex_Combination of M
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M
proof end;

theorem :: CONVEX2:11
for V being RealLinearSpace ex L being Linear_Combination of V st L is convex by Lm3;

theorem :: CONVEX2:12
for V being RealLinearSpace
for M being non empty Subset of V ex L being Linear_Combination of M st L is convex by Lm4;

begin

theorem :: CONVEX2:13
for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2) by Lm5;

theorem :: CONVEX2:14
for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2) by Lm6;

theorem :: CONVEX2:15
for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by Lm7;

theorem :: CONVEX2:16
for F, G being Function st F,G are_fiberwise_equipotent holds
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 :: CONVEX2:17
for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A by Lm9;