:: Convex Sets and Convex Combinations
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received November 5, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

definition
let V be non empty RLSStruct ;
let M be Subset of V;
let r be Real;
funcr * M ->  Subset of V equals :: CONVEX1:def 1
 {  (r * v) where v is Element of V : v in M  }  ;
coherence
  {  (r * v) where v is Element of V : v in M  }  is Subset of V
proofend;
end;

:: deftheorem  defines * CONVEX1:def_1_:_
 for V being non empty RLSStruct
for M being Subset of V
for r being Real holds r * M =  {  (r * v) where v is Element of V : v in M  }  ;

definition
let V be non empty RLSStruct ;
let M be Subset of V;
attrM is convex  means :Def2: :: CONVEX1:def 2
 for u, v being VECTOR of V
for r being Real st 0 < r &amp; r < 1 &amp; u in M &amp; v in M holds
(r * u) + ((1 - r) * v) in M;
end;

:: deftheorem Def2 defines convex CONVEX1:def_2_:_
 for V being non empty RLSStruct
for M being Subset of V holds
( M is convex iff for u, v being VECTOR of V
for r being Real st 0 < r &amp; r < 1 &amp; u in M &amp; v in M holds
(r * u) + ((1 - r) * v) in M );

theorem :: CONVEX1:1
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r being Real st M is convex holds
r * M is convex
proofend;

theorem :: CONVEX1:2
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M, N being Subset of V st M is convex &amp; N is convex holds
M + N is convex
proofend;

theorem :: CONVEX1:3
for V being RealLinearSpace
for M, N being Subset of V st M is convex &amp; N is convex holds
M - N is convex
proofend;

theorem Th4: :: CONVEX1:4
for V being non empty RLSStruct
for M being Subset of V holds
( M is convex iff for r being Real st 0 < r &amp; r < 1 holds
(r * M) + ((1 - r) * M) c= M )
proofend;

theorem :: CONVEX1:5
for V being non empty Abelian RLSStruct
for M being Subset of V st M is convex holds
for r being Real st 0 < r &amp; r < 1 holds
((1 - r) * M) + (r * M) c= M
proofend;

theorem :: CONVEX1:6
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M, N being Subset of V st M is convex &amp; N is convex holds
for r being Real holds (r * M) + ((1 - r) * N) is convex
proofend;

Lm1:  for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V holds 1 * M = M
proofend;

Lm2:  for V being RealLinearSpace
for M being non empty Subset of V holds 0 * M = {(0. V)}
proofend;

Lm3:  for V being non empty add-associative addLoopStr
for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3)
proofend;

Lm4:  for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M
proofend;

Lm5:  for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2)
proofend;

theorem :: CONVEX1:7
for V being RealLinearSpace
for M being Subset of V
for v being VECTOR of V holds
( M is convex iff v + M is convex )
proofend;

theorem :: CONVEX1:8
for V being RealLinearSpace holds Up ((0). V) is convex
proofend;

theorem Th9: :: CONVEX1:9
for V being RealLinearSpace holds Up ((Omega). V) is convex
proofend;

theorem Th10: :: CONVEX1:10
for V being non empty RLSStruct
for M being Subset of V st M = {} holds
M is convex
proofend;

theorem Th11: :: CONVEX1:11
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r1, r2 being Real st M1 is convex &amp; M2 is convex holds
(r1 * M1) + (r2 * M2) is convex
proofend;

theorem Th12: :: CONVEX1:12
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds (r1 + r2) * M c= (r1 * M) + (r2 * M)
proofend;

Lm6:  for V being non empty RLSStruct
for M, N being Subset of V
for r being Real st M c= N holds
r * M c= r * N
proofend;

Lm7:  for V being non empty RLSStruct
for M being empty Subset of V
for r being Real holds r * M = {}
proofend;

Lm8:  for V being non empty addLoopStr
for M being empty Subset of V
for N being Subset of V holds M + N = {}
proofend;

Lm9:  for V being non empty right_zeroed addLoopStr
for M being Subset of V holds M + {(0. V)} = M
proofend;

Lm10:  for V being RealLinearSpace
for M being Subset of V
for r1, r2 being Real st r1 >= 0 &amp; r2 >= 0 &amp; M is convex holds
(r1 * M) + (r2 * M) c= (r1 + r2) * M
proofend;

theorem :: CONVEX1:13
for V being RealLinearSpace
for M being Subset of V
for r1, r2 being Real st r1 >= 0 &amp; r2 >= 0 &amp; M is convex holds
(r1 * M) + (r2 * M) = (r1 + r2) * M
proofend;

theorem :: CONVEX1:14
for V being non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2, M3 being Subset of V
for r1, r2, r3 being Real st M1 is convex &amp; M2 is convex &amp; M3 is convex holds
((r1 * M1) + (r2 * M2)) + (r3 * M3) is convex
proofend;

