:: Complex Linear Space of Complex Sequences
:: by Noboru Endou
::
:: Received January 26, 2004
:: Copyright (c) 2004-2026 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, COMSEQ_1, FUNCT_2, TARSKI, RSSPACE, BINOP_1,
SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, COMPLEX1, FUNCOP_1,
RLVECT_1, CLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0,
RLSUB_1, REALSET1, SERIES_1, CARD_1, XXREAL_0, REAL_1, SQUARE_1, BHSP_1,
PRE_TOPC, PROB_2, XCMPLX_0, RVSUM_1, NORMSP_1, METRIC_1, NAT_1, CARD_3,
SEQ_2, ORDINAL2, CSSPACE, CLOPBAN1, CFUNCDOM;
notations TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, RELAT_1, DOMAIN_1, FUNCT_1,
FUNCT_2, FUNCOP_1, VALUED_1, BINOP_1, REALSET1, XCMPLX_0, XXREAL_0,
REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, ZFMISC_1, NUMBERS, SQUARE_1,
XREAL_0, COMPLEX1, COMSEQ_1, COMSEQ_2, SERIES_1, COMSEQ_3, RLVECT_1,
VFUNCT_1, NORMSP_1, BHSP_1, CLVECT_1, CFUNCDOM;
constructors BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, COMSEQ_2, COMSEQ_3,
REALSET1, BHSP_1, CLVECT_1, RELSET_1, VFUNCT_1, CFUNCDOM, FUNCSDOM;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2,
NUMBERS, XCMPLX_0, XXREAL_0, MEMBERED, REALSET1, STRUCT_0, CLVECT_1,
ALGSTR_0, VALUED_1, VALUED_0, VFUNCT_1, SERIES_1, XREAL_0, SQUARE_1,
CFUNCDOM;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, FUNCT_2, RLVECT_1, CLVECT_1, ALGSTR_0, VALUED_0;
equalities CLVECT_1, STRUCT_0, REALSET1, SQUARE_1, BINOP_1, ALGSTR_0,
CFUNCDOM, ORDINAL1;
expansions CLVECT_1, BINOP_1, VALUED_0;
theorems XBOOLE_0, RELAT_1, SQUARE_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1,
SERIES_1, COMSEQ_3, FUNCT_1, FUNCT_2, RLVECT_1, XCMPLX_0, COMSEQ_1,
CLVECT_1, COMPLEX1, COMSEQ_2, NORMSP_1, FUNCOP_1, XREAL_1, XXREAL_0,
BHSP_1, ALGSTR_0, VALUED_1, ORDINAL1, CFUNCDOM;
schemes NAT_1, BINOP_1, XBOOLE_0;
begin
definition
func the_set_of_ComplexSequences -> non empty set equals
Funcs(NAT,COMPLEX);
coherence;
end;
definition
let z be object such that
A1: z in the_set_of_ComplexSequences;
func seq_id(z) -> Complex_Sequence equals
:Def2:
z;
coherence by A1,FUNCT_2:66;
end;
registration
let z be Element of the_set_of_ComplexSequences;
reduce seq_id(z) to z;
reducibility by Def2;
end;
definition
let z be object such that
A1: z is Complex;
func C_id(z) -> Complex equals
:Def3:
z;
coherence by A1;
end;
registration
let z be Complex;
reduce C_id(z) to z;
reducibility by Def3;
end;
definition
::$CD 2
func CZeroseq -> Element of the_set_of_ComplexSequences equals
NAT --> 0c;
coherence by FUNCT_2:8;
end;
registration
let x be Complex_Sequence;
reduce seq_id x to x;
reducibility
proof
x in the_set_of_ComplexSequences by FUNCT_2:8;
hence thesis by Def2;
end;
end;
theorem
for x being Complex_Sequence holds seq_id x = x;
definition
func Linear_Space_of_ComplexSequences -> strict non empty CLSStruct equals
ComplexVectSpace(NAT);
coherence;
end;
registration
cluster Linear_Space_of_ComplexSequences -> Abelian add-associative
right_zeroed right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence;
end;
registration
let z be VECTOR of Linear_Space_of_ComplexSequences;
reduce seq_id(z) to z;
reducibility by Def2;
end;
theorem Th2:
for v,w being VECTOR of Linear_Space_of_ComplexSequences holds
v + w = seq_id(v) + seq_id(w)
proof
let v,w be VECTOR of Linear_Space_of_ComplexSequences;
reconsider v1 = v, w1 = w as Element of Funcs(NAT,COMPLEX);
reconsider f = (ComplexFuncAdd NAT).(v1,w1) as Function of NAT,COMPLEX
by FUNCT_2:66;
f = seq_id(v)+seq_id(w)
proof
let n be Element of NAT;
thus f.n = v1.n+w1.n by CFUNCDOM:1
.= (seq_id(v)+seq_id(w)).n by VALUED_1:1;
end;
hence thesis;
end;
theorem Th3:
for z being Complex, v being VECTOR of Linear_Space_of_ComplexSequences holds
z * v = z(#)seq_id(v)
proof
let z be Complex;
let v be VECTOR of Linear_Space_of_ComplexSequences;
reconsider r1 = z as Element of COMPLEX by XCMPLX_0:def 2;
reconsider v1 = v as Element of Funcs(NAT,COMPLEX);
reconsider h = (ComplexFuncExtMult NAT).(r1,v1) as Complex_Sequence
by FUNCT_2:66;
h = z(#)seq_id(v)
proof
let n be Element of NAT;
thus h.n = z*(v1.n) by CFUNCDOM:4
.= (z(#)seq_id(v)).n by VALUED_1:6;
end;
hence thesis;
end;
theorem Th4:
for n being object holds (seq_id CZeroseq).n = 0
proof
set f = seq_id CZeroseq;
let n be object;
per cases;
suppose
A1: n in dom f;
dom f = NAT by FUNCT_2:def 1;
hence thesis by A1,FUNCOP_1:7;
end;
suppose not n in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
theorem
for f being Element of the_set_of_ComplexSequences st
for n being Nat holds (seq_id f).n = 0 holds
f = CZeroseq
proof
let f be Element of the_set_of_ComplexSequences;
set g = seq_id f;
assume
A1: for n being Nat holds g.n = 0;
A2: dom g = NAT by FUNCT_2:def 1;
for z being object st z in dom g holds g.z = 0 by A1;
hence f = CZeroseq by A2,FUNCOP_1:11;
end;
::$CT 5
definition
let X be ComplexLinearSpace;
let X1 be Subset of X such that
A1: X1 is linearly-closed;
func Add_(X1,X) -> BinOp of X1 equals
:Def6:
(the addF of X) || X1;
correctness
proof
A2: dom (the addF of X) = [:the carrier of X,the carrier of X:] by
FUNCT_2:def 1;
A3: for z be object st z in [:X1,X1:] holds ((the addF of X) || X1).z in X1
proof
let z be object such that
A4: z in [:X1,X1:];
consider r,x be object such that
A5: r in X1 and
A6: x in X1 and
A7: z=[r,x] by A4,ZFMISC_1:def 2;
reconsider y=x,r1=r as VECTOR of X by A5,A6;
[r,x] in dom ((the addF of X) || X1) by A2,A4,A7,RELAT_1:62,ZFMISC_1:96;
then ((the addF of X) || X1).z = r1+y by A7,FUNCT_1:47;
hence thesis by A1,A5,A6;
end;
dom ((the addF of X) || X1) =[:X1,X1:] by A2,RELAT_1:62,ZFMISC_1:96;
hence thesis by A3,FUNCT_2:3;
end;
end;
definition
let X be ComplexLinearSpace;
let X1 be Subset of X such that
A1: X1 is linearly-closed;
func Mult_(X1,X) -> Function of [:COMPLEX,X1:], X1 equals
:Def7:
(the Mult
of X) | [:COMPLEX,X1:];
correctness
proof
A2: dom (the Mult of X) = [:COMPLEX,the carrier of X:] by FUNCT_2:def 1;
A3: [:COMPLEX,X1:] c= [:COMPLEX,the carrier of X:] by ZFMISC_1:95;
A4: for z be object st z in [:COMPLEX,X1:] holds ((the Mult of X) | [:COMPLEX
,X1:]).z in X1
proof
let z be object such that
A5: z in [:COMPLEX,X1:];
consider r,x be object such that
A6: r in COMPLEX and
A7: x in X1 and
A8: z=[r,x] by A5,ZFMISC_1:def 2;
reconsider r as Complex by A6;
reconsider y=x as VECTOR of X by A7;
[r,x] in dom ((the Mult of X) | [:COMPLEX,X1:]) by A3,A2,A5,A8,RELAT_1:62
;
then ((the Mult of X) | [:COMPLEX,X1:]).z = r*y by A8,FUNCT_1:47;
hence thesis by A1,A7;
end;
dom ((the Mult of X) | [:COMPLEX,X1:]) =[:COMPLEX,X1:] by A3,A2,RELAT_1:62;
hence thesis by A4,FUNCT_2:3;
end;
end;
definition
let X be ComplexLinearSpace, X1 be Subset of X such that
A1: X1 is linearly-closed and
A2: X1 is non empty;
func Zero_(X1,X) -> Element of X1 equals
:Def8:
0.X;
correctness
proof
set v = the Element of X1;
v in X1 by A2;
then reconsider v as Element of X;
v-v=0.X by RLVECT_1:15;
hence thesis by A1,A2,CLVECT_1:22;
end;
end;
theorem Th6:
for V be ComplexLinearSpace, V1 be Subset of V
st V1 is linearly-closed non empty
holds CLSStruct (# V1,Zero_(V1,V), Add_(V1,V), Mult_(V1,V) #)
is Subspace of V
proof
let V be ComplexLinearSpace;
let V1 be Subset of V such that
A1: V1 is linearly-closed and
A2: V1 is non empty;
A3: Add_(V1,V)= (the addF of V) || V1 by A1,Def6;
A4: Mult_(V1,V) = (the Mult of V) | [:COMPLEX,V1:] by A1,Def7;
Zero_(V1,V) = 0.V by A1,A2,Def8;
hence thesis by A2,A3,A4,CLVECT_1:43;
end;
definition
func the_set_of_l2ComplexSequences -> Subset of
Linear_Space_of_ComplexSequences means
:Def9:
for x being object holds x in it iff x in the_set_of_ComplexSequences &
|.seq_id(x).| (#) |.seq_id(x).| is summable;
existence
proof
defpred P[object] means |.seq_id($1).|(#)|.seq_id($1).| is summable;
consider IT being set such that
A1: for x being object holds x in IT iff x in the_set_of_ComplexSequences
& P[x] from XBOOLE_0:sch 1;
for x be object st x in IT holds x in the_set_of_ComplexSequences by A1;
then IT is Subset of the_set_of_ComplexSequences by TARSKI:def 3;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of Linear_Space_of_ComplexSequences;
assume that
A2: for x being object holds x in X1 iff x in
the_set_of_ComplexSequences & |.seq_id(x).|(#)|.seq_id(x).| is summable and
A3: for x being object holds x in X2 iff x in
the_set_of_ComplexSequences & |.seq_id(x).|(#)|.seq_id(x).| is summable;
A4: X2 c= X1
proof
let x be object;
assume
A5: x in X2;
then |.seq_id(x).|(#)|.seq_id(x).| is summable by A3;
hence thesis by A2,A5;
end;
X1 c= X2
proof
let x be object;
assume
A6: x in X1;
then |.seq_id(x).|(#)|.seq_id(x).| is summable by A2;
hence thesis by A3,A6;
end;
hence thesis by A4,XBOOLE_0:def 10;
end;
end;
Lm1:
|.seq_id(CZeroseq).|(#)|.seq_id(CZeroseq).| is absolutely_summable
proof
set f = seq_id(CZeroseq);
now
let n be Nat;
A1: f.n = 0 by Th4;
thus (|.f.|(#)|.f.|).n =|.f.| .n * |.f.| .n by SEQ_1:8
.= |.f.| .n * |.f.n.| by VALUED_1:18
.= 0 by A1,COMPLEX1:44;
end;
hence thesis by COMSEQ_3:3;
end;
registration
cluster the_set_of_l2ComplexSequences -> non empty;
coherence by Lm1,Def9;
end;
theorem Th7:
the_set_of_l2ComplexSequences is linearly-closed
proof
set W = the_set_of_l2ComplexSequences;
hereby
let v,u be VECTOR of Linear_Space_of_ComplexSequences such that
A1: v in W and
A2: u in W;
|.seq_id(v+u).|(#)|.seq_id(v+u).| is summable
proof
set r = |.seq_id(v+u).|(#)|.seq_id(v+u).|;
set q = |.seq_id(u).|(#)|.seq_id(u).|;
set p = |.seq_id(v).|(#)|.seq_id(v).|;
A3: for n be Nat holds 0<=r.n
proof
let n be Nat;
r.n=(|.seq_id(v+u).|).n * (|.seq_id(v+u).|).n by SEQ_1:8;
hence thesis by XREAL_1:63;
end;
A4: for n be Nat holds r.n <=(2(#)p+2(#)q).n
proof
set t = |.seq_id(u).|;
set s = |.seq_id(v).|;
let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
reconsider sn=s.n, tn=t.n as Real;
A6: r.n = ((|.seq_id(v+u).|).n)^2 by SEQ_1:8;
(2(#)p+2(#)q).n=(2(#)p).n +(2(#)q).n by SEQ_1:7
.= 2*p.n + (2(#)q).n by SEQ_1:9
.= 2*p.n + 2*q.n by SEQ_1:9
.= 2*(s.n*s.n) + 2*q.n by SEQ_1:8
.= 2*sn^2 + 2*tn^2 by SEQ_1:8;
then
A7: (2(#)p+2(#)q).n - (sn^2 + 2*sn*tn + tn^2) = (sn-tn)^2;
A8: v+u=seq_id(v)+seq_id(u) by Th2;
(|.seq_id(v+u).|).n = |.(seq_id(v+u)).n .| by VALUED_1:18
.= |.(seq_id(v)).n + (seq_id(u)).n.| by A8,VALUED_1:1,A5;
then (|.seq_id(v+u).|).n <= |.(seq_id(v)).n.| + |.(seq_id(u)).n.| by
COMPLEX1:56;
then (|.seq_id(v+u).|).n <= s.n + |.((seq_id(u)).n).| by VALUED_1:18;
then
A9: (|.seq_id(v+u).|).n <= s.n + t.n by VALUED_1:18;
A10: 0 + (sn^2 + 2*sn*tn + tn^2) <= (2(#)p+2(#)q).n by A7,XREAL_1:19,63;
0 <= |.(seq_id(v+u)).n.| by COMPLEX1:46;
then 0 <= (|.seq_id(v+u).|).n by VALUED_1:18;
then ((|.seq_id(v+u).|).n)^2 <= (s.n + t.n)^2 by A9,SQUARE_1:15;
hence thesis by A6,A10,XXREAL_0:2;
end;
|.seq_id(u).|(#)|.seq_id(u).| is summable by A2,Def9;
then
A11: 2(#)q is summable by SERIES_1:10;
|.seq_id(v).|(#)|.seq_id(v).| is summable by A1,Def9;
then 2(#)p is summable by SERIES_1:10;
then 2(#)p+2(#)q is summable by A11,SERIES_1:7;
hence thesis by A3,A4,SERIES_1:20;
end;
hence v+u in W by Def9;
end;
let z be Complex;
let v be VECTOR of Linear_Space_of_ComplexSequences;
assume v in W;
then
A12: |.seq_id(v).|(#)|.seq_id(v).| is summable by Def9;
z*v=z(#)seq_id(v) by Th3;
then |.seq_id(z*v).| = |.z.|(#)|.seq_id(v).| by COMSEQ_1:50;
then |.seq_id(z*v).|(#)|.seq_id(z*v).| =|.z.|(#)(|.z.|(#)|.seq_id(v).|(#)
|.seq_id(v).|) by SEQ_1:18
.=|.z.|(#)(|.z.|(#)(|.seq_id(v).|(#)|.seq_id(v).|)) by SEQ_1:18
.=(|.z.|*|.z.|)(#)(|.seq_id(v).|(#)|.seq_id(v).|) by SEQ_1:23;
then |.seq_id(z*v).|(#)|.seq_id(z*v).| is summable by A12,SERIES_1:10;
hence thesis by Def9;
end;
registration
cluster the_set_of_l2ComplexSequences -> linearly-closed;
coherence by Th7;
end;
registration
let z be Element of the_set_of_l2ComplexSequences;
reduce seq_id(z) to z;
reducibility;
end;
theorem
CLSStruct(# the_set_of_l2ComplexSequences, Zero_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) #) is Subspace
of Linear_Space_of_ComplexSequences by Th6;
theorem Th9:
CLSStruct (# the_set_of_l2ComplexSequences, Zero_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) #) is
ComplexLinearSpace by Th6;
theorem
the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences
&
(for x be set holds x is VECTOR of Linear_Space_of_ComplexSequences iff
x is Complex_Sequence) &
(for u be VECTOR of Linear_Space_of_ComplexSequences holds u =seq_id(u)) &
(for u,v be VECTOR of Linear_Space_of_ComplexSequences holds
u+v =seq_id(u)+seq_id(v)) &
for z be Complex for u be VECTOR of Linear_Space_of_ComplexSequences holds
z*u =z(#)seq_id(u) by FUNCT_2:8,66,Th2,Th3;
begin :: Unitary space with complex coefficient
definition
struct(CLSStruct) CUNITSTR (# carrier -> set,
ZeroF -> Element of the carrier,
addF -> BinOp of the carrier,
Mult -> Function of [:COMPLEX, the carrier:], the carrier,
scalar -> Function of [: the carrier, the carrier :], COMPLEX #);
end;
registration
cluster non empty strict for CUNITSTR;
existence
proof
set D = the non empty set, Z = the Element of D,a = the BinOp of D,
m =the Function of [:COMPLEX, D:], D,s = the Function of [: D,D:],COMPLEX;
take CUNITSTR (#D,Z,a,m,s#);
thus thesis;
end;
end;
registration
let D be non empty set, Z be Element of D, a be BinOp of D,m be Function of
[:COMPLEX, D:], D, s be Function of [: D,D:],COMPLEX;
cluster CUNITSTR (#D,Z,a,m,s#) -> non empty;
coherence;
end;
reserve X for non empty CUNITSTR;
reserve a, b for Complex;
reserve x, y for Point of X;
deffunc 09(CUNITSTR) = 0.$1;
definition
let X;
let x, y;
func x .|. y -> Complex equals
(the scalar of X).(x,y);
correctness;
end;
set V0 = the ComplexLinearSpace;
Lm2: the carrier of (0).V0 = {0.V0} by CLVECT_1:def 9;
reconsider nilfunc = [: the carrier of (0).V0, the carrier of (0).V0 :] --> 0c
as Function of [: the carrier of (0).V0, the carrier of (0).V0 :], COMPLEX;
Lm3: for x, y being VECTOR of (0).V0 holds nilfunc.[x,y] = 0c by FUNCOP_1:7;
0.V0 in the carrier of (0).V0 by Lm2,TARSKI:def 1;
then
Lm4: nilfunc.[0.V0,0.V0] = 0c by Lm3;
Lm5: for u being VECTOR of (0).V0 holds 0 <= Re(nilfunc.[u,u]) & Im(nilfunc.[u
,u]) = 0 by COMPLEX1:4,FUNCOP_1:7;
Lm6: for u, v being VECTOR of (0).V0 holds nilfunc.[u,v] = (nilfunc.[v,u])*'
proof
let u, v be VECTOR of (0).V0;
A1: v = 0.V0 by Lm2,TARSKI:def 1;
u = 0.V0 by Lm2,TARSKI:def 1;
hence thesis by A1,Lm4,COMPLEX1:28;
end;
Lm7: for u, v, w being VECTOR of (0).V0 holds nilfunc.[u+v,w] = nilfunc.[u,w]
+ nilfunc.[v,w]
proof
let u, v, w be VECTOR of (0).V0;
A1: v = 0.V0 by Lm2,TARSKI:def 1;
A2: w = 0.V0 by Lm2,TARSKI:def 1;
u = 0.V0 by Lm2,TARSKI:def 1;
hence thesis by A1,A2,Lm2,Lm4,TARSKI:def 1;
end;
Lm8: for u,v being VECTOR of (0).V0, a holds nilfunc.[a*u,v] = a * nilfunc.[u,
v]
proof
let u, v be VECTOR of (0).V0;
let a;
A1: v = 0.V0 by Lm2,TARSKI:def 1;
u = 0.V0 by Lm2,TARSKI:def 1;
hence thesis by A1,Lm2,Lm4,TARSKI:def 1;
end;
set X0 = CUNITSTR(# the carrier of (0).V0,0.((0).V0),the addF of (0).V0, the
Mult of (0).V0, nilfunc #);
Lm9: now
let x, y, z be Point of X0;
let a;
09(X0) = 0.V0 by CLVECT_1:30;
hence x .|. x = 0c iff x = 09(X0) by Lm2,Lm3,TARSKI:def 1;
thus 0 <= Re(x .|. x) & 0 = Im(x .|. x) by Lm5;
thus x .|. y = (y .|. x)*' by Lm6;
thus (x+y) .|. z = x .|. z + y .|. z
proof
reconsider u = x, v = y, w = z as VECTOR of (0).V0;
(x+y) .|. z = nilfunc.[u+v,w];
hence thesis by Lm7;
end;
thus (a*x) .|. y = a * ( x .|. y )
proof
reconsider u = x, v = y as VECTOR of (0).V0;
(a*x) .|. y = nilfunc.[a*u,v];
hence thesis by Lm8;
end;
end;
definition
let IT be non empty CUNITSTR;
attr IT is ComplexUnitarySpace-like means
:Def11:
for x,y,w being Point of IT, a holds ( x .|. x = 0 iff x = 0.IT ) &
0 <= Re(x .|. x) & 0 = Im(x .|. x) &
x .|. y = (y .|. x)*' & (x+y) .|. w = x .|. w + y .|. w &
(a*x) .|. y = a * ( x .|. y );
end;
registration
cluster ComplexUnitarySpace-like vector-distributive scalar-distributive
scalar-associative scalar-unital Abelian add-associative right_zeroed
right_complementable strict for non empty CUNITSTR;
existence
proof
take X0;
thus X0 is ComplexUnitarySpace-like by Lm9;
thus X0 is vector-distributive scalar-distributive scalar-associative
scalar-unital
proof
thus for a for v,w being VECTOR of X0 holds a * (v + w) = a * v + a * w
proof
let a;
let v,w be VECTOR of X0;
reconsider v9= v, w9 = w as VECTOR of (0).V0;
thus a * (v + w) = a *( v9 + w9) .= a * v9 + a * w9 by CLVECT_1:def 2
.= a * v + a * w;
end;
thus for a,b for v being VECTOR of X0 holds (a+ b) * v = a* v + b * v
proof
let a,b;
let v be VECTOR of X0;
reconsider v9= v as VECTOR of (0).V0;
thus (a + b) * v = (a + b) * v9 .= a * v9 + b * v9 by CLVECT_1:def 3
.= a * v + b * v;
end;
thus for a,b for v being VECTOR of X0 holds (a * b) * v = a * (b * v)
proof
let a,b;
let v be VECTOR of X0;
reconsider v9= v as VECTOR of (0).V0;
thus (a * b) * v = (a * b) * v9 .= a * (b * v9) by CLVECT_1:def 4
.= a * (b * v);
end;
let v be VECTOR of X0;
reconsider v9= v as VECTOR of (0).V0;
thus 1r * v = 1r * v9 .= v by CLVECT_1:def 5;
end;
A1: for x,y be VECTOR of X0 for x9,y9 be VECTOR of (0).V0 st x = x9 & y =
y9 holds x + y = x9 + y9 & for a holds a * x = a * x9;
thus for v,w being VECTOR of X0 holds v + w = w + v
proof
let v,w be VECTOR of X0;
reconsider v9= v, w9= w as VECTOR of (0).V0;
thus v + w = w9+ v9 by A1
.= w + v;
end;
thus for u,v,w being VECTOR of X0 holds (u + v) + w = u + (v + w)
proof
let u,v,w be VECTOR of X0;
reconsider u9= u, v9= v, w9= w as VECTOR of (0).V0;
thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w);
end;
thus for v being VECTOR of X0 holds v + 0.X0 = v
proof
let v be VECTOR of X0;
reconsider v9= v as VECTOR of (0).V0;
thus v + 0.X0 = v9+ 0.(0).V0 .=v by RLVECT_1:4;
end;
thus X0 is right_complementable
proof
let v be VECTOR of X0;
reconsider v9= v as VECTOR of (0).V0;
consider w9 be VECTOR of (0).V0 such that
A2: v9 + w9 = 0.(0).V0 by ALGSTR_0:def 11;
reconsider w = w9 as VECTOR of X0;
take w;
thus thesis by A2;
end;
thus thesis;
end;
end;
definition
mode ComplexUnitarySpace is ComplexUnitarySpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital Abelian add-associative
right_zeroed right_complementable non empty CUNITSTR;
end;
reserve X for ComplexUnitarySpace;
reserve x, y, z, u, v for Point of X;
theorem
(0.X).|.(0.X) = 0 by Def11;
theorem Th12:
x.|.(y+z) = x.|.y + x.|.z
proof
thus x.|.(y+z) = ((y+z).|.x)*' by Def11
.= (y.|.x + z.|.x)*' by Def11
.= (y.|.x)*' + (z.|.x)*' by COMPLEX1:32
.= x.|.y + (z.|.x)*' by Def11
.= x.|.y + x.|.z by Def11;
end;
theorem Th13:
x.|.(a*y) = (a*') * x.|.y
proof
thus x.|.(a*y) = ((a*y).|.x)*' by Def11
.= (a*(y.|.x))*' by Def11
.= (a*') * (y.|.x)*' by COMPLEX1:35
.= (a*') * (x.|.y) by Def11;
end;
theorem Th14:
(a*x).|.y = x.|.((a*')*y)
proof
(a*x) .|. y = a * x .|. y by Def11
.= (a*')*' * (y.|.x)*' by Def11
.= ((a*')*(y.|.x))*' by COMPLEX1:35
.= (((a*')*y).|.x)*' by Def11;
hence thesis by Def11;
end;
theorem Th15:
(a*x + b*y).|.z = a * x.|.z + b * y.|.z
proof
(a*x+b*y) .|. z = (a*x) .|. z + (b*y) .|. z by Def11
.= a * x .|. z + (b*y) .|. z by Def11;
hence thesis by Def11;
end;
theorem Th16:
x.|.(a*y + b*z) = (a*') * x.|.y + (b*') * x.|.z
proof
x.|.(a*y + b*z) = ((a*y + b*z).|.x)*' by Def11
.= ( a * y.|.x + b * z.|.x )*' by Th15
.= ( a * y.|.x )*' + ( b * z.|.x )*' by COMPLEX1:32
.= (a*') * (y.|.x)*' + ( b * z.|.x )*' by COMPLEX1:35
.= (a*') * (y.|.x)*' + (b*') * (z.|.x)*' by COMPLEX1:35
.= (a*') * x.|.y + (b*') * (z.|.x)*' by Def11;
hence thesis by Def11;
end;
theorem Th17:
(-x) .|. y = x .|. (-y)
proof
(-x) .|. y = ((-1r)*x) .|. y by CLVECT_1:3
.= x.|.( (-(1r))*' * y) by Th14
.= x.|.( (-1r) * y) by COMPLEX1:30,33;
hence thesis by CLVECT_1:3;
end;
theorem Th18:
(-x).|.y = - x.|.y
proof
(-x) .|. y = ((-1r)*x) .|. y by CLVECT_1:3
.= (-1) * x .|. y by Def11,COMPLEX1:def 4;
hence thesis;
end;
theorem Th19:
x.|.(-y) = - x.|.y
proof
x.|.(-y) = (-x).|.y by Th17;
hence thesis by Th18;
end;
theorem Th20:
(-x).|.(-y) = x.|.y
proof
(-x).|.(-y) = - x.|.(-y) by Th18
.= - ( - x .|. y ) by Th19;
hence thesis;
end;
theorem Th21:
(x-y).|.z = x.|.z - y.|.z
proof
(x - y) .|. z = x .|. z + (-y) .|. z by Def11
.= x .|. z + ( - y .|. z ) by Th18;
hence thesis;
end;
theorem Th22:
x.|.(y-z) = x.|.y - x.|.z
proof
x .|. (y - z) = x .|. y + x .|. (-z) by Th12
.= x .|. y + ( - x .|. z ) by Th19;
hence thesis;
end;
theorem
(x-y).|.(u-v) = x.|.u - x.|.v - y.|.u + y.|.v
proof
(x - y) .|. (u - v) = x .|. (u - v) - y .|. (u - v) by Th21
.= ( x .|. u - x .|. v ) - y .|. (u - v) by Th22
.= ( x .|. u - x .|. v ) - ( y .|. u - y .|. v ) by Th22;
hence thesis;
end;
theorem Th24:
(0.X).|.x = 0
proof
09(X) .|. x = (x + (-x)) .|. x by RLVECT_1:5
.= x .|. x + (-x) .|. x by Def11
.= x .|. x + ( - x .|. x ) by Th18;
hence thesis;
end;
theorem Th25:
x.|.0.X = 0
proof
x.|.0.X = ((0.X).|.x)*' by Def11
.= 0c by Th24,COMPLEX1:28;
hence thesis;
end;
theorem Th26:
(x+y).|.(x+y) = x.|.x + x.|.y + y.|.x + y.|.y
proof
(x+y).|.(x+y) = x.|.(x+y) + y.|.(x+y) by Def11
.= (x.|.x + x.|.y) + y.|.(x+y) by Th12
.= (x.|.x + x.|.y) + (y.|.x + y.|.y) by Th12;
hence thesis;
end;
theorem
(x+y).|.(x-y) = x.|.x - x.|.y + y.|.x - y.|.y
proof
(x + y) .|. (x - y) = x .|. (x - y) + y .|. (x - y) by Def11
.= (x .|. x - x .|. y) + y .|. (x - y) by Th22
.= (x .|. x - x .|. y) + (y .|. x - y .|. y) by Th22
.= (x.|.x - x.|.y) + y.|.x + -y.|.y;
hence thesis;
end;
theorem Th28:
(x-y).|.(x-y) = x.|.x - x.|.y - y.|.x + y.|.y
proof
(x - y) .|. (x - y) = x .|. (x - y) - y .|. (x - y) by Th21
.= x .|. x - x .|. y - y .|. (x - y) by Th22
.= x.|.x - x.|.y - ( y.|.x - y.|.y ) by Th22;
hence thesis;
end;
Lm10: for p,q being Complex, x,y being Point of X holds (p*x + q*y).|.(p*x + q
*y) = p*p*' *(x.|.x) + p*q*' *(x.|.y) + p*' *q*(y.|.x) + q*q*' *(y.|.y)
proof
let p,q be Complex;
let x,y being Point of X;
(p*x+q*y).|.(p*x+q*y) = p * (x.|.(p*x + q*y)) + q * (y.|.(p*x + q*y)) by Th15
.= p * (p*' *(x.|.x) + q*' *(x.|.y)) + q * (y.|.(p*x + q*y)) by Th16
.= p*p*' *(x.|.x) + p*q*' *(x.|.y) + (q * (p*' *(y.|.x) + q*' *(y.|.y)))
by Th16
.= p*p*' *(x.|.x) + p*q*' *(x.|.y) + (q*p*' *(y.|.x) + q*q*' *(y.|.y));
hence thesis;
end;
theorem Th29:
|.(x.|.x).| = Re(x.|.x)
proof
A1: Im (x.|.x) = 0 by Def11;
Re (x.|.x) >= 0 by Def11;
then |.Re(x.|.x)+Im(x.|.x)*<i>.| = Re (x.|.x) by A1,ABSVALUE:def 1;
hence thesis by COMPLEX1:13;
end;
theorem Th30: ::Schwarz's inequality
|.(x.|.y).| <= sqrt|.(x.|.x).| * sqrt|.(y.|.y).|
proof
A1: y <> 09(X) implies |.(x.|.y).| <= sqrt|.(x.|.x).| * sqrt|.(y.|.y).|
proof
assume y <> 09(X);
then y.|.y <> 0c by Def11;
then
A2: |.(y.|.y).| <> 0 by COMPLEX1:45;
A3: (Re(x.|.y))^2 >= 0 by XREAL_1:63;
set c2 = -(x.|.y);
reconsider c1 = |.(y.|.y).|+0*<i> as Element of COMPLEX by XCMPLX_0:def 2;
A4: Re( c1*(c1*(x.|.x) + c2*(y.|.x)) ) = Re c1 * Re (c1*(x.|.x) + c2*(y
.|.x)) - Im c1 * Im (c1*(x.|.x) + c2*(y.|.x)) by COMPLEX1:9
.= Re c1 * Re (c1*(x.|.x) + c2*(y.|.x)) - 0 * Im (c1*(x.|.x) + c2*(y
.|.x)) by COMPLEX1:12
.= Re c1 * Re (c1*(x.|.x) + c2*(y.|.x));
A5: Re (c2*(y.|.x)) = Re (-(x.|.y)*(y.|.x))
.= - Re(x.|.y * y.|.x) by COMPLEX1:17
.= - Re((x.|.y) * (x.|.y)*') by Def11;
A6: Im((x.|.y) * (x.|.y)*') = 0 by COMPLEX1:40;
A7: Im (y.|.y) = 0 by Def11;
A8: Re (y.|.y) >= 0 by Def11;
then |.Re(y.|.y)+Im(y.|.y)*<i>.| = Re (y.|.y) by A7,ABSVALUE:def 1;
then
A9: |.(y.|.y).| = Re (y.|.y) by COMPLEX1:13;
then
A10: (y.|.y) = c1 by A7,COMPLEX1:13;
((c1*x+c2*y).|.(c1*x+c2*y)) = c1*c1*' *(x.|.x) + c1*c2*' *(x.|.y) +c1
*' *c2*(y.|.x) + c2*c2*' *(y.|.y) by Lm10
.= c1*(c1*' *(x.|.x)) + c1*(c2*' *(x.|.y)) +c1*' *(c2*(y.|.x)) + c1*(
c2*c2*') by A7,A9,COMPLEX1:13
.= c1*(c1*' *(x.|.x) + c2*' *(x.|.y)) +c1*(c2*(y.|.x)) + c1*(c2*c2*')
by A10,Def11
.= c1*(c1*' *(x.|.x) + c2*' *(x.|.y) + c2*(y.|.x) + c2*c2*')
.= c1*(c1*(x.|.x) + (x.|.y)*c2*' + c2*(y.|.x) + c2*c2*') by A10,Def11
.= c1*(c1*(x.|.x) + c2*(y.|.x));
then
Re c1 >= 0 & Re (c1*(x.|.x) + c2*(y.|.x)) >= 0 or Re c1 <= 0 & Re (c1
*(x.|.x) + c2*(y.|.x)) <= 0 by A4,Def11;
then Re (c1*(x.|.x)) + Re (c2*(y.|.x)) >= 0 by A8,A7,A9,A2,COMPLEX1:8,13;
then Re (c1*(x.|.x)) - Re((x.|.y) * (x.|.y)*') >= 0 by A5;
then
A11: Re (c1*(x.|.x)) >= Re((x.|.y) * (x.|.y)*') + 0 by XREAL_1:19;
A12: Im(x.|.x) = 0 by Def11;
A13: (Im(x.|.y))^2 >= 0 by XREAL_1:63;
Im c1 = 0 by A7,A9,COMPLEX1:13;
then Im(c1*(x.|.x)) = Re c1 * 0 + Re (x.|.x)*0 by A12,COMPLEX1:9;
then
A14: |.c1*(x.|.x).| = |.Re (c1*(x.|.x)).| by COMPLEX1:50;
Re((x.|.y) * (x.|.y)*') = (Re(x.|.y))^2 + (Im(x.|.y))^2 by COMPLEX1:40;
then
A15: Re((x.|.y) * (x.|.y)*') >= 0 + 0 by A3,A13;
then |.Re((x.|.y) * (x.|.y)*').| = Re((x.|.y) * (x.|.y)*') by
ABSVALUE:def 1;
then |.Re (c1*(x.|.x)).| >= |.Re((x.|.y) * (x.|.y)*').| by A11,A15,
ABSVALUE:def 1;
then |.c1*(x.|.x).| >= |.(x.|.y)*(x.|.y)*' .| by A6,A14,COMPLEX1:50;
then |.(x.|.x).|*|.(y.|.y).| >= |.(x.|.y)*(x.|.y)*'.| by A10,COMPLEX1:65;
then |.(x.|.x).|*|.(y.|.y).| >= |.(x.|.y).|*|.(x.|.y)*'.| by COMPLEX1:65;
then
A16: |.(x.|.x).|*|.(y.|.y).| >= |.(x.|.y).|*|.(x.|.y).| by COMPLEX1:53;
|.(x.|.y).|^2 >= 0 by XREAL_1:63;
then
A17: sqrt(|.(x.|.x).|*|.(y.|.y).|) >= sqrt(|.(x.|.y).|^2) by A16,SQUARE_1:26;
A18: |.(y.|.y).| >= 0 by COMPLEX1:46;
|.(x.|.x).| >= 0 by COMPLEX1:46;
then sqrt|.(x.|.x).| * sqrt|.(y.|.y).| >= sqrt(|.(x.|.y).|^2) by A17,A18,
SQUARE_1:29;
hence thesis by COMPLEX1:46,SQUARE_1:22;
end;
y = 09(X) implies |.(x.|.y).| <= sqrt|.(x.|.x).| * sqrt|.(y.|.y).|
proof
assume
A19: y = 09(X);
then y.|.y = 0c by Def11;
hence thesis by A19,Th25,COMPLEX1:44;
end;
hence thesis by A1;
end;
definition
let X;
let x, y;
pred x, y are_orthogonal means
:Def12:
x .|. y = 0;
symmetry by Def11,COMPLEX1:28;
end;
theorem
x, y are_orthogonal implies x, - y are_orthogonal
proof
assume x, y are_orthogonal;
then - x .|. y = - 0;
hence thesis by Th19;
end;
theorem
x, y are_orthogonal implies -x, y are_orthogonal
proof
assume x, y are_orthogonal;
then - x .|. y = - 0;
hence thesis by Th18;
end;
theorem
x, y are_orthogonal implies -x, -y are_orthogonal by Th20;
theorem
x, 0.X are_orthogonal
proof
(0.X).|.x = 0 by Th24;
hence thesis by Def12;
end;
theorem
x,y are_orthogonal implies (x+y).|.(x+y) = x.|.x + y.|.y
proof
assume
A1: x, y are_orthogonal;
then y .|. x = 0c by Def12;
then (x + y) .|. (x + y) = x.|.x + 0c + y.|.y by A1,Th26;
hence thesis;
end;
theorem
x,y are_orthogonal implies (x-y).|.(x-y) = x.|.x + y.|.y
proof
assume
A1: x,y are_orthogonal;
(x-y).|.(x-y) = x.|.x - x.|.y - y.|.x + y.|.y by Th28
.= x.|.x + y.|.y - 0 by A1,Def12;
hence thesis;
end;
definition
let X, x;
func ||.x.|| -> Real equals
sqrt |.(x.|.x).|;
correctness;
end;
theorem Th37:
||.x.|| = 0 iff x = 0.X
proof
thus ||.x.|| = 0 implies x = 09(X)
proof
0 <= Re (x.|.x) by Def11;
then
A1: 0 <= |.(x.|.x).| by Th29;
assume ||.x.|| = 0;
then |.(x.|.x).| = 0 by A1,SQUARE_1:24;
then x.|.x = 0c by COMPLEX1:45;
hence thesis by Def11;
end;
assume x = 09(X);
hence thesis by Def11,COMPLEX1:44,SQUARE_1:17;
end;
theorem Th38:
||.a * x.|| = |.a.| * ||.x.||
proof
A1: 0 <= |.a*a.| by COMPLEX1:46;
0 <= Re (x.|.x) by Def11;
then
A2: 0 <= |.(x.|.x).| by Th29;
||.a*x.|| = sqrt |.(a*(x.|.(a*x))).| by Def11
.= sqrt |.(a*(a*' *(x.|.x))).| by Th13
.= sqrt |.((a*a*')*(x.|.x)).|
.= sqrt (|.(a*a*').|*|.(x.|.x).|) by COMPLEX1:65
.= sqrt (|.a*a.| * |.(x.|.x).|) by COMPLEX1:69
.= sqrt |.a*a.| * sqrt |.(x.|.x).| by A1,A2,SQUARE_1:29
.= sqrt (|.a.|^2) * sqrt |.(x.|.x).| by COMPLEX1:65
.= |.a.| * sqrt |.(x.|.x).| by COMPLEX1:46,SQUARE_1:22;
hence thesis;
end;
theorem Th39:
0 <= ||.x.||
proof
0 <= Re(x.|.x) by Def11;
then 0 <= |.(x.|.x).| by Th29;
hence thesis by SQUARE_1:def 2;
end;
theorem
|.(x.|.y).| <= ||.x.|| * ||.y.|| by Th30;
theorem Th41:
||.x + y.|| <= ||.x.|| + ||.y.||
proof
A1: ||.x + y.||^2 >= 0 by XREAL_1:63;
Re ((x+y).|.(x+y)) >= 0 by Def11;
then
A2: |.((x + y).|.(x + y)).| >= 0 by Th29;
sqrt ||.x + y.||^2 = sqrt |.((x + y).|.(x + y)).| by Th39,SQUARE_1:22;
then
A3: ||.x + y.||^2 = |.((x + y).|.(x + y)).| by A2,A1,SQUARE_1:28;
|.(y.|.y).| >= 0 by COMPLEX1:46;
then
A4: |.(y.|.y).| = ||.y.||^2 by SQUARE_1:def 2;
A5: -Im(x.|.y) = Im((x.|.y)*') by COMPLEX1:27
.= Im(y.|.x) by Def11;
Im(x.|.x + x.|.y + y.|.x + y.|.y) = Im(x.|.x + x.|.y + y.|.x) + Im(y.|.y
) by COMPLEX1:8
.= Im(x.|.x + x.|.y) + Im(y.|.x) + Im(y.|.y) by COMPLEX1:8
.= Im(x.|.x) + Im(x.|.y) + Im(y.|.x) + Im(y.|.y) by COMPLEX1:8
.= 0 + Im(x.|.y) + Im(y.|.x) + Im(y.|.y) by Def11
.= Im(x.|.y) + Im(y.|.x) + 0 by Def11;
then
A6: (x.|.x + x.|.y + y.|.x + y.|.y) = Re(x.|.x + x.|.y + y.|.x + y.|.y)+0*
<i> by A5,COMPLEX1:13;
A7: Re(x.|.y) = Re((x.|.y)*') by COMPLEX1:27
.= Re(y.|.x) by Def11;
A8: Re(x.|.y) <= |.(x.|.y).| by COMPLEX1:54;
|.(x.|.y).| <= ||.x.||*||.y.|| by Th30;
then Re(x.|.y) <= ||.x.||*||.y.|| by A8,XXREAL_0:2;
then
A9: 2*Re(x.|.y) <= 2*(||.x.||*||.y.||) by XREAL_1:64;
Re(x.|.x + x.|.y + y.|.x + y.|.y) = Re((x + y).|.(x + y)) by Th26;
then
A10: Re(x.|.x + x.|.y + y.|.x + y.|.y) >= 0 by Def11;
Re(x.|.x + x.|.y + y.|.x + y.|.y) = Re(x.|.x + x.|.y + y.|.x) + Re(y.|.y
) by COMPLEX1:8
.= Re(x.|.x + x.|.y) + Re(y.|.x) + Re(y.|.y) by COMPLEX1:8
.= Re(x.|.x) + Re(x.|.y) + Re(y.|.x) + Re(y.|.y) by COMPLEX1:8
.= |.(x.|.x).| + Re(x.|.y) + Re(y.|.x) + Re(y.|.y) by Th29
.= |.(x.|.x).| + Re(x.|.y) + Re(y.|.x) + |.(y.|.y).| by Th29;
then |.(x.|.x + x.|.y + y.|.x + y.|.y).| = |.(x.|.x).| + 2*Re(x.|.y) + |.(y
.|.y).| by A7,A10,A6,ABSVALUE:def 1;
then
A11: ||.x + y.||^2 = 2*Re(x.|.y) + (|.(x.|.x).| + |.(y.|.y).|) by A3,Th26;
A12: ||.y.|| >= 0 by Th39;
|.(x.|.x).| >= 0 by COMPLEX1:46;
then (sqrt |.(x.|.x).|)^2 = |.(x.|.x).| by SQUARE_1:def 2;
then
||.x + y.||^2 <= 2*(||.x.||*||.y.||) + (||.x.||^2 + |.(y.|.y).|) by A11,A9,
XREAL_1:6;
then
A13: ||.x + y.||^2 <= (||.x.|| + ||.y.||)^2 by A4;
||.x.|| >= 0 by Th39;
hence thesis by A12,A13,SQUARE_1:16;
end;
theorem Th42:
||.-x.|| = ||.x.||
proof
||.-x.|| = ||.(-1r) * x.|| by CLVECT_1:3
.= |.-1r.| * ||.x.|| by Th38
.= |.1r.| * ||.x.|| by COMPLEX1:52;
hence thesis by COMPLEX1:48;
end;
theorem Th43:
||.x.|| - ||.y.|| <= ||.x - y.||
proof
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - 09(X) by RLVECT_1:15
.= x by RLVECT_1:13;
then ||.x.|| <= ||.x - y.|| + ||.y.|| by Th41;
hence thesis by XREAL_1:20;
end;
theorem
|.||.x.|| - ||.y.||.| <= ||.x - y.||
proof
(y - x) + x = y - (x - x) by RLVECT_1:29
.= y - 09(X) by RLVECT_1:15
.= y by RLVECT_1:13;
then ||.y.|| <= ||.y - x.|| + ||.x.|| by Th41;
then ||.y.|| - ||.x.|| <= ||.y - x.|| by XREAL_1:20;
then ||.y.|| - ||.x.|| <= ||.-(x - y).|| by RLVECT_1:33;
then ||.y.|| - ||.x.|| <= ||.x - y.|| by Th42;
then
A1: -(||.x - y.||) <= -(||.y.|| - ||.x.||) by XREAL_1:24;
||.x.|| - ||.y.|| <= ||.x - y.|| by Th43;
hence thesis by A1,ABSVALUE:5;
end;
definition
let X, x, y;
func dist(x,y) -> Real equals
||.x - y.||;
correctness;
end;
definition
let X, x, y;
redefine func dist(x,y); :: redefines dist (CSSPACE, definition)
commutativity
proof let x,y;
thus dist(x,y) = ||.-(y-x).|| by RLVECT_1:33
.= dist(y,x) by Th42;
end;
end;
theorem Th45:
dist(x,x) = 0
proof
thus dist(x,x) = ||.09(X).|| by RLVECT_1:15
.= 0 by Th37;
end;
theorem
dist(x,z) <= dist(x,y) + dist(y,z)
proof
dist(x,z) = ||.(x-z)+09(X).|| by RLVECT_1:4
.= ||.(x-z)+(y-y).|| by RLVECT_1:15
.= ||.x-(z-(y-y)).|| by RLVECT_1:29
.= ||.x-(y+(z-y)).|| by RLVECT_1:29
.= ||.(x-y)-(z-y).|| by RLVECT_1:27
.= ||.(x-y)+(y-z).|| by RLVECT_1:33;
hence thesis by Th41;
end;
theorem Th47:
x <> y iff dist(x,y) <> 0
proof
thus x <> y implies dist(x,y) <> 0
proof
assume that
A1: x <> y and
A2: dist(x,y) = 0;
x - y = 09(X) by A2,Th37;
hence contradiction by A1,RLVECT_1:21;
end;
thus thesis by Th45;
end;
theorem
dist(x,y) >= 0 by Th39;
theorem
x <> y iff dist(x,y) > 0
proof
thus x <> y implies dist(x,y) > 0
proof
assume x <> y;
then dist(x,y) <> 0 by Th47;
hence thesis by Th39;
end;
thus thesis by Th45;
end;
theorem
dist(x,y) = sqrt |.((x-y) .|. (x-y)).|;
theorem
dist(x + y,u + v) <= dist(x,u) + dist(y,v)
proof
dist(x + y,u + v) = ||.((-u) + (-v)) + (x + y).|| by RLVECT_1:31
.= ||.x + ((-u) + (-v)) + y.|| by RLVECT_1:def 3
.= ||.x - u + (-v) + y.|| by RLVECT_1:def 3
.= ||.x - u + (y - v).|| by RLVECT_1:def 3;
hence thesis by Th41;
end;
theorem
dist(x - y,u - v) <= dist(x,u) + dist(y,v)
proof
dist(x - y,u - v) = ||.((x - y) - u) + v.|| by RLVECT_1:29
.= ||.(x - (u + y)) + v.|| by RLVECT_1:27
.= ||.((x - u) - y) + v.|| by RLVECT_1:27
.= ||.(x - u) - (y - v).|| by RLVECT_1:29
.= ||.(x - u) + -(y - v).||;
then dist(x - y,u - v) <= ||.x - u.|| + ||.-(y - v).|| by Th41;
hence thesis by Th42;
end;
theorem
dist(x - z, y - z) = dist(x,y)
proof
thus dist(x - z,y - z) = ||.((x - z) - y) + z.|| by RLVECT_1:29
.= ||.(x - (y + z)) + z.|| by RLVECT_1:27
.= ||.((x - y) - z) + z.|| by RLVECT_1:27
.= ||.(x - y) - (z - z).|| by RLVECT_1:29
.= ||.(x - y) - 09(X).|| by RLVECT_1:15
.= dist(x,y) by RLVECT_1:13;
end;
theorem
dist(x - z,y - z) <= dist(z,x) + dist(z,y)
proof
dist(x - z,y - z) = ||.(x - z) + (z - y).|| by RLVECT_1:33
.= ||.-(z - x) + (z - y).|| by RLVECT_1:33;
then dist(x - z,y - z) <= ||.-(z - x).|| + ||.z - y.|| by Th41;
hence thesis by Th42;
end;
reserve seq, seq1, seq2, seq3 for sequence of X;
reserve n for Nat;
definition
let X, seq1, seq2;
redefine func seq1 + seq2; :: redefines + (NORMSP_1, definition)
commutativity
proof let seq1, seq2;
now
let n be Element of NAT;
thus (seq1 + seq2).n = seq2.n + seq1.n by NORMSP_1:def 2
.= (seq2 + seq1).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3
proof
now
let n be Element of NAT;
thus (seq1 + (seq2 + seq3)).n = seq1.n + (seq2 + seq3).n by NORMSP_1:def 2
.= seq1.n + (seq2.n + seq3.n) by NORMSP_1:def 2
.= (seq1.n + seq2.n) + seq3.n by RLVECT_1:def 3
.= (seq1 + seq2).n + seq3.n by NORMSP_1:def 2
.= ((seq1 + seq2) + seq3).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq1 is constant & seq2 is constant & seq = seq1 + seq2 implies
seq is constant
proof
assume that
A1: seq1 is constant and
A2: seq2 is constant and
A3: seq = seq1 + seq2;
consider x such that
A4: for n being Nat holds seq1.n = x by A1;
consider y such that
A5: for n being Nat holds seq2.n = y by A2;
take z = x + y;
let n be Nat;
thus seq.n = seq1.n + seq2.n by A3,NORMSP_1:def 2
.= x + seq2.n by A4
.= z by A5;
end;
theorem
seq1 is constant & seq2 is constant & seq = seq1 - seq2 implies
seq is constant
proof
assume that
A1: seq1 is constant and
A2: seq2 is constant and
A3: seq = seq1 - seq2;
consider x such that
A4: for n being Nat holds seq1.n = x by A1;
consider y such that
A5: for n being Nat holds seq2.n = y by A2;
take z = x - y;
let n be Nat;
thus seq.n = seq1.n - seq2.n by A3,NORMSP_1:def 3
.= x - seq2.n by A4
.= z by A5;
end;
theorem
seq1 is constant & seq = a * seq1 implies seq is constant
proof
assume that
A1: seq1 is constant and
A2: seq = a * seq1;
consider x such that
A3: for n being Nat holds seq1.n = x by A1;
take z = a * x;
let n be Nat;
thus seq.n = a * seq1.n by A2,CLVECT_1:def 14
.= z by A3;
end;
theorem
seq1 - seq2 = seq1 + -seq2
proof
now
let n be Element of NAT;
thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3
.= seq1.n + (-seq2).n by BHSP_1:44
.= (seq1 + -seq2).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq = seq + 0.X
proof
now
let n be Element of NAT;
thus (seq + 09(X)).n = seq.n + 09(X) by BHSP_1:def 6
.= seq.n by RLVECT_1:4;
end;
hence thesis by FUNCT_2:63;
end;
theorem
a * (seq1 + seq2) = a * seq1 + a * seq2
proof
now
let n be Element of NAT;
thus (a * (seq1 + seq2)).n = a * (seq1 + seq2).n by CLVECT_1:def 14
.= a * (seq1.n + seq2.n) by NORMSP_1:def 2
.= a * seq1.n + a * seq2.n by CLVECT_1:def 2
.= (a * seq1).n + a * seq2.n by CLVECT_1:def 14
.= (a * seq1).n + (a * seq2).n by CLVECT_1:def 14
.= (a * seq1 + a * seq2).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(a + b) * seq = a * seq + b * seq
proof
now
let n be Element of NAT;
thus ((a + b) * seq).n = (a + b) * seq.n by CLVECT_1:def 14
.= a * seq.n + b * seq.n by CLVECT_1:def 3
.= (a * seq).n + b * seq.n by CLVECT_1:def 14
.= (a * seq).n + (b * seq).n by CLVECT_1:def 14
.= (a * seq + b * seq).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(a * b) * seq = a * (b * seq)
proof
now
let n be Element of NAT;
thus ((a * b) * seq).n = (a * b) * seq.n by CLVECT_1:def 14
.= a * (b * seq.n) by CLVECT_1:def 4
.= a * (b * seq).n by CLVECT_1:def 14
.= (a * (b * seq)).n by CLVECT_1:def 14;
end;
hence thesis by FUNCT_2:63;
end;
theorem
1r * seq = seq
proof
now
let n be Element of NAT;
thus (1r * seq).n = 1r * seq.n by CLVECT_1:def 14
.= seq.n by CLVECT_1:def 5;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(-1r) * seq = - seq
proof
now
let n be Element of NAT;
thus ((-1r) * seq).n = (-1r) * seq.n by CLVECT_1:def 14
.= - seq.n by CLVECT_1:3
.= (-seq).n by BHSP_1:44;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq - x = seq + -x
proof
now
let n be Element of NAT;
thus (seq - x).n = seq.n - x by NORMSP_1:def 4
.= (seq + -x).n by BHSP_1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq1 - seq2 = - (seq2 - seq1)
proof
now
let n be Element of NAT;
thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3
.= - (seq2.n - seq1.n) by RLVECT_1:33
.= - (seq2 - seq1).n by NORMSP_1:def 3
.= (- (seq2 - seq1)).n by BHSP_1:44;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq = seq - 0.X
proof
now
let n be Element of NAT;
thus (seq - 09(X)).n = seq.n - 09(X) by NORMSP_1:def 4
.= seq.n by RLVECT_1:13;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq = - ( - seq )
proof
now
let n be Element of NAT;
thus (- ( - seq )).n = - (- seq).n by BHSP_1:44
.= - ( - seq.n) by BHSP_1:44
.= seq.n by RLVECT_1:17;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof
now
let n be Element of NAT;
thus (seq1 - (seq2 + seq3)).n = seq1.n - (seq2 + seq3).n by NORMSP_1:def 3
.= seq1.n - (seq2.n + seq3.n) by NORMSP_1:def 2
.= (seq1.n - seq2.n) - seq3.n by RLVECT_1:27
.= (seq1 - seq2).n - seq3.n by NORMSP_1:def 3
.= ((seq1 - seq2) - seq3).n by NORMSP_1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)
proof
now
let n be Element of NAT;
thus ((seq1 + seq2) - seq3).n = (seq1 + seq2).n - seq3.n by NORMSP_1:def 3
.= (seq1.n + seq2.n) - seq3.n by NORMSP_1:def 2
.= seq1.n + (seq2.n - seq3.n) by RLVECT_1:def 3
.= seq1.n + (seq2 - seq3).n by NORMSP_1:def 3
.= (seq1 + (seq2 - seq3)).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof
now
let n be Element of NAT;
thus (seq1 - (seq2 - seq3)).n = seq1.n - (seq2 - seq3).n by NORMSP_1:def 3
.= seq1.n - (seq2.n - seq3.n) by NORMSP_1:def 3
.= (seq1.n - seq2.n) + seq3.n by RLVECT_1:29
.= (seq1 - seq2).n + seq3.n by NORMSP_1:def 3
.= ((seq1 - seq2) + seq3).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
a * (seq1 - seq2) = a * seq1 - a * seq2
proof
now
let n be Element of NAT;
thus (a * (seq1 - seq2)).n = a * (seq1 - seq2).n by CLVECT_1:def 14
.= a * (seq1.n - seq2.n) by NORMSP_1:def 3
.= a * seq1.n - a * seq2.n by CLVECT_1:9
.= (a * seq1).n - a * seq2.n by CLVECT_1:def 14
.= (a * seq1).n - (a * seq2).n by CLVECT_1:def 14
.= (a * seq1 - a * seq2).n by NORMSP_1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
begin :: Complex unitary space of complex sequence
definition
func cl_scalar -> Function of [:the_set_of_l2ComplexSequences,
the_set_of_l2ComplexSequences:], COMPLEX means
for x,y be object st x in
the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds it.(x,
y) = Sum(seq_id(x)(#)(seq_id(y))*');
existence
proof
deffunc F(object,object) = Sum(seq_id($1)(#)(seq_id($2))*');
set X = the_set_of_l2ComplexSequences;
A1: for x,y being object st x in X & y in X holds F(x,y) in COMPLEX;
ex f being Function of [:X,X:],COMPLEX st for x,y being object st x in X &
y in X holds f.(x,y) = F(x,y) from BINOP_1:sch 2(A1);
hence thesis;
end;
uniqueness
proof
set X = the_set_of_l2ComplexSequences;
let scalar1, scalar2 be Function of [: X, X :], COMPLEX such that
A2: for x,y be object st x in X & y in X holds scalar1.(x,y) = Sum(seq_id
(x)(#)(seq_id(y))*') and
A3: for x,y be object st x in X & y in X holds scalar2.(x,y) = Sum(seq_id
(x)(#)(seq_id(y))*');
for x, y be set st x in X & y in X holds scalar1.(x,y) = scalar2.(x,y)
proof
let x,y be set such that
A4: x in X and
A5: y in X;
thus scalar1.(x,y) = Sum(seq_id(x)(#)(seq_id(y))*') by A2,A4,A5
.= scalar2.(x,y) by A3,A4,A5;
end;
hence thesis;
end;
end;
registration
cluster CUNITSTR (# the_set_of_l2ComplexSequences, Zero_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), cl_scalar #)
-> non empty;
coherence;
end;
definition
func Complex_l2_Space -> non empty CUNITSTR equals
CUNITSTR (#
the_set_of_l2ComplexSequences, Zero_(the_set_of_l2ComplexSequences,
Linear_Space_of_ComplexSequences), Add_(the_set_of_l2ComplexSequences,
Linear_Space_of_ComplexSequences), Mult_(the_set_of_l2ComplexSequences,
Linear_Space_of_ComplexSequences), cl_scalar #);
correctness;
end;
theorem Th74:
for l be CLSStruct st the CLSStruct of l is ComplexLinearSpace
holds l is ComplexLinearSpace
proof
let l be CLSStruct such that
A1: the CLSStruct of l is ComplexLinearSpace;
reconsider l as non empty CLSStruct by A1;
reconsider l0=CLSStruct (# the carrier of l, 0.l, the addF of l, the Mult of
l #) as ComplexLinearSpace by A1;
A2: l is Abelian
proof
let v,w be VECTOR of l;
reconsider v1=v as VECTOR of l0;
reconsider w1=w as VECTOR of l0;
thus v+w =v1+w1 .= w1+v1
.= w +v;
end;
A3: l is add-associative
proof
let u,v,w be VECTOR of l;
reconsider u1=u as VECTOR of l0;
reconsider v1=v as VECTOR of l0;
reconsider w1=w as VECTOR of l0;
thus (u + v) + w = (u1+v1)+w1 .= u1+(v1+w1) by RLVECT_1:def 3
.= u+(v+w);
end;
A4: l is vector-distributive scalar-distributive scalar-associative
scalar-unital
proof
thus for z being Complex, v,w being VECTOR of l holds z * (v + w) = z * v
+ z * w
proof
let z be Complex;
let v,w be VECTOR of l;
reconsider v1=v, w1=w as VECTOR of l0;
thus z*(v+w) =z*(v1+w1) .=z*v1+z*w1 by CLVECT_1:def 2
.= z*v +z*w;
end;
thus for z1,z2 being Complex, v being VECTOR of l holds (z1 + z2) * v = z1
* v + z2 * v
proof
let z1,z2 be Complex;
let v be VECTOR of l;
reconsider v1=v as VECTOR of l0;
thus (z1+z2)*v =(z1+z2)*v1 .=z1*v1+z2*v1 by CLVECT_1:def 3
.= z1*v +z2*v;
end;
thus for z1,z2 being Complex, v being VECTOR of l holds (z1 * z2) * v = z1
* (z2 * v)
proof
let z1,z2 be Complex;
let v be VECTOR of l;
reconsider v1=v as VECTOR of l0;
thus (z1*z2)*v =(z1*z2)*v1 .=z1*(z2*v1) by CLVECT_1:def 4
.= z1*(z2*v);
end;
let v be VECTOR of l;
reconsider v1=v as VECTOR of l0;
thus 1r*v= 1r*v1 .= v by CLVECT_1:def 5;
end;
A5: l is right_complementable
proof
let v be VECTOR of l;
reconsider v1=v as VECTOR of l0;
consider w1 being VECTOR of l0 such that
A6: v1 + w1 = 0.l0 by ALGSTR_0:def 11;
reconsider w = w1 as VECTOR of l;
take w;
thus thesis by A6;
end;
l is right_zeroed
proof
let v be VECTOR of l;
reconsider v1=v as VECTOR of l0;
thus v+0.l= v1 + 0.l0 .= v by RLVECT_1:def 4;
end;
hence thesis by A2,A3,A5,A4;
end;
theorem
for seq be Complex_Sequence st (for n be Nat holds seq.n=0c
) holds seq is summable & Sum seq = 0c
proof
let seq be Complex_Sequence such that
A1: for n be Nat holds seq.n=0c;
A2: for m be Nat holds Partial_Sums (seq).m = 0c
proof
defpred P[Nat] means seq.$1 = (Partial_Sums seq).$1;
let m be Nat;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: seq.k = (Partial_Sums (seq)).k;
thus seq.(k+1) = 0c + (seq).(k+1) .= seq.k + seq.(k+1) by A1
.= (Partial_Sums seq).(k+1) by A4,SERIES_1:def 1;
end;
A5: P[0] by SERIES_1:def 1;
for n be Nat holds P[n] from NAT_1:sch 2(A5,A3);
hence (Partial_Sums (seq)).m = seq.m .= 0c by A1;
end;
A6: for p be Real
st 0<p ex n be Nat st for m be Nat
st n<=m holds |.((Partial_Sums seq).m-0c).|<p
proof
let p be Real such that
A7: 0<p;
take 0;
let m be Nat such that
0<=m;
thus thesis by A2,A7,COMPLEX1:44;
end;
then
A8: Partial_Sums (seq) qua Complex_Sequence is convergent by COMSEQ_2:def 5;
then lim (Partial_Sums (seq)) = 0c by A6,COMSEQ_2:def 6;
hence thesis by A8,COMSEQ_3:def 7,def 8;
end;
registration
cluster Complex_l2_Space -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence by Th9,Th74;
end;
theorem
|.seq_id(CZeroseq).|(#)|.seq_id(CZeroseq).| is absolutely_summable by Lm1;