:: Convex Sets and Convex Combinations :: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama :: :: Received November 5, 2002 :: Copyright (c) 2002-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, RLVECT_1, SUBSET_1, REAL_1, RELAT_1, CARD_1, ARYTM_3, ARYTM_1, TARSKI, SUPINF_2, ALGSTR_0, RUSUB_4, RLSUB_1, STRUCT_0, XXREAL_0, SETFAM_1, BHSP_1, PROB_2, RLVECT_2, FINSEQ_1, FUNCT_1, CARD_3, NAT_1, PARTFUN1, VALUED_1, CONVEX1; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, ALGSTR_0, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, NAT_1, REAL_1, PARTFUN1, FINSEQ_1, RLVECT_1, RLSUB_1, RLVECT_2, RVSUM_1, BHSP_1, RUSUB_4, RUSUB_5, XXREAL_0; constructors SETFAM_1, DOMAIN_1, XXREAL_0, REAL_1, PARTFUN1, BINOP_2, FINSEQ_4, FINSOP_1, RVSUM_1, RLVECT_2, RUSUB_5, RELSET_1; registrations SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, STRUCT_0, RLVECT_1, RUSUB_4, VALUED_0, FINSEQ_1, CARD_1, ORDINAL1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Convex Sets definition let V be non empty RLSStruct, M be Subset of V, r be Real; func r*M -> Subset of V equals :: CONVEX1:def 1 {r * v where v is Element of V: v in M}; end; definition let V be non empty RLSStruct, M be Subset of V; attr M is convex means :: CONVEX1:def 2 for u,v being VECTOR of V, r be Real st 0 < r & r < 1 & u in M & v in M holds r*u + (1-r)*v in M; end; theorem :: CONVEX1:1 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M being Subset of V, r being Real st M is convex holds r*M is convex; theorem :: CONVEX1:2 for V being Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M,N being Subset of V st M is convex & N is convex holds M + N is convex; theorem :: CONVEX1:3 for V being RealLinearSpace, M,N being Subset of V st M is convex & N is convex holds M - N is convex; theorem :: CONVEX1:4 for V being non empty RLSStruct, M being Subset of V holds M is convex iff for r being Real st 0 < r & r < 1 holds r*M + (1-r)*M c= M; theorem :: CONVEX1:5 for V being Abelian non empty RLSStruct, M being Subset of V st M is convex for r being Real st 0 < r & r < 1 holds (1-r)*M + r*M c= M; theorem :: CONVEX1:6 for V being Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M,N being Subset of V st M is convex & N is convex holds for r being Real holds r*M + (1-r)*N is convex; theorem :: CONVEX1:7 for V being RealLinearSpace, M being Subset of V, v being VECTOR of V holds M is convex iff v + M is convex; theorem :: CONVEX1:8 for V being RealLinearSpace holds Up((0).V) is convex; theorem :: CONVEX1:9 for V being RealLinearSpace holds Up((Omega).V) is convex; theorem :: CONVEX1:10 for V being non empty RLSStruct, M being Subset of V st M = {} holds M is convex; theorem :: CONVEX1:11 for V being Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M1,M2 being Subset of V, r1,r2 being Real st M1 is convex & M2 is convex holds r1*M1 + r2*M2 is convex; theorem :: CONVEX1:12 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M being Subset of V, r1,r2 being Real holds (r1 + r2)*M c= r1*M + r2*M; theorem :: CONVEX1:13 for V being RealLinearSpace, M being Subset of V, r1,r2 being Real st r1 >= 0 & r2 >= 0 & M is convex holds r1*M + r2*M = (r1 + r2)*M; theorem :: CONVEX1:14 for V being Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M1,M2,M3 being Subset of V, r1,r2,r3 being Real st M1 is convex & M2 is convex & M3 is convex holds r1*M1 + r2*M2 + r3*M3 is convex; theorem :: CONVEX1:15 for V being non empty RLSStruct, 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; theorem :: CONVEX1:16 for V being non empty RLSStruct, M being Subset of V st M is Affine holds M is convex; registration let V be non empty RLSStruct; cluster non empty convex for Subset of V; end; registration let V be non empty RLSStruct; cluster empty convex for Subset of V; end; theorem :: CONVEX1:17 for V being RealUnitarySpace-like non empty UNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : u .|. v >= r} holds M is convex; theorem :: CONVEX1:18 for V being RealUnitarySpace-like non empty UNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : u .|. v > r} holds M is convex; theorem :: CONVEX1:19 for V being RealUnitarySpace-like non empty UNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : u .|. v <= r} holds M is convex; theorem :: CONVEX1:20 for V being RealUnitarySpace-like non empty UNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : u .|. v < r} holds M is convex; begin :: Convex Combinations definition let V be RealLinearSpace, L be Linear_Combination of V; attr L is convex means :: CONVEX1:def 3 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; end; theorem :: CONVEX1:21 for V being RealLinearSpace, L being Linear_Combination of V st L is convex holds Carrier(L) <> {}; theorem :: CONVEX1:22 for V being RealLinearSpace, L being Linear_Combination of V, v being VECTOR of V st L is convex & L.v <= 0 holds not v in Carrier(L); theorem :: CONVEX1:23 for V being RealLinearSpace, L being Linear_Combination of V st L is convex holds L <> ZeroLC(V); theorem :: CONVEX1:24 for V being RealLinearSpace, v being VECTOR of V, L being Linear_Combination of {v} st L is convex holds L.v = 1 & Sum(L) = L.v * v; theorem :: CONVEX1:25 for V being RealLinearSpace, v1,v2 being VECTOR of V, L being Linear_Combination of {v1,v2} st v1 <> v2 & L is convex holds L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2; theorem :: CONVEX1:26 for V being RealLinearSpace, v1,v2,v3 being VECTOR of V, L being Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex holds L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 & Sum(L ) = L.v1 * v1 + L.v2 * v2 + L.v3 * v3; theorem :: CONVEX1:27 for V being RealLinearSpace, v being VECTOR of V, L being Linear_Combination of V st L is convex & Carrier(L) = {v} holds L.v = 1 ; theorem :: CONVEX1:28 for V being RealLinearSpace, v1,v2 being VECTOR of V, L being Linear_Combination of V st L is convex & Carrier(L) = {v1,v2} & v1 <> v2 holds L.v1 + L.v2 = 1 & L.v1 >= 0 & L.v2 >= 0; theorem :: CONVEX1:29 for V being RealLinearSpace, v1,v2,v3 being VECTOR of V, L being Linear_Combination of V st L is convex & Carrier(L) = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds L.v1 + L.v2 + L.v3 = 1 & L.v1 >= 0 & L.v2 >= 0 & L.v3 >= 0 & Sum(L) = L.v1 * v1 + L.v2 * v2 + L.v3 * v3; begin :: Convex Hull definition let V be non empty RLSStruct, M be Subset of V; func Convex-Family M -> Subset-Family of V means :: CONVEX1:def 4 for N being Subset of V holds N in it iff N is convex & M c= N; end; definition let V be non empty RLSStruct, M be Subset of V; func conv(M) -> convex Subset of V equals :: CONVEX1:def 5 meet (Convex-Family M); end; theorem :: CONVEX1:30 for V being non empty RLSStruct, M being Subset of V, N being convex Subset of V st M c= N holds conv(M) c= N; begin :: Miscellaneous theorem :: CONVEX1:31 for p being FinSequence, x,y,z being set st p is one-to-one & rng p = {x,y,z} & x <> y & y <> z & z <> x holds p = <* x,y,z *> or p = <* x,z,y *> or p = <* y,x,z *> or p = <* y,z,x *> or p = <* z,x,y *> or p = <* z,y,x *>; theorem :: CONVEX1:32 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M being Subset of V holds 1*M = M; theorem :: CONVEX1:33 for V being non empty RLSStruct, M being empty Subset of V, r being Real holds r * M = {}; theorem :: CONVEX1:34 for V being RealLinearSpace, M be non empty Subset of V holds 0 * M = {0.V}; theorem :: CONVEX1:35 for V being right_zeroed non empty addLoopStr, M being Subset of V holds M + {0.V} = M; theorem :: CONVEX1:36 for V be add-associative non empty addLoopStr, M1,M2,M3 be Subset of V holds (M1 + M2) + M3 = M1 + (M2 + M3); theorem :: CONVEX1:37 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M being Subset of V, r1,r2 being Real holds r1*(r2*M) = (r1*r2)*M; theorem :: CONVEX1:38 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, M1,M2 being Subset of V, r being Real holds r*(M1 + M2) = r*M1 + r*M2; theorem :: CONVEX1:39 for V being non empty RLSStruct, M,N being Subset of V, r being Real st M c= N holds r*M c= r*N; theorem :: CONVEX1:40 for V being non empty addLoopStr, M being empty Subset of V, N being Subset of V holds M + N = {}; begin ::Addenda :: from CONVEX2, 2008.07.07, A.T. registration let V be non empty RLSStruct, M,N be convex Subset of V; cluster M /\ N -> convex for Subset of V; end; registration let V be RealLinearSpace, M be Subset of V; cluster Convex-Family M -> non empty; end; theorem :: CONVEX1:41 for V being RealLinearSpace, M being Subset of V holds M c= conv(M);