:: Complex Linear Space and Complex Normed Space :: by Noboru Endou :: :: Received January 26, 2004 :: Copyright (c) 2004-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, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, RLVECT_1, FUNCT_1, ZFMISC_1, XBOOLE_0, FUNCT_7, RELAT_1, ARYTM_3, COMPLEX1, FUNCT_5, MCART_1, CARD_1, SUPINF_2, ARYTM_1, CARD_3, FINSEQ_1, XXREAL_0, TARSKI, XCMPLX_0, RLSUB_1, REALSET1, NORMSP_1, PRE_TOPC, REAL_1, FUNCOP_1, NAT_1, SEQ_2, ORDINAL2, CLVECT_1, NORMSP_0, METRIC_1, RELAT_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, DOMAIN_1, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, REALSET1, FINSEQ_1, NAT_1, FUNCT_3, FUNCT_5, FINSEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, SEQ_2, NORMSP_0, NORMSP_1; constructors BINOP_1, FUNCOP_1, REAL_1, COMPLEX1, SEQ_2, REALSET1, NORMSP_1, FUNCT_3, FUNCT_5, RELSET_1, FINSEQ_4, COMSEQ_2; registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REALSET1, STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1, NORMSP_0, NAT_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Complex Linear Space definition struct (addLoopStr) CLSStruct (# carrier -> set, ZeroF -> Element of the carrier, addF -> BinOp of the carrier, Mult -> Function of [:COMPLEX, the carrier:], the carrier #); end; registration cluster non empty for CLSStruct; end; definition let V be CLSStruct; mode VECTOR of V is Element of V; end; definition let V be non empty CLSStruct, v be VECTOR of V, z be Complex; func z * v -> Element of V equals :: CLVECT_1:def 1 (the Mult of V).[z,v]; end; registration let ZS be non empty set, O be Element of ZS, F be BinOp of ZS, G be Function of [:COMPLEX,ZS:],ZS; cluster CLSStruct (# ZS,O,F,G #) -> non empty; end; reserve a,b for Complex; definition let IT be non empty CLSStruct; attr IT is vector-distributive means :: CLVECT_1:def 2 for a for v,w being VECTOR of IT holds a * (v + w) = a * v + a * w; attr IT is scalar-distributive means :: CLVECT_1:def 3 for a,b for v being VECTOR of IT holds (a + b) * v = a * v + b * v; attr IT is scalar-associative means :: CLVECT_1:def 4 for a,b for v being VECTOR of IT holds (a * b) * v = a * (b * v); attr IT is scalar-unital means :: CLVECT_1:def 5 for v being VECTOR of IT holds 1r * v = v; end; definition func Trivial-CLSStruct -> strict CLSStruct equals :: CLVECT_1:def 6 CLSStruct(#{0},op0,op2,pr2(COMPLEX,{0})#); end; registration cluster Trivial-CLSStruct -> 1-element; end; registration cluster strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital for non empty CLSStruct; end; definition mode ComplexLinearSpace is Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty CLSStruct; end; :: :: Axioms of complex linear space. :: reserve V,X,Y for ComplexLinearSpace; reserve u,u1,u2,v,v1,v2 for VECTOR of V; reserve z,z1,z2 for Complex; theorem :: CLVECT_1:1 z = 0 or v = 0.V implies z * v = 0.V; theorem :: CLVECT_1:2 z * v = 0.V implies z = 0 or v = 0.V; theorem :: CLVECT_1:3 - v = (- 1r) * v; theorem :: CLVECT_1:4 v = - v implies v = 0.V; theorem :: CLVECT_1:5 v + v = 0.V implies v = 0.V; theorem :: CLVECT_1:6 z * (- v) = (- z) * v; theorem :: CLVECT_1:7 z * (- v) = - (z * v); theorem :: CLVECT_1:8 (- z) * (- v) = z * v; theorem :: CLVECT_1:9 z * (v - u) = z * v - z * u; theorem :: CLVECT_1:10 (z1 - z2) * v = z1 * v - z2 * v; theorem :: CLVECT_1:11 z <> 0 & z * v = z * u implies v = u; theorem :: CLVECT_1:12 v <> 0.V & z1 * v = z2 * v implies z1 = z2; theorem :: CLVECT_1:13 for F,G being FinSequence of the carrier of V st len F = len G & (for k being Nat,v being VECTOR of V st k in dom F & v = G.k holds F.k = z * v) holds Sum(F) = z * Sum(G); theorem :: CLVECT_1:14 z * Sum(<*>(the carrier of V)) = 0.V; theorem :: CLVECT_1:15 z * Sum<* v,u *> = z * v + z * u; theorem :: CLVECT_1:16 z * Sum<* u,v1,v2 *> = z * u + z * v1 + z * v2; theorem :: CLVECT_1:17 Sum<* v,v *> = (1r+1r) * v; theorem :: CLVECT_1:18 Sum<* - v,- v *> = (-(1r+1r)) * v; theorem :: CLVECT_1:19 Sum<* v,v,v *> = (1r+1r+1r) * v; begin :: Subspace and Cosets of Subspaces in Complex Linear Space reserve V1,V2,V3 for Subset of V; definition let V, V1; attr V1 is linearly-closed means :: CLVECT_1:def 7 (for v,u being VECTOR of V st v in V1 & u in V1 holds v + u in V1) & for z being Complex, v being VECTOR of V st v in V1 holds z * v in V1; end; theorem :: CLVECT_1:20 V1 <> {} & V1 is linearly-closed implies 0.V in V1; theorem :: CLVECT_1:21 V1 is linearly-closed implies for v being VECTOR of V st v in V1 holds - v in V1; theorem :: CLVECT_1:22 V1 is linearly-closed implies for v,u being VECTOR of V st v in V1 & u in V1 holds v - u in V1; theorem :: CLVECT_1:23 {0.V} is linearly-closed; theorem :: CLVECT_1:24 the carrier of V = V1 implies V1 is linearly-closed; theorem :: CLVECT_1:25 V1 is linearly-closed & V2 is linearly-closed & V3 = {v + u : v in V1 & u in V2} implies V3 is linearly-closed; theorem :: CLVECT_1:26 V1 is linearly-closed & V2 is linearly-closed implies V1 /\ V2 is linearly-closed; definition let V; mode Subspace of V -> ComplexLinearSpace means :: CLVECT_1:def 8 the carrier of it c= the carrier of V & 0.it = 0.V & the addF of it = (the addF of V)||the carrier of it & the Mult of it = (the Mult of V) | [:COMPLEX, the carrier of it:]; end; :: Axioms of the subspaces of real linear spaces. reserve W,W1,W2 for Subspace of V; reserve x for set; reserve w,w1,w2 for VECTOR of W; theorem :: CLVECT_1:27 x in W1 & W1 is Subspace of W2 implies x in W2; theorem :: CLVECT_1:28 for x being object holds x in W implies x in V; theorem :: CLVECT_1:29 w is VECTOR of V; theorem :: CLVECT_1:30 0.W = 0.V; theorem :: CLVECT_1:31 0.W1 = 0.W2; theorem :: CLVECT_1:32 w1 = v & w2 = u implies w1 + w2 = v + u; theorem :: CLVECT_1:33 w = v implies z * w = z * v; theorem :: CLVECT_1:34 w = v implies - v = - w; theorem :: CLVECT_1:35 w1 = v & w2 = u implies w1 - w2 = v - u; theorem :: CLVECT_1:36 0.V in W; theorem :: CLVECT_1:37 0.W1 in W2; theorem :: CLVECT_1:38 0.W in V; theorem :: CLVECT_1:39 u in W & v in W implies u + v in W; theorem :: CLVECT_1:40 v in W implies z * v in W; theorem :: CLVECT_1:41 v in W implies - v in W; theorem :: CLVECT_1:42 u in W & v in W implies u - v in W; reserve D for non empty set; reserve d1 for Element of D; reserve A for BinOp of D; reserve M for Function of [:COMPLEX,D:],D; theorem :: CLVECT_1:43 V1 = D & d1 = 0.V & A = (the addF of V)||V1 & M = (the Mult of V) | [:COMPLEX,V1:] implies CLSStruct (# D,d1,A,M #) is Subspace of V; theorem :: CLVECT_1:44 V is Subspace of V; theorem :: CLVECT_1:45 for V,X being strict ComplexLinearSpace holds V is Subspace of X & X is Subspace of V implies V = X; theorem :: CLVECT_1:46 V is Subspace of X & X is Subspace of Y implies V is Subspace of Y; theorem :: CLVECT_1:47 the carrier of W1 c= the carrier of W2 implies W1 is Subspace of W2; theorem :: CLVECT_1:48 (for v st v in W1 holds v in W2) implies W1 is Subspace of W2; registration let V; cluster strict for Subspace of V; end; theorem :: CLVECT_1:49 for W1,W2 being strict Subspace of V holds the carrier of W1 = the carrier of W2 implies W1 = W2; theorem :: CLVECT_1:50 for W1,W2 being strict Subspace of V holds (for v holds v in W1 iff v in W2) implies W1 = W2; theorem :: CLVECT_1:51 for V being strict ComplexLinearSpace, W being strict Subspace of V holds the carrier of W = the carrier of V implies W = V; theorem :: CLVECT_1:52 for V being strict ComplexLinearSpace, W being strict Subspace of V holds (for v being VECTOR of V holds v in W iff v in V) implies W = V; theorem :: CLVECT_1:53 the carrier of W = V1 implies V1 is linearly-closed; theorem :: CLVECT_1:54 V1 <> {} & V1 is linearly-closed implies ex W being strict Subspace of V st V1 = the carrier of W; :: Definition of zero subspace and improper subspace of complex linear space. definition let V; func (0).V -> strict Subspace of V means :: CLVECT_1:def 9 the carrier of it = {0.V}; end; definition let V; func (Omega).V -> strict Subspace of V equals :: CLVECT_1:def 10 the CLSStruct of V; end; :: Definitional theorems of zero subspace and improper subspace. theorem :: CLVECT_1:55 (0).W = (0).V; theorem :: CLVECT_1:56 (0).W1 = (0).W2; theorem :: CLVECT_1:57 (0).W is Subspace of V; theorem :: CLVECT_1:58 (0).V is Subspace of W; theorem :: CLVECT_1:59 (0).W1 is Subspace of W2; theorem :: CLVECT_1:60 for V being strict ComplexLinearSpace holds V is Subspace of (Omega).V; :: Introduction of the cosets of subspace. definition let V; let v,W; func v + W -> Subset of V equals :: CLVECT_1:def 11 {v + u : u in W}; end; definition let V; let W; mode Coset of W -> Subset of V means :: CLVECT_1:def 12 ex v st it = v + W; end; reserve B,C for Coset of W; :: Definitional theorems of the cosets. theorem :: CLVECT_1:61 0.V in v + W iff v in W; theorem :: CLVECT_1:62 v in v + W; theorem :: CLVECT_1:63 0.V + W = the carrier of W; theorem :: CLVECT_1:64 v + (0).V = {v}; theorem :: CLVECT_1:65 v + (Omega).V = the carrier of V; theorem :: CLVECT_1:66 0.V in v + W iff v + W = the carrier of W; theorem :: CLVECT_1:67 v in W iff v + W = the carrier of W; theorem :: CLVECT_1:68 v in W implies (z * v) + W = the carrier of W; theorem :: CLVECT_1:69 z <> 0 & (z * v) + W = the carrier of W implies v in W; theorem :: CLVECT_1:70 v in W iff - v + W = the carrier of W; theorem :: CLVECT_1:71 u in W iff v + W = (v + u) + W; theorem :: CLVECT_1:72 u in W iff v + W = (v - u) + W; theorem :: CLVECT_1:73 v in u + W iff u + W = v + W; theorem :: CLVECT_1:74 v + W = (- v) + W iff v in W; theorem :: CLVECT_1:75 u in v1 + W & u in v2 + W implies v1 + W = v2 + W; theorem :: CLVECT_1:76 u in v + W & u in (- v) + W implies v in W; theorem :: CLVECT_1:77 z <> 1r & z * v in v + W implies v in W; theorem :: CLVECT_1:78 v in W implies z * v in v + W; theorem :: CLVECT_1:79 - v in v + W iff v in W; theorem :: CLVECT_1:80 u + v in v + W iff u in W; theorem :: CLVECT_1:81 v - u in v + W iff u in W; theorem :: CLVECT_1:82 u in v + W iff ex v1 st v1 in W & u = v + v1; theorem :: CLVECT_1:83 u in v + W iff ex v1 st v1 in W & u = v - v1; theorem :: CLVECT_1:84 (ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W; theorem :: CLVECT_1:85 v + W = u + W implies ex v1 st v1 in W & v + v1 = u; theorem :: CLVECT_1:86 v + W = u + W implies ex v1 st v1 in W & v - v1 = u; theorem :: CLVECT_1:87 for W1,W2 being strict Subspace of V holds v + W1 = v + W2 iff W1 = W2; theorem :: CLVECT_1:88 for W1,W2 being strict Subspace of V holds v + W1 = u + W2 implies W1 = W2; :: Theorems concerning cosets of subspace :: regarded as subsets of the carrier. theorem :: CLVECT_1:89 C is linearly-closed iff C = the carrier of W; theorem :: CLVECT_1:90 for W1,W2 being strict Subspace of V, C1 being Coset of W1, C2 being Coset of W2 holds C1 = C2 implies W1 = W2; theorem :: CLVECT_1:91 {v} is Coset of (0).V; theorem :: CLVECT_1:92 V1 is Coset of (0).V implies ex v st V1 = {v}; theorem :: CLVECT_1:93 the carrier of W is Coset of W; theorem :: CLVECT_1:94 the carrier of V is Coset of (Omega).V; theorem :: CLVECT_1:95 V1 is Coset of (Omega).V implies V1 = the carrier of V; theorem :: CLVECT_1:96 0.V in C iff C = the carrier of W; theorem :: CLVECT_1:97 u in C iff C = u + W; theorem :: CLVECT_1:98 u in C & v in C implies ex v1 st v1 in W & u + v1 = v; theorem :: CLVECT_1:99 u in C & v in C implies ex v1 st v1 in W & u - v1 = v; theorem :: CLVECT_1:100 (ex C st v1 in C & v2 in C) iff v1 - v2 in W; theorem :: CLVECT_1:101 u in B & u in C implies B = C; begin :: Complex Normed Space definition struct(CLSStruct,N-ZeroStr) CNORMSTR (# carrier -> set, ZeroF -> Element of the carrier, addF -> BinOp of the carrier, Mult -> Function of [:COMPLEX, the carrier:], the carrier, normF -> Function of the carrier, REAL #); end; registration cluster non empty for CNORMSTR; end; definition let IT be non empty CNORMSTR; attr IT is ComplexNormSpace-like means :: CLVECT_1:def 13 for x, y being Point of IT, z holds ||.z * x.|| = |.z.| * ||.x.|| & ||.x + y .|| <= ||.x.|| + ||.y.||; end; registration cluster reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty CNORMSTR; end; definition mode ComplexNormSpace is reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty CNORMSTR; end; reserve CNS for ComplexNormSpace; reserve x, y, w, g, g1, g2 for Point of CNS; theorem :: CLVECT_1:102 ||.0.CNS.|| = 0; theorem :: CLVECT_1:103 ||.-x.|| = ||.x.||; theorem :: CLVECT_1:104 ||.x - y.|| <= ||.x.|| + ||.y.||; theorem :: CLVECT_1:105 0 <= ||.x.||; theorem :: CLVECT_1:106 ||.z1 * x + z2 * y.|| <= |.z1.| * ||.x.|| + |.z2.| * ||.y.||; theorem :: CLVECT_1:107 ||.x - y.|| = 0 iff x = y; theorem :: CLVECT_1:108 ||.x - y.|| = ||.y - x.||; theorem :: CLVECT_1:109 ||.x.|| - ||.y.|| <= ||.x - y.||; theorem :: CLVECT_1:110 |.||.x.|| - ||.y.||.| <= ||.x - y.||; theorem :: CLVECT_1:111 ||.x - w.|| <= ||.x - y.|| + ||.y - w.||; theorem :: CLVECT_1:112 x <> y implies ||.x - y.|| <> 0; reserve S, S1, S2 for sequence of CNS; reserve n, m, m1, m2 for Nat; reserve r for Real; definition let CNS be ComplexLinearSpace; let S be sequence of CNS; let z; func z * S -> sequence of CNS means :: CLVECT_1:def 14 for n holds it.n = z * S.n; end; definition let CNS; let S; attr S is convergent means :: CLVECT_1:def 15 ex g st for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r; end; theorem :: CLVECT_1:113 S1 is convergent & S2 is convergent implies S1 + S2 is convergent; theorem :: CLVECT_1:114 S1 is convergent & S2 is convergent implies S1 - S2 is convergent; theorem :: CLVECT_1:115 S is convergent implies S - x is convergent; theorem :: CLVECT_1:116 S is convergent implies z * S is convergent; theorem :: CLVECT_1:117 S is convergent implies ||.S.|| is convergent; definition let CNS; let S; assume S is convergent; func lim S -> Point of CNS means :: CLVECT_1:def 16 for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - it.|| < r; end; theorem :: CLVECT_1:118 S is convergent & lim S = g implies ||.S - g.|| is convergent & lim ||.S - g.|| = 0; theorem :: CLVECT_1:119 S1 is convergent & S2 is convergent implies lim(S1+S2) = (lim S1) + ( lim S2 ); theorem :: CLVECT_1:120 S1 is convergent & S2 is convergent implies lim (S1-S2) = (lim S1) - ( lim S2 ); theorem :: CLVECT_1:121 S is convergent implies lim (S - x) = (lim S) - x; theorem :: CLVECT_1:122 S is convergent implies lim (z * S) = z * (lim S); theorem :: CLVECT_1:123 for V,V1,v for w be VECTOR of CLSStruct (# D,d1,A,M #) st V1 = D & M = (the Mult of V) | [:COMPLEX,V1:] & w = v holds z*w = z*v;