:: Convex Sets and Convex Combinations on Complex Linear Spaces :: by Hidenori Matsuzaki , Noboru Endou and Yasunari Shidama :: :: Received March 3, 2008 :: Copyright (c) 2008-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, STRUCT_0, SUBSET_1, FUNCT_2, FINSET_1, FUNCT_1, CARD_1, FUNCOP_1, COMPLEX1, ALGSTR_0, RLVECT_2, TARSKI, NAT_1, CLVECT_1, FINSEQ_1, VALUED_1, RELAT_1, PARTFUN1, XXREAL_0, RLVECT_1, CARD_3, SUPINF_2, RLSUB_1, ARYTM_3, ARYTM_1, QC_LANG1, BINOP_1, ZFMISC_1, RUSUB_4, REAL_1, REALSET1, XCMPLX_0, CONVEX1, SETFAM_1, CSSPACE, PROB_2, CONVEX4, PRE_POLY, FUNCT_7; notations TARSKI, XBOOLE_0, ENUMSET1, DOMAIN_1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PRE_POLY, RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_4, ALGSTR_0, RLVECT_1, SETFAM_1, STRUCT_0, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, FINSET_1, PARTFUN1, FUNCOP_1, CARD_1, VALUED_1, XCMPLX_0, COMPLEX1, RVSUM_1, RUSUB_4, RUSUB_5, BINOP_1, REAL_1, RLVECT_2, CLVECT_1, CSSPACE, REALSET1; constructors SETFAM_1, BINOP_1, FUNCOP_1, REAL_1, FINSEQ_4, COMPLEX1, REALSET1, BINOP_2, FINSOP_1, RVSUM_1, RLVECT_2, RUSUB_5, CSSPACE, RELSET_1; registrations STRUCT_0, MEMBERED, XXREAL_0, CSSPACE, RLVECT_1, RELSET_1, FINSET_1, XREAL_0, SUBSET_1, XCMPLX_0, CLVECT_1, NUMBERS, NAT_1, FUNCT_2, VALUED_1, VALUED_0, CARD_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Complex Linear Combinations definition let V be non empty 1-sorted; mode C_Linear_Combination of V -> Element of Funcs(the carrier of V, COMPLEX) means :: CONVEX4:def 1 ex T being finite Subset of V st for v being Element of V st not v in T holds it.v = 0; end; notation let V be non empty addLoopStr, L be Element of Funcs(the carrier of V,COMPLEX); synonym Carrier L for support L; end; definition let V be non empty addLoopStr, L be Element of Funcs(the carrier of V,COMPLEX); redefine func Carrier L -> Subset of V equals :: CONVEX4:def 2 {v where v is Element of V : L.v <> 0c}; end; registration let V be non empty addLoopStr, L be C_Linear_Combination of V; cluster Carrier L -> finite; end; theorem :: CONVEX4:1 for V be non empty addLoopStr, L be C_Linear_Combination of V, v be Element of V holds L.v = 0c iff not v in Carrier L; definition let V be non empty addLoopStr; func ZeroCLC V -> C_Linear_Combination of V means :: CONVEX4:def 3 Carrier it = {}; end; registration let V be non empty addLoopStr; cluster Carrier ZeroCLC V -> empty; end; theorem :: CONVEX4:2 for V be non empty addLoopStr, v be Element of V holds (ZeroCLC V ).v = 0c; definition let V be non empty addLoopStr; let A be Subset of V; mode C_Linear_Combination of A -> C_Linear_Combination of V means :: CONVEX4:def 4 Carrier it c= A; end; theorem :: CONVEX4:3 for V be non empty addLoopStr, A,B be Subset of V, l be C_Linear_Combination of A st A c= B holds l is C_Linear_Combination of B; theorem :: CONVEX4:4 for V be non empty addLoopStr, A be Subset of V holds ZeroCLC V is C_Linear_Combination of A; theorem :: CONVEX4:5 for V being non empty addLoopStr, l being C_Linear_Combination of {}the carrier of V holds l = ZeroCLC V; reserve x,y for set, i for Nat; definition let V be non empty CLSStruct; let F be FinSequence of the carrier of V; let f be Function of the carrier of V,COMPLEX; func f (#) F -> FinSequence of the carrier of V means :: CONVEX4:def 5 len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i; end; reserve V for non empty CLSStruct, u,v,v1,v2,v3 for VECTOR of V, A for Subset of V, l, l1, l2 for C_Linear_Combination of A, x,y,y1,y2 for set, a,b for Complex, F for FinSequence of the carrier of V, f for Function of the carrier of V, COMPLEX; theorem :: CONVEX4:6 x in dom F & v = F.x implies (f (#) F).x = f.v * v; theorem :: CONVEX4:7 f (#) <*>(the carrier of V) = <*>(the carrier of V); theorem :: CONVEX4:8 f (#) <* v *> = <* f.v * v *>; theorem :: CONVEX4:9 f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>; theorem :: CONVEX4:10 f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>; reserve K,L,L1,L2,L3 for C_Linear_Combination of V; definition let V be Abelian add-associative right_zeroed right_complementable non empty CLSStruct; let L be C_Linear_Combination of V; func Sum L -> Element of V means :: CONVEX4:def 6 ex F being FinSequence of the carrier of V st F is one-to-one & rng F = Carrier L & it = Sum(L (#) F); end; theorem :: CONVEX4:11 for V being Abelian add-associative right_zeroed right_complementable non empty CLSStruct holds Sum(ZeroCLC V) = 0.V; theorem :: CONVEX4:12 for V being ComplexLinearSpace, A being Subset of V holds A <> {} implies ( A is linearly-closed iff for l being C_Linear_Combination of A holds Sum l in A ); theorem :: CONVEX4:13 for V being Abelian add-associative right_zeroed right_complementable non empty CLSStruct, l being C_Linear_Combination of {}(the carrier of V) holds Sum l = 0.V; theorem :: CONVEX4:14 for V being ComplexLinearSpace, v being VECTOR of V, l being C_Linear_Combination of {v} holds Sum l = l.v * v; theorem :: CONVEX4:15 for V being ComplexLinearSpace, v1, v2 being VECTOR of V holds v1 <> v2 implies for l being C_Linear_Combination of {v1,v2} holds Sum l = l.v1 * v1 + l.v2 * v2; theorem :: CONVEX4:16 for V being Abelian add-associative right_zeroed right_complementable non empty CLSStruct, L being C_Linear_Combination of V holds Carrier L = {} implies Sum L = 0.V; theorem :: CONVEX4:17 for V being ComplexLinearSpace, L being C_Linear_Combination of V, v being VECTOR of V holds Carrier L = {v} implies Sum L = L.v * v; theorem :: CONVEX4:18 for V being ComplexLinearSpace, L being C_Linear_Combination of V, v1, v2 being VECTOR of V holds Carrier L = {v1,v2} & v1 <> v2 implies Sum L = L.v1 * v1 + L.v2 * v2; definition let V be non empty addLoopStr; let L1,L2 be C_Linear_Combination of V; redefine pred L1 = L2 means :: CONVEX4:def 7 for v being Element of V holds L1.v = L2.v; end; definition let V be non empty addLoopStr; let L1,L2 be C_Linear_Combination of V; redefine func L1 + L2 -> C_Linear_Combination of V means :: CONVEX4:def 8 for v being Element of V holds it.v = L1.v + L2.v; end; theorem :: CONVEX4:19 Carrier(L1 + L2) c= Carrier L1 \/ Carrier L2; theorem :: CONVEX4:20 L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A implies L1 + L2 is C_Linear_Combination of A; definition let V,A; let L1,L2 be C_Linear_Combination of A; redefine func L1 + L2 -> C_Linear_Combination of A; end; theorem :: CONVEX4:21 for V be non empty addLoopStr, L1,L2 be C_Linear_Combination of V holds L1 + L2 = L2 + L1; theorem :: CONVEX4:22 L1 + (L2 + L3) = L1 + L2 + L3; theorem :: CONVEX4:23 L + ZeroCLC V = L; definition let V; let a be Complex; let L; func a * L -> C_Linear_Combination of V means :: CONVEX4:def 9 for v holds it.v = a * L.v; end; theorem :: CONVEX4:24 a <> 0c implies Carrier (a * L) = Carrier L; theorem :: CONVEX4:25 0c * L = ZeroCLC V; theorem :: CONVEX4:26 L is C_Linear_Combination of A implies a * L is C_Linear_Combination of A; theorem :: CONVEX4:27 (a + b) * L = a * L + b * L; theorem :: CONVEX4:28 a * (L1 + L2) = a * L1 + a * L2; theorem :: CONVEX4:29 a * (b * L) = (a * b) * L; theorem :: CONVEX4:30 1r * L = L; definition let V,L; func - L -> C_Linear_Combination of V equals :: CONVEX4:def 10 (- 1r) * L; end; theorem :: CONVEX4:31 (- L).v = - L.v; theorem :: CONVEX4:32 L1 + L2 = ZeroCLC V implies L2 = - L1; theorem :: CONVEX4:33 - (- L) = L; definition let V; let L1,L2; func L1 - L2 -> C_Linear_Combination of V equals :: CONVEX4:def 11 L1 + (- L2); end; theorem :: CONVEX4:34 (L1 - L2).v = L1.v - L2.v; theorem :: CONVEX4:35 Carrier(L1 - L2) c= Carrier L1 \/ Carrier L2; theorem :: CONVEX4:36 L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A implies L1 - L2 is C_Linear_Combination of A; theorem :: CONVEX4:37 L - L = ZeroCLC V; definition let V; func C_LinComb V -> set means :: CONVEX4:def 12 x in it iff x is C_Linear_Combination of V; end; registration let V; cluster C_LinComb V -> non empty; end; reserve e,e1,e2 for Element of C_LinComb V; definition let V; let e; func @e -> C_Linear_Combination of V equals :: CONVEX4:def 13 e; end; definition let V; let L; func @L -> Element of C_LinComb V equals :: CONVEX4:def 14 L; end; definition let V; func C_LCAdd V -> BinOp of C_LinComb V means :: CONVEX4:def 15 for e1,e2 holds it.(e1, e2) = @e1 + @e2; end; definition let V; func C_LCMult V -> Function of [:COMPLEX,C_LinComb V:], C_LinComb V means :: CONVEX4:def 16 for a,e holds it.[a,e] = a * @e; end; definition let V; func LC_CLSpace V -> ComplexLinearSpace equals :: CONVEX4:def 17 CLSStruct (# C_LinComb V, @ ZeroCLC V, C_LCAdd V, C_LCMult V #); end; registration let V; cluster LC_CLSpace V -> strict non empty; end; theorem :: CONVEX4:38 vector(LC_CLSpace V,L1) + vector(LC_CLSpace V,L2) = L1 + L2; theorem :: CONVEX4:39 a * vector(LC_CLSpace V,L) = a * L; theorem :: CONVEX4:40 - vector(LC_CLSpace V,L) = - L; theorem :: CONVEX4:41 vector(LC_CLSpace V,L1) - vector(LC_CLSpace V,L2) = L1 - L2; definition let V; let A; func LC_CLSpace A -> strict Subspace of LC_CLSpace V means :: CONVEX4:def 18 the carrier of it = the set of all l ; end; begin :: Preliminaries for Complex Convex Sets definition let V be ComplexLinearSpace, W be Subspace of V; func Up W -> Subset of V equals :: CONVEX4:def 19 the carrier of W; end; registration let V be ComplexLinearSpace, W be Subspace of V; cluster Up W -> non empty; end; definition let V be non empty CLSStruct, S be Subset of V; attr S is Affine means :: CONVEX4:def 20 for x,y being VECTOR of V, z being Complex st z is Real & x in S & y in S holds (1r - z) * x + z * y in S; end; definition let V be ComplexLinearSpace; func (Omega).V -> strict Subspace of V equals :: CONVEX4:def 21 the CLSStruct of V; end; registration let V be non empty CLSStruct; cluster [#]V -> Affine; cluster empty -> Affine for Subset of V; end; registration let V be non empty CLSStruct; cluster non empty Affine for Subset of V; cluster empty Affine for Subset of V; end; theorem :: CONVEX4:42 for a being Real, z being Complex holds Re(a*z)=a* Re(z); theorem :: CONVEX4:43 for a being Real, z being Complex holds Im(a*z) = a*Im(z); theorem :: CONVEX4:44 for a being Real , z being Complex st 0<=a & a<=1 holds |.a*z.| = a*|.z.| & |.(1r-a)*z.| = (1r-a)*|.z.|; begin :: Complex Convex Sets definition let V be non empty CLSStruct; let M be Subset of V; let r be Complex; func r*M -> Subset of V equals :: CONVEX4:def 22 {r * v where v is Element of V: v in M}; end; definition let V be non empty CLSStruct; let M be Subset of V; attr M is convex means :: CONVEX4:def 23 for u,v being VECTOR of V, z be Complex st (ex r be Real st z=r & 0 < r & r < 1 ) & u in M & v in M holds z*u + (1r-z)*v in M; end; theorem :: CONVEX4:45 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M being Subset of V, z being Complex st M is convex holds z*M is convex; theorem :: CONVEX4:46 for V being Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M,N being Subset of V st M is convex & N is convex holds M + N is convex; theorem :: CONVEX4:47 for V being ComplexLinearSpace, M,N being Subset of V st M is convex & N is convex holds M - N is convex; theorem :: CONVEX4:48 for V being non empty CLSStruct, M being Subset of V holds M is convex iff for z being Complex st (ex r being Real st z=r & 0 < r & r < 1) holds z*M + (1r-z)*M c= M; theorem :: CONVEX4:49 for V being Abelian non empty CLSStruct, M being Subset of V st M is convex holds for z being Complex st (ex r being Real st z=r & 0 < r & r < 1) holds (1r-z)*M + z*M c= M; theorem :: CONVEX4:50 for V being Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M,N being Subset of V st M is convex & N is convex holds for z being Complex holds z*M + (1r-z)*N is convex; theorem :: CONVEX4:51 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M be Subset of V holds 1r*M = M; theorem :: CONVEX4:52 for V being ComplexLinearSpace, M be non empty Subset of V holds 0c * M = {0.V}; ::$CT theorem :: CONVEX4:54 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M being Subset of V, z1,z2 being Complex holds z1*(z2*M) = (z1*z2)*M; theorem :: CONVEX4:55 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M1,M2 being Subset of V, z being Complex holds z*(M1 + M2) = z*M1 + z*M2; theorem :: CONVEX4:56 for V being ComplexLinearSpace, M being Subset of V, v being VECTOR of V holds M is convex iff v + M is convex; theorem :: CONVEX4:57 for V being ComplexLinearSpace holds Up((0).V) is convex; theorem :: CONVEX4:58 for V being ComplexLinearSpace holds Up((Omega).V) is convex; theorem :: CONVEX4:59 for V being non empty CLSStruct, M being Subset of V st M = {} holds M is convex; theorem :: CONVEX4:60 for V being Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M1,M2 being Subset of V, z1,z2 being Complex st M1 is convex & M2 is convex holds z1*M1 + z2*M2 is convex; theorem :: CONVEX4:61 for V being vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M being Subset of V, z1,z2 being Complex holds (z1 + z2)*M c= z1*M + z2*M; theorem :: CONVEX4:62 for V being non empty CLSStruct, M,N being Subset of V, z being Complex st M c= N holds z*M c= z*N; theorem :: CONVEX4:63 for V being non empty CLSStruct, M being empty Subset of V, z being Complex holds z * M = {}; ::$CT 2 theorem :: CONVEX4:66 for V being ComplexLinearSpace, M being Subset of V, z1,z2 being Complex st (ex r1,r2 being Real st z1 = r1 & z2 = r2 & r1 >= 0 & r2 >= 0) & M is convex holds z1*M + z2*M = (z1 + z2)*M; theorem :: CONVEX4:67 for V being Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct, M1,M2,M3 being Subset of V, z1,z2,z3 being Complex st M1 is convex & M2 is convex & M3 is convex holds z1*M1 + z2*M2 + z3*M3 is convex; theorem :: CONVEX4:68 for V being non empty CLSStruct, 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 :: CONVEX4:69 for V being non empty CLSStruct, M being Subset of V st M is Affine holds M is convex; registration let V be non empty CLSStruct; cluster non empty convex for Subset of V; end; registration let V be non empty CLSStruct; cluster empty convex for Subset of V; end; theorem :: CONVEX4:70 for V being ComplexUnitarySpace-like non empty CUNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : Re(u .|. v) >= r } holds M is convex; theorem :: CONVEX4:71 for V being ComplexUnitarySpace-like non empty CUNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : Re(u .|. v) > r } holds M is convex; theorem :: CONVEX4:72 for V being ComplexUnitarySpace-like non empty CUNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : Re(u .|. v) <= r } holds M is convex; theorem :: CONVEX4:73 for V being ComplexUnitarySpace-like non empty CUNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : Re(u .|. v) < r } holds M is convex; theorem :: CONVEX4:74 for V being ComplexUnitarySpace-like non empty CUNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : Im(u .|. v) >= r } holds M is convex; theorem :: CONVEX4:75 for V being ComplexUnitarySpace-like non empty CUNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : Im(u .|. v) > r } holds M is convex; theorem :: CONVEX4:76 for V being ComplexUnitarySpace-like non empty CUNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : Im(u .|. v) <= r } holds M is convex; theorem :: CONVEX4:77 for V being ComplexUnitarySpace-like non empty CUNITSTR, M being Subset of V, v being VECTOR of V, r being Real st M = {u where u is VECTOR of V : Im(u .|. v) < r } holds M is convex; theorem :: CONVEX4:78 for V being ComplexUnitarySpace-like non empty CUNITSTR, 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 :: CONVEX4:79 for V being ComplexUnitarySpace-like non empty CUNITSTR, 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 :: Complex Convex Combinations definition let V be ComplexLinearSpace, L be C_Linear_Combination of V; attr L is convex means :: CONVEX4:def 24 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 :: CONVEX4:80 for V being ComplexLinearSpace, L being C_Linear_Combination of V st L is convex holds Carrier L <> {}; theorem :: CONVEX4:81 for V being ComplexLinearSpace, L being C_Linear_Combination of V, v being VECTOR of V st L is convex & ( ex r being Real st r = L.v & r <= 0 ) holds not v in Carrier L; theorem :: CONVEX4:82 for V being ComplexLinearSpace, L being C_Linear_Combination of V st L is convex holds L <> ZeroCLC V; theorem :: CONVEX4:83 for V being ComplexLinearSpace, v being VECTOR of V, L being C_Linear_Combination of V st L is convex & Carrier L = {v} holds ( ex r being Real st r = L.v & r = 1 ) & Sum L = L.v * v; theorem :: CONVEX4:84 for V being ComplexLinearSpace, v1,v2 being VECTOR of V, L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2} & v1 <> v2 holds ( ex r1, r2 being Real st r1 = L.v1 & r2 = L.v2 & r1 + r2 = 1 & r1 >= 0 & r2 >= 0 ) & Sum L = L.v1 * v1 + L.v2 * v2; theorem :: CONVEX4:85 for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V, L being C_Linear_Combination of V st L is convex & Carrier L = {v1,v2,v3} & v1 <> v2 & v2 <> v3 & v3 <> v1 holds ( ex r1, r2, r3 being Real st r1 = L.v1 & r2 = L.v2 & r3 = L.v3 & r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3; theorem :: CONVEX4:86 for V being ComplexLinearSpace, v being VECTOR of V, L being C_Linear_Combination of {v} st L is convex holds ( ex r being Real st r = L.v & r = 1 ) & Sum L = L.v * v; theorem :: CONVEX4:87 for V being ComplexLinearSpace, v1,v2 being VECTOR of V, L being C_Linear_Combination of {v1,v2} st v1 <> v2 & L is convex holds ( ex r1, r2 being Real st r1 = L.v1 & r2 = L.v2 &r1 >= 0 & r2 >= 0 )& Sum L = L.v1 * v1 + L.v2 * v2; theorem :: CONVEX4:88 for V being ComplexLinearSpace, v1,v2,v3 being VECTOR of V, L being C_Linear_Combination of {v1,v2,v3} st v1 <> v2 & v2 <> v3 & v3 <> v1 & L is convex holds ( ex r1, r2, r3 being Real st r1 = L.v1 & r2 = L.v2 & r3 = L.v3 & r1 + r2 + r3 = 1 & r1 >= 0 & r2 >= 0 & r3 >= 0 ) & Sum L = L.v1 * v1 + L .v2 * v2 + L.v3 * v3; begin :: Complex Convex Hull definition let V be non empty CLSStruct, M be Subset of V; func Convex-Family M -> Subset-Family of V means :: CONVEX4:def 25 for N being Subset of V holds N in it iff N is convex & M c= N; end; definition let V be non empty CLSStruct, M be Subset of V; func conv M -> convex Subset of V equals :: CONVEX4:def 26 meet (Convex-Family M); end; theorem :: CONVEX4:89 for V being non empty CLSStruct, M being Subset of V, N being convex Subset of V st M c= N holds conv M c= N;