theorem Th15: :: CONVEX1:15
for V being non empty RLSStruct
for F being Subset-Family of V st ( for M being Subset of V st M in F holds
M is convex ) holds
meet F is convex
proofend;

theorem Th16: :: CONVEX1:16
for V being non empty RLSStruct
for M being Subset of V st M is Affine holds
M is convex
proofend;

registration
let V be non empty RLSStruct ;
cluster non empty convex for Element of K10( the carrier of V);
existence
 ex b1 being Subset of V st
( not b1 is empty &amp; b1 is convex )
proofend;
end;

registration
let V be non empty RLSStruct ;
cluster empty convex for Element of K10( the carrier of V);
existence
 ex b1 being Subset of V st
( b1 is empty &amp; b1 is convex )
proofend;
end;

theorem :: CONVEX1:17
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : u .|. v >= r  }  holds
M is convex
proofend;

theorem :: CONVEX1:18
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : u .|. v > r  }  holds
M is convex
proofend;

theorem :: CONVEX1:19
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : u .|. v <= r  }  holds
M is convex
proofend;

theorem :: CONVEX1:20
for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for v being VECTOR of V
for r being Real st M =  {  u where u is VECTOR of V : u .|. v < r  }  holds
M is convex
proofend;

begin

definition
let V be RealLinearSpace;
let L be Linear_Combination of V;
attrL is convex  means :Def3: :: CONVEX1:def 3
 ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; ex f being FinSequence of REAL st
( len f = len F &amp; Sum f = 1 &amp; ( for n being Nat st n in dom f holds
( f . n = L . (F . n) &amp; f . n >= 0 ) ) ) );
end;

:: deftheorem Def3 defines convex CONVEX1:def_3_:_
 for V being RealLinearSpace
for L being Linear_Combination of V holds
( L is convex iff ex F being FinSequence of the carrier of V st
( F is one-to-one &amp; rng F = Carrier L &amp; ex f being FinSequence of REAL st
( len f = len F &amp; Sum f = 1 &amp; ( for n being Nat st n in dom f holds
( f . n = L . (F . n) &amp; f . n >= 0 ) ) ) ) );

theorem Th21: :: CONVEX1:21
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex holds
Carrier L <> {}
proofend;

theorem :: CONVEX1:22
for V being RealLinearSpace
for L being Linear_Combination of V
for v being VECTOR of V st L is convex &amp; L . v <= 0 holds
not v in Carrier L
proofend;

theorem :: CONVEX1:23
for V being RealLinearSpace
for L being Linear_Combination of V st L is convex holds
L <> ZeroLC V
proofend;

Lm11:  for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st L is convex &amp; Carrier L = {v} holds
( L . v = 1 &amp; Sum L = (L . v) * v )
proofend;

Lm12:  for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of V st L is convex &amp; Carrier L = {v1,v2} &amp; v1 <> v2 holds
( (L . v1) + (L . v2) = 1 &amp; L . v1 >= 0 &amp; L . v2 >= 0 &amp; Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
proofend;

Lm13:  for p being FinSequence
for x, y, z being set st p is one-to-one &amp; rng p = {x,y,z} &amp; x <> y &amp; y <> z &amp; z <> x &amp; not p = <*x,y,z*> &amp; not p = <*x,z,y*> &amp; not p = <*y,x,z*> &amp; not p = <*y,z,x*> &amp; not p = <*z,x,y*> holds
p = <*z,y,x*>
proofend;

Lm14:  for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of {v1,v2,v3} st v1 <> v2 &amp; v2 <> v3 &amp; v3 <> v1 holds
Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3)
proofend;

Lm15:  for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of V st L is convex &amp; Carrier L = {v1,v2,v3} &amp; v1 <> v2 &amp; v2 <> v3 &amp; v3 <> v1 holds
( ((L . v1) + (L . v2)) + (L . v3) = 1 &amp; L . v1 >= 0 &amp; L . v2 >= 0 &amp; L . v3 >= 0 &amp; Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
proofend;

theorem :: CONVEX1:24
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of {v} st L is convex holds
( L . v = 1 &amp; Sum L = (L . v) * v )
proofend;

theorem :: CONVEX1:25
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of {v1,v2} st v1 <> v2 &amp; L is convex holds
( (L . v1) + (L . v2) = 1 &amp; L . v1 >= 0 &amp; L . v2 >= 0 &amp; Sum L = ((L . v1) * v1) + ((L . v2) * v2) )
proofend;

theorem :: CONVEX1:26
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of {v1,v2,v3} st v1 <> v2 &amp; v2 <> v3 &amp; v3 <> v1 &amp; L is convex holds
( ((L . v1) + (L . v2)) + (L . v3) = 1 &amp; L . v1 >= 0 &amp; L . v2 >= 0 &amp; L . v3 >= 0 &amp; Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) )
proofend;

theorem :: CONVEX1:27
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V st L is convex &amp; Carrier L = {v} holds
L . v = 1 by Lm11;

theorem :: CONVEX1:28
for V being RealLinearSpace
for v1, v2 being VECTOR of V
for L being Linear_Combination of V st L is convex &amp; Carrier L = {v1,v2} &amp; v1 <> v2 holds
( (L . v1) + (L . v2) = 1 &amp; L . v1 >= 0 &amp; L . v2 >= 0 ) by Lm12;

theorem :: CONVEX1:29
for V being RealLinearSpace
for v1, v2, v3 being VECTOR of V
for L being Linear_Combination of V st L is convex &amp; Carrier L = {v1,v2,v3} &amp; v1 <> v2 &amp; v2 <> v3 &amp; v3 <> v1 holds
( ((L . v1) + (L . v2)) + (L . v3) = 1 &amp; L . v1 >= 0 &amp; L . v2 >= 0 &amp; L . v3 >= 0 &amp; Sum L = (((L . v1) * v1) + ((L . v2) * v2)) + ((L . v3) * v3) ) by Lm15;

begin

definition
let V be non empty RLSStruct ;
let M be Subset of V;
func Convex-Family M ->  Subset-Family of V means :Def4: :: CONVEX1:def 4
 for N being Subset of V holds
( N in it iff ( N is convex &amp; M c= N ) );
existence
 ex b1 being Subset-Family of V st
for N being Subset of V holds
( N in b1 iff ( N is convex &amp; M c= N ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of V st ( for N being Subset of V holds
( N in b1 iff ( N is convex &amp; M c= N ) ) ) &amp; ( for N being Subset of V holds
( N in b2 iff ( N is convex &amp; M c= N ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Convex-Family CONVEX1:def_4_:_
 for V being non empty RLSStruct
for M being Subset of V
for b3 being Subset-Family of V holds
( b3 = Convex-Family M iff for N being Subset of V holds
( N in b3 iff ( N is convex &amp; M c= N ) ) );

definition
let V be non empty RLSStruct ;
let M be Subset of V;
func conv M ->  convex Subset of V equals :: CONVEX1:def 5
 meet (Convex-Family M);
coherence
 meet (Convex-Family M) is convex Subset of V
proofend;
end;

:: deftheorem  defines conv CONVEX1:def_5_:_
 for V being non empty RLSStruct
for M being Subset of V holds conv M = meet (Convex-Family M);

theorem :: CONVEX1:30
for V being non empty RLSStruct
for M being Subset of V
for N being convex Subset of V st M c= N holds
conv M c= N
proofend;

begin

theorem :: CONVEX1:31
for p being FinSequence
for x, y, z being set st p is one-to-one &amp; rng p = {x,y,z} &amp; x <> y &amp; y <> z &amp; z <> x &amp; not p = <*x,y,z*> &amp; not p = <*x,z,y*> &amp; not p = <*y,x,z*> &amp; not p = <*y,z,x*> &amp; not p = <*z,x,y*> holds
p = <*z,y,x*> by Lm13;

theorem :: CONVEX1:32
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V holds 1 * M = M by Lm1;

theorem :: CONVEX1:33
for V being non empty RLSStruct
for M being empty Subset of V
for r being Real holds r * M = {} by Lm7;

theorem :: CONVEX1:34
for V being RealLinearSpace
for M being non empty Subset of V holds 0 * M = {(0. V)} by Lm2;

theorem :: CONVEX1:35
for V being non empty right_zeroed addLoopStr
for M being Subset of V holds M + {(0. V)} = M by Lm9;

theorem :: CONVEX1:36
for V being non empty add-associative addLoopStr
for M1, M2, M3 being Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3) by Lm3;

theorem :: CONVEX1:37
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M being Subset of V
for r1, r2 being Real holds r1 * (r2 * M) = (r1 * r2) * M by Lm4;

theorem :: CONVEX1:38
for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for M1, M2 being Subset of V
for r being Real holds r * (M1 + M2) = (r * M1) + (r * M2) by Lm5;

theorem :: CONVEX1:39
for V being non empty RLSStruct
for M, N being Subset of V
for r being Real st M c= N holds
r * M c= r * N by Lm6;

theorem :: CONVEX1:40
for V being non empty addLoopStr
for M being empty Subset of V
for N being Subset of V holds M + N = {} by Lm8;

begin

:: from CONVEX2, 2008.07.07, A.T.
registration
let V be non empty RLSStruct ;
let M, N be convex Subset of V;
clusterM /\ N ->  convex for Subset of V;
coherence
 for b1 being Subset of V st b1 = M /\ N holds
b1 is convex
proofend;
end;

registration
let V be RealLinearSpace;
let M be Subset of V;
cluster Convex-Family M ->  non empty ;
coherence
 not Convex-Family M is empty
proofend;
end;

theorem :: CONVEX1:41
for V being RealLinearSpace
for M being Subset of V holds M c= conv M
proofend;