:: 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 S₁[ 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 b₁ being set st
for L being set holds
( L in b₁ iff L is Linear_Combination of M )

proof end;

uniqueness
for b₁, b₂ being set st ( for L being set holds
( L in b₁ iff L is Linear_Combination of M ) ) & ( for L being set holds
( L in b₂ iff L is Linear_Combination of M ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines LinComb CONVEX2:def 1 :
for V being RealLinearSpace
for M being Subset of V
for b₃ being set holds
( b₃ = LinComb M iff for L being set holds
( L in b₃ 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 b₁ being Linear_Combination of V st b₁ 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 b₁ being Linear_Combination of M st b₁ 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;