:: Complex Linear Space and Complex Normed Space
:: by Noboru Endou
::
:: Received January 26, 2004
:: Copyright (c) 2004-2017 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;