:: 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;
definitions FUNCT_1, TARSKI, XBOOLE_0, ALGSTR_0;
equalities XBOOLE_0, BINOP_1, RELAT_1, STRUCT_0, REALSET1, FINSEQ_1, CLVECT_1,
COMPLEX1, RVSUM_1, XCMPLX_0, ALGSTR_0, RUSUB_4, RUSUB_5;
expansions TARSKI, BINOP_1, STRUCT_0, CLVECT_1, ALGSTR_0;
theorems RVSUM_1, SETFAM_1, ENUMSET1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_3,
FINSEQ_4, FUNCT_1, FUNCT_2, NAT_1, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1,
RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, COMPLEX1, XCMPLX_1, FUNCOP_1,
XREAL_1, XXREAL_0, FINSOP_1, CLVECT_1, CSSPACE, CONVEX1, PARTFUN1,
XREAL_0, VALUED_1, ALGSTR_0, PRE_POLY, XCMPLX_0;
schemes DOMAIN_1, BINOP_1, SUBSET_1, FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0;
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
:Def1:
ex T being finite Subset of V st for v being Element of V st not v in T
holds it.v = 0;
existence
proof
reconsider f = (the carrier of V) --> 0c as
Element of Funcs(the carrier of V, COMPLEX) by FUNCT_2:8;
take f,{}V;
thus thesis by FUNCOP_1:7;
end;
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;
Lm1: now
let V be non empty addLoopStr,
L be Element of Funcs(the carrier of V, COMPLEX);
A1: support L c= dom L by PRE_POLY:37;
thus Carrier L c= the carrier of V
proof
let x be object;
assume x in support L;
then x in dom L by A1;
hence thesis;
end;
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
{v where v is Element of V : L.v <> 0c};
coherence by Lm1;
compatibility
proof
let X be Subset of V;
set A = Carrier L;
set B = {v where v is Element of V : L.v <> 0};
thus X = A implies X = B
proof
assume
A1: X = A;
thus X c= B
proof
let x be object;
assume
A2: x in X;
then L.x <> 0 by A1,PRE_POLY:def 7;
hence thesis by A2;
end;
let x be object;
assume x in B;
then ex v be Element of V st x = v & L.v <> 0;
hence thesis by A1,PRE_POLY:def 7;
end;
assume
A3: X = B;
thus X c= A
proof
let x be object;
assume x in X;
then ex v be Element of V st x = v & L.v <> 0 by A3;
hence thesis by PRE_POLY:def 7;
end;
let x be object;
assume
A4: x in A;
then
A5: L.x <> 0 by PRE_POLY:def 7;
Carrier L c= the carrier of V by Lm1;
hence thesis by A3,A4,A5;
end;
end;
registration
let V be non empty addLoopStr, L be C_Linear_Combination of V;
cluster Carrier L -> finite;
coherence
proof
set A = Carrier L;
consider T being finite Subset of V such that
A1: for v being Element of V st not v in T holds L.v = 0c by Def1;
now
let x be object;
assume x in A;
then ex v being Element of V st x = v & L.v <> 0c;
hence x in T by A1;
end;
then A c= T;
hence thesis;
end;
end;
theorem Th1:
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
proof
let V be non empty addLoopStr, L be C_Linear_Combination of V, v be Element
of V;
thus L.v = 0c implies not v in Carrier L
proof
assume
A1: L.v = 0c;
assume not thesis;
then ex u being Element of V st v=u & L.u <> 0c;
hence thesis by A1;
end;
thus thesis;
end;
definition
let V be non empty addLoopStr;
func ZeroCLC V -> C_Linear_Combination of V means
:Def3:
Carrier it = {};
existence
proof
reconsider f = (the carrier of V) --> 0c as
Element of Funcs(the carrier of V, COMPLEX) by FUNCT_2:8;
f is C_Linear_Combination of V
proof
take {}V;
thus thesis by FUNCOP_1:7;
end;
then reconsider f as C_Linear_Combination of V;
take f;
set C = {v where v is Element of V : f.v <> 0c};
now
set x = the Element of C;
assume C <> {};
then x in C;
then ex v being Element of V st x = v & f.v <> 0c;
hence contradiction by FUNCOP_1:7;
end;
hence thesis;
end;
uniqueness
proof
let L,L9 be C_Linear_Combination of V;
assume
A1: Carrier L = {} & Carrier L9 = {};
now
let x be object;
assume x in the carrier of V;
then reconsider v = x as Element of V;
A2: L9.v <> 0c implies v in {u where u is Element of V : L9.u <> 0c};
L.v <> 0c implies v in {u where u is Element of V : L.u <> 0c};
hence L.x = L9.x by A1,A2;
end;
hence L = L9 by FUNCT_2:12;
end;
end;
registration
let V be non empty addLoopStr;
cluster Carrier ZeroCLC V -> empty;
coherence by Def3;
end;
theorem Th2:
for V be non empty addLoopStr, v be Element of V holds (ZeroCLC V ).v = 0c
proof
let V be non empty addLoopStr, v be Element of V;
Carrier (ZeroCLC V) = {} & not v in {};
hence thesis;
end;
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
:Def4:
Carrier it c= A;
existence
proof
take L = ZeroCLC V;
thus thesis;
end;
end;
theorem
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
proof
let V be non empty addLoopStr;
let A,B be Subset of V;
let l be C_Linear_Combination of A;
assume
A1: A c= B;
Carrier l c= A by Def4;
then Carrier l c= B by A1;
hence thesis by Def4;
end;
theorem Th4:
for V be non empty addLoopStr, A be Subset of V holds ZeroCLC V
is C_Linear_Combination of A
proof
let V be non empty addLoopStr;
let A be Subset of V;
Carrier ZeroCLC V = {} & {} c= A;
hence thesis by Def4;
end;
theorem Th5:
for V being non empty addLoopStr, l being C_Linear_Combination of
{}the carrier of V holds l = ZeroCLC V
proof
let V be non empty addLoopStr;
let l be C_Linear_Combination of {}(the carrier of V);
Carrier l c= {} by Def4;
then Carrier l = {};
hence thesis by Def3;
end;
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
:Def5:
len it = len F & for i st i in dom it holds it.i = f.(F/.i) * F/.i;
existence
proof
deffunc Q(set)= f.(F/.$1) * F/.$1;
consider G being FinSequence such that
A1: len G = len F and
A2: for n be Nat st n in dom G holds G.n = Q(n) from FINSEQ_1:sch 2;
rng G c= the carrier of V
proof
let x be object;
assume x in rng G;
then consider y being object such that
A3: y in dom G and
A4: G.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A3;
G.y = f.(F/.y) * F/.y by A2,A3;
hence thesis by A4;
end;
then reconsider G as FinSequence of the carrier of V by FINSEQ_1:def 4;
take G;
thus thesis by A1,A2;
end;
uniqueness
proof
let H1,H2 be FinSequence of the carrier of V;
assume that
A5: len H1 = len F and
A6: for i st i in dom H1 holds H1.i = f.(F/.i) * F/.i and
A7: len H2 = len F and
A8: for i st i in dom H2 holds H2.i = f.(F/.i) * F/.i;
now
let k be Nat;
assume 1 <= k & k <= len H1;
then
A9: k in Seg len H1;
then k in dom H1 by FINSEQ_1:def 3;
then
A10: H1.k = f.(F/.k) * F/.k by A6;
k in dom H2 by A5,A7,A9,FINSEQ_1:def 3;
hence H1.k = H2.k by A8,A10;
end;
hence thesis by A5,A7,FINSEQ_1:14;
end;
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 Th6:
x in dom F & v = F.x implies (f (#) F).x = f.v * v
proof
assume that
A1: x in dom F and
A2: v = F.x;
A3: F/.x = F.x by A1,PARTFUN1:def 6;
len(f (#) F) = len F by Def5;
then x in dom(f (#) F) by A1,FINSEQ_3:29;
hence thesis by A2,A3,Def5;
end;
theorem
f (#) <*>(the carrier of V) = <*>(the carrier of V)
proof
len(f (#) <*>(the carrier of V)) = len(<*>(the carrier of V)) by Def5
.= 0;
hence thesis;
end;
theorem Th8:
f (#) <* v *> = <* f.v * v *>
proof
A1: 1 in {1} by FINSEQ_1:2;
A2: len(f (#) <* v *>) = len<* v *> by Def5
.= 1 by FINSEQ_1:40;
then dom(f (#)<* v *>) = {1} by FINSEQ_1:2,def 3;
then (f (#) <* v *>).1 = f.(<* v *>/.1) * <* v *>/.1 by A1,Def5
.= f.(<* v *>/.1) * v by FINSEQ_4:16
.= f.v * v by FINSEQ_4:16;
hence thesis by A2,FINSEQ_1:40;
end;
theorem Th9:
f (#) <* v1,v2 *> = <* f.v1 * v1, f.v2 * v2 *>
proof
A1: len(f (#) <* v1,v2 *>) = len<* v1,v2 *> by Def5
.= 2 by FINSEQ_1:44;
then
A2: dom(f (#) <* v1,v2 *>) = {1,2} by FINSEQ_1:2,def 3;
2 in {1,2} by FINSEQ_1:2;
then
A3: (f (#) <* v1,v2 *>).2 = f.(<* v1,v2 *>/.2) * <* v1,v2 *>/.2 by A2,Def5
.= f.(<* v1,v2 *>/.2) * v2 by FINSEQ_4:17
.= f.v2 * v2 by FINSEQ_4:17;
1 in {1,2} by FINSEQ_1:2;
then (f (#) <* v1,v2 *>).1 = f.(<* v1,v2 *>/.1) * <* v1,v2 *>/.1 by A2,Def5
.= f.(<* v1,v2 *>/.1) * v1 by FINSEQ_4:17
.= f.v1 * v1 by FINSEQ_4:17;
hence thesis by A1,A3,FINSEQ_1:44;
end;
theorem Th10:
f (#) <* v1,v2,v3 *> = <* f.v1 * v1, f.v2 * v2, f.v3 * v3 *>
proof
A1: len(f (#) <* v1,v2,v3 *>) = len<* v1,v2,v3 *> by Def5
.= 3 by FINSEQ_1:45;
then
A2: dom(f (#)<* v1,v2,v3 *>) = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
3 in {1,2,3} by FINSEQ_3:1;
then
A3: (f (#) <* v1,v2,v3 *>).3 = f.(<* v1,v2,v3 *>/.3) * <* v1,v2,v3 *>/.3 by A2
,Def5
.= f.(<* v1,v2,v3 *>/.3) * v3 by FINSEQ_4:18
.= f.v3 * v3 by FINSEQ_4:18;
2 in {1,2,3} by FINSEQ_3:1;
then
A4: (f (#) <* v1,v2,v3 *>).2 = f.(<* v1,v2,v3 *>/.2) * <* v1,v2,v3 *>/.2 by A2
,Def5
.= f.(<* v1,v2,v3 *>/.2) * v2 by FINSEQ_4:18
.= f.v2 * v2 by FINSEQ_4:18;
1 in {1,2,3} by FINSEQ_3:1;
then
(f (#) <* v1,v2,v3 *>).1 = f.(<* v1,v2,v3 *>/.1) * <* v1,v2,v3 *>/.1 by A2
,Def5
.= f.(<* v1,v2,v3 *>/.1) * v1 by FINSEQ_4:18
.= f.v1 * v1 by FINSEQ_4:18;
hence thesis by A1,A4,A3,FINSEQ_1:45;
end;
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
:Def6:
ex F being FinSequence of the
carrier of V st F is one-to-one & rng F = Carrier L & it = Sum(L (#) F);
existence
proof
consider F being FinSequence such that
A1: rng F = Carrier L and
A2: F is one-to-one by FINSEQ_4:58;
reconsider F as FinSequence of the carrier of V by A1,FINSEQ_1:def 4;
take Sum(L (#) F);
take F;
thus thesis by A1,A2;
end;
uniqueness
proof
let v1,v2 be Element of V;
given F1 being FinSequence of the carrier of V such that
A3: F1 is one-to-one and
A4: rng F1 = Carrier L and
A5: v1 = Sum(L (#) F1);
given F2 being FinSequence of the carrier of V such that
A6: F2 is one-to-one and
A7: rng F2 = Carrier L and
A8: v2 = Sum(L (#) F2);
defpred P[object,object] means {$2} = F1"{F2.$1};
A9: len F1 = len F2 by A3,A4,A6,A7,FINSEQ_1:48;
A10: dom F1 = Seg len F1 by FINSEQ_1:def 3;
A11: dom F2 = Seg len F2 by FINSEQ_1:def 3;
A12: for x being object st x in dom F1
ex y being object st y in dom F1 & P[x,y]
proof
let x be object;
assume x in dom F1;
then F2.x in rng F1 by A4,A7,A9,A10,A11,FUNCT_1:def 3;
then consider y being object such that
A13: F1"{F2.x} = {y} by A3,FUNCT_1:74;
take y;
y in F1"{F2.x} by A13,TARSKI:def 1;
hence thesis by A13,FUNCT_1:def 7;
end;
consider f being Function of dom F1, dom F1 such that
A14: for x being object st x in dom F1 holds P[x,f.x] from FUNCT_2:sch 1(A12);
A15: rng f = dom F1
proof
thus rng f c= dom F1 by RELAT_1:def 19;
let y be object;
assume
A16: y in dom F1;
then F1.y in rng F2 by A4,A7,FUNCT_1:def 3;
then consider x being object such that
A17: x in dom F2 and
A18: F2.x = F1.y by FUNCT_1:def 3;
F1"{F2.x} = F1"Im(F1,y) by A16,A18,FUNCT_1:59;
then F1"{F2.x} c= {y} by A3,FUNCT_1:82;
then {f.x} c= {y} by A9,A10,A11,A14,A17;
then
A19: f.x = y by ZFMISC_1:18;
x in dom f by A9,A10,A11,A17,FUNCT_2:def 1;
hence thesis by A19,FUNCT_1:def 3;
end;
set G1 = L (#) F1;
A20: len G1 = len F1 by Def5;
A21: f is one-to-one
proof
let y1,y2 be object;
assume that
A22: y1 in dom f and
A23: y2 in dom f and
A24: f.y1 = f.y2;
F2.y1 in rng F1 by A4,A7,A9,A10,A11,A22,FUNCT_1:def 3;
then
A25: {F2.y1} c= rng F1 by ZFMISC_1:31;
F2.y2 in rng F1 by A4,A7,A9,A10,A11,A23,FUNCT_1:def 3;
then
A26: {F2.y2} c= rng F1 by ZFMISC_1:31;
F1"{F2.y1} = {f.y1} & F1"{F2.y2} = {f.y2} by A14,A22,A23;
then {F2.y1} = {F2.y2} by A24,A25,A26,FUNCT_1:91;
then F2.y1 = F2.y2 by ZFMISC_1:3;
hence thesis by A6,A9,A10,A11,A22,A23,FUNCT_1:def 4;
end;
set G2 = L (#) F2;
A27: dom G2 = Seg len G2 by FINSEQ_1:def 3;
reconsider f as Permutation of dom F1 by A15,A21,FUNCT_2:57;
dom F1 = Seg len F1 & dom G1 = Seg len G1 by FINSEQ_1:def 3;
then reconsider f as Permutation of dom G1 by A20;
A28: len G2 = len F2 by Def5;
A29: dom G1 = Seg len G1 by FINSEQ_1:def 3;
now
let i be Nat;
assume
A30: i in dom G2;
then
A31: G2.i = L.(F2/.i) * F2/.i & F2.i = F2/.i by A28,A11,A27,Def5,
PARTFUN1:def 6;
i in dom f by A9,A28,A10,A27,A30,FUNCT_2:def 1;
then
A32: f.i in dom F1 by A15,FUNCT_1:def 3;
then reconsider m = f.i as Element of NAT;
{F1.(f.i)} = Im(F1,f.i) by A32,FUNCT_1:59
.= F1.:(F1"{F2.i}) by A9,A28,A10,A27,A14,A30;
then
A33: F2.i = F1.m by FUNCT_1:75,ZFMISC_1:18;
F1.m = F1/.m by A32,PARTFUN1:def 6;
hence G2.i = G1.(f.i) by A20,A10,A29,A32,A33,A31,Def5;
end;
hence thesis by A3,A4,A5,A6,A7,A8,A20,A28,FINSEQ_1:48,RLVECT_2:6;
end;
end;
theorem Th11:
for V being Abelian add-associative right_zeroed
right_complementable non empty CLSStruct holds Sum(ZeroCLC V) = 0.V
proof
let V be Abelian add-associative right_zeroed right_complementable non empty
CLSStruct;
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A1: rng F = Carrier (ZeroCLC V) and
A2: Sum(ZeroCLC V) = Sum(ZeroCLC V (#) F) by Def6;
F = {} by A1,RELAT_1:41;
then len(ZeroCLC V (#) F) = 0 by Def5,CARD_1:27;
hence thesis by A2,RLVECT_1:75;
end;
theorem
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 )
proof
let V be ComplexLinearSpace;
let A be Subset of V;
assume
A1: A <> {};
thus A is linearly-closed implies for l being C_Linear_Combination of A
holds Sum l in A
proof
defpred P[Nat] means for l being C_Linear_Combination of A st card(Carrier
l) = $1 holds Sum l in A;
assume
A2: A is linearly-closed;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
hereby
let l be C_Linear_Combination of A;
deffunc F(Element of V)= l.$1;
consider F being FinSequence of the carrier of V such that
A5: F is one-to-one and
A6: rng F = Carrier l and
A7: Sum l = Sum(l (#) F) by Def6;
reconsider G = F | Seg k as FinSequence of the carrier of V by
FINSEQ_1:18;
assume
A8: card(Carrier l) = k + 1;
then
A9: len F = k + 1 by A5,A6,FINSEQ_4:62;
then
A10: len(l (#) F) = k + 1 by Def5;
k + 1 in Seg(k + 1) by FINSEQ_1:4;
then
A11: k + 1 in dom F by A9,FINSEQ_1:def 3;
then reconsider v = F.(k + 1) as VECTOR of V by FUNCT_1:102;
consider f being Function of the carrier of V, COMPLEX such that
A12: f.v = 0c & for u being Element of V st u <> v holds f.u = F(u
) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V, COMPLEX) by
FUNCT_2:8;
now
let u be VECTOR of V;
assume not u in Carrier l;
then l.u = 0c;
hence f.u = 0c by A12;
end;
then reconsider f as C_Linear_Combination of V by Def1;
A13: Carrier f = Carrier l \ {v}
proof
now
let x be object;
assume x in Carrier f;
then
A14: ex u being VECTOR of V st u = x & f.u <> 0c;
then f.x = l.x by A12;
then
A15: x in Carrier l by A14;
not x in {v} by A12,A14,TARSKI:def 1;
hence x in Carrier l \ {v} by A15,XBOOLE_0:def 5;
end;
hence Carrier f c= Carrier l \ {v};
let x be object;
assume
A16: x in Carrier l \ {v};
then not x in {v} by XBOOLE_0:def 5;
then x <> v by TARSKI:def 1;
then
A17: l.x = f.x by A12,A16;
x in Carrier l by A16,XBOOLE_0:def 5;
then ex u being VECTOR of V st x = u & l.u <> 0c;
hence thesis by A17;
end;
A18: Carrier l c= A by Def4;
then Carrier f c= A \ {v} by A13,XBOOLE_1:33;
then Carrier f c= A by XBOOLE_1:106;
then reconsider f as C_Linear_Combination of A by Def4;
A19: len G = k by A9,FINSEQ_3:53;
then
A20: len (f (#) G) = k by Def5;
A21: rng G = Carrier f
proof
thus rng G c= Carrier f
proof
let x be object;
assume x in rng G;
then consider y being object such that
A22: y in dom G and
A23: G.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A22;
A24: dom G c= dom F & G.y = F.y by A22,FUNCT_1:47,RELAT_1:60;
then x = v implies k + 1 = y & y <= k & k < k + 1 by A5,A19,A11,A22
,A23,FINSEQ_3:25,FUNCT_1:def 4,XREAL_1:29;
then
A25: not x in {v} by TARSKI:def 1;
x in rng F by A22,A23,A24,FUNCT_1:def 3;
hence thesis by A6,A13,A25,XBOOLE_0:def 5;
end;
let x be object;
assume
A26: x in Carrier f;
then x in rng F by A6,A13,XBOOLE_0:def 5;
then consider y being object such that
A27: y in dom F and
A28: F.y = x by FUNCT_1:def 3;
now
assume not y in Seg k;
then y in dom F \ Seg k by A27,XBOOLE_0:def 5;
then y in Seg(k + 1) \ Seg k by A9,FINSEQ_1:def 3;
then y in {k + 1} by FINSEQ_3:15;
then y = k + 1 by TARSKI:def 1;
then not v in {v} by A13,A26,A28,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
then y in dom F /\ Seg k by A27,XBOOLE_0:def 4;
then
A29: y in dom G by RELAT_1:61;
then G.y = F.y by FUNCT_1:47;
hence thesis by A28,A29,FUNCT_1:def 3;
end;
Seg(k + 1) /\ Seg k = Seg k by FINSEQ_1:7,NAT_1:12
.= dom(f (#) G) by A20,FINSEQ_1:def 3;
then
A30: dom(f (#) G) = dom(l (#) F) /\ Seg k by A10,FINSEQ_1:def 3;
now
let x be object;
assume
A31: x in dom(f (#) G);
then
A32: x in dom G by A19,A20,FINSEQ_3:29;
then
A33: G.x in rng G by FUNCT_1:def 3;
then reconsider u = G.x as VECTOR of V;
A34: F.x = u by A32,FUNCT_1:47;
not u in {v} by A13,A21,A33,XBOOLE_0:def 5;
then
A35: u <> v by TARSKI:def 1;
x in dom(l (#) F) by A30,A31,XBOOLE_0:def 4;
then
A36: x in dom F by A9,A10,FINSEQ_3:29;
(f (#) G).x = f.u * u by A32,Th6
.= l.u * u by A12,A35;
hence (f (#) G).x = (l (#) F).x by A36,A34,Th6;
end;
then
A37: f (#) G = (l (#) F) | Seg k by A30,FUNCT_1:46;
v in rng F by A11,FUNCT_1:def 3;
then {v} c= Carrier l by A6,ZFMISC_1:31;
then card(Carrier f) = k + 1 - card{v} by A8,A13,CARD_2:44;
then card(Carrier f) = k + 1 - 1 by CARD_1:30;
then
A38: Sum f in A by A4;
v in Carrier l by A6,A11,FUNCT_1:def 3;
then
A39: l.v * v in A by A2,A18;
G is one-to-one by A5,FUNCT_1:52;
then
A40: Sum(f (#) G) = Sum f by A21,Def6;
dom(f (#) G) = Seg len (f (#) G) & (l (#) F).(len F) = l.v * v by A9
,A11,Th6,FINSEQ_1:def 3;
then Sum(l (#) F) = Sum(f (#) G) + l.v * v by A9,A10,A20,A37,
RLVECT_1:38;
hence Sum l in A by A2,A7,A39,A40,A38;
end;
end;
let l be C_Linear_Combination of A;
A41: card(Carrier l) = card(Carrier l);
now
let l be C_Linear_Combination of A;
assume card(Carrier l) = 0;
then Carrier l = {};
then l = ZeroCLC V by Def3;
then Sum l = 0.V by Th11;
hence Sum l in A by A1,A2,CLVECT_1:20;
end;
then
A42: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A42,A3);
hence thesis by A41;
end;
assume
A43: for l be C_Linear_Combination of A holds Sum l in A;
ZeroCLC V is C_Linear_Combination of A & Sum(ZeroCLC V) = 0.V by Th4,Th11;
then
A44: 0.V in A by A43;
A45: for a being Complex,v being VECTOR of V st v in A holds a * v in A
proof
let a be Complex, v be VECTOR of V;
assume
A46: v in A;
now
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
deffunc F(Element of V) = 0c;
consider f being Function of the carrier of V, COMPLEX such that
A47: f.v = a1 & for u being Element of V st u <> v holds f.u = F(u)
from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V,COMPLEX) by FUNCT_2:8;
now
let u be VECTOR of V;
assume not u in {v};
then u <> v by TARSKI:def 1;
hence f.u = 0 by A47;
end;
then reconsider f as C_Linear_Combination of V by Def1;
assume
A48: a <> 0;
A49: Carrier f = {v}
proof
now
let x be object;
assume x in Carrier f;
then ex u being VECTOR of V st x = u & f.u <> 0;
then x = v by A47;
hence x in {v} by TARSKI:def 1;
end;
hence Carrier f c= {v};
let x be object;
assume x in {v};
then x = v by TARSKI:def 1;
hence thesis by A48,A47;
end;
{v} c= A by A46,ZFMISC_1:31;
then reconsider f as C_Linear_Combination of A by A49,Def4;
consider F being FinSequence of the carrier of V such that
A50: F is one-to-one & rng F = Carrier f and
A51: Sum(f(#)F) = Sum f by Def6;
F = <* v *> by A49,A50,FINSEQ_3:97;
then f (#) F = <* f.v * v *> by Th8;
then Sum f = a * v by A47,A51,RLVECT_1:44;
hence thesis by A43;
end;
hence thesis by A44,CLVECT_1:1;
end;
for v,u being VECTOR of V st v in A & u in A holds v + u in A
proof
let v,u be VECTOR of V;
assume that
A52: v in A and
A53: u in A;
A54: 1r * v = v by CLVECT_1:def 5;
A55: 1r * u = u by CLVECT_1:def 5;
A56: now
deffunc F(Element of V)=0c;
assume
A57: v <> u;
consider f being Function of the carrier of V, COMPLEX such that
A58: f.v = 1r & f.u = 1r and
A59: for w being Element of V st w <> v & w <> u holds f.w = F(w)
from FUNCT_2:sch 7(A57);
reconsider f as Element of Funcs(the carrier of V, COMPLEX) by FUNCT_2:8;
now
let w be VECTOR of V;
assume not w in {v,u};
then w <> v & w <> u by TARSKI:def 2;
hence f.w = 0 by A59;
end;
then reconsider f as C_Linear_Combination of V by Def1;
A60: Carrier f = {v,u}
proof
thus Carrier f c= {v,u}
proof
let x be object;
assume x in Carrier f;
then ex w being VECTOR of V st x = w & f.w <> 0c;
then x = v or x = u by A59;
hence thesis by TARSKI:def 2;
end;
let x be object;
assume x in {v,u};
then x = v or x = u by TARSKI:def 2;
hence thesis by A58;
end;
then Carrier f c= A by A52,A53,ZFMISC_1:32;
then reconsider f as C_Linear_Combination of A by Def4;
consider F being FinSequence of the carrier of V such that
A61: F is one-to-one & rng F = Carrier f and
A62: Sum(f (#) F) = Sum f by Def6;
F = <* v,u *> or F = <* u,v *> by A57,A60,A61,FINSEQ_3:99;
then f(#)F = <* 1r*v, 1r*u *> or f(#)F = <* 1r*u, 1r*v *> by A58,Th9;
then Sum f = v + u by A55,A54,A62,RLVECT_1:45;
hence thesis by A43;
end;
v + v = (1r + 1r) * v by A54,CLVECT_1:def 3;
hence thesis by A45,A52,A56;
end;
hence thesis by A45;
end;
theorem
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
proof
let V be Abelian add-associative right_zeroed right_complementable non empty
CLSStruct;
let l be C_Linear_Combination of {}(the carrier of V);
l = ZeroCLC V by Th5;
hence thesis by Th11;
end;
theorem Th14:
for V being ComplexLinearSpace, v being VECTOR of V, l being
C_Linear_Combination of {v} holds Sum l = l.v * v
proof
let V be ComplexLinearSpace;
let v be VECTOR of V;
let l be C_Linear_Combination of {v};
A1: Carrier l c= {v} by Def4;
per cases by A1,ZFMISC_1:33;
suppose
Carrier l = {};
then
A2: l = ZeroCLC V by Def3;
hence Sum l = 0.V by Th11
.= 0c * v by CLVECT_1:1
.= l.v * v by A2,Th2;
end;
suppose
Carrier l = {v};
then consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = {v} and
A4: Sum l = Sum(l (#) F) by Def6;
F = <* v *> by A3,FINSEQ_3:97;
then l (#) F = <* l.v * v *> by Th8;
hence thesis by A4,RLVECT_1:44;
end;
end;
theorem Th15:
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
proof
let V be ComplexLinearSpace;
let v1, v2 be VECTOR of V;
assume
A1: v1 <> v2;
let l be C_Linear_Combination of {v1,v2};
A2: 0.V = 0c*v1 by CLVECT_1:1;
A3: Carrier l c= {v1,v2} by Def4;
A4: 0.V = 0c*v2 by CLVECT_1:1;
per cases by A3,ZFMISC_1:36;
suppose
Carrier l = {};
then
A5: l = ZeroCLC V by Def3;
hence Sum l = 0.V by Th11
.= 0.V + 0.V
.= l.v1 * v1 + 0c* v2 by A4,A5,Th2,CLVECT_1:1
.= l.v1 * v1 + l.v2 * v2 by A5,Th2;
end;
suppose
A6: Carrier l = {v1};
then reconsider L = l as C_Linear_Combination of {v1} by Def4;
Sum L = l.v1 * v1 by Th14;
then
A7: Sum l = l.v1 * v1 + 0.V;
not v2 in Carrier l by A1,A6,TARSKI:def 1;
hence thesis by A4,A7;
end;
suppose
A8: Carrier l = {v2};
then reconsider L = l as C_Linear_Combination of {v2} by Def4;
Sum L = l.v2 * v2 by Th14;
then
A9: Sum l = 0.V + l.v2 * v2;
not v1 in Carrier l by A1,A8,TARSKI:def 1;
hence thesis by A2,A9;
end;
suppose
Carrier l = {v1,v2};
then consider F being FinSequence of the carrier of V such that
A10: F is one-to-one & rng F = {v1,v2} and
A11: Sum l = Sum(l (#) F) by Def6;
F = <* v1,v2 *> or F = <* v2,v1 *> by A1,A10,FINSEQ_3:99;
then l (#) F = <* l.v1 * v1, l.v2 * v2 *> or l (#) F = <* l.v2 * v2, l.v1
* v1 *> by Th9;
hence thesis by A11,RLVECT_1:45;
end;
end;
theorem
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
proof
let V be Abelian add-associative right_zeroed right_complementable non empty
CLSStruct;
let L be C_Linear_Combination of V;
assume Carrier L = {};
then L = ZeroCLC V by Def3;
hence thesis by Th11;
end;
theorem
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
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
let v be VECTOR of V;
assume Carrier L = {v};
then L is C_Linear_Combination of {v} by Def4;
hence thesis by Th14;
end;
theorem Th18:
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
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
let v1, v2 be VECTOR of V;
assume that
A1: Carrier L = {v1,v2} and
A2: v1 <> v2;
L is C_Linear_Combination of {v1,v2} by A1,Def4;
hence thesis by A2,Th15;
end;
definition
let V be non empty addLoopStr;
let L1,L2 be C_Linear_Combination of V;
redefine pred L1 = L2 means
for v being Element of V holds L1.v = L2.v;
compatibility by FUNCT_2:63;
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
:Def8:
for v being Element of V holds it.v = L1.v + L2.v;
coherence
proof
reconsider f = L1+L2 as Element of Funcs(the carrier of V,COMPLEX) by
FUNCT_2:8;
now
let v be Element of V;
assume
A1: not v in Carrier(L1) \/ Carrier(L2);
then not v in Carrier(L2) by XBOOLE_0:def 3;
then
A2: L2.v = 0;
not v in Carrier(L1) by A1,XBOOLE_0:def 3;
then L1.v = 0;
hence f.v = 0 + 0 by A2,VALUED_1:1
.= 0;
end;
hence thesis by Def1;
end;
compatibility
proof
let f be C_Linear_Combination of V;
thus f=L1+L2 implies for v being Element of V holds f.v = L1.v + L2.v by
VALUED_1:1;
assume for v being Element of V holds f.v = L1.v + L2.v;
then
A3: for c being object st c in dom f holds f.c = L1.c + L2.c;
dom L1 = the carrier of V & dom L2 = the carrier of V by FUNCT_2:92;
then dom f = dom L1 /\ dom L2 by FUNCT_2:92;
hence f=L1+L2 by A3,VALUED_1:def 1;
end;
end;
theorem Th19:
Carrier(L1 + L2) c= Carrier L1 \/ Carrier L2
proof
let x be object;
assume x in Carrier(L1 + L2);
then consider u such that
A1: x = u and
A2: (L1 + L2).u <> 0c;
(L1 + L2).u = L1.u + L2.u by Def8;
then L1.u <> 0c or L2.u <> 0c by A2;
then x in Carrier L1 or x in Carrier L2 by A1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th20:
L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of
A implies L1 + L2 is C_Linear_Combination of A
proof
assume L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A;
then Carrier L1 c= A & Carrier L2 c= A by Def4;
then
A1: Carrier L1 \/ Carrier L2 c= A by XBOOLE_1:8;
Carrier(L1 + L2) c= Carrier L1 \/ Carrier L2 by Th19;
hence Carrier(L1 + L2) c= A by A1;
end;
definition
let V,A;
let L1,L2 be C_Linear_Combination of A;
redefine func L1 + L2 -> C_Linear_Combination of A;
coherence by Th20;
end;
theorem
for V be non empty addLoopStr, L1,L2 be C_Linear_Combination of V
holds L1 + L2 = L2 + L1;
theorem Th22:
L1 + (L2 + L3) = L1 + L2 + L3
proof
let v;
thus (L1 + (L2 + L3)).v = L1.v + (L2 + L3).v by Def8
.= L1.v + (L2.v + L3.v) by Def8
.= L1.v + L2.v + L3.v
.= (L1 + L2).v + L3.v by Def8
.= (L1 + L2 + L3).v by Def8;
end;
theorem Th23:
L + ZeroCLC V = L
proof
let v;
thus (L + ZeroCLC V).v = L.v + (ZeroCLC V).v by Def8
.= L.v + 0c by Th2
.= L.v;
end;
definition
let V; let a be Complex;
let L;
func a * L -> C_Linear_Combination of V means
:Def9:
for v holds it.v = a * L.v;
existence
proof
reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
deffunc F(Element of V)=In(a * L.$1,COMPLEX);
consider f being Function of the carrier of V, COMPLEX such that
A1: for v being Element of V holds f.v = F(v) from FUNCT_2:sch 4;
reconsider f as Element of Funcs(the carrier of V,COMPLEX) by FUNCT_2:8;
now
let v;
assume not v in Carrier L;
then
A2: L.v = 0c;
thus f.v = F(v) by A1
.= 0c by A2;
end;
then reconsider f as C_Linear_Combination of V by Def1;
take f;
let v;
f.v = F(v) by A1;
hence thesis;
end;
uniqueness
proof
let L1,L2;
assume
A3: for v holds L1.v = a * L.v;
assume
A4: for v holds L2.v = a * L.v;
let v;
thus L1.v = a * L.v by A3
.= L2.v by A4;
end;
end;
theorem Th24:
a <> 0c implies Carrier (a * L) = Carrier L
proof
set T = {u : (a * L).u <> 0c};
set S = {v : L.v <> 0c};
assume
A1: a <> 0c;
T = S
proof
thus T c= S
proof
let x be object;
assume x in T;
then consider u such that
A2: x = u and
A3: (a * L).u <> 0c;
(a * L).u = a * L.u by Def9;
then L.u <> 0c by A3;
hence thesis by A2;
end;
let x be object;
assume x in S;
then consider v such that
A4: x = v & L.v <> 0c;
(a * L).v = a * L.v by Def9;
hence thesis by A1,A4;
end;
hence thesis;
end;
theorem Th25:
0c * L = ZeroCLC V
proof
let v;
thus (0c * L).v = 0c * L.v by Def9
.= (ZeroCLC V).v by Th2;
end;
theorem Th26:
L is C_Linear_Combination of A implies a * L is C_Linear_Combination of A
proof
assume
A1: L is C_Linear_Combination of A;
A2: now
assume a <> 0c;
then Carrier (a * L) = Carrier L by Th24;
hence thesis by A1,Def4;
end;
a = 0c implies a*L = ZeroCLC V by Th25;
hence thesis by A2,Th4;
end;
theorem Th27:
(a + b) * L = a * L + b * L
proof
let v;
thus ((a + b) * L).v = (a + b) * L.v by Def9
.= a * L.v + b * L.v
.= (a * L).v + b * L.v by Def9
.= (a * L).v + (b * L). v by Def9
.= ((a * L) + (b * L)).v by Def8;
end;
theorem Th28:
a * (L1 + L2) = a * L1 + a * L2
proof
let v;
thus (a * (L1 + L2)).v = a * (L1 + L2).v by Def9
.= a * (L1.v + L2.v) by Def8
.= a * L1.v + a * L2.v
.= (a * L1).v + a * L2.v by Def9
.= (a * L1).v + (a * L2). v by Def9
.= ((a * L1) + (a * L2)).v by Def8;
end;
theorem Th29:
a * (b * L) = (a * b) * L
proof
let v;
thus (a * (b * L)).v = a * (b * L).v by Def9
.= a * (b * L.v) by Def9
.= a * b * L.v
.= ((a * b) * L).v by Def9;
end;
theorem Th30:
1r * L = L
proof
let v;
thus (1r * L).v = 1r * L.v by Def9
.= L.v;
end;
definition
let V,L;
func - L -> C_Linear_Combination of V equals
(- 1r) * L;
correctness;
end;
theorem Th31:
(- L).v = - L.v
proof
thus (- L).v = (- 1r) * L.v by Def9
.= - L.v;
end;
theorem
L1 + L2 = ZeroCLC V implies L2 = - L1
proof
assume
A1: L1 + L2 = ZeroCLC V;
let v;
L1.v + L2.v = (ZeroCLC V).v by A1,Def8
.= 0c by Th2;
hence L2.v = - L1.v .= (- L1).v by Th31;
end;
theorem
- (- L) = L
proof
let v;
thus (- (- L)).v = ((- 1r) * (- 1r) * L).v by Th29
.= 1r * L.v by Def9
.= L.v;
end;
definition
let V;
let L1,L2;
func L1 - L2 -> C_Linear_Combination of V equals
L1 + (- L2);
correctness;
end;
theorem Th34:
(L1 - L2).v = L1.v - L2.v
proof
thus (L1 - L2).v = L1.v + (- L2).v by Def8
.= L1.v - L2.v by Th31;
end;
theorem
Carrier(L1 - L2) c= Carrier L1 \/ Carrier L2
proof
Carrier(L1 - L2) c= Carrier L1 \/ Carrier -L2 by Th19;
hence thesis by Th24;
end;
theorem
L1 is C_Linear_Combination of A & L2 is C_Linear_Combination of A
implies L1 - L2 is C_Linear_Combination of A
proof
assume that
A1: L1 is C_Linear_Combination of A and
A2: L2 is C_Linear_Combination of A;
- L2 is C_Linear_Combination of A by A2,Th26;
hence thesis by A1,Th20;
end;
theorem Th37:
L - L = ZeroCLC V
proof
let v;
thus (L - L).v = L.v - L.v by Th34
.= (ZeroCLC V).v by Th2;
end;
definition
let V;
func C_LinComb V -> set means
:Def12:
x in it iff x is C_Linear_Combination of V;
existence
proof
defpred P[object] means $1 is C_Linear_Combination of V;
consider A being set such that
A1: for x being object
holds x in A iff x in Funcs(the carrier of V, COMPLEX) & P[x
] from XBOOLE_0:sch 1;
take A;
let x;
thus x in A implies x is C_Linear_Combination of V by A1;
assume x is C_Linear_Combination of V;
hence thesis by A1;
end;
uniqueness
proof
let D1,D2 be set;
assume
A2: for x holds x in D1 iff x is C_Linear_Combination of V;
assume
A3: for x holds x in D2 iff x is C_Linear_Combination of V;
thus D1 c= D2
proof
let x be object;
assume x in D1;
then x is C_Linear_Combination of V by A2;
hence thesis by A3;
end;
let x be object;
assume x in D2;
then x is C_Linear_Combination of V by A3;
hence thesis by A2;
end;
end;
registration
let V;
cluster C_LinComb V -> non empty;
coherence
proof
set x = the C_Linear_Combination of V;
x in C_LinComb V by Def12;
hence thesis;
end;
end;
reserve e,e1,e2 for Element of C_LinComb V;
definition
let V;
let e;
func @e -> C_Linear_Combination of V equals
e;
coherence by Def12;
end;
definition
let V;
let L;
func @L -> Element of C_LinComb V equals
L;
coherence by Def12;
end;
definition
let V;
func C_LCAdd V -> BinOp of C_LinComb V means
:Def15:
for e1,e2 holds it.(e1, e2) = @e1 + @e2;
existence
proof
deffunc F(Element of C_LinComb V,Element of C_LinComb V)=@(@$1 + @$2);
consider o being BinOp of C_LinComb V such that
A1: for e1,e2 holds o.(e1,e2) = F(e1,e2) from BINOP_1:sch 4;
take o;
let e1,e2;
thus o.(e1,e2) = @(@e1 + @e2) by A1
.= @e1 + @e2;
end;
uniqueness
proof
let o1,o2 be BinOp of C_LinComb V;
assume
A2: for e1,e2 holds o1.(e1,e2) = @e1 + @e2;
assume
A3: for e1,e2 holds o2.(e1,e2) = @e1 + @e2;
now
let e1,e2;
thus o1.(e1,e2) = @e1 + @e2 by A2
.= o2.(e1,e2) by A3;
end;
hence thesis;
end;
end;
definition
let V;
func C_LCMult V -> Function of [:COMPLEX,C_LinComb V:], C_LinComb V means
:Def16: for a,e holds it.[a,e] = a * @e;
existence
proof
defpred P[Element of COMPLEX,Element of C_LinComb V,set] means ex a st a =
$1 & $3 = a * @$2;
A1: for x being (Element of COMPLEX), e1 ex e2 st P[x,e1,e2]
proof
let x be (Element of COMPLEX), e1;
take @(x * @e1);
take x;
thus thesis;
end;
consider g being Function of [:COMPLEX,C_LinComb V:], C_LinComb V such
that
A2: for x being Element of COMPLEX, e holds P[x,e,g.(x,e)] from
BINOP_1:sch 3(A1);
take g;
let a,e;
a in COMPLEX by XCMPLX_0:def 2;
then ex b st b = a & g.(a,e) = b * @e by A2;
hence thesis;
end;
uniqueness
proof
let g1,g2 be Function of [:COMPLEX,C_LinComb V:], C_LinComb V;
assume
A3: for a,e holds g1.[a,e] = a * @e;
assume
A4: for a,e holds g2.[a,e] = a * @e;
now
let x be (Element of COMPLEX), e;
thus g1.(x,e) = x * @e by A3
.= g2.(x,e) by A4;
end;
hence thesis;
end;
end;
definition
let V;
func LC_CLSpace V -> ComplexLinearSpace equals
CLSStruct (# C_LinComb V, @
ZeroCLC V, C_LCAdd V, C_LCMult V #);
coherence
proof
set S = CLSStruct (# C_LinComb V, @ZeroCLC V, C_LCAdd V, C_LCMult V #);
A1: now
let a,b be Complex, v,u,w be VECTOR of S;
reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider x = v, y = u, z = w, yx = u + v, xz = v + w, ax = a1 * v, az =
a1 * w, bx = b1 * v as Element of C_LinComb V;
A2: @z = w & @yx = u + v;
A3: @xz = v + w & @ax = a * v;
A4: @az = a * w & @bx = b * v;
@x = v & @y = u;
then reconsider
K = v, L = u, M = w, LK = u + v, KM = v + w, aK = a * v, aM =
a * w, bK = b * v as C_Linear_Combination of V by A2,A3,A4;
A5: now
let v,u be (VECTOR of S), K,L;
A6: @@K = K & @@L = L;
assume v = K & u = L;
hence v + u = K + L by A6,Def15;
end;
hence v + w = K + M .= w + v by A5;
thus (u + v) + w = LK + M by A5
.= L + K + M by A5
.= L + (K + M) by Th22
.= L + KM by A5
.= u + (v + w) by A5;
thus v + 0.S = K + ZeroCLC V by A5
.= v by Th23;
- K in the carrier of S by Def12;
then - K in S;
then - K = vector(S,- K) by RLVECT_2:def 1;
then v + vector(S,- K) = K - K by A5
.= 0.S by Th37;
hence ex w being VECTOR of S st v + w = 0.S;
A7: now
let v be (VECTOR of S), L; let a be Complex;
assume v = L;
then (C_LCMult V).[a,v] = a*@@L by Def16;
hence a*v = a*L;
end;
hence a * (v + w) = a1 * KM .= a1 * (K + M) by A5
.= a1 * K + a1 * M by Th28
.= aK + a1 * M by A7
.= aK + aM by A7
.= a * v + a * w by A5;
thus (a + b) * v = (a1 + b1) * K by A7
.= a1 * K + b1 * K by Th27
.= aK + b * K by A7
.= aK + bK by A7
.= a * v + b * v by A5;
thus (a * b) * v = (a * b) * K by A7
.= a1 * (b1 * K) by Th29
.= a * (bK) by A7
.= a * (b * v) by A7;
thus 1r * v = 1r * K by A7
.= v by Th30;
end;
A8: for v be Element of S holds v is right_complementable by A1;
for u,v,w being VECTOR of S holds (u + v) + w = u + (v + w) by A1;
hence thesis by A1,A8,ALGSTR_0:def 16,CLVECT_1:def 2,def 3,def 4,def 5
,RLVECT_1:def 2,def 3,def 4;
end;
end;
registration
let V;
cluster LC_CLSpace V -> strict non empty;
coherence;
end;
theorem Th38:
vector(LC_CLSpace V,L1) + vector(LC_CLSpace V,L2) = L1 + L2
proof
set v2 = vector(LC_CLSpace V,L2);
A1: L1 = @@L1 & L2 = @@L2;
L2 in the carrier of LC_CLSpace V by Def12;
then
A2: L2 in LC_CLSpace V;
L1 in the carrier of LC_CLSpace V by Def12;
then L1 in LC_CLSpace V;
hence
vector(LC_CLSpace V,L1) + vector(LC_CLSpace V,L2) = (C_LCAdd V).[L1,v2]
by RLVECT_2:def 1
.= (C_LCAdd V).(@L1,@L2) by A2,RLVECT_2:def 1
.= L1 + L2 by A1,Def15;
end;
theorem Th39:
a * vector(LC_CLSpace V,L) = a * L
proof
L in the carrier of LC_CLSpace V by Def12;
then L in LC_CLSpace V;
then
A1: (C_LCMult V).[a,vector(LC_CLSpace V,L)] = (C_LCMult V).[a,@L] by
RLVECT_2:def 1;
@@L = L;
hence thesis by A1,Def16;
end;
theorem Th40:
- vector(LC_CLSpace V,L) = - L
proof
thus - vector(LC_CLSpace V,L) = (- 1r) * (vector(LC_CLSpace V,L)) by
CLVECT_1:3
.= - L by Th39;
end;
theorem
vector(LC_CLSpace V,L1) - vector(LC_CLSpace V,L2) = L1 - L2
proof
- L2 in C_LinComb V by Def12;
then
A1: - L2 in LC_CLSpace V;
- vector(LC_CLSpace V,L2) = - L2 by Th40
.= vector(LC_CLSpace V,- L2) by A1,RLVECT_2:def 1;
hence thesis by Th38;
end;
definition
let V;
let A;
func LC_CLSpace A -> strict Subspace of LC_CLSpace V means
the carrier of it = the set of all l ;
existence
proof
set X = the set of all l ;
X c= the carrier of LC_CLSpace V
proof
let x be object;
assume x in X;
then ex l st x = l;
hence thesis by Def12;
end;
then reconsider X as Subset of LC_CLSpace V;
A1: for v,u being VECTOR of LC_CLSpace V st v in X & u in X holds v + u in X
proof
let v,u be VECTOR of LC_CLSpace V;
assume that
A2: v in X and
A3: u in X;
consider l1 such that
A4: v = l1 by A2;
consider l2 such that
A5: u = l2 by A3;
A6: u = vector(LC_CLSpace V,l2) by A5,RLVECT_2:1;
v = vector(LC_CLSpace V,l1) by A4,RLVECT_2:1;
then v + u = l1 + l2 by A6,Th38;
hence thesis;
end;
ZeroCLC V is C_Linear_Combination of A by Th4;
then
A7: ZeroCLC V in X;
for a being Complex, v being VECTOR of LC_CLSpace V st v in X holds a
*v in X
proof
let a be Complex;
let v be VECTOR of LC_CLSpace V;
assume v in X;
then consider l such that
A8: v = l;
a * v = a * vector(LC_CLSpace V,l) by A8,RLVECT_2:1
.= a * l by Th39;
then a * v is C_Linear_Combination of A by Th26;
hence thesis;
end;
then X is linearly-closed by A1;
hence thesis by A7,CLVECT_1:54;
end;
uniqueness by CLVECT_1:49;
end;
begin :: Preliminaries for Complex Convex Sets
definition
let V be ComplexLinearSpace, W be Subspace of V;
func Up W -> Subset of V equals
the carrier of W;
coherence by CLVECT_1:def 8;
end;
registration
let V be ComplexLinearSpace, W be Subspace of V;
cluster Up W -> non empty;
coherence;
end;
definition
let V be non empty CLSStruct, S be Subset of V;
attr S is Affine means
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
the CLSStruct of V;
coherence
proof
set W = the CLSStruct of V;
A1: for v,w being VECTOR of W holds v + w = w + v
proof
let v,w be VECTOR of W;
reconsider v9=v,w9=w as VECTOR of V;
v+w = v9+w9;
hence v + w = w9 + v9 .= w + v;
end;
A2: for u,v,w being VECTOR of W holds (u + v) + w = u + (v + w)
proof
let u,v,w be VECTOR of W;
reconsider u9=u,v9=v,w9=w as VECTOR of V;
(u9 + v9) + w9 = u9 + (v9 + w9) by RLVECT_1:def 3;
hence thesis;
end;
A3: for v being VECTOR of W holds v is right_complementable
proof
let v be VECTOR of W;
reconsider v9 = v as VECTOR of V;
v9 is right_complementable by ALGSTR_0:def 16;
then consider w9 being VECTOR of V such that
A4: v9 + w9 = 0.V;
reconsider w = w9 as VECTOR of W;
take w;
thus thesis by A4;
end;
A5: for v being VECTOR of W holds v + 0.W = v
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus v + 0.W = v9 + 0.V .= v;
end;
A6: for a,b for v being VECTOR of W holds (a * b) * v = a * (b * v)
proof
let a,b;
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
(a * b) * v9 = a * (b * v9) by CLVECT_1:def 4;
hence thesis;
end;
A7: for a,b for v being VECTOR of W holds (a + b) * v = a * v + b * v
proof
let a,b;
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
(a + b) * v9 = a * v9 + b * v9 by CLVECT_1:def 3;
hence thesis;
end;
A8: for a for v,w being VECTOR of W holds a * (v + w) = a * v + a * w
proof
let a;
let v,w be VECTOR of W;
reconsider v9=v,w9=w as VECTOR of V;
a * (v9 + w9) = a * v9 + a * w9 by CLVECT_1:def 2;
hence thesis;
end;
for v being VECTOR of W holds 1r * v = v
proof
let v be VECTOR of W;
reconsider v9=v as VECTOR of V;
thus 1r * v = 1r * v9 .= v by CLVECT_1:def 5;
end;
then reconsider W as ComplexLinearSpace by A1,A2,A5,A3,A8,A7,A6,
ALGSTR_0:def 16,CLVECT_1:def 2,def 3,def 4,def 5,RLVECT_1:def 2,def 3,def 4;
A9: the Mult of W = (the Mult of V) | [:COMPLEX, the carrier of W:] by
RELSET_1:19;
0.W = 0.V & the addF of W = (the addF of V) || (the carrier of W) by
RELSET_1:19;
hence thesis by A9,CLVECT_1:def 8;
end;
end;
registration
let V be non empty CLSStruct;
cluster [#]V -> Affine;
coherence;
cluster empty -> Affine for Subset of V;
coherence;
end;
registration
let V be non empty CLSStruct;
cluster non empty Affine for Subset of V;
existence
proof
take [#]V;
thus thesis;
end;
cluster empty Affine for Subset of V;
existence
proof
take {}V;
thus thesis;
end;
end;
theorem Th42:
for a being Real, z being Complex holds Re(a*z)=a* Re(z)
proof
let a be Real;
let z be Complex;
Re(a * z) = Re a * Re z - Im a * Im z by COMPLEX1:9
.= Re a * Re z - 0 * Im z by COMPLEX1:def 2
.= a * Re (z) by COMPLEX1:def 1;
hence thesis;
end;
theorem Th43:
for a being Real, z being Complex holds Im(a*z) = a*Im(z)
proof
let a be Real;
let z be Complex;
Im(a * z) = Re a * Im z + Re z * Im a by COMPLEX1:9
.= Re a * Im z + Re z * 0 by COMPLEX1:def 2
.= a * Im (z) by COMPLEX1:def 1;
hence thesis;
end;
theorem Th44:
for a being Real , z being Complex st 0<=a & a<=1
holds |.a*z.| = a*|.z.| & |.(1r-a)*z.| = (1r-a)*|.z.|
proof
let a be Real;
let z be Complex;
assume that
A1: 0<=a and
A2: a<=1;
A3: |.(1r-a)*z.| = |.1r-a.|*|.z.| by COMPLEX1:65
.= (1r-a)*|.z.| by A2,COMPLEX1:43,XREAL_1:48;
|.a*z.| = |.a.|*|.z.| by COMPLEX1:65
.= a * |.z.| by A1,COMPLEX1:43;
hence thesis by A3;
end;
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
{r * v where v is Element of V: v in M};
coherence
proof
deffunc F(Element of V) = r * $1;
defpred P[set] means $1 in M;
{F(v) where v is Element of V: P[v]} is Subset of V from DOMAIN_1:sch 8;
hence thesis;
end;
end;
definition
let V be non empty CLSStruct;
let M be Subset of V;
attr M is convex means
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
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
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct;
let M be Subset of V;
let z be Complex;
assume
A1: M is convex;
for u,v being VECTOR of V, s being Complex st (ex p being Real st s=p &
0 < p & p < 1) & u in z*M & v in z*M holds s*u + (1r-s)*v in z*M
proof
let u,v be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: u in z*M and
A4: v in z*M;
consider v9 be Element of V such that
A5: v = z*v9 and
A6: v9 in M by A4;
consider u9 be Element of V such that
A7: u = z * u9 and
A8: u9 in M by A3;
A9: s*u + (1r-s)*v = s*z*u9 + (1r-s)*(z*v9) by A7,A5,CLVECT_1:def 4
.= z*s*u9 + z*(1r-s)*v9 by CLVECT_1:def 4
.= z*(s*u9) + z*(1r-s)*v9 by CLVECT_1:def 4
.= z*(s*u9) + z*((1r-s)*v9) by CLVECT_1:def 4
.= z*(s*u9 + (1r-s)*v9) by CLVECT_1:def 2;
s*u9 + (1r-s)*v9 in M by A1,A2,A8,A6;
hence thesis by A9;
end;
hence thesis;
end;
theorem
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
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
CLSStruct;
let M,N be Subset of V;
assume
A1: M is convex & N is convex;
for u,v being VECTOR of V, z being Complex st (ex r being Real st z=r &
0 < r & r < 1) & u in M+N & v in M+N holds z*u + (1r-z)*v in M+N
proof
let u,v be VECTOR of V;
let z be Complex;
assume that
A2: ex r being Real st z=r & 0 < r & r < 1 and
A3: u in M+N and
A4: v in M+N;
consider x2,y2 being Element of V such that
A5: v = x2 + y2 and
A6: x2 in M & y2 in N by A4;
consider x1,y1 being Element of V such that
A7: u = x1 + y1 and
A8: x1 in M & y1 in N by A3;
A9: z*u + (1r-z)*v = z*x1 + z*y1 + (1r-z)*(x2+y2) by A7,A5,CLVECT_1:def 2
.= z*x1 + z*y1 + ((1r-z)*x2 + (1r-z)*y2) by CLVECT_1:def 2
.= z*x1 + z*y1 + (1r-z)*x2 + (1r-z)*y2 by RLVECT_1:def 3
.= z*x1 + (1r-z)*x2 + z*y1 + (1r-z)*y2 by RLVECT_1:def 3
.= (z*x1 + (1r-z)*x2) + (z*y1 + (1r-z)*y2) by RLVECT_1:def 3;
z*x1 + (1r-z)*x2 in M & z*y1 + (1r-z)*y2 in N by A1,A2,A8,A6;
hence thesis by A9;
end;
hence thesis;
end;
theorem
for V being ComplexLinearSpace, M,N being Subset of V st M is convex &
N is convex holds M - N is convex
proof
let V be ComplexLinearSpace;
let M,N be Subset of V;
assume
A1: M is convex & N is convex;
for u,v being VECTOR of V, z being Complex st (ex r being Real st z=r &
0 < r & r < 1) & u in M-N & v in M-N holds z*u + (1r-z)*v in M-N
proof
let u,v be VECTOR of V;
let z be Complex;
assume that
A2: ex r being Real st z=r & 0 < r & r < 1 and
A3: u in M-N and
A4: v in M-N;
consider x2,y2 being Element of V such that
A5: v = x2 - y2 and
A6: x2 in M & y2 in N by A4;
consider x1,y1 being Element of V such that
A7: u = x1 - y1 and
A8: x1 in M & y1 in N by A3;
A9: z*u + (1r-z)*v = z*x1 - z*y1 + (1r-z)*(x2-y2) by A7,A5,CLVECT_1:9
.= z*x1 - z*y1 + ((1r-z)*x2 - (1r-z)*y2) by CLVECT_1:9
.= z*x1 - z*y1 + (1r-z)*x2 - (1r-z)*y2 by RLVECT_1:def 3
.= z*x1 - (z*y1 - (1r-z)*x2) - (1r-z)*y2 by RLVECT_1:29
.= z*x1 + ((1r-z)*x2 + (-z*y1)) - (1r-z)*y2 by RLVECT_1:33
.= z*x1 + (1r-z)*x2 + (-z*y1) - (1r-z)*y2 by RLVECT_1:def 3
.= z*x1 + (1r-z)*x2 + ((-z*y1) - (1r-z)*y2) by RLVECT_1:def 3
.= (z*x1 + (1r-z)*x2) - (z*y1 + (1r-z)*y2) by RLVECT_1:30;
z*x1 + (1r-z)*x2 in M & z*y1 + (1r-z)*y2 in N by A1,A2,A8,A6;
hence thesis by A9;
end;
hence thesis;
end;
theorem Th48:
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
proof
let V be non empty CLSStruct;
let M be Subset of V;
A1: M is convex implies for z being Complex st (ex r being Real st z=r & 0 <
r & r < 1) holds z*M + (1r-z)*M c= M
proof
assume
A2: M is convex;
let z be Complex;
assume
A3: ex r being Real st z=r & 0 < r & r < 1;
for x being Element of V st x in z*M + (1r-z)*M holds x in M
proof
let x be Element of V;
assume x in z*M + (1r-z)*M;
then consider u,v be Element of V such that
A4: x = u + v and
A5: u in z*M & v in (1r-z)*M;
( ex w1 be Element of V st u = z * w1 & w1 in M)& ex w2 be Element
of V st v = (1r-z)*w2 & w2 in M by A5;
hence thesis by A2,A3,A4;
end;
hence thesis;
end;
( for z being Complex st ( ex r being Real st z=r & 0 < r & r < 1 )
holds z*M + (1r-z)*M c= M ) implies M is convex
proof
assume
A6: for z being Complex st (ex r being Real st z=r & 0 < r & r < 1)
holds z*M + (1r-z)*M c= M;
let u,v be VECTOR of V;
let z be Complex;
assume ex r being Real st z=r & 0 < r & r < 1;
then
A7: z*M + (1r-z)*M c= M by A6;
assume u in M & v in M;
then z*u in z*M & (1r-z)*v in (1r-z)*M;
then z*u + (1r-z)*v in z*M + (1r-z)*M;
hence thesis by A7;
end;
hence thesis by A1;
end;
theorem
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
proof
let V be Abelian non empty CLSStruct;
let M be Subset of V;
assume
A1: M is convex;
let z be Complex;
assume
A2: ex r being Real st z=r & 0 < r & r < 1;
for x being Element of V st x in (1r-z)*M + z*M holds x in M
proof
let x be Element of V;
assume x in (1r-z)*M + z*M;
then consider u,v be Element of V such that
A3: x = u + v and
A4: u in (1r-z)*M & v in z*M;
( ex w1 be Element of V st u = (1r-z) * w1 & w1 in M)& ex w2 be
Element of V st v = z*w2 & w2 in M by A4;
hence thesis by A1,A2,A3;
end;
hence thesis;
end;
theorem
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
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
CLSStruct;
let M,N be Subset of V;
assume that
A1: M is convex and
A2: N is convex;
let z be Complex;
let u,v be VECTOR of V;
let s be Complex;
assume that
A3: ex p being Real st s=p & 0 < p & p < 1 and
A4: u in z*M + (1r-z)*N and
A5: v in z*M + (1r-z)*N;
consider x2,y2 be VECTOR of V such that
A6: v = x2 + y2 and
A7: x2 in z*M and
A8: y2 in (1r-z)*N by A5;
consider x1,y1 be VECTOR of V such that
A9: u = x1 + y1 and
A10: x1 in z*M and
A11: y1 in (1r-z)*N by A4;
consider mx2 be VECTOR of V such that
A12: x2 = z*mx2 and
A13: mx2 in M by A7;
consider mx1 be VECTOR of V such that
A14: x1 = z*mx1 and
A15: mx1 in M by A10;
A16: s*x1 + (1r-s)*x2 = s*z*mx1 + (1r-s)*(z*mx2) by A14,A12,CLVECT_1:def 4
.= s*z*mx1 + (1r-s)*z*mx2 by CLVECT_1:def 4
.= z*(s*mx1) + (1r-s)*z*mx2 by CLVECT_1:def 4
.= z*(s*mx1) + z*((1r-s)*mx2) by CLVECT_1:def 4
.= z*(s*mx1 + (1r-s)*mx2) by CLVECT_1:def 2;
consider ny2 be VECTOR of V such that
A17: y2 = (1r-z)*ny2 and
A18: ny2 in N by A8;
consider ny1 be VECTOR of V such that
A19: y1 = (1r-z)*ny1 and
A20: ny1 in N by A11;
A21: s*y1 + (1r-s)*y2 = s*(1r-z)*ny1 + (1r-s)*((1r-z)*ny2) by A19,A17,
CLVECT_1:def 4
.= s*(1r-z)*ny1 + (1r-s)*(1r-z)*ny2 by CLVECT_1:def 4
.= (1r-z)*(s*ny1) + (1r-s)*(1r-z)*ny2 by CLVECT_1:def 4
.= (1r-z)*(s*ny1) + (1r-z)*((1r-s)*ny2) by CLVECT_1:def 4
.= (1r-z)*(s*ny1 + (1r-s)*ny2) by CLVECT_1:def 2;
s*ny1 + (1r-s)*ny2 in N by A2,A3,A20,A18;
then
A22: s*y1 + (1r-s)*y2 in (1r-z)*N by A21;
s*mx1 + (1r-s)*mx2 in M by A1,A3,A15,A13;
then
A23: s*x1 + (1r-s)*x2 in z*M by A16;
s*u + (1r-s)*v = s*x1 + s*y1 + (1r-s)*(x2 + y2) by A9,A6,CLVECT_1:def 2
.= s*x1 + s*y1 + ((1r-s)*x2 + (1r-s)*y2) by CLVECT_1:def 2
.= s*x1 + s*y1 + (1r-s)*x2 + (1r-s)*y2 by RLVECT_1:def 3
.= s*x1 + (1r-s)*x2 + s*y1 + (1r-s)*y2 by RLVECT_1:def 3
.= (s*x1 + (1r-s)*x2) + (s*y1 + (1r-s)*y2) by RLVECT_1:def 3;
hence thesis by A23,A22;
end;
theorem Th51:
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct, M be
Subset of V holds 1r*M = M
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct;
let M be Subset of V;
for v being Element of V st v in M holds v in 1r*M
proof
let v be Element of V;
A1: v = 1r*v by CLVECT_1:def 5;
assume v in M;
hence thesis by A1;
end;
then
A2: M c= 1r*M;
for v being Element of V st v in 1r*M holds v in M
proof
let v be Element of V;
assume v in 1r*M;
then ex x be Element of V st v = 1r*x & x in M;
hence thesis by CLVECT_1:def 5;
end;
then 1r*M c= M;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th52:
for V being ComplexLinearSpace, M be non empty Subset of V holds
0c * M = {0.V}
proof
let V be ComplexLinearSpace;
let M be non empty Subset of V;
for v being Element of V st v in {0.V} holds v in 0c * M
proof
let v be Element of V;
consider x being object such that
A1: x in M by XBOOLE_0:def 1;
reconsider x as Element of V by A1;
assume v in {0.V};
then v = 0.V by TARSKI:def 1;
then v = 0c * x by CLVECT_1:1;
hence thesis by A1;
end;
then
A2: {0.V} c= 0c * M;
for v being Element of V st v in 0c * M holds v in {0.V}
proof
let v be Element of V;
assume v in 0c * M;
then ex x be Element of V st v = 0c * x & x in M;
then v = 0.V by CLVECT_1:1;
hence thesis by TARSKI:def 1;
end;
then 0c * M c= {0.V};
hence thesis by A2,XBOOLE_0:def 10;
end;
::$CT
theorem Th53:
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
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct;
let M be Subset of V;
let z1,z2 be Complex;
for x being VECTOR of V st x in z1*(z2*M) holds x in (z1*z2)*M
proof
let x be VECTOR of V;
assume x in z1*(z2*M);
then consider w1 be VECTOR of V such that
A1: x = z1*w1 and
A2: w1 in z2*M;
consider w2 be VECTOR of V such that
A3: w1 = z2*w2 and
A4: w2 in M by A2;
x = (z1*z2)*w2 by A1,A3,CLVECT_1:def 4;
hence thesis by A4;
end;
then
A5: z1*(z2*M) c= (z1*z2)*M;
for x being VECTOR of V st x in (z1*z2)*M holds x in z1*(z2*M)
proof
let x be VECTOR of V;
assume x in (z1*z2)*M;
then consider w1 be VECTOR of V such that
A6: x = (z1*z2)*w1 & w1 in M;
x = z1*(z2*w1) & z2*w1 in z2*M by A6,CLVECT_1:def 4;
hence thesis;
end;
then (z1*z2)*M c= z1*(z2*M);
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem Th54:
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
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct;
let M1,M2 be Subset of V;
let z be Complex;
for x being VECTOR of V st x in z*M1 + z*M2 holds x in z*(M1+M2)
proof
let x be VECTOR of V;
assume x in z*M1 + z*M2;
then consider w1,w2 be VECTOR of V such that
A1: x = w1 + w2 and
A2: w1 in z*M1 and
A3: w2 in z*M2;
consider v2 be VECTOR of V such that
A4: w2 = z * v2 and
A5: v2 in M2 by A3;
consider v1 be VECTOR of V such that
A6: w1 = z * v1 and
A7: v1 in M1 by A2;
A8: v1 + v2 in M1 + M2 by A7,A5;
x = z*(v1 + v2) by A1,A6,A4,CLVECT_1:def 2;
hence thesis by A8;
end;
then
A9: z*M1 + z*M2 c= z*(M1+M2);
for x being VECTOR of V st x in z*(M1+M2) holds x in z*M1 + z*M2
proof
let x be VECTOR of V;
assume x in z*(M1+M2);
then consider w9 be VECTOR of V such that
A10: x = z*w9 and
A11: w9 in M1 + M2;
consider w1,w2 be VECTOR of V such that
A12: w9 = w1 + w2 and
A13: w1 in M1 & w2 in M2 by A11;
A14: z*w1 in z*M1 & z*w2 in z*M2 by A13;
x = z*w1 + z*w2 by A10,A12,CLVECT_1:def 2;
hence thesis by A14;
end;
then z*(M1 + M2) c= z*M1 + z*M2;
hence thesis by A9,XBOOLE_0:def 10;
end;
theorem
for V being ComplexLinearSpace, M being Subset of V, v being VECTOR of
V holds M is convex iff v + M is convex
proof
let V be ComplexLinearSpace;
let M be Subset of V;
let v be VECTOR of V;
A1: v + M is convex implies M is convex
proof
assume
A2: v + M is convex;
let w1,w2 be VECTOR of V;
let z be Complex;
assume that
A3: ex r being Real st z=r & 0 < r & r < 1 and
A4: w1 in M & w2 in M;
set x1 = v + w1, x2 = v + w2;
x1 in v + M & x2 in {v + w where w is VECTOR of V : w in M} by A4;
then
A5: z*x1 + (1r-z)*x2 in v + M by A2,A3;
z*x1 + (1r-z)*x2 = z*v + z*w1 + (1r-z)*(v + w2) by CLVECT_1:def 2
.= z*v + z*w1 + ((1r-z)*v + (1r-z)*w2) by CLVECT_1:def 2
.= z*v + z*w1 + (1r-z)*v + (1r-z)*w2 by RLVECT_1:def 3
.= z*v + (1r-z)*v + z*w1 + (1r-z)*w2 by RLVECT_1:def 3
.= (z+(1r-z))*v + z*w1 + (1r-z)*w2 by CLVECT_1:def 3
.= v + z*w1 + (1r-z)*w2 by CLVECT_1:def 5
.= v + (z*w1 + (1r-z)*w2) by RLVECT_1:def 3;
then
ex w be VECTOR of V st v + (z*w1 + (1r-z)*w2) = v + w & w in M by A5;
hence thesis by RLVECT_1:8;
end;
M is convex implies v + M is convex
proof
assume
A6: M is convex;
let w1,w2 be VECTOR of V;
let z be Complex;
assume that
A7: ex r being Real st z=r & 0 < r & r < 1 and
A8: w1 in v + M and
A9: w2 in v + M;
consider x2 be VECTOR of V such that
A10: w2 = v + x2 and
A11: x2 in M by A9;
consider x1 be VECTOR of V such that
A12: w1 = v + x1 and
A13: x1 in M by A8;
A14: z*w1 + (1r-z)*w2 = z*v + z*x1 + (1r-z)*(v+x2) by A12,A10,CLVECT_1:def 2
.= z*v + z*x1 + ((1r-z)*v + (1r-z)*x2) by CLVECT_1:def 2
.= z*v + z*x1 + (1r-z)*v + (1r-z)*x2 by RLVECT_1:def 3
.= z*v + (1r-z)*v + z*x1 + (1r-z)*x2 by RLVECT_1:def 3
.= (z+(1r-z))*v + z*x1 + (1r-z)*x2 by CLVECT_1:def 3
.= v + z*x1 + (1r-z)*x2 by CLVECT_1:def 5
.= v + (z*x1 + (1r-z)*x2) by RLVECT_1:def 3;
z*x1 + (1r-z)*x2 in M by A6,A7,A13,A11;
hence thesis by A14;
end;
hence thesis by A1;
end;
theorem
for V being ComplexLinearSpace holds Up((0).V) is convex
proof
let V be ComplexLinearSpace;
let u,v be VECTOR of V;
let z be Complex;
assume that
ex r being Real st z=r & 0 < r & r < 1 and
A1: u in Up((0).V) and
A2: v in Up((0).V);
v in {0.V} by A2,CLVECT_1:def 9;
then
A3: v = 0.V by TARSKI:def 1;
u in {0.V} by A1,CLVECT_1:def 9;
then u = 0.V by TARSKI:def 1;
then z * u + (1r-z) * v = 0.V + (1r-z) * 0.V by A3,CLVECT_1:1
.= 0.V + 0.V by CLVECT_1:1
.= 0.V;
then z * u + (1r-z) * v in {0.V} by TARSKI:def 1;
hence thesis by CLVECT_1:def 9;
end;
theorem
for V being ComplexLinearSpace holds Up((Omega).V) is convex;
theorem
for V being non empty CLSStruct, M being Subset of V st M = {}
holds M is convex;
theorem Th59:
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
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
CLSStruct;
let M1,M2 be Subset of V;
let z1,z2 be Complex;
assume that
A1: M1 is convex and
A2: M2 is convex;
let u,v be VECTOR of V;
let s be Complex;
assume that
A3: ex p being Real st s=p & 0 < p & p < 1 and
A4: u in z1*M1 + z2*M2 and
A5: v in z1*M1 + z2*M2;
consider v1,v2 be VECTOR of V such that
A6: v = v1 + v2 and
A7: v1 in z1*M1 and
A8: v2 in z2*M2 by A5;
consider u1,u2 be VECTOR of V such that
A9: u = u1 + u2 and
A10: u1 in z1*M1 and
A11: u2 in z2*M2 by A4;
consider y1 be VECTOR of V such that
A12: v1 = z1*y1 and
A13: y1 in M1 by A7;
consider x1 be VECTOR of V such that
A14: u1 = z1*x1 and
A15: x1 in M1 by A10;
A16: s*u1 + (1r-s)*v1 = z1*s*x1 + (1r-s)*(z1*y1) by A14,A12,CLVECT_1:def 4
.= z1*s*x1 + z1*(1r-s)*y1 by CLVECT_1:def 4
.= z1*(s*x1) + z1*(1r-s)*y1 by CLVECT_1:def 4
.= z1*(s*x1) + z1*((1r-s)*y1) by CLVECT_1:def 4
.= z1*(s*x1 + (1r-s)*y1) by CLVECT_1:def 2;
consider y2 be VECTOR of V such that
A17: v2 = z2*y2 and
A18: y2 in M2 by A8;
consider x2 be VECTOR of V such that
A19: u2 = z2*x2 and
A20: x2 in M2 by A11;
A21: s*u2 + (1r-s)*v2 = z2*s*x2 + (1r-s)*(z2*y2) by A19,A17,CLVECT_1:def 4
.= z2*s*x2 + z2*(1r-s)*y2 by CLVECT_1:def 4
.= z2*(s*x2) + z2*(1r-s)*y2 by CLVECT_1:def 4
.= z2*(s*x2) + z2*((1r-s)*y2) by CLVECT_1:def 4
.= z2*(s*x2 + (1r-s)*y2) by CLVECT_1:def 2;
s*x2 + (1r-s)*y2 in M2 by A2,A3,A20,A18;
then
A22: s*u2 + (1r-s)*v2 in z2*M2 by A21;
s*x1 + (1r-s)*y1 in M1 by A1,A3,A15,A13;
then
A23: s*u1 + (1r-s)*v1 in z1*M1 by A16;
s*(u1+u2) + (1r-s)*(v1+v2) = s*u1 + s*u2 + (1r-s)*(v1+v2) by CLVECT_1:def 2
.= s*u1 + s*u2 + ((1r-s)*v1 + (1r-s)*v2) by CLVECT_1:def 2
.= s*u1 + s*u2 + (1r-s)*v1 + (1r-s)*v2 by RLVECT_1:def 3
.= s*u1 + (1r-s)*v1 + s*u2 + (1r-s)*v2 by RLVECT_1:def 3
.= s*u1 + (1r-s)*v1 + (s*u2 + (1r-s)*v2) by RLVECT_1:def 3;
hence thesis by A9,A6,A23,A22;
end;
theorem Th60:
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
proof
let V be vector-distributive scalar-distributive scalar-associative
scalar-unital non empty CLSStruct;
let M be Subset of V;
let z1,z2 be Complex;
for x being VECTOR of V st x in (z1+z2)*M holds x in z1*M + z2*M
proof
let x be VECTOR of V;
assume x in (z1+z2)*M;
then consider w be VECTOR of V such that
A1: x = (z1 + z2)*w and
A2: w in M;
A3: z2*w in z2*M by A2;
x = z1*w + z2*w & z1*w in z1*M by A1,A2,CLVECT_1:def 3;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th61:
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
proof
let V be non empty CLSStruct;
let M,N be Subset of V;
let z be Complex;
assume
A1: M c= N;
now
let x be VECTOR of V;
assume x in z*M;
then ex w be VECTOR of V st x = z*w & w in M;
hence x in z*N by A1;
end;
hence thesis;
end;
theorem Th62:
for V being non empty CLSStruct, M being empty Subset of V, z
being Complex holds z * M = {}
proof
let V be non empty CLSStruct;
let M be empty Subset of V;
let z be Complex;
now
let x be VECTOR of V;
assume x in z * M;
then ex v be VECTOR of V st x = z * v & v in {};
hence x in {};
end;
then z * M c= {};
hence thesis;
end;
Lm2: 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 c= (z1 + z2)*M
proof
let V be ComplexLinearSpace;
let M be Subset of V;
let z1,z2 be Complex;
assume that
A1: ex r1, r2 being Real st z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0 and
A2: M is convex;
consider r1, r2 being Real such that
A3: z1=r1 and
A4: z2=r2 and
A5: r1 >= 0 and
A6: r2 >= 0 by A1;
per cases;
suppose
M is empty;
then z1*M = {} & (z1+z2)*M = {} by Th62;
hence thesis by CONVEX1:40;
end;
suppose
A7: M is non empty;
per cases;
suppose
A8: z1 = 0;
then z1*M = {0.V} by A7,Th52;
hence thesis by A8,CONVEX1:35;
end;
suppose
A9: z2 = 0;
then z2*M = {0.V} by A7,Th52;
hence thesis by A9,CONVEX1:35;
end;
suppose
A10: z1 <> 0 & z2 <> 0;
then r1 + r2 > r1 by A4,A6,XREAL_1:29;
then r1/(r1+r2) < 1 by A5,XREAL_1:189;
then
z1/(z1+z2) * M + (1r - z1/(z1+z2)) * M c= M by A2,A3,A4,A5,A6,A10,Th48;
then
A11: (z1+z2)*(z1/(z1+z2)*M + (1r-z1/(z1+z2))*M) c= (z1+z2)*M by Th61;
1-r1/(r1+r2) = (r1+r2)/(r1+r2) - r1/(r1+r2) by A3,A5,A6,A10,XCMPLX_1:60;
then 1-r1/(r1+r2) = (r1+r2-r1)/(r1+r2);
then
A12: (z1+z2)*((1r-z1/(z1+z2))*M) = z2/(z1+z2)*(z1+z2)*M by A3,A4,Th53
.= z2*M by A3,A4,A5,A6,A10,XCMPLX_1:87;
(z1+z2)*(z1/(z1+z2)*M) = (z1/(z1+z2))*(z1+z2)*M by Th53
.= z1*M by A3,A4,A5,A6,A10,XCMPLX_1:87;
hence thesis by A11,A12,Th54;
end;
end;
end;
::$CT 2
theorem
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
proof
let V be ComplexLinearSpace, M be Subset of V, z1,z2 be Complex;
assume
( ex r1,r2 being Real st z1=r1 & z2=r2 & r1 >= 0 & r2 >= 0)& M is convex;
hence z1*M + z2*M c= (z1 + z2)*M by Lm2;
thus thesis by Th60;
end;
theorem
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
proof
let V be Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
CLSStruct;
let M1,M2,M3 be Subset of V;
let z1,z2,z3 be Complex;
assume that
A1: M1 is convex & M2 is convex and
A2: M3 is convex;
z1*M1 + z2*M2 is convex by A1,Th59;
then 1r*(z1*M1 + z2*M2) + z3*M3 is convex by A2,Th59;
hence thesis by Th51;
end;
theorem Th65:
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
proof
let V be non empty CLSStruct;
let F be Subset-Family of V;
assume
A1: for M being Subset of V st M in F holds M is convex;
per cases;
suppose
F = {};
then meet F = {} by SETFAM_1:def 1;
hence thesis;
end;
suppose
A2: F <> {};
thus meet F is convex
proof
let u,v be VECTOR of V;
let z be Complex;
assume that
A3: ex r being Real st z=r & 0 < r & r < 1 and
A4: u in meet F and
A5: v in meet F;
for M being set st M in F holds z*u + (1r-z)*v in M
proof
let M be set;
assume
A6: M in F;
then reconsider M as Subset of V;
A7: v in M by A5,A6,SETFAM_1:def 1;
M is convex & u in M by A1,A4,A6,SETFAM_1:def 1;
hence thesis by A3,A7;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
end;
end;
theorem Th66:
for V being non empty CLSStruct, M being Subset of V st M is
Affine holds M is convex
proof
let V be non empty CLSStruct;
let M be Subset of V;
assume
A1: M is Affine;
let u,v be VECTOR of V;
let z be Complex;
assume that
A2: ex r being Real st z=r & 0 < r & r < 1 and
A3: u in M & v in M;
set s = 1r-z;
consider r being Real such that
A4: z=r and
0 < r and
r < 1 by A2;
s=1-r by A4;
then (1r-s)*u+s*v in M by A1,A3;
hence thesis;
end;
registration
let V be non empty CLSStruct;
cluster non empty convex for Subset of V;
existence
proof
set M = the non empty Affine Subset of V;
M is convex by Th66;
hence thesis;
end;
end;
registration
let V be non empty CLSStruct;
cluster empty convex for Subset of V;
existence
proof
{}V is convex;
hence thesis;
end;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) >= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) >= r by A1,A4;
consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
1-p > 0 by A8,XREAL_1:50;
then
A9: (1-p)*Re(y.|.v) >= (1-p)*r by A5,XREAL_1:64;
ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) >= r by A1,A3;
then p*Re(x.|.v) >= p*r by A7,XREAL_1:64;
then
A10: p*Re(x.|.v) + (1-p)*Re(y.|.v ) >= p*r + (1-p)*r by A9,XREAL_1:7;
Re( (s*x+(1r-s)*y).|.v ) = Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:8
.= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A6,Th42
.= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A6,Th42;
hence thesis by A1,A10;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) > r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) > r by A1,A4;
consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
1-p > 0 by A8,XREAL_1:50;
then
A9: (1-p)*Re(y.|.v) > (1-p)*r by A5,XREAL_1:68;
ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) > r by A1,A3;
then p*Re(x.|.v) > p*r by A7,XREAL_1:68;
then
A10: p*Re(x.|.v) + (1-p)*Re(y.|.v ) > p*r + (1-p)*r by A9,XREAL_1:8;
Re( (s*x+(1r-s)*y).|.v ) = Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:8
.= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A6,Th42
.= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A6,Th42;
hence thesis by A1,A10;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) <= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) <= r by A1,A4;
consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
1-p > 0 by A8,XREAL_1:50;
then
A9: (1-p)*Re(y.|.v) <= (1-p)*r by A5,XREAL_1:64;
ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) <= r by A1,A3;
then p*Re(x.|.v) <= p*r by A7,XREAL_1:64;
then
A10: p*Re(x.|.v) + (1-p)*Re(y.|.v ) <= p*r + (1-p)*r by A9,XREAL_1:7;
Re( (s*x+(1r-s)*y).|.v ) = Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:8
.= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A6,Th42
.= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A6,Th42;
hence thesis by A1,A10;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Re(u.|.v) < r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Re(u2.|.v) < r by A1,A4;
consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
1-p > 0 by A8,XREAL_1:50;
then
A9: (1-p)*Re(y.|.v) < (1-p)*r by A5,XREAL_1:68;
ex u1 be VECTOR of V st x = u1 & Re(u1.|.v) < r by A1,A3;
then p*Re(x.|.v) < p*r by A7,XREAL_1:68;
then
A10: p*Re(x.|.v) + (1-p)*Re(y.|.v ) < p*r + (1-p)*r by A9,XREAL_1:8;
Re( (s*x+(1r-s)*y).|.v ) = Re( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Re( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Re( s*(x.|.v))+Re((1r-s)*(y.|.v)) by COMPLEX1:8
.= p*Re( x.|.v ) + Re((1r-s)*(y.|.v)) by A6,Th42
.= p*Re( x.|.v ) + (1-p)*Re( y.|.v ) by A6,Th42;
hence thesis by A1,A10;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) >= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) >= r by A1,A4;
consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
1-p > 0 by A8,XREAL_1:50;
then
A9: (1-p)*Im(y.|.v) >= (1-p)*r by A5,XREAL_1:64;
ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) >= r by A1,A3;
then p*Im(x.|.v) >= p*r by A7,XREAL_1:64;
then
A10: p*Im(x.|.v) + (1-p)*Im(y.|.v ) >= p*r + (1-p)*r by A9,XREAL_1:7;
Im( (s*x+(1r-s)*y).|.v ) = Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:8
.= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A6,Th43
.= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A6,Th43;
hence thesis by A1,A10;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) > r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) > r by A1,A4;
consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
1-p > 0 by A8,XREAL_1:50;
then
A9: (1-p)*Im(y.|.v) > (1-p)*r by A5,XREAL_1:68;
ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) > r by A1,A3;
then p*Im(x.|.v) > p*r by A7,XREAL_1:68;
then
A10: p*Im(x.|.v) + (1-p)*Im(y.|.v ) > p*r + (1-p)*r by A9,XREAL_1:8;
Im( (s*x+(1r-s)*y).|.v ) = Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:8
.= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A6,Th43
.= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A6,Th43;
hence thesis by A1,A10;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) <= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) <= r by A1,A4;
consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
1-p > 0 by A8,XREAL_1:50;
then
A9: (1-p)*Im(y.|.v) <= (1-p)*r by A5,XREAL_1:64;
ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) <= r by A1,A3;
then p*Im(x.|.v) <= p*r by A7,XREAL_1:64;
then
A10: p*Im(x.|.v) + (1-p)*Im(y.|.v ) <= p*r + (1-p)*r by A9,XREAL_1:7;
Im( (s*x+(1r-s)*y).|.v ) = Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:8
.= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A6,Th43
.= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A6,Th43;
hence thesis by A1,A10;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : Im(u.|.v) < r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
A5: ex u2 be VECTOR of V st y = u2 & Im(u2.|.v) < r by A1,A4;
consider p being Real such that
A6: s=p and
A7: 0 < p and
A8: p < 1 by A2;
1-p > 0 by A8,XREAL_1:50;
then
A9: (1-p)*Im(y.|.v) < (1-p)*r by A5,XREAL_1:68;
ex u1 be VECTOR of V st x = u1 & Im(u1.|.v) < r by A1,A3;
then p*Im(x.|.v) < p*r by A7,XREAL_1:68;
then
A10: p*Im(x.|.v) + (1-p)*Im(y.|.v ) < p*r + (1-p)*r by A9,XREAL_1:8;
Im( (s*x+(1r-s)*y).|.v ) = Im( (s*x).|.v+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+((1r-s)*y).|.v ) by CSSPACE:def 13
.= Im( s*(x.|.v)+(1r-s)*(y.|.v) ) by CSSPACE:def 13
.= Im( s*(x.|.v))+Im((1r-s)*(y.|.v)) by COMPLEX1:8
.= p*Im( x.|.v ) + Im((1r-s)*(y.|.v)) by A6,Th43
.= p*Im( x.|.v ) + (1-p)*Im( y.|.v ) by A6,Th43;
hence thesis by A1,A10;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : |.u.|.v.| <= r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
consider p being Real such that
A5: s=p and
A6: 0 < p and
A7: p < 1 by A2;
A8: 1-p > 0 by A7,XREAL_1:50;
ex u2 be VECTOR of V st y = u2 & |.u2.|.v.| <= r by A1,A4;
then
A9: (1-p)*|.y.|.v.| <= (1-p)*r by A8,XREAL_1:64;
ex u1 be VECTOR of V st x = u1 & |.u1.|.v.| <= r by A1,A3;
then p*|.x.|.v.| <= p*r by A6,XREAL_1:64;
then
A10: p*|.x.|.v.|+(1-p)*|.y.|.v.| <= p*r + (1-p)*r by A9,XREAL_1:7;
|.s*(x.|.v).| = p*|.x.|.v.| & |.(1r-s)*(y.|.v).| = (1-p)*|.y.|.v.| by A5,A6
,A7,Th44;
then
A11: |.s*(x.|.v)+(1r-s)*(y.|.v).| <= p*|.x.|.v.| + (1-p)*|.y.|.v.| by
COMPLEX1:56;
|.(s*x+(1r-s)*y).|.v.| = |.(s*x).|.v+((1r-s)*y).|.v.| by CSSPACE:def 13
.= |.s*(x.|.v)+((1r-s)*y).|.v.| by CSSPACE:def 13
.= |. s*(x.|.v)+(1r-s)*(y.|.v).| by CSSPACE:def 13;
then |.(s*x+(1r-s)*y).|.v.| <= r by A11,A10,XXREAL_0:2;
hence thesis by A1;
end;
theorem
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
proof
let V be ComplexUnitarySpace-like non empty CUNITSTR;
let M be Subset of V;
let v be VECTOR of V;
let r be Real;
assume
A1: M = {u where u is VECTOR of V : |.u.|.v.| < r };
let x,y be VECTOR of V;
let s be Complex;
assume that
A2: ex p being Real st s=p & 0 < p & p < 1 and
A3: x in M and
A4: y in M;
consider p being Real such that
A5: s=p and
A6: 0 < p and
A7: p < 1 by A2;
A8: 1-p > 0 by A7,XREAL_1:50;
ex u2 be VECTOR of V st y = u2 & |.u2.|.v.| < r by A1,A4;
then
A9: (1-p)*|.y.|.v.| < (1-p)*r by A8,XREAL_1:68;
ex u1 be VECTOR of V st x = u1 & |.u1.|.v.| < r by A1,A3;
then p*|.x.|.v.| < p*r by A6,XREAL_1:68;
then
A10: p*|.x.|.v.|+(1-p)*|.y.|.v.| < p*r + (1-p)*r by A9,XREAL_1:8;
|.s*(x.|.v).| = p*|.x.|.v.| & |.(1r-s)*(y.|.v).| = (1-p)*|.y.|.v.| by A5,A6
,A7,Th44;
then
A11: |.s*(x.|.v)+(1r-s)*(y.|.v).| <= p*|.x.|.v.| + (1-p)*|.y.|.v.| by
COMPLEX1:56;
|.(s*x+(1r-s)*y).|.v.| = |.(s*x).|.v+((1r-s)*y).|.v.| by CSSPACE:def 13
.= |.s*(x.|.v)+((1r-s)*y).|.v.| by CSSPACE:def 13
.= |. s*(x.|.v)+(1r-s)*(y.|.v).| by CSSPACE:def 13;
then |.(s*x+(1r-s)*y).|.v.| < r by A11,A10,XXREAL_0:2;
hence thesis by A1;
end;
begin :: Complex Convex Combinations
definition
let V be ComplexLinearSpace, L be C_Linear_Combination of V;
attr L is convex means
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 Th77:
for V being ComplexLinearSpace, L being C_Linear_Combination of
V st L is convex holds Carrier L <> {}
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
assume L is convex;
then consider F being FinSequence of the carrier of V such that
A1: F is one-to-one & rng F = Carrier L and
A2: 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;
consider f being FinSequence of REAL such that
A3: 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 by A2;
assume Carrier L = {};
then len F = 0 by A1,CARD_1:27,FINSEQ_4:62;
then f = <*>the carrier of V by A3;
hence contradiction by A3,RVSUM_1:72;
end;
theorem
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
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
let v be VECTOR of V;
assume that
A1: L is convex and
A2: ex r being Real st r = L.v & r <= 0;
consider r being Real such that
A3: r = L.v and
A4: r <= 0 by A2;
per cases by A4;
suppose
r = 0;
hence thesis by A3,Th1;
end;
suppose
A5: r < 0;
now
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A6: rng F = Carrier L and
A7: 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 by A1;
assume v in Carrier L;
then consider n be object such that
A8: n in dom F and
A9: F.n = v by A6,FUNCT_1:def 3;
reconsider n as Element of NAT by A8;
consider f being FinSequence of REAL such that
A10: len f = len F and
Sum f = 1 and
A11: for n being Nat st n in dom f holds f.n =L.(F.n) & f.n >= 0 by A7;
n in Seg len F by A8,FINSEQ_1:def 3;
then
A12: n in dom f by A10,FINSEQ_1:def 3;
then L.v = f.n by A11,A9;
hence contradiction by A3,A5,A11,A12;
end;
hence thesis;
end;
end;
theorem
for V being ComplexLinearSpace, L being C_Linear_Combination of V st L
is convex holds L <> ZeroCLC V
proof
let V be ComplexLinearSpace;
let L be C_Linear_Combination of V;
assume L is convex;
then
A1: Carrier L <> {} by Th77;
assume L = ZeroCLC V;
hence contradiction by A1;
end;
theorem Th80:
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
proof
let V be ComplexLinearSpace;
let v be VECTOR of V;
let L be C_Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier L = {v};
reconsider L as C_Linear_Combination of {v} by A2,Def4;
consider F being FinSequence of the carrier of V such that
A3: F is one-to-one & rng F = Carrier L and
A4: 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 by A1;
A5: F = <*v*> by A2,A3,FINSEQ_3:97;
consider f be FinSequence of REAL such that
A6: len f = len F and
A7: Sum f = 1 and
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A4;
reconsider r = f/.1 as Element of REAL;
card Carrier L = 1 by A2,CARD_1:30;
then len F = 1 by A3,FINSEQ_4:62;
then
A9: dom f = Seg 1 by A6,FINSEQ_1:def 3;
then
A10: 1 in dom f;
then
A11: f.1 = f/.1 by PARTFUN1:def 6;
then
A12: f = <* r *> by A9,FINSEQ_1:def 8;
f.1 = L.(F.1) by A8,A10;
then r = L.v by A11,A5,FINSEQ_1:def 8;
hence thesis by A7,A12,Th14,FINSOP_1:11;
end;
theorem Th81:
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
proof
let V be ComplexLinearSpace;
let v1,v2 be VECTOR of V;
let L be C_Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier L = {v1,v2} and
A3: v1 <> v2;
reconsider L as C_Linear_Combination of {v1,v2} by A2,Def4;
consider F being FinSequence of the carrier of V such that
A4: F is one-to-one & rng F = Carrier L and
A5: 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 by A1;
consider f be FinSequence of REAL such that
A6: len f = len F and
A7: Sum f = 1 and
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A5;
len F = card {v1,v2} by A2,A4,FINSEQ_4:62;
then
A9: len f = 2 by A3,A6,CARD_2:57;
then
A10: dom f = {1,2} by FINSEQ_1:2,def 3;
then
A11: 2 in dom f by TARSKI:def 2;
then
A12: f.2 = L.(F.2) by A8;
then f/.2 = L.(F.2) by A11,PARTFUN1:def 6;
then reconsider r2 = L.(F.2) as Real;
A13: f.2 >= 0 by A8,A11;
A14: 1 in dom f by A10,TARSKI:def 2;
then
A15: f.1 = L.(F.1) by A8;
then f/.1 = L.(F.1) by A14,PARTFUN1:def 6;
then reconsider r1 = L.(F.1) as Real;
A16: f = <*r1,r2*> by A9,A15,A12,FINSEQ_1:44;
ex c1,c2 being Real st c1=L.v1 & c2=L.v2 & c1+c2=1 & c1>=0 &c2>=0
proof
per cases by A2,A3,A4,FINSEQ_3:99;
suppose
F = <*v1,v2*>;
then
A17: r1 = L.v1 & r2 = L.v2 by FINSEQ_1:44;
r1 + r2 = 1 & r1 >= 0 by A7,A8,A14,A15,A16,RVSUM_1:77;
hence thesis by A12,A13,A17;
end;
suppose
F = <*v2,v1*>;
then
A18: r1 = L.v2 & r2 = L.v1 by FINSEQ_1:44;
r1 + r2 = 1 & r1 >= 0 by A7,A8,A14,A15,A16,RVSUM_1:77;
hence thesis by A12,A13,A18;
end;
end;
hence thesis by A3,Th15;
end;
Lm3: 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 holds
Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3
proof
let V be ComplexLinearSpace;
let v1,v2,v3 be VECTOR of V;
let L be C_Linear_Combination of {v1,v2,v3};
assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1;
A4: Carrier L c= {v1,v2,v3} by Def4;
per cases by A4,ZFMISC_1:118;
suppose
Carrier L = {};
then
A5: L = ZeroCLC V by Def3;
then Sum L = 0.V by Th11
.= 0.V + 0.V
.= 0.V + 0.V + 0.V
.= 0c * v1 + 0.V + 0.V by CLVECT_1:1
.= 0c * v1 + 0c * v2 + 0.V by CLVECT_1:1
.= 0c * v1 + 0c * v2 + 0c * v3 by CLVECT_1:1
.= L.v1 * v1 + 0c * v2 + 0c * v3 by A5,Th2
.= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A5,Th2
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A5,Th2;
hence thesis;
end;
suppose
A6: Carrier L = {v1};
then reconsider L as C_Linear_Combination of {v1} by Def4;
A7: not v2 in Carrier L by A1,A6,TARSKI:def 1;
A8: not v3 in Carrier L by A3,A6,TARSKI:def 1;
Sum L = L.v1 * v1 by Th14
.= L.v1 * v1 + 0.V
.= L.v1 * v1 + 0.V + 0.V
.= L.v1 * v1 + 0c * v2 + 0.V by CLVECT_1:1
.= L.v1 * v1 + 0c * v2 + 0c * v3 by CLVECT_1:1
.= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A7
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A8;
hence thesis;
end;
suppose
A9: Carrier L = {v2};
then reconsider L as C_Linear_Combination of {v2} by Def4;
A10: not v1 in Carrier L by A1,A9,TARSKI:def 1;
A11: not v3 in Carrier L by A2,A9,TARSKI:def 1;
Sum L = L.v2 * v2 by Th14
.= 0.V + L.v2 * v2
.= 0.V + L.v2 * v2 + 0.V
.= 0c * v1 + L.v2 * v2 + 0.V by CLVECT_1:1
.= 0c * v1 + L.v2 * v2 + 0c * v3 by CLVECT_1:1
.= L.v1 * v1 + L.v2 * v2 + 0c * v3 by A10
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A11;
hence thesis;
end;
suppose
A12: Carrier L = {v3};
then reconsider L as C_Linear_Combination of {v3} by Def4;
A13: not v1 in Carrier L by A3,A12,TARSKI:def 1;
A14: not v2 in Carrier L by A2,A12,TARSKI:def 1;
Sum L = L.v3 * v3 by Th14
.= 0.V + L.v3 * v3
.= 0.V + 0.V + L.v3 * v3
.= 0c * v1 + 0.V + L.v3 * v3 by CLVECT_1:1
.= 0c * v1 + 0c * v2 + L.v3 * v3 by CLVECT_1:1
.= L.v1 * v1 + 0c * v2 + L.v3 * v3 by A13
.= L.v1 * v1 + L.v2 * v2 + L.v3 * v3 by A14;
hence thesis;
end;
suppose
A15: Carrier L = {v1,v2};
then
A16: Sum L = L.v1 * v1 + L.v2 * v2 by A1,Th18
.= L.v1 * v1 + L.v2 * v2 + 0.V
.= L.v1 * v1 + L.v2 * v2 + 0c * v3 by CLVECT_1:1;
not v3 in Carrier L by A2,A3,A15,TARSKI:def 2;
hence thesis by A16;
end;
suppose
A17: Carrier L = {v1,v3};
then
A18: Sum L = L.v1 * v1 + L.v3 * v3 by A3,Th18
.= L.v1 * v1 + 0.V + L.v3 * v3
.= L.v1 * v1 + 0c * v2 + L.v3 * v3 by CLVECT_1:1;
not v2 in Carrier L by A1,A2,A17,TARSKI:def 2;
hence thesis by A18;
end;
suppose
A19: Carrier L = {v2,v3};
then
A20: Sum L = L.v2 * v2 + L.v3 * v3 by A2,Th18
.= 0.V + L.v2 * v2 + L.v3 * v3
.= 0c * v1 + L.v2 * v2 + L.v3 * v3 by CLVECT_1:1;
not v1 in Carrier L by A1,A3,A19,TARSKI:def 2;
hence thesis by A20;
end;
suppose
Carrier L = {v1,v2,v3};
then consider F be FinSequence of the carrier of V such that
A21: F is one-to-one & rng F = {v1,v2,v3} and
A22: Sum L = Sum(L (#) F) by Def6;
F = <* v1,v2,v3 *> or F = <* v1,v3,v2 *> or F = <* v2,v1,v3 *> or F =
<* v2,v3,v1 *> or F = <* v3,v1,v2 *> or F = <* v3,v2,v1 *> by A1,A2,A3,A21,
CONVEX1:31;
then L (#) F = <* L.v1 * v1, L.v2 * v2, L.v3 * v3 *> or L (#) F = <* L.v1
* v1, L.v3 * v3, L.v2 * v2 *> or L (#) F = <* L.v2 * v2, L.v1 * v1, L.v3 * v3
*> or L (#) F = <* L.v2 * v2, L.v3 * v3, L.v1 * v1 *> or L (#) F = <* L.v3 * v3
, L.v1 * v1, L.v2 * v2 *> or L (#) F = <* L.v3 * v3, L.v2 * v2, L.v1 * v1 *>
by Th10;
then Sum L = L.v1 * v1 + L.v2 * v2 + L.v3 * v3 or Sum L = L.v1 * v1 + (L.
v2 * v2 + L.v3 * v3) or Sum L = L.v2 * v2 + (L.v1 * v1 + L.v3 * v3) by A22,
RLVECT_1:46;
hence thesis by RLVECT_1:def 3;
end;
end;
theorem Th82:
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
proof
let V be ComplexLinearSpace;
let v1,v2,v3 be VECTOR of V;
let L be C_Linear_Combination of V;
assume that
A1: L is convex and
A2: Carrier L = {v1,v2,v3} and
A3: v1 <> v2 & v2 <> v3 & v3 <> v1;
reconsider L as C_Linear_Combination of {v1,v2,v3} by A2,Def4;
consider F being FinSequence of the carrier of V such that
A4: F is one-to-one & rng F = Carrier L and
A5: 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 by A1;
consider f be FinSequence of REAL such that
A6: len f = len F and
A7: Sum f = 1 and
A8: for n being Nat st n in dom f holds f.n = L.(F.n) & f.n >= 0 by A5;
len F = card {v1,v2,v3} by A2,A4,FINSEQ_4:62;
then
A9: len f = 3 by A3,A6,CARD_2:58;
then
A10: dom f = {1,2,3} by FINSEQ_1:def 3,FINSEQ_3:1;
then
A11: 2 in dom f by ENUMSET1:def 1;
then
A12: f.2 = L.(F.2) by A8;
then f/.2 = L.(F.2) by A11,PARTFUN1:def 6;
then reconsider r2 = L.(F.2) as Element of REAL;
A13: f.2 >= 0 by A8,A11;
A14: 3 in dom f by A10,ENUMSET1:def 1;
then
A15: f.3 = L.(F.3) by A8;
then f/.3 = L.(F.3) by A14,PARTFUN1:def 6;
then reconsider r3 = L.(F.3) as Element of REAL;
A16: f.3 >= 0 by A8,A14;
A17: 1 in dom f by A10,ENUMSET1:def 1;
then
A18: f.1 = L.(F.1) by A8;
then f/.1 = L.(F.1) by A17,PARTFUN1:def 6;
then reconsider r1 = L.(F.1) as Element of REAL;
A19: f = <*r1,r2,r3*> by A9,A18,A12,A15,FINSEQ_1:45;
then
A20: r1 + r2 + r3 = 1 by A7,RVSUM_1:78;
A21: f.1 >= 0 by A8,A17;
ex a, b, c being Real st a = L.v1 & b = L.v2 & c = L.v3 & a + b
+ c = 1 & a >= 0 & b >= 0 & c >= 0
proof
per cases by A2,A3,A4,CONVEX1:31;
suppose
A22: F = <*v1,v2,v3*>;
then
A23: r1 = L.v1 & r2 = L.v2 by FINSEQ_1:45;
A24: r2 >= 0 by A8,A11,A12;
A25: r3 = L.v3 by A22,FINSEQ_1:45;
r1 + r2 + r3 = 1 & r1 >= 0 by A7,A8,A17,A18,A19,RVSUM_1:78;
hence thesis by A15,A16,A23,A25,A24;
end;
suppose
A26: F = <*v1,v3,v2*>;
then
A27: r1 = L.v1 & r3 = L.v2 by FINSEQ_1:45;
A28: r3 >= 0 by A8,A14,A15;
A29: r2 = L.v3 by A26,FINSEQ_1:45;
r1 + r3 + r2 = 1 & r1 >= 0 by A8,A17,A18,A20;
hence thesis by A12,A13,A27,A29,A28;
end;
suppose
A30: F = <*v2,v1,v3*>;
then
A31: r2 = L.v1 & r1 = L.v2 by FINSEQ_1:45;
A32: r1 >= 0 by A8,A17,A18;
A33: r3 = L.v3 by A30,FINSEQ_1:45;
r2 + r1 + r3 = 1 & r2 >= 0 by A7,A8,A11,A12,A19,RVSUM_1:78;
hence thesis by A15,A16,A31,A33,A32;
end;
suppose
A34: F = <*v2,v3,v1*>;
then
A35: r3 = L.v1 & r1 = L.v2 by FINSEQ_1:45;
A36: r1 >= 0 by A8,A17,A18;
A37: r2 = L.v3 by A34,FINSEQ_1:45;
r3 + r1 + r2 = 1 & r3 >= 0 by A8,A14,A15,A20;
hence thesis by A12,A13,A35,A37,A36;
end;
suppose
A38: F = <*v3,v1,v2*>;
then
A39: r2 = L.v1 & r3 = L.v2 by FINSEQ_1:45;
A40: r3 >= 0 by A8,A14,A15;
A41: r1 = L.v3 by A38,FINSEQ_1:45;
r2 + r3 + r1 = 1 & r2 >= 0 by A8,A11,A12,A20;
hence thesis by A18,A21,A39,A41,A40;
end;
suppose
A42: F = <*v3,v2,v1*>;
then
A43: r3 = L.v1 & r2 = L.v2 by FINSEQ_1:45;
A44: r2 >= 0 by A8,A11,A12;
A45: r1 = L.v3 by A42,FINSEQ_1:45;
r3 + r2 + r1 = 1 & r3 >= 0 by A8,A14,A15,A20;
hence thesis by A18,A21,A43,A45,A44;
end;
end;
hence thesis by A3,Lm3;
end;
theorem
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
proof
let V be ComplexLinearSpace;
let v be VECTOR of V;
let L be C_Linear_Combination of {v};
Carrier L c= {v} by Def4;
then
A1: Carrier L = {} or Carrier L = {v} by ZFMISC_1:33;
assume L is convex;
hence thesis by A1,Th77,Th80;
end;
theorem
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
proof
let V be ComplexLinearSpace;
let v1,v2 be VECTOR of V;
let L be C_Linear_Combination of {v1,v2};
assume that
A1: v1 <> v2 and
A2: L is convex;
A3: Carrier L c= {v1,v2} by Def4;
A4: Carrier L <> {} by A2,Th77;
ex r1, r2 being Real st r1 = L.v1 & r2 = L.v2 & r1 >= 0 & r2 >= 0
proof
per cases by A3,A4,ZFMISC_1:36;
suppose
A5: Carrier L = {v1};
then not v2 in Carrier(L) by A1,TARSKI:def 1;
then
A6: 0 = L.v2;
ex r being Real st r = L.v1 & r = 1 by A2,A5,Th80;
hence thesis by A6;
end;
suppose
A7: Carrier L = {v2};
then not v1 in Carrier L by A1,TARSKI:def 1;
then
A8: 0=L.v1;
ex r being Real st r =L.v2 & r = 1 by A2,A7,Th80;
hence thesis by A8;
end;
suppose
Carrier L = {v1,v2};
then ex r1,r2 being Real st r1=L.v1 & r2 = L.v2 & r1 + r2 = 1 & r1 >= 0
& r2 >=0 by A1,A2,Th81;
hence thesis;
end;
end;
hence thesis by A1,Th15;
end;
theorem
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
proof
let V be ComplexLinearSpace;
let v1,v2,v3 be VECTOR of V;
let L be C_Linear_Combination of {v1,v2,v3};
assume that
A1: v1 <> v2 and
A2: v2 <> v3 and
A3: v3 <> v1 and
A4: L is convex;
A5: Carrier L c= {v1,v2,v3} by Def4;
A6: Carrier L <> {} by A4,Th77;
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
proof
per cases by A5,A6,ZFMISC_1:118;
suppose
A7: Carrier L = {v1};
then not v2 in Carrier L by A1,TARSKI:def 1;
then
A8: 0 = L.v2;
A9: 1 + 0 + 0 =1;
not v3 in Carrier L by A3,A7,TARSKI:def 1;
then
A10: 0 = L.v3;
ex r being Real st r = L.v1 & r = 1 by A4,A7,Th80;
hence thesis by A8,A10,A9;
end;
suppose
A11: Carrier L = {v2};
then not v1 in Carrier L by A1,TARSKI:def 1;
then
A12: 0 = L.v1;
A13: 0 + 1 + 0 =1;
not v3 in Carrier L by A2,A11,TARSKI:def 1;
then
A14: 0 = L.v3;
ex r being Real st r = L.v2 & r = 1 by A4,A11,Th80;
hence thesis by A12,A14,A13;
end;
suppose
A15: Carrier L = {v3};
then not v1 in Carrier L by A3,TARSKI:def 1;
then
A16: 0 = L.v1;
A17: 0 + 0 + 1 =1;
not v2 in Carrier L by A2,A15,TARSKI:def 1;
then
A18: 0 = L.v2;
ex r being Real st r = L.v3 & r = 1 by A4,A15,Th80;
hence thesis by A16,A18,A17;
end;
suppose
A19: Carrier L = {v1,v2};
set r3 = 0;
not v3 in {v where v is Element of V : L.v <> 0} by A2,A3,A19,
TARSKI:def 2;
then
A20: r3 = L.v3;
consider r1, r2 being Real such that
A21: r1 = L.v1 & r2 = L.v2 and
A22: r1 + r2 = 1 and
A23: r1 >= 0 & r2 >= 0 by A1,A4,A19,Th81;
r1 + r2 + r3 = 1 by A22;
hence thesis by A21,A23,A20;
end;
suppose
A24: Carrier L = {v2,v3};
set r1 = 0;
not v1 in Carrier L by A1,A3,A24,TARSKI:def 2;
then
A25: r1 = L.v1;
consider r2,r3 being Real such that
A26: r2 = L.v2 & r3 = L.v3 and
A27: r2 + r3 = 1 and
A28: r2 >= 0 & r3 >= 0 by A2,A4,A24,Th81;
r1 + r2 + r3 = 1 by A27;
hence thesis by A26,A28,A25;
end;
suppose
A29: Carrier L = {v1,v3};
set r2 = 0;
not v2 in Carrier(L) by A1,A2,A29,TARSKI:def 2;
then
A30: r2 = L.v2;
consider r1, r3 being Real such that
A31: r1 = L.v1 & r3 = L.v3 and
A32: r1 + r3 = 1 and
A33: r1 >= 0 & r3 >= 0 by A3,A4,A29,Th81;
r1 + r2 + r3 = 1 by A32;
hence thesis by A31,A33,A30;
end;
suppose
Carrier L = {v1,v2,v3};
hence thesis by A1,A2,A3,A4,Th82;
end;
end;
hence thesis by A1,A2,A3,Lm3;
end;
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
:Def25:
for N being Subset of V holds N in it iff N is convex & M c= N;
existence
proof
defpred P[Subset of V] means $1 is convex & M c= $1;
thus ex F be Subset-Family of V st for N being Subset of V holds N in F
iff P[N] from SUBSET_1:sch 3;
end;
uniqueness
proof
let SF,SG be Subset-Family of V;
assume that
A1: for N being Subset of V holds N in SF iff N is convex & M c= N and
A2: for N being Subset of V holds N in SG iff N is convex & M c= N;
for Y being Subset of V holds Y in SF iff Y in SG
proof
let Y be Subset of V;
hereby
assume Y in SF;
then Y is convex & M c= Y by A1;
hence Y in SG by A2;
end;
assume Y in SG;
then Y is convex & M c= Y by A2;
hence thesis by A1;
end;
hence thesis by SETFAM_1:31;
end;
end;
definition
let V be non empty CLSStruct, M be Subset of V;
func conv M -> convex Subset of V equals
meet (Convex-Family M);
coherence
proof
for N being Subset of V st N in Convex-Family M holds N is convex by Def25;
hence thesis by Th65;
end;
end;
theorem
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
proof
let V be non empty CLSStruct;
let M be Subset of V;
let N be convex Subset of V;
assume M c= N;
then N in Convex-Family M by Def25;
hence thesis by SETFAM_1:3;
end;