:: Hilbert Space of Complex Sequences
:: by Noboru Endou
::
:: Received February 24, 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, COMSEQ_1, ARYTM_3, FUNCT_1, SUBSET_1, COMPLEX1, ARYTM_1,
RELAT_1, XCMPLX_0, SERIES_1, CARD_1, REAL_1, XXREAL_0, SQUARE_1, CARD_3,
ORDINAL2, SEQ_2, VALUED_1, CSSPACE, RSSPACE, SUPINF_2, RLVECT_1,
ALGSTR_0, ZFMISC_1, STRUCT_0, REALSET1, PROB_2, BHSP_1, SEQ_1, PRE_TOPC,
FUNCOP_1, NAT_1, BHSP_3, NORMSP_1, XXREAL_2, REWRITE1, CSSPACE2;
notations SUBSET_1, ZFMISC_1, ORDINAL1, XCMPLX_0, XXREAL_0, NUMBERS, COMPLEX1,
XREAL_0, NAT_1, STRUCT_0, ALGSTR_0, RELAT_1, DOMAIN_1, PARTFUN1, FUNCT_1,
FUNCT_2, BINOP_1, FUNCOP_1, REALSET1, PRE_TOPC, SQUARE_1, VALUED_1,
SEQ_1, SEQ_2, SERIES_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, NORMSP_0, CLVECT_1,
CLVECT_2, CSSPACE;
constructors BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, COMSEQ_2, COMSEQ_3,
REALSET1, CLVECT_2, SEQ_2, RELSET_1, CFUNCDOM;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
XCMPLX_0, XXREAL_0, MEMBERED, COMSEQ_2, COMSEQ_3, REALSET1, STRUCT_0,
CSSPACE, VALUED_1, VALUED_0, SEQ_2, XREAL_0, SQUARE_1, NAT_1, INT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions CLVECT_2;
equalities SQUARE_1, REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, VALUED_1, CSSPACE,
CFUNCDOM;
theorems RELAT_1, SQUARE_1, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SEQM_3,
SERIES_1, INT_1, FUNCT_1, FUNCT_2, RLVECT_1, SEQ_4, RSSPACE, XCMPLX_1,
CSSPACE, CLVECT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, COMPLEX1, CLVECT_2,
RSSPACE2, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, XCMPLX_0, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2, COMSEQ_1;
begin
Lm1: for seq be Complex_Sequence holds Partial_Sums (seq*') = (Partial_Sums
seq)*'
proof
let seq be Complex_Sequence;
defpred P[Nat] means
Partial_Sums(seq*').$1 = (Partial_Sums seq)*'.$1;
A1: now
let n be Nat;
A2: n in NAT by ORDINAL1:def 12;
assume
A3: P[n];
Partial_Sums(seq*').(n+1) = Partial_Sums(seq*').n + seq*'.(n+1) by
SERIES_1:def 1
.= (Partial_Sums seq)*'.n + (seq.(n+1))*' by A3,COMSEQ_2:def 2
.= ((Partial_Sums seq).n)*' + (seq.(n+1))*' by COMSEQ_2:def 2,A2
.= ((Partial_Sums seq).n + seq.(n+1))*' by COMPLEX1:32
.= ((Partial_Sums seq).(n+1))*' by SERIES_1:def 1;
hence P[n+1] by COMSEQ_2:def 2;
end;
Partial_Sums(seq*').0 = seq*'.0 by SERIES_1:def 1
.= (seq.0)*' by COMSEQ_2:def 2
.= ((Partial_Sums seq).0)*' by SERIES_1:def 1;
then
A4: P[0] by COMSEQ_2:def 2;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A1);
then for n be Element of NAT holds P[n];
hence thesis by FUNCT_2:63;
end;
Lm2: for a,b be Real holds 0 <= a^2 + b^2
proof
let a,b be Real;
0<=a^2 & 0<=b^2 by XREAL_1:63;
then 0 +0 <=a^2 + b^2;
hence thesis;
end;
Lm3: for z1, z2 be Complex st (Re z1)*(Im z2) = (Re z2)*(Im z1) & (Re z1)*(Re
z2)+(Im z1)*(Im z2) >= 0 holds |.z1 + z2.| = |.z1.| + |.z2.|
proof
let z1, z2 be Complex;
assume that
A1: (Re z1)*(Im z2) = (Re z2)*(Im z1) and
A2: (Re z1)*(Re z2) + (Im z1)*(Im z2) >= 0;
set r1 = Re z1, r2 = Re z2, i1 = Im z1, i2 = Im z2;
A3: (Re(z1 + z2))^2 = (r1+ r2)^2 by COMPLEX1:8
.= r1^2 + 2*r1*r2 + r2^2;
r1*r2+i1*i2 = |.r1*r2+i1*i2.| by A2,ABSVALUE:def 1;
then
A4: r1*r2+i1*i2 = sqrt (r1*r2+i1*i2)^2 by COMPLEX1:72;
A5: (Im(z1 + z2))^2 = (i1 + i2)^2 by COMPLEX1:8
.= i1^2 + 2*i1*i2 + i2^2;
A6: 0 <= r2^2+i2^2 by Lm2;
then
A7: (sqrt (r2^2+i2^2))^2 = r2^2+i2^2 by SQUARE_1:def 2;
A8: 0 <= sqrt (r2^2+i2^2) by A6,SQUARE_1:def 2;
A9: 0 <= r1^2+i1^2 by Lm2;
then 0 <= sqrt (r1^2+i1^2) by SQUARE_1:def 2;
then
A10: 0 + 0 <= sqrt (r1^2+i1^2) + sqrt (r2^2+i2^2) by A8;
(r1^2+i1^2)*(r2^2+i2^2)-(r1*r2+i1*i2)^2 = (r1*i2-i1*r2)^2;
then sqrt (r1*r2+i1*i2)^2 = sqrt ((r1^2+i1^2)*(r2^2+i2^2)) by A1,XCMPLX_1:15;
then
A11: sqrt (r1*r2+i1*i2)^2 = sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2) by A9,A6,
SQUARE_1:29;
(sqrt (r1^2+i1^2))^2 = r1^2+i1^2 by A9,SQUARE_1:def 2;
then sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) = sqrt ((sqrt (r1^2+i1^2) +
sqrt (r2^2+i2^2))^2) by A7,A3,A5,A4,A11;
then
sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) = (sqrt (r1^2+i1^2) + sqrt (r2
^2+i2^2)) by A10,SQUARE_1:22;
then
sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) = sqrt (r1^2+i1^2) + |.z2.| by
COMPLEX1:def 12;
then sqrt ((Re(z1 + z2))^2+(Im(z1 + z2))^2) = |.z1.|+|.z2.| by
COMPLEX1:def 12;
hence thesis by COMPLEX1:def 12;
end;
Lm4: for seq be Complex_Sequence, n be Nat st
(for i be Nat
holds (Re seq).i >= 0 & (Im seq).i = 0) holds (|.Partial_Sums seq.|).n = (
Partial_Sums |.seq.|).n
proof
let seq be Complex_Sequence;
let n be Nat;
defpred P[Nat] means
(|.Partial_Sums seq.|).$1 = (Partial_Sums |.seq.|).$1;
assume
A1: for i be Nat holds (Re seq).i >= 0 & (Im seq).i = 0;
A2: now
let m be Nat;
assume
A3: P[m];
thus P[m+1]
proof
for i be Nat holds (Partial_Sums Re seq).i >= 0
proof
defpred Q1[Nat] means (Partial_Sums Re seq).$1 >= 0;
let i be Nat;
A4: now
let k be Nat;
assume
A5: Q1[k];
(Partial_Sums Re seq).(k+1) = (Partial_Sums Re seq).k + (Re seq
).(k+1) & (Re seq).(k+1) >= 0 by A1,SERIES_1:def 1;
then (Partial_Sums Re seq).(k+1) >= 0 + 0 by A5;
hence Q1[k+1];
end;
(Partial_Sums Re seq).0 = (Re seq).0 by SERIES_1:def 1;
then
A6: Q1[0] by A1;
for i be Nat holds Q1[i] from NAT_1:sch 2(A6,A4);
hence thesis;
end;
then (Partial_Sums Re seq).m >= 0;
then (Re (Partial_Sums seq)).m >= 0 by COMSEQ_3:26;
then
A7: Re(Partial_Sums seq.m) >= 0 by COMSEQ_3:def 5;
set z2 = seq.(m+1);
set z1 = Partial_Sums seq.m;
A8: (|.Partial_Sums seq.|).(m+1) = |.(Partial_Sums seq).(m+1).| by
VALUED_1:18
.= |.Partial_Sums seq.m + seq.(m+1).| by SERIES_1:def 1;
for i be Nat holds (Partial_Sums Im seq).i = 0
proof
defpred Q2[Nat] means (Partial_Sums Im seq).$1 = 0;
let i be Nat;
A9: now
let k be Nat;
A10: (Partial_Sums Im seq).(k+1) = (Partial_Sums Im seq).k + (Im seq
).(k+1) by SERIES_1:def 1;
assume Q2[k];
hence Q2[k+1] by A1,A10;
end;
(Partial_Sums Im seq).0 = (Im seq).0 by SERIES_1:def 1;
then
A11: Q2[0] by A1;
for i be Nat holds Q2[i] from NAT_1:sch 2(A11,A9);
hence thesis;
end;
then (Partial_Sums Im seq).m = 0;
then (Im (Partial_Sums seq)).m = 0 by COMSEQ_3:26;
then
A12: Im(Partial_Sums seq.m) = 0 by COMSEQ_3:def 6;
(Im seq).(m+1) = 0 by A1;
then Im(seq.(m+1)) = 0 by COMSEQ_3:def 6;
then
A13: (Re z1)*(Im z2) = (Re z2)*(Im z1) by A12;
(Re seq).(m+1) >= 0 by A1;
then Re(seq.(m+1)) >=0 by COMSEQ_3:def 5;
then (Re z1)*(Re z2)+(Im z1)*(Im z2) >= 0 by A7,A12;
then
(|.Partial_Sums seq.|).(m+1) = |.(Partial_Sums seq.m).| + |.(seq.(m
+1)).| by A8,A13,Lm3
.= (|.Partial_Sums seq.|).m + |.(seq.(m+1)).| by VALUED_1:18
.= (Partial_Sums |.seq.|).m + (|.seq.|).(m+1) by A3,VALUED_1:18;
hence thesis by SERIES_1:def 1;
end;
end;
(|.Partial_Sums seq.|).0 = |.((Partial_Sums seq).0).| by VALUED_1:18
.= |.(seq.0).| by SERIES_1:def 1
.= (|.seq.|).0 by VALUED_1:18;
then
A14: P[0] by SERIES_1:def 1;
for m be Nat holds P[m] from NAT_1:sch 2(A14,A2);
hence thesis;
end;
Lm5: for seq be Complex_Sequence st seq is summable holds Sum (seq*') = (Sum
seq)*'
proof
let seq be Complex_Sequence;
assume
A1: seq is summable;
Sum(seq*') = lim Partial_Sums (seq*') by COMSEQ_3:def 7
.= lim ((Partial_Sums seq)*') by Lm1
.= (lim Partial_Sums seq)*' by A1,COMSEQ_2:12;
hence thesis by COMSEQ_3:def 7;
end;
Lm6: for seq be Complex_Sequence st seq is absolutely_summable holds |. Sum
seq .| <= Sum |.seq.|
proof
let seq be Complex_Sequence;
A1: for k be Nat holds (|.Partial_Sums seq.|).k <= (Partial_Sums
|.seq.|).k
proof
let k be Nat;
|.Partial_Sums seq .k .| <= Partial_Sums(|.seq.|).k by COMSEQ_3:30;
hence thesis by VALUED_1:18;
end;
assume
A2: seq is absolutely_summable;
then reconsider Pseq = Partial_Sums seq as convergent Complex_Sequence;
A3: |. Sum seq .| = |. lim Partial_Sums seq .| by COMSEQ_3:def 7
.= lim |.Partial_Sums seq.| by A2,SEQ_2:27;
|.Pseq.| is convergent & Partial_Sums |.seq.| is convergent by A2,
SERIES_1:def 2;
then lim |.Partial_Sums(seq).| <= lim Partial_Sums(|.seq.|) by A1,SEQ_2:18;
hence thesis by A3,SERIES_1:def 3;
end;
Lm7: for seq be Complex_Sequence st seq is summable & (for n be Nat
holds (Re seq).n >= 0 & (Im seq).n = 0) holds |. Sum seq .| = Sum |.seq.|
proof
let seq be Complex_Sequence;
assume that
A1: seq is summable and
A2: for n be Nat holds (Re seq).n >= 0 & (Im seq).n = 0;
for x be object st x in NAT holds (|.Partial_Sums seq.|).x = (Partial_Sums
|.seq.|).x by A2,Lm4;
then |.Partial_Sums seq.| = Partial_Sums |.seq.| by FUNCT_2:12;
then lim |.Partial_Sums seq.| = Sum |.seq.| by SERIES_1:def 3;
then |.lim Partial_Sums seq.| = Sum |.seq.| by A1,SEQ_2:27;
hence thesis by COMSEQ_3:def 7;
end;
Lm8: for seq be Complex_Sequence, n be Nat holds (Re (seq(#)seq*'))
.n >= 0 & (Im (seq(#)seq*')).n = 0
proof
let seq be Complex_Sequence;
let n be Nat;
A1: n in NAT by ORDINAL1:def 12;
then reconsider nn=n as Element of NAT;
reconsider z1 = seq.nn as Element of COMPLEX;
A2: 0 <= (Re z1)^2 & 0 <= (Im z1)^2 by XREAL_1:63;
(Re(seq(#)seq*')).n = Re((seq(#)seq*').n) by COMSEQ_3:def 5
.= Re (seq.n * seq*'.n) by VALUED_1:5
.= Re (seq.n * (seq.n)*') by COMSEQ_2:def 2,A1
.= (Re z1)^2 + (Im z1)^2 by COMPLEX1:40;
then (Re(seq(#)seq*')).n >= 0+0 by A2;
hence (Re (seq(#)seq*')).n >= 0;
(Im (seq(#)seq*')).n = Im((seq(#)seq*').n) by COMSEQ_3:def 6
.= Im (seq.n * seq*'.n) by VALUED_1:5
.= Im (seq.n * (seq.n)*') by COMSEQ_2:def 2,A1;
hence thesis by COMPLEX1:40;
end;
Lm9: for x be set holds x is Element of Complex_l2_Space iff x is
Complex_Sequence & |.seq_id(x).|(#)|.seq_id(x).| is summable
proof
for x be set holds x is Element of Complex_l2_Space iff x is
Complex_Sequence & |.seq_id(x).|(#)|.seq_id(x).| is summable
proof
let x be set;
x in the_set_of_ComplexSequences iff x is Complex_Sequence
by FUNCT_2:8,66;
hence thesis by CSSPACE:def 11;
end;
hence thesis;
end;
Lm10: 0.Complex_l2_Space = CZeroseq
proof
thus 0.Complex_l2_Space = 0.Linear_Space_of_ComplexSequences
by CSSPACE:def 10
.= CZeroseq;
end;
Lm12: for u,v be VECTOR of Complex_l2_Space holds u+v =seq_id(u)+seq_id(v)
proof
set W = the_set_of_l2ComplexSequences;
set L1 = Linear_Space_of_ComplexSequences;
let u,v be VECTOR of Complex_l2_Space;
reconsider u1=u,v1=v as VECTOR of Linear_Space_of_ComplexSequences by
CLVECT_1:29,CSSPACE:13;
dom (the addF of L1) = [:the carrier of L1,the carrier of L1:] by
FUNCT_2:def 1;
then
A1: dom ((the addF of Linear_Space_of_ComplexSequences)||W) =[:W,W:] by
RELAT_1:62,ZFMISC_1:96;
u+v =((the addF of Linear_Space_of_ComplexSequences)||W).[u,v] by CSSPACE:def
8
.=u1+v1 by A1,FUNCT_1:47;
hence thesis by CSSPACE:15;
end;
Lm13: for r be Complex for u be VECTOR of Complex_l2_Space holds r*u =r(#)
seq_id(u)
proof
set W = the_set_of_l2ComplexSequences;
set L1=Linear_Space_of_ComplexSequences;
let r be Complex;
let u be VECTOR of Complex_l2_Space;
reconsider u1=u as VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1:29
,CSSPACE:13;
dom (the Mult of L1) = [:COMPLEX,the carrier of L1:] by FUNCT_2:def 1;
then
A1: dom ((the Mult of Linear_Space_of_ComplexSequences) | [:COMPLEX,W:]) =[:
COMPLEX,W:] by RELAT_1:62,ZFMISC_1:96;
reconsider r as Element of COMPLEX by XCMPLX_0:def 2;
r*u =(the Mult of Complex_l2_Space).[r,u] by CLVECT_1:def 1
.=((the Mult of Linear_Space_of_ComplexSequences)|[:COMPLEX,W:]).[r,u]
by CSSPACE:def 9
.=(the Mult of Linear_Space_of_ComplexSequences).[r,u] by A1,FUNCT_1:47
.=r*u1 by CLVECT_1:def 1;
hence thesis by CSSPACE:15;
end;
Lm14: for u be VECTOR of Complex_l2_Space holds -u =-seq_id(u) & seq_id(-u)=-
seq_id(u)
proof
let u be VECTOR of Complex_l2_Space;
-u = (-1r)*u by CLVECT_1:3
.= (-1r)(#)seq_id(u) by Lm13
.= -seq_id(u) by COMSEQ_1:11;
hence thesis;
end;
Lm15: for u,v be VECTOR of Complex_l2_Space holds u-v =seq_id(u)-seq_id(v)
proof
let u,v be VECTOR of Complex_l2_Space;
thus u-v = seq_id(u)+seq_id(-v) by Lm12
.= seq_id(u)-seq_id(v) by Lm14;
end;
Lm16: for v,w be VECTOR of Complex_l2_Space holds |.seq_id(v).|(#)|.seq_id(w)
.| is summable
proof
set q0 = 1/2;
let u,v be VECTOR of Complex_l2_Space;
set p = |.(seq_id(v)).|(#)|.(seq_id(v)).|;
set q = |.(seq_id(u)).|(#)|.(seq_id(u)).|;
set r = |.|.(seq_id(u)).|(#)|.(seq_id(v)).| .|;
A1: for n be Nat holds 0<=(2(#)r).n
proof
set rr=|.(seq_id(u)).|(#)|.(seq_id(v)).|;
let n be Nat;
set tt=|.rr.n.|;
A2: 0 <= tt by COMPLEX1:46;
(2(#)r).n = 2*r.n by SEQ_1:9
.= 2*|.rr.n.| by SEQ_1:12;
hence thesis by A2;
end;
A3: for n be Nat holds (2(#)r).n <=(p+q).n
proof
set s = seq_id v, t = seq_id u;
let n be Nat;
set sn=|.(s.n).|,tn=|.(t.n).|;
set ss=|.sn.|,tt=|.tn.|;
A4: (p+q).n = p.n +q.n by SEQ_1:7
.= ((|.s.|).n*(|.s.|).n) + q.n by SEQ_1:8
.= ((|.s.|).n*(|.s.|).n) + ((|.t.|).n*(|.t.|).n) by SEQ_1:8
.= (|.(s.n).|*(|.s.|).n) + ((|.t.|).n*(|.t.|).n) by VALUED_1:18
.= sn^2 + ((|.t.|).n*(|.t.|).n) by VALUED_1:18
.= sn^2 + (|.(t.n).|*(|.t.|).n) by VALUED_1:18
.=(|.sn.|)^2 + (|.tn.|)^2 by VALUED_1:18;
A5: 0 <= (|.sn.|-|.tn.|)^2 by XREAL_1:63;
(2(#)r).n =2*r.n by SEQ_1:9
.=2*|. (|.seq_id(u).|(#)|.seq_id(v).|).n .| by SEQ_1:12
.=2*(|. (|.seq_id(u).|).n * (|.seq_id(v).|).n .|) by SEQ_1:8
.=2*(|. (|.seq_id(u).|).n .| * |. (|.seq_id(v).|).n .|) by COMPLEX1:65
.=2*(|. (|.((seq_id(u)).n).|) .| * |. (|.seq_id(v).|).n .|) by
VALUED_1:18
.= 2*(ss*tt) by VALUED_1:18
.= 2*|.sn.|*|.tn.|;
then 0 + (2(#)r).n <= (p+q).n - (2(#)r).n + (2(#)r).n by A4,A5,XREAL_1:7;
hence thesis;
end;
A6: q0(#)(2(#)r)=(q0*2)(#)r by SEQ_1:23
.=r by SEQ_1:27;
|.(seq_id(v)).|(#)|.(seq_id(v)).| is summable & |.(seq_id(u)).|(#)|.(
seq_id( u)).| is summable by CSSPACE:def 11;
then p+q is summable by SERIES_1:7;
then 2(#)r is summable by A1,A3,SERIES_1:20;
then r is summable by A6,SERIES_1:10;
then |.seq_id(u).|(#)|.seq_id(v).| is absolutely_summable by SERIES_1:def 4;
hence thesis;
end;
Lm18: for seq being Complex_Sequence holds |.seq.| = |.seq*'.|
proof
let seq be Complex_Sequence;
reconsider rseq1 = |.seq.| as Real_Sequence;
reconsider rseq2 = |.seq*'.| as Real_Sequence;
for n being Nat holds (|.seq.|).n = (|.seq*'.|).n
proof
let n be Nat;
A1: n in NAT by ORDINAL1:def 12;
(|.seq*'.|).n = |.((seq*').n).| by VALUED_1:18
.= |.(seq.n)*'.| by COMSEQ_2:def 2,A1
.= |.(seq.n).| by COMPLEX1:53;
hence thesis by VALUED_1:18;
end;
then for n be object st n in NAT holds rseq1.n = rseq2.n;
hence thesis by FUNCT_2:12;
end;
Lm19: for x be set holds x is Element of Complex_l2_Space iff x is
Complex_Sequence & seq_id(x)(#)(seq_id(x))*' is absolutely_summable
proof
A1: for x be set holds x is Element of Complex_l2_Space implies x is
Complex_Sequence & seq_id(x)(#)(seq_id(x))*' is absolutely_summable
proof
let x be set;
A2: |.seq_id(x).| = |.(seq_id(x))*'.| by Lm18;
assume
A3: x is Element of Complex_l2_Space;
then x in the_set_of_ComplexSequences by CSSPACE:def 11;
hence x is Complex_Sequence by FUNCT_2:66;
|.seq_id(x).|(#)|.seq_id(x).| is summable by A3,Lm16;
then |.seq_id(x)(#)(seq_id(x))*'.| is summable by A2,COMSEQ_1:46;
hence thesis by COMSEQ_3:def 9;
end;
for x be set holds x is Complex_Sequence & seq_id(x)(#)(seq_id(x))*' is
absolutely_summable implies x is Element of Complex_l2_Space
proof
let x be set;
assume that
A4: x is Complex_Sequence and
A5: seq_id(x)(#)(seq_id(x))*' is absolutely_summable;
|.seq_id(x)(#)(seq_id(x))*'.| is summable by A5;
then |.seq_id(x).|(#)|.(seq_id(x))*'.| is summable by COMSEQ_1:46;
then
A6: |.seq_id(x).|(#)|.(seq_id(x)).| is summable by Lm18;
x in the_set_of_ComplexSequences by A4,FUNCT_2:8;
hence thesis by A6,CSSPACE:def 11;
end;
hence thesis by A1;
end;
theorem
the carrier of Complex_l2_Space = the_set_of_l2ComplexSequences & (for
x be set holds x is Element of Complex_l2_Space iff x is Complex_Sequence & |.
seq_id(x).|(#)|.seq_id(x).| is summable) & (for x be set holds x is Element of
Complex_l2_Space iff x is Complex_Sequence & seq_id(x)(#)(seq_id(x))*' is
absolutely_summable ) & 0.Complex_l2_Space = CZeroseq & (for u be VECTOR of
Complex_l2_Space holds u =seq_id(u)) & (for u,v be VECTOR of Complex_l2_Space
holds u+v =seq_id(u)+seq_id(v)) & (for r be Complex for u be VECTOR of
Complex_l2_Space holds r*u =r(#)seq_id(u)) & (for u be VECTOR of
Complex_l2_Space holds -u =-seq_id(u) & seq_id(-u)=-seq_id(u)) & (for u,v be
VECTOR of Complex_l2_Space holds u-v =seq_id(u)-seq_id(v)) & for v,w be VECTOR
of Complex_l2_Space holds |.seq_id(v).|(#)|.seq_id(w).| is summable & for v,w
be VECTOR of Complex_l2_Space holds v.|.w = Sum(seq_id(v)(#)(seq_id(w))*')
by Lm9,Lm10,Lm12,Lm13,Lm14,Lm15,Lm16,Lm19,CSSPACE:def 17;
theorem Th2:
for x,y,z being Point of Complex_l2_Space for a be Complex holds
( x.|.x = 0 iff x = 0.Complex_l2_Space ) & Re(x.|.x) >= 0 & Im(x.|.x) = 0 & x
.|.y = (y.|.x)*' & (x+y).|.z = x.|.z + y.|.z & (a*x).|.y = a*(x.|.y)
proof
let x, y, z be Point of Complex_l2_Space;
let a be Complex;
set seqx = seq_id(x);
A1: x .|. x = Sum(seqx(#)seqx*') by CSSPACE:def 17;
A2: seqx(#)seqx*' is absolutely_summable by Lm19;
then Sum(seqx(#)seqx*') = Sum(Re(seqx(#)seqx*'))+Sum(Im(seqx(#)seqx*'))*<i>
by COMSEQ_3:53;
then
A3: Re(x.|.x) = Sum(Re(seqx(#)seqx*')) & Im(x.|.x) = Sum(Im(seqx(#)seqx*'))
by A1,COMPLEX1:12;
A4: now
set seq = seq_id(x);
A5: x .|. x = Sum(seq_id(x)(#)(seq_id(x))*') by CSSPACE:def 17;
set rseq = Re(seq(#)seq*');
A6: for n be Nat holds rseq.n = (Re(seq.n))^2 + (Im(seq.n))^2
proof
let n be Nat;
A7: n in NAT by ORDINAL1:def 12;
rseq.n = ( Re seq (#) Re (seq*') -Im seq (#) Im (seq*') ).n by
COMSEQ_3:21
.= ( Re seq (#) Re (seq*') ).n + ( -Im seq (#) Im (seq*') ).n by
SEQ_1:7
.= ( Re seq (#) Re (seq*') ).n + -( (Im seq (#) Im (seq*'))).n by
SEQ_1:10
.= ( Re seq (#) Re (seq*') ).n - ( (Im seq (#) Im (seq*'))).n
.= (Re seq).n * (Re (seq*')).n - ((Im seq (#) Im (seq*'))).n by SEQ_1:8
.= (Re seq).n * (Re (seq*')).n - ((Im seq).n * (Im (seq*')).n) by
SEQ_1:8
.= Re (seq.n) * (Re (seq*')).n - ((Im seq).n * (Im (seq*')).n) by
COMSEQ_3:def 5
.= Re (seq.n) * Re (seq*'.n) - ((Im seq).n * (Im (seq*')).n) by
COMSEQ_3:def 5
.= Re (seq.n) * Re (seq*'.n) - (Im(seq.n) * (Im (seq*')).n) by
COMSEQ_3:def 6
.= Re (seq.n) * Re (seq*'.n) - (Im(seq.n) * Im (seq*'.n)) by
COMSEQ_3:def 6
.= Re (seq.n) * Re ((seq.n)*') - (Im(seq.n) * Im (seq*'.n)) by
COMSEQ_2:def 2,A7
.= Re (seq.n) * Re ((seq.n)*') - (Im(seq.n) * Im((seq.n)*')) by
COMSEQ_2:def 2,A7
.= Re (seq.n) * Re (seq.n) - (Im(seq.n) * Im((seq.n)*')) by COMPLEX1:27
.= Re(seq.n) * Re(seq.n) - (Im(seq.n) * -Im(seq.n)) by COMPLEX1:27
.= (Re(seq.n))^2 + Im(seq.n) * Im(seq.n);
hence thesis;
end;
A8: for n be Nat holds 0 <= rseq.n
proof
let n be Nat;
A9: (Im(seq.n))^2 >= 0 by XREAL_1:63;
rseq.n = (Re(seq.n))^2 + (Im(seq.n))^2 & (Re(seq.n))^2 >= 0 by A6,
XREAL_1:63;
then rseq.n >= 0 + 0 by A9;
hence thesis;
end;
A10: seq_id(x)(#)(seq_id(x))*' is absolutely_summable by Lm19;
assume x .|. x = 0;
then
Sum(Re(seq_id(x)(#)(seq_id(x))*'))+ (Sum(Im(seq_id(x)(#)(seq_id(x))*')
))*<i> = 0 by A5,A10,COMSEQ_3:53;
then
A11: Sum(Re(seq_id(x)(#)(seq_id(x))*')) = 0 by COMPLEX1:4,12;
A12: for n be Nat holds (seq_id(x)).n = 0
proof
let n be Nat;
rseq.n = (Re(seq.n))^2 + (Im(seq.n))^2 by A6;
then (Re(seq.n))^2 + (Im(seq.n))^2 = 0 by A10,A11,A8,RSSPACE:17;
hence thesis by COMPLEX1:5;
end;
x is Element of the_set_of_ComplexSequences by CSSPACE:def 11;
hence x=0.Complex_l2_Space by A12,Lm10,CSSPACE:5;
end;
A13: now
assume
A14: x=0.Complex_l2_Space;
A15: for n be Nat holds (seq_id(x)(#)(seq_id(x))*').n=0
proof
let n be Nat;
thus (seq_id(x)(#)(seq_id(x))*').n = (seq_id(x)).n * ((seq_id(x))*').n
by VALUED_1:5
.=0c * ((seq_id(x))*').n by A14,Lm10,CSSPACE:4
.= 0;
end;
thus x.|.x = Sum(seq_id(x)(#)(seq_id(x))*') by CSSPACE:def 17
.=0 by A15,CSSPACE:80;
end;
set seqy = seq_id(y);
A16: for n being Nat holds 0 <= (Re(seqx(#)seqx*')).n
proof
let n be Nat;
A17: n in NAT by ORDINAL1:def 12;
A18: (Re(seqx.n))^2 >= 0 & (Im(seqx.n))^2 >= 0 by XREAL_1:63;
(Re(seqx(#)seqx*')).n = Re((seqx(#)seqx*').n) by COMSEQ_3:def 5
.= Re( seqx.n * seqx*'.n ) by VALUED_1:5
.= Re( seqx.n * (seqx.n)*') by COMSEQ_2:def 2,A17
.= (Re(seqx.n))^2 + (Im(seqx.n))^2 by COMPLEX1:40;
then (Re(seqx(#)seqx*')).n >= 0 + 0 by A18;
hence thesis;
end;
|.seqx.|(#)|.seqy.| is summable by Lm16;
then |.seqx*'.|(#)|.seqy.| is summable by Lm18;
then |.seqx*'(#)seqy.| is summable by COMSEQ_1:46;
then
A19: seqx*'(#)seqy is absolutely_summable by COMSEQ_3:def 9;
set seqz = seq_id(z);
A20: for n being Nat holds (Im(seqx(#)seqx*')).n = 0
proof
let n be Nat;
A21: n in NAT by ORDINAL1:def 12;
(Im(seqx(#)seqx*')).n = Im((seqx(#)seqx*').n) by COMSEQ_3:def 6
.= Im( seqx.n * seqx*'.n ) by VALUED_1:5
.= Im( seqx.n * (seqx.n)*') by COMSEQ_2:def 2,A21;
hence thesis by COMPLEX1:40;
end;
|.seqx.|(#)|.seqz.| is summable by Lm16;
then |.seqx.|(#)|.seqz*'.| is summable by Lm18;
then |.seqx(#)seqz*'.| is summable by COMSEQ_1:46;
then
A22: seqx(#)seqz*' is absolutely_summable by COMSEQ_3:def 9;
|.seqy.|(#)|.seqz.| is summable by Lm16;
then |.seqy.|(#)|.seqz*'.| is summable by Lm18;
then |.seqy(#)seqz*'.| is summable by COMSEQ_1:46;
then
A23: seqy(#)seqz*' is absolutely_summable by COMSEQ_3:def 9;
A24: (x+y).|.z = Sum(seq_id(x+y)(#)seqz*') by CSSPACE:def 17
.= Sum(seq_id(seqx+seqy)(#)seqz*') by Lm12
.= Sum(seqx(#)seqz*'+seqy(#)seqz*') by COMSEQ_1:10
.= Sum(seqx(#)seqz*')+Sum(seqy(#)seqz*') by A22,A23,COMSEQ_3:54
.=(the scalar of Complex_l2_Space).(x,z)+Sum(seqy(#)seqz*') by
CSSPACE:def 17
.= x.|.z + y.|.z by CSSPACE:def 17;
|.seqx.|(#)|.seqy.| is summable by Lm16;
then |.seqx.|(#)|.seqy*'.| is summable by Lm18;
then |.seqx(#)seqy*'.| is summable by COMSEQ_1:46;
then
A25: seqx(#)seqy*' is absolutely_summable by COMSEQ_3:def 9;
A26: (a*x).|.y =Sum(seq_id(a*x)(#)seqy*') by CSSPACE:def 17
.=Sum(seq_id(a(#)seqx)(#)seqy*') by Lm13
.=Sum(a(#)(seqx(#)seqy*')) by COMSEQ_1:12
.=a*Sum(seqx(#)seqy*') by A25,COMSEQ_3:56
.=a*(x.|.y) by CSSPACE:def 17;
x .|. y = Sum((seqx*')*'(#)seqy*') by CSSPACE:def 17
.= Sum( (seqx*'(#)seqy)*' ) by COMSEQ_2:5
.= (Sum (seqx*'(#)seqy) )*' by A19,Lm5
.=(y .|. x)*' by CSSPACE:def 17;
hence thesis by A4,A13,A2,A3,A16,A20,A24,A26,RSSPACE:16,SERIES_1:18;
end;
registration
cluster Complex_l2_Space -> ComplexUnitarySpace-like;
coherence by Th2,CSSPACE:def 13;
end;
Lm20: for x,y be Complex holds 2*|.x*y.| <= |.x.|^2 + |.y.|^2
proof
let x,y be Complex;
set a = |.x.|;
set b = |.y.|;
(a - b)^2 = a*a - (a*b + a*b) + b*b;
then a*b = |.x*y.| & a*a + b*b - (a*b + a*b) >= 0 by COMPLEX1:65,XREAL_1:63;
hence thesis by XREAL_1:49;
end;
Lm21: for x,y be Complex holds |.x+y.|*|.x+y.| <= 2*|.x.|*|.x.| + 2*|.y.|*|.y
.| & |.x.|*|.x.| <= 2*|.x-y.|*|.x-y.| + 2*|.y.|*|.y.|
proof
A1: now
let x,y be Complex;
A2: |.x*x.| = |.x.|*|.x.| & |.y*y.| = |.y.|*|.y.| by COMPLEX1:65;
|.x*x + x*y + x*y + y*y.| <= |.x*x + x*y + x*y.| + |.y*y.| by COMPLEX1:56;
then
A3: |.x*x + x*y + x*y + y*y.| - |.y*y.| <= |.x*x + x*y + x*y.| by XREAL_1:20;
|.x*x + x*y + x*y.| <= |.x*x + x*y.| + |.x*y.| by COMPLEX1:56;
then
|.x*x + x*y.| <= |.x*x.| + |.x*y.| & |.x*x + x*y + x*y.| - |.x*y.| <=
|.x*x + x*y.| by COMPLEX1:56,XREAL_1:20;
then |.x*x + x*y + x*y.| - |.x*y.| <= |.x*x.| + |.x*y.| by XXREAL_0:2;
then
A4: |.x*x + x*y + x*y.| <= |.x*x.| + |.x*y.| + |.x*y.| by XREAL_1:20;
|.x+y.|*|.x+y.| =|.(x+y)*(x+y).| by COMPLEX1:65
.= |.x*x + x*y + x*y + y*y.|;
then |.x+y.|*|.x+y.| - |.y*y.| <= |.x*x.| + 2*|.x*y.| by A3,A4,XXREAL_0:2;
then
A5: |.x+y.|*|.x+y.| - |.y*y.| - |.x*x.| <= 2*|.x*y.| by XREAL_1:20;
2*|.x*y.| <= |.x.|^2 + |.y.|^2 by Lm20;
then |.x+y.|*|.x+y.| - |.y*y.| - |.x*x.| <= |.x.|^2 + |.y.|^2 by A5,
XXREAL_0:2;
then |.x+y.|*|.x+y.|- |.y.|*|.y.| <= |.x.|*|.x.| + |.y.|*|.y.| + |.x.|*|.
x.| by A2,XREAL_1:20;
then
|.x+y.|*|.x+y.| <= 2*(|.x.|*|.x.|) + |.y.|*|.y.| + |.y.|*|.y.| by XREAL_1:20;
hence |.x+y.|*|.x+y.| <=2*|.x.|*|.x.|+2*|.y.|*|.y.|;
end;
now
let x,y be Complex;
|.(x-y)+y.|=|.x.|;
hence |.x.|*|.x.| <= 2*|.x-y.|*|.x-y.|+2*|.y.|*|.y.| by A1;
end;
hence thesis by A1;
end;
Lm22: for c be Complex, seq be Complex_Sequence st seq is convergent for rseq
be Real_Sequence st (for m be Nat holds rseq .m = |.seq.m-c.|*|.seq.
m-c.|) holds rseq is convergent & lim rseq = |.lim seq-c.|*|.lim seq-c.|
proof
let c be Complex;
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider cseq = NAT --> c1 as Complex_Sequence;
A1: for n be Nat holds cseq.n=c
by ORDINAL1:def 12,FUNCOP_1:7;
then
A2: cseq is convergent by COMSEQ_2:9;
let seq be Complex_Sequence such that
A3: seq is convergent;
reconsider seq1 = seq -cseq as convergent Complex_Sequence by A3,A2;
|.seq1.| is convergent;
then
A4: lim (|.seq -cseq.|(#)|.seq -cseq.|) = (lim |.seq -cseq.|)*(lim |.seq -
cseq.|) by SEQ_2:15
.= |.lim seq - lim cseq.|*(lim |.seq -cseq.|) by A3,A2,SEQ_2:31
.= |.lim seq - lim cseq.|*|.lim seq - lim cseq.| by A3,A2,SEQ_2:31
.= |.lim seq - c.|*|.lim seq - lim cseq.| by A1,COMSEQ_2:10
.= |.lim seq - c.|*|.lim seq - c.| by A1,COMSEQ_2:10;
let rseq be Real_Sequence such that
A5: for i be Nat holds rseq .i = |.seq.i-c.|*|.seq.i-c.|;
now
let i be Nat;
A6: i in NAT by ORDINAL1:def 12;
thus rseq.i=|.seq.i-c.|*|.seq.i-c.| by A5
.=|.seq.i-(cseq.i).|*|.seq.i-c.| by FUNCOP_1:7,A6
.=|.seq.i-(cseq.i).|*|.seq.i-(cseq.i).| by FUNCOP_1:7,A6
.=|.seq.i+(-cseq).i.|*|.seq.i+-(cseq.i).| by VALUED_1:8
.=|.seq.i+(-cseq).i.|*|.seq.i+(-cseq).i.| by VALUED_1:8
.=|.( seq+(-cseq)).i.|*|.seq.i+(-cseq).i.| by VALUED_1:1,A6
.=|. ( seq -cseq ).i.|*|.( seq + (-cseq) ).i.| by VALUED_1:1,A6
.=(|.seq -cseq.| .i)*|.(seq -cseq).i.| by VALUED_1:18
.=(|.seq -cseq.| .i)*(|.seq -cseq.| .i) by VALUED_1:18
.=(|.seq -cseq.|(#)|.seq -cseq.|) .i by SEQ_1:8;
end;
then
A7: for x be object st x in NAT
holds rseq.x =(|.seq -cseq.|(#)|.seq -cseq .|) .x;
|.seq1.|(#)|.seq1.| is convergent;
hence thesis by A7,A4,FUNCT_2:12;
end;
Lm23: for c be Complex, seq1 be Real_Sequence, seq be Complex_Sequence st seq
is convergent & seq1 is convergent for rseq be Real_Sequence st (for i be
Nat holds rseq.i = |.seq.i-c.|*|.seq.i-c.|+seq1.i) holds rseq is
convergent & lim rseq = |.lim seq-c.|*|.lim seq-c.|+lim seq1
proof
let c be Complex;
let seq1 be Real_Sequence;
let seq be Complex_Sequence;
assume that
A1: seq is convergent and
A2: seq1 is convergent;
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider cseq = NAT --> c1 as Complex_Sequence;
A3: for n be Nat holds cseq.n=c
by ORDINAL1:def 12,FUNCOP_1:7;
then
A4: cseq is convergent by COMSEQ_2:9;
then reconsider s = seq-cseq as convergent Complex_Sequence by A1;
A5: |.s.| is convergent;
then
A6: |.seq-cseq.|(#)|.seq-cseq.| is convergent;
let rseq be Real_Sequence such that
A7: for i be Nat holds rseq .i = |.seq.i-c.|*|.seq.i-c.|+seq1 .i;
now
let i be Element of NAT;
thus rseq.i=|.seq.i-c.|*|.seq.i-c.| +seq1.i by A7
.=|.seq.i-cseq.i.|*|.seq.i-c.| +seq1.i by FUNCOP_1:7
.=|.seq.i-cseq.i.|*|.seq.i-cseq.i.| +seq1.i by FUNCOP_1:7
.=|.seq.i+(-cseq).i.|*|.seq.i+-(cseq.i).| +seq1.i by VALUED_1:8
.=|.seq.i+(-cseq).i.|*|.seq.i+(-cseq).i.| +seq1.i by VALUED_1:8
.=|.(seq+(-cseq)).i.|*|.seq.i+(-cseq).i.| +seq1.i by VALUED_1:1
.=|.(seq-cseq).i.|*|.(seq+(-cseq)).i.| +seq1.i by VALUED_1:1
.=(|.seq-cseq.|).i * |.(seq-cseq).i.| +seq1.i by VALUED_1:18
.=(|.seq-cseq.|).i * (|.seq-cseq.|).i +seq1.i by VALUED_1:18
.=(|.seq-cseq.|(#)|.seq-cseq.|).i +seq1.i by SEQ_1:8
.=(|.seq -cseq.|(#)|.seq -cseq.|+seq1).i by SEQ_1:7;
end;
then
A8: rseq = |.seq -cseq.|(#)|.seq-cseq.|+seq1 by FUNCT_2:63;
lim (|.seq-cseq.|(#)|.seq-cseq.|) = (lim (|.seq-cseq.|))*(lim (|.seq-
cseq.|)) by A5,SEQ_2:15
.= (|.(lim seq)-(lim cseq).|)*(lim (|.seq-cseq.|)) by A1,A4,SEQ_2:31
.= (|.(lim seq)-(lim cseq).|)*(|.(lim seq)-(lim cseq).|) by A1,A4,SEQ_2:31
.= (|.(lim seq)-c.|)*(|.(lim seq)-(lim cseq).|) by A3,COMSEQ_2:10
.= (|.(lim seq)-c.|)*(|.(lim seq)-c.|) by A3,COMSEQ_2:10;
hence thesis by A2,A8,A6,SEQ_2:6;
end;
registration
cluster Complex_l2_Space -> complete;
coherence
proof
let vseq be sequence of Complex_l2_Space such that
A1: vseq is Cauchy;
defpred P[object,object] means ex i be Nat st $1=i & ex seqi be
Complex_Sequence st (for n be Nat holds seqi.n=(seq_id(vseq.n)).i) &
seqi is convergent & $2=lim seqi;
A2: for x be object st x in NAT ex y be object st y in COMPLEX & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
deffunc F(set)=(seq_id(vseq.$1)).i;
consider seqi be Complex_Sequence such that
A3: for n be Nat holds seqi.n=F(n) from COMSEQ_1:sch 1;
take lim seqi;
thus lim seqi in COMPLEX by XCMPLX_0:def 2;
now
let e be Real such that
A4: e > 0;
thus ex k be Nat st for m be Nat st k<=m holds |.(
seqi.m -seqi.k).| < e
proof
set e1 = e;
consider k be Nat such that
A5: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n
) - (vseq.m).|| < e1 by A1,A4,CLVECT_2:58;
A6: i in NAT by ORDINAL1:def 12;
now
set vk = vseq.k;
let m be Nat such that
A7: k<=m;
set vm = vseq.m;
||.vm - vk.|| < e by A5,A7;
then
A8: sqrt |.(vm-vk).|.(vm-vk).| < e;
set seqmk = seq_id(vm-vk);
A9: sqrt (|.(seqi.m-seqi.k).|*|.(seqi.m-seqi.k).|) =sqrt ((|.(seqi.
m-seqi.k).|)^2)
.=|.(seqi.m-seqi.k).| by COMPLEX1:46,SQUARE_1:22;
seq_id((vseq.m) - (vseq.k)) =seq_id(seq_id((vseq.m))-seq_id((
vseq.k))) by Lm15
.= seq_id(vseq.m)+-seq_id(vseq.k);
then seqmk.i =(seq_id(vseq.m)).i+(-seq_id(vseq.k)).i by VALUED_1:1,A6
.=(seq_id(vseq.m)).i+(-(seq_id(vseq.k)).i) by VALUED_1:8
.=(seq_id(vseq.m)).i-(seq_id(vseq.k)).i
.=seqi.m -(seq_id(vseq.k)).i by A3
.=seqi.m-seqi.k by A3;
then |.(seqi.m-seqi.k).|*|.(seqi.m-seqi.k).| = (|.seqmk.|).i*|.(
seqmk.i).| by VALUED_1:18
.= (|.seqmk.|).i*(|.seqmk.|).i by VALUED_1:18;
then (|.seqmk.|).i*(|.seqmk*'.|).i =|.(seqi.m-seqi.k).|*|.(seqi.m-
seqi.k).| by Lm18;
then
A10: |.(seqi.m-seqi.k).|*|.(seqi.m-seqi.k).| = (|.seqmk.|(#)|.seqmk
*'.|).i by SEQ_1:8;
0 <= |.(seqi.m-seqi.k).| by COMPLEX1:46;
then
A11: 0 <= |.(seqi.m-seqi.k).|*|.(seqi.m-seqi.k).|;
seqmk(#)seqmk*' is absolutely_summable &
for j be Nat holds (Re( seqmk(#)seqmk*')).j >= 0 &
(Im(seqmk(#)seqmk*')).j = 0 by Lm8,Lm19;
then |.Sum(seqmk(#)seqmk*').| = Sum |.seqmk(#)seqmk*'.| by Lm7
.= Sum(|.seqmk.|(#)|.seqmk*'.|) by COMSEQ_1:46;
then
A12: sqrt Sum(|.seqmk.|(#)|.seqmk*'.|) < e by A8,CSSPACE:def 17;
A13: for i be Nat holds 0 <= (|.seqmk.|(#)|.seqmk*'.|).i
proof
let i be Nat;
(|.seqmk.| (#) |.seqmk*'.|).i =(|.seqmk.|).i * (|.seqmk*'.|).
i by SEQ_1:8
.=(|.seqmk.|).i * (|.seqmk.|).i by Lm18;
hence thesis by XREAL_1:63;
end;
|.seqmk.|(#)|.seqmk.| is summable by CSSPACE:def 11;
then
A14: |.seqmk.|(#)|.seqmk*'.| is summable by Lm18;
then
A15: 0 <= Sum(|.seqmk.|(#)|.seqmk*'.|) by A13,SERIES_1:18;
then 0 <= sqrt Sum(|.seqmk.|(#)|.seqmk*'.|) by SQUARE_1:def 2;
then (sqrt Sum(|.seqmk.|(#)|.seqmk*'.|) )^2 < e1^2 by A12,SQUARE_1:16
;
then
A16: Sum(|.seqmk.|(#)|.seqmk*'.|) < e*e by A15,SQUARE_1:def 2;
(|.seqmk.|(#)|.seqmk*'.|).i <= Sum(|.seqmk.|(#)|.seqmk*'.|) by A14
,A13,RSSPACE2:3;
then
A17: |.(seqi.m-seqi.k).|*|.(seqi.m-seqi.k).| < e*e by A16,A10,XXREAL_0:2;
sqrt (e*e)=sqrt (e1^2) .=e by A4,SQUARE_1:22;
hence |.(seqi.m-seqi.k).| < e by A11,A17,A9,SQUARE_1:27;
end;
hence thesis;
end;
end;
then seqi is convergent by COMSEQ_3:46;
hence thesis by A3;
end;
consider f be sequence of COMPLEX such that
A18: for x be object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A2);
reconsider tseq=f as Complex_Sequence;
set seqt = seq_id(tseq);
A19: now
let i be Nat;
reconsider x=i as set;
i in NAT by ORDINAL1:def 12;
then
ex i0 be Nat st x=i0 & ex seqi be Complex_Sequence st (
for n be Nat holds seqi.n=(seq_id(vseq.n)).i0 ) & seqi is convergent
& f.x=lim seqi by A18;
hence
ex seqi be Complex_Sequence st ( for n be Nat holds seqi.n
=(seq_id(vseq.n)).i ) & seqi is convergent & tseq.i=lim seqi;
end;
A20: for e be Real st e >0
ex k be Nat st for n be Nat
st n >= k holds |.seqt-seq_id(vseq.n).|(#)|.seqt-seq_id(vseq.n).| is summable &
|.Sum((seqt-seq_id(vseq.n))(#)(seqt-seq_id(vseq.n))*').| < e*e
proof
let e1 be Real such that
A21: e1 >0;
set e=e1/2;
A22: e > 0 by A21;
then consider k be Nat such that
A23: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A1,CLVECT_2:58;
e < e1 by A21,XREAL_1:216;
then
A24: e*e < e1*e1 by A22,XREAL_1:97;
A25: for m,n be Nat st n >= k & m >= k holds |.seq_id(vseq.n-
vseq.m).|(#)|.seq_id(vseq.n-vseq.m).| is summable & Sum( |.seq_id(vseq.n-vseq.m
).|(#)|.seq_id(vseq.n-vseq.m).|) < e*e & for i be Nat holds 0 <= (|.
seq_id(vseq.n-vseq.m).|(#)|.seq_id(vseq.n-vseq.m).|).i
proof
let m,n be Nat;
assume n >= k & m >= k;
then ||.(vseq.n) - (vseq.m).|| < e by A23;
then
A26: sqrt |.((vseq.n-vseq.m).|.(vseq.n-vseq.m)).| < e;
seq_id(vseq.n-vseq.m)(#)(seq_id(vseq.n-vseq.m))*' is
absolutely_summable & for j be Nat holds (Re(seq_id(vseq.n-vseq.m)
(#)(seq_id(vseq.n-vseq.m ))*')).j >= 0 & (Im(seq_id(vseq.n-vseq.m)(#)(seq_id(
vseq.n-vseq.m))*')).j = 0 by Lm8,Lm19;
then |.Sum(seq_id(vseq.n-vseq.m) (#)(seq_id(vseq.n-vseq.m))*').| = Sum
|.seq_id(vseq.n-vseq.m) (#)(seq_id(vseq.n-vseq.m))*'.| by Lm7
.= Sum(|.seq_id(vseq.n-vseq.m).| (#)|.(seq_id(vseq.n-vseq.m))*'.|)
by COMSEQ_1:46
.= Sum(|.seq_id(vseq.n-vseq.m).| (#)|.seq_id(vseq.n-vseq.m).|) by Lm18
.= Sum(|.seq_id(vseq.n-vseq.m) (#)seq_id(vseq.n-vseq.m).|) by
COMSEQ_1:46;
then
A27: sqrt ( Sum|.seq_id(vseq.n-vseq.m) (#)seq_id(vseq.n-vseq.m).| ) < e
by A26,CSSPACE:def 17;
A28: for i be Nat holds 0 <= (|.seq_id(vseq.n-vseq.m).|(#)|.
seq_id(vseq.n-vseq.m).|).i
proof
let i be Nat;
(|.seq_id(vseq.n-vseq.m).|(#)|.seq_id(vseq.n-vseq.m).|).i =(|.
seq_id(vseq.n-vseq.m)(#)seq_id(vseq.n-vseq.m).|).i by COMSEQ_1:46
.=|.(seq_id(vseq.n-vseq.m)(#)seq_id(vseq.n-vseq.m)).i .| by
VALUED_1:18;
hence thesis by COMPLEX1:46;
end;
|.seq_id(vseq.n-vseq.m).|(#)|.seq_id(vseq.n-vseq.m).| is summable
by CSSPACE:def 11;
then
0<= Sum (|.seq_id(vseq.n-vseq.m).| (#)|.seq_id(vseq.n-vseq.m).|) by A28,
SERIES_1:18;
then
A29: 0<= Sum |.seq_id(vseq.n-vseq.m) (#)seq_id(vseq.n-vseq.m).| by COMSEQ_1:46
;
then
0 <= sqrt ( Sum|.seq_id(vseq.n-vseq.m) (#)seq_id(vseq.n-vseq.m).| )
by SQUARE_1:def 2;
then
(sqrt ( Sum|.seq_id(vseq.n-vseq.m) (#)seq_id(vseq.n-vseq.m).| ) )^2
< e^2 by A27,SQUARE_1:16;
then Sum|.seq_id(vseq.n-vseq.m)(#)seq_id(vseq.n-vseq.m).| < e*e by A29,
SQUARE_1:def 2;
hence thesis by A28,COMSEQ_1:46,CSSPACE:def 11;
end;
A30: for n,i be Nat holds for rseq be Real_Sequence st ( for m
be Nat holds rseq.m=Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.
seq_id(vseq.m-vseq.n).|).i ) holds rseq is convergent & lim rseq =Partial_Sums(
|.seqt-seq_id(vseq.n).| (#)|.(seqt-seq_id(vseq.n)).|).i
proof
let n be Nat;
defpred P[Nat] means
for rseq be Real_Sequence st (for m be
Nat holds rseq.m=Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(
vseq.m-vseq.n).|).$1 ) holds (rseq is convergent & lim rseq =Partial_Sums(|.
seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n).|).$1);
A31: for m,k be Nat holds seq_id((vseq.m)-(vseq.k))=seq_id(
vseq.m)-seq_id(vseq.k) by Lm15;
now
let i be Nat such that
A32: for rseq be Real_Sequence st ( for m be Nat holds
rseq.m=Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.n).|).i )
holds rseq is convergent & lim rseq =Partial_Sums(|.seqt-seq_id(vseq.n).| (#)|.
seqt-seq_id(vseq.n).|).i;
thus for rseq be Real_Sequence st ( for m be Nat holds rseq
.m=Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.n).|).(i+1) )
holds rseq is convergent & lim rseq =Partial_Sums(|.seqt-seq_id(vseq.n).| (#)|.
seqt-seq_id(vseq.n).| ).(i+1)
proof
deffunc F(Nat)=Partial_Sums(|.seq_id(vseq.$1-vseq.n).|
(#)|.seq_id(vseq.$1-vseq.n).|).i;
consider rseqb be Real_Sequence such that
A33: for m be Nat holds rseqb.m = F(m) from SEQ_1:sch
1;
consider seq0 be Complex_Sequence such that
A34: for m be Nat holds seq0.m=(seq_id(vseq.m)).(i+1) and
A35: seq0 is convergent and
A36: tseq.(i+1)=lim seq0 by A19;
let rseq be Real_Sequence such that
A37: for m be Nat holds rseq.m=Partial_Sums(|.seq_id(
vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.n).|).(i+1);
A38: now
let m be Nat;
thus rseq.m = Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(
vseq.m-vseq.n).|).(i+1) by A37
.= (|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.n).|).(i
+1) + Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.n).|).i
by SERIES_1:def 1
.= ( |.seq_id(vseq.m)-seq_id(vseq.n).| (#)|.seq_id(vseq.m-vseq
.n).|).(i+1) + Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.n
).|).i by A31
.= ( |.seq_id(vseq.m)-seq_id(vseq.n).| (#)|.seq_id(vseq.m-vseq
.n).|).(i+1) + rseqb.m by A33
.= ( |.seq_id(vseq.m)-seq_id(vseq.n).| (#)|.seq_id(vseq.m)-
seq_id(vseq.n).|).(i+1)+rseqb.m by A31
.= ( |.seq_id(vseq.m)+-seq_id(vseq.n).| ).(i+1) * ( |.seq_id(
vseq.m)-seq_id(vseq.n).| ).(i+1) +rseqb.m by SEQ_1:8
.= |.(seq_id(vseq.m)+-seq_id(vseq.n)).(i+1).| * ( |.seq_id(
vseq.m)+-seq_id(vseq.n).| ).(i+1) +rseqb.m by VALUED_1:18
.= |.(seq_id(vseq.m)+-seq_id(vseq.n)).(i+1).| * |.(seq_id(vseq
.m)+-seq_id(vseq.n)).(i+1).| +rseqb.m by VALUED_1:18
.= |.(seq_id(vseq.m)).(i+1)+(-seq_id(vseq.n)).(i+1).| * |.(
seq_id(vseq.m)+-seq_id(vseq.n)).(i+1).| +rseqb.m by VALUED_1:1
.= |.(seq_id(vseq.m)).(i+1)+(-seq_id(vseq.n)).(i+1).| * |.(
seq_id(vseq.m)).(i+1)+(-seq_id(vseq.n)).(i+1).| +rseqb.m by VALUED_1:1
.= |.(seq_id(vseq.m)).(i+1)+-(seq_id(vseq.n)).(i+1).| * |.(
seq_id(vseq.m)).(i+1)+(-seq_id(vseq.n)).(i+1).| +rseqb.m by VALUED_1:8
.= |.(seq_id(vseq.m)).(i+1)-(seq_id(vseq.n)).(i+1).| * |.(
seq_id(vseq.m)).(i+1)+-(seq_id(vseq.n)).(i+1).| +rseqb.m by VALUED_1:8
.= |.seq0.m-(seq_id(vseq.n)).(i+1).| * |.(seq_id(vseq.m)).(i+1
)-(seq_id(vseq.n)).(i+1).| +rseqb.m by A34
.= |.seq0.m-(seq_id(vseq.n)).(i+1).| * |.seq0.m-(seq_id(vseq.n
)).(i+1).| +rseqb.m by A34;
end;
A39: rseqb is convergent by A32,A33;
then
lim rseq = |. lim seq0-(seq_id(vseq.n)).(i+1) .| * |. lim seq0-
(seq_id(vseq.n)).(i+1) .| + lim rseqb by A35,A38,Lm23
.= |. tseq.(i+1)+(-seq_id(vseq.n)).(i+1) .| * |. tseq.(i+1)+-(
seq_id(vseq.n)).(i+1) .| + lim rseqb by A36,VALUED_1:8
.= |. tseq.(i+1)+(-seq_id(vseq.n)).(i+1) .| * |. tseq.(i+1)+(-
seq_id(vseq.n)).(i+1) .| + lim rseqb by VALUED_1:8
.= |.(tseq+(-seq_id(vseq.n))).(i+1).| * |. tseq.(i+1)+(-seq_id(
vseq.n)).(i+1) .| + lim rseqb by VALUED_1:1
.= |.(tseq+(-seq_id(vseq.n))).(i+1).| * |.(tseq+(-seq_id(vseq.n)
)).(i+1).| + lim rseqb by VALUED_1:1
.= (|.tseq+(-seq_id(vseq.n)).|).(i+1) * |.(tseq+(-seq_id(vseq.n)
)).(i+1).| + lim rseqb by VALUED_1:18
.= (|.tseq-seq_id(vseq.n).|).(i+1) * (|.tseq+(-seq_id(vseq.n)).|
).(i+1) + lim rseqb by VALUED_1:18
.= ( |.tseq-seq_id(vseq.n).|(#)|.tseq-seq_id(vseq.n).|).(i+1) +
lim rseqb by SEQ_1:8
.= ( |.tseq-seq_id(vseq.n).|(#)|.tseq-seq_id(vseq.n).|).(i+1) +
Partial_Sums(|.seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n).| ).i by A32,A33
.= Partial_Sums(|.seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n)
.|).(i+1) by SERIES_1:def 1;
hence thesis by A39,A35,A38,Lm23;
end;
end;
then
A40: for i be Nat st P[i] holds P[i+1];
now
let rseq be Real_Sequence such that
A41: for m be Nat holds rseq.m=Partial_Sums(|.seq_id(
vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.n).|).0;
thus rseq is convergent & lim rseq =Partial_Sums(|.seqt-seq_id(vseq.n)
.| (#)|.seqt-seq_id(vseq.n).| ).0
proof
consider rseq0 be Complex_Sequence such that
A42: for m be Nat holds rseq0.m=(seq_id(vseq.m)).0 and
A43: rseq0 is convergent and
A44: tseq.0=lim rseq0 by A19;
A45: now
let m be Nat;
thus rseq.m=Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(
vseq.m-vseq.n).|).0 by A41
.=(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.n).|).0
by SERIES_1:def 1
.=(|.seq_id(vseq.m)-seq_id(vseq.n).| (#)|.seq_id(vseq.m-vseq.n
).|).0 by A31
.=(|.seq_id(vseq.m)-seq_id(vseq.n).| (#)|.seq_id(vseq.m)-
seq_id(vseq.n).|).0 by A31
.=(|.seq_id(vseq.m)+-seq_id(vseq.n).|).0 * (|.seq_id(vseq.m)-
seq_id(vseq.n).| ).0 by SEQ_1:8
.=|.(seq_id(vseq.m)+(-seq_id(vseq.n))).0 .| * (|.seq_id(vseq.m
)+-seq_id(vseq.n).|).0 by VALUED_1:18
.=|.(seq_id(vseq.m)+(-seq_id(vseq.n))).0 .| * |.(seq_id(vseq.m
)+(-seq_id(vseq.n))).0 .| by VALUED_1:18
.=|.(seq_id(vseq.m)).0+(-seq_id(vseq.n)).0 .| * |.(seq_id(vseq
.m)+(-seq_id(vseq.n))).0 .| by VALUED_1:1
.=|.(seq_id(vseq.m)).0+(-seq_id(vseq.n)).0 .| * |.(seq_id(vseq
.m)).0+(-seq_id(vseq.n)).0 .| by VALUED_1:1
.=|.(seq_id(vseq.m)).0+-(seq_id(vseq.n)).0 .| * |.(seq_id(vseq
.m)).0+(-seq_id(vseq.n)).0 .| by VALUED_1:8
.=|.(seq_id(vseq.m)).0+-(seq_id(vseq.n)).0 .| * |.(seq_id(vseq
.m)).0+-(seq_id(vseq.n)).0 .| by VALUED_1:8
.=|.rseq0.m-(seq_id(vseq.n)).0 .| * |.(seq_id(vseq.m)).0-(
seq_id(vseq.n)).0 .| by A42
.=|.rseq0.m-(seq_id(vseq.n)).0 .| * |.rseq0.m-(seq_id(vseq.n))
.0 .| by A42;
end;
then lim rseq = |.tseq.0-(seq_id(vseq.n)).0 .| * |.tseq.0-(seq_id(
vseq.n)).0 .| by A43,A44,Lm22
.= |.tseq.0+(-seq_id(vseq.n)).0 .| * |.tseq.0+-(seq_id(vseq.n)).
0 .| by VALUED_1:8
.= |.tseq.0+(-seq_id(vseq.n)).0 .| * |.tseq.0+(-seq_id(vseq.n)).
0 .| by VALUED_1:8
.= |.(tseq+(-seq_id(vseq.n))).0 .| * |.tseq.0+(-seq_id(vseq.n)).
0 .| by VALUED_1:1
.= |.(tseq-seq_id(vseq.n)).0 .| * |.(tseq+(-seq_id(vseq.n))).0
.| by VALUED_1:1
.= (|.tseq-seq_id(vseq.n).|).0 * |.(tseq-seq_id(vseq.n)).0 .| by
VALUED_1:18
.= (|.tseq-seq_id(vseq.n).|).0 * (|.tseq-seq_id(vseq.n).|).0 by
VALUED_1:18
.= (|.tseq-seq_id(vseq.n).| (#)|.tseq-seq_id(vseq.n).|).0 by
SEQ_1:8
.=Partial_Sums(|.seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n)
.|).0 by SERIES_1:def 1;
hence thesis by A43,A45,Lm22;
end;
end;
then
A46: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A46,A40);
hence thesis;
end;
for n be Nat st n >= k holds |.seqt-seq_id(vseq.n).|(#)|.
seqt-seq_id(vseq.n).| is summable & |.Sum((seqt-seq_id(vseq.n))(#)(seqt-seq_id(
vseq.n))*').| < e1*e1
proof
let n be Nat such that
A47: n >= k;
A48: for i be Nat st 0 <= i holds Partial_Sums(|.seqt-seq_id(
vseq.n).| (#)|.seqt-seq_id(vseq.n).| ).i <=e*e
proof
let i be Nat such that
0 <=i;
deffunc F(Nat) = Partial_Sums(|.(seq_id(vseq.$1 - vseq.n))
.| (#)|.(seq_id(vseq.$1 - vseq.n)).|).i;
consider rseq be Real_Sequence such that
A49: for m be Nat holds rseq.m=F(m) from SEQ_1:sch 1;
A50: for m be Nat st m >= k holds rseq.m <= e*e
proof
let m be Nat such that
A51: m >= k;
|.seq_id(vseq.m-vseq.n).|(#)|.seq_id(vseq.m-vseq.n).| is
summable & for i be Nat holds 0 <= (|.seq_id(vseq.m-vseq.n).|(#)|.
seq_id(vseq.m-vseq.n) .| ).i by A25,A47,A51;
then
A52: Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(vseq.m-vseq.
n).|).i <=Sum(|.seq_id(vseq.m-vseq.n).|(#)|.seq_id(vseq.m-vseq.n).|) by
RSSPACE2:3;
A53: rseq.m=Partial_Sums(|.seq_id(vseq.m-vseq.n).| (#)|.seq_id(vseq.
m-vseq.n).|).i by A49;
Sum(|.seq_id(vseq.m-vseq.n).|(#)|.seq_id(vseq.m-vseq.n).|) < e*
e by A25,A47,A51;
hence thesis by A53,A52,XXREAL_0:2;
end;
rseq is convergent & lim rseq = Partial_Sums(|.seqt-seq_id(vseq.n
).| (#)|. seqt-seq_id(vseq.n).| ).i by A30,A49;
hence thesis by A50,RSSPACE2:5;
end;
now
let i be Nat;
Partial_Sums(|.seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n).| )
.i <=e*e by A48;
hence
Partial_Sums(|.seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n).| )
.i < e1*e1 by A24,XXREAL_0:2;
end;
then
A54: Partial_Sums(|.seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n).| )
is bounded_above by SEQ_2:def 3;
A55: for i be Nat holds 0 <= ( |.seqt-seq_id(vseq.n).|(#)|.
seqt-seq_id(vseq.n).|) .i
proof
let i be Nat;
(|.seqt-seq_id(vseq.n).|(#)|.seqt-seq_id(vseq.n).|).i =(|.seqt-
seq_id(vseq.n).|).i *(|.seqt-seq_id(vseq.n).|).i by SEQ_1:8;
hence thesis by XREAL_1:63;
end;
then
A56: |.seqt-seq_id(vseq.n).|(#)|.seqt-seq_id(vseq.n).| is summable by A54,
SERIES_1:17;
then Partial_Sums( |.seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n).| )
is convergent by SERIES_1:def 2;
then Sum(|.seqt-seq_id(vseq.n).|(#)|.seqt-seq_id(vseq.n).|) = lim
Partial_Sums( |. seqt-seq_id(vseq.n).| (#)|.seqt-seq_id(vseq.n).| ) & lim
Partial_Sums(|.seqt- seq_id(vseq.n).|(#)|.seqt-seq_id(vseq.n).|) <=e*e by A48,
RSSPACE2:5,SERIES_1:def 3;
then
A57: Sum(|.seqt-seq_id(vseq.n).|(#)|.seqt-seq_id(vseq.n).|) < e1*e1 by A24,
XXREAL_0:2;
|.seqt-seq_id(vseq.n).|(#)|.(seqt-seq_id(vseq.n))*'.| is summable
by A56,Lm18;
then |.(seqt-seq_id(vseq.n))(#)(seqt-seq_id(vseq.n))*'.| is summable by
COMSEQ_1:46;
then (seqt-seq_id(vseq.n))(#)(seqt-seq_id(vseq.n))*' is
absolutely_summable by COMSEQ_3:def 9;
then
A58: |.Sum((seqt-seq_id(vseq.n))(#)(seqt-seq_id(vseq.n))*').| <= Sum(|.
(seqt-seq_id(vseq.n))(#)(seqt-seq_id(vseq.n))*'.|) by Lm6;
|.seqt-seq_id(vseq.n).| = |.(seqt-seq_id(vseq.n))*'.| by Lm18;
then Sum(|.(seqt-seq_id(vseq.n))(#)(seqt-seq_id(vseq.n))*'.|) < e1* e1
by A57,COMSEQ_1:46;
hence thesis by A55,A54,A58,SERIES_1:17,XXREAL_0:2;
end;
hence thesis;
end;
A59: |.seq_id(tseq).|(#)|.seq_id(tseq).| is summable
proof
set d=|.seqt.|(#)|.seqt.|;
A60: for i be Nat holds 0 <= (|.seq_id(tseq).|(#)|.seq_id(tseq
).|).i
proof
let i be Nat;
(|.seq_id(tseq).|(#)|.seq_id(tseq).|).i =(|.seq_id(tseq).|).i * (
|.seq_id(tseq).|).i by SEQ_1:8;
hence thesis by XREAL_1:63;
end;
consider m be Nat such that
A61: for n be Nat st n >= m holds |.seqt-seq_id(vseq.n).|
(#)|.seqt-seq_id(vseq.n).| is summable & |.Sum((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n))*').| < 1*1 by A20;
set b=|.seq_id(vseq.m).|(#)|.seq_id(vseq.m).|;
set a=|.seqt-seq_id(vseq.m).|(#)|.seqt-seq_id(vseq.m).|;
|.seq_id(vseq.m).|(#)|.seq_id(vseq.m).| is summable by CSSPACE:def 11;
then
A62: 2(#)b is summable by SERIES_1:10;
A63: for i be Nat holds d.i <= (2(#)a + 2(#)b).i
proof
let i be Nat;
A64: i in NAT by ORDINAL1:def 12;
A65: (2(#)a + 2(#)b).i = (2(#)a).i + (2(#)b).i by SEQ_1:7
.=2*(a.i)+ (2(#)b).i by SEQ_1:9
.=2*(a.i)+ 2*(b.i) by SEQ_1:9;
set y=(seq_id(vseq.m)).i;
set x=(seqt).i;
A66: 2*(b.i)=2*( (|.seq_id(vseq.m).|).i*(|.seq_id(vseq.m).|).i ) by SEQ_1:8
.=2*(|.y.|*(|.seq_id(vseq.m).|).i) by VALUED_1:18
.=2*(|.y.|*|.y.|) by VALUED_1:18
.=2*|.y.|*|.y.|;
(|.seqt-seq_id(vseq.m).|).i = |.((seqt+-seq_id(vseq.m)).i).| by
VALUED_1:18
.= |.((seqt).i+(-seq_id(vseq.m)).i).| by VALUED_1:1,A64
.= |.((seqt).i+(-(seq_id(vseq.m)).i)).| by VALUED_1:8
.= |.((seqt).i-(seq_id(vseq.m)).i).|;
then a.i = |.((seqt).i-(seq_id(vseq.m)).i).| *|.((seq_id(tseq)).i-(
seq_id(vseq.m)).i).| by SEQ_1:8;
then
A67: 2*(a.i)=2*|.(x-y).|*|.(x-y).|;
d.i=(|.seqt.|).i * (|.seqt.|).i by SEQ_1:8
.=|.((seqt).i).| * (|.seqt.|).i by VALUED_1:18
.=|.((seqt).i).| * |.((seqt).i).| by VALUED_1:18;
hence thesis by A65,A67,A66,Lm21;
end;
|.seqt-seq_id(vseq.m).|(#)|.seqt-seq_id(vseq.m).| is summable by A61;
then 2(#)a is summable by SERIES_1:10;
then 2(#)a + 2(#)b is summable by A62,SERIES_1:7;
hence thesis by A60,A63,SERIES_1:20;
end;
tseq in the_set_of_ComplexSequences by FUNCT_2:8;
then reconsider tv=tseq as Point of Complex_l2_Space by A59,CSSPACE:def 11;
for e be Real st e > 0 ex m be Nat st
for n be Nat st n >= m holds ||.(vseq.n) - tv.|| < e
proof
let e be Real such that
A68: e > 0;
consider m be Nat such that
A69: for n be Nat st n >= m holds |.seqt-seq_id(vseq.n).|
(#)|.seqt-seq_id(vseq.n).| is summable & |.Sum((seqt-(seq_id(vseq.n)))(#)(seqt-
(seq_id(vseq.n)))*').| < e*e by A20,A68;
now
tseq in the_set_of_ComplexSequences by FUNCT_2:8;
then reconsider u=tseq as VECTOR of Complex_l2_Space by A59,
CSSPACE:def 11;
let n be Nat such that
A70: n >= m;
reconsider v=vseq.n as VECTOR of Complex_l2_Space;
set seqvn = seq_id(vseq.n);
0 <= Re ((u-v).|.(u-v)) by CSSPACE:def 13;
then
A71: 0 <= |.((u-v).|.(u-v)).| by CSSPACE:34;
A72: seq_id(u-v)=seqt-seqvn by Lm15;
|.Sum((seqt-seqvn)(#)(seqt-seqvn)*').| < e*e by A69,A70;
then |.((u-v).|.(u-v)).| < e*e by A72,CSSPACE:def 17;
then
A73: sqrt |.((u-v).|.(u-v)).| < sqrt (e^2) by A71,SQUARE_1:27;
||.(vseq.n) - tv.|| =||.-(tv-(vseq.n)).|| by RLVECT_1:33
.=||.tv-(vseq.n).|| by CSSPACE:47
.=sqrt |.((u-v).|.(u-v)).|;
hence ||.(vseq.n) - tv.|| < e by A68,A73,SQUARE_1:22;
end;
hence thesis;
end;
hence thesis by CLVECT_2:9;
end;
end;
registration
cluster complete for ComplexUnitarySpace;
existence
proof
take Complex_l2_Space;
thus thesis;
end;
end;
definition
mode ComplexHilbertSpace is complete ComplexUnitarySpace;
end;
begin :: Some corollaries of complex sequences
theorem
for z1, z2 be Complex st (Re z1)*(Im z2) = (Re z2)*(Im z1) & (Re z1)*(
Re z2)+(Im z1)*(Im z2) >= 0 holds |.z1 + z2.| = |.z1.| + |.z2.| by Lm3;
theorem
for x,y be Complex holds 2*|.x*y.| <= |.x.|^2 + |.y.|^2 by Lm20;
theorem
for x,y be Complex holds |.x+y.|*|.x+y.| <= 2*|.x.|*|.x.| + 2*|.y.|*|.
y.| & |.x.|*|.x.| <= 2*|.x-y.|*|.x-y.| + 2*|.y.|*|.y.| by Lm21;
::$CT
theorem
for seq be Complex_Sequence holds Partial_Sums (seq*') = (Partial_Sums
seq) *' by Lm1;
theorem
for seq be Complex_Sequence, n be Nat st
(for i be Nat holds (Re seq).i >= 0 & (Im seq).i = 0)
holds (|.Partial_Sums seq.|).n = (Partial_Sums |.seq.|).n by Lm4;
theorem
for seq be Complex_Sequence st seq is summable holds Sum (seq*') = (
Sum seq)*' by Lm5;
theorem
for seq be Complex_Sequence st seq is absolutely_summable holds |. Sum
seq .| <= Sum |.seq.| by Lm6;
theorem
for seq be Complex_Sequence st seq is summable &
(for n be Nat holds (Re seq).n >= 0 & (Im seq).n = 0)
holds |. Sum seq .| = Sum |.seq.|
by Lm7;
theorem
for seq be Complex_Sequence, n be Nat holds (Re (seq(#)seq
*')).n >= 0 & (Im (seq(#)seq*')).n = 0 by Lm8;
theorem
for seq be Complex_Sequence st seq is absolutely_summable & Sum |.seq
.|=0 holds for n be Nat holds seq.n =0c
proof
let seq be Complex_Sequence such that
A1: seq is absolutely_summable and
A2: Sum |.seq.|=0;
A3: for n be Nat holds (Partial_Sums |.seq.|).n <= Sum |.seq.|
proof
let n be Nat;
(Partial_Sums(|.seq.|)).n <= lim Partial_Sums |.seq.| by A1,SEQ_4:37;
hence thesis by SERIES_1:def 3;
end;
A4: now
assume ex n be Nat st (|.seq.|).n <> 0;
then consider n1 be Nat such that
A5: (|.seq.|).n1 <> 0;
A6: for n be Nat holds 0 <= Partial_Sums(|.seq.|).n
proof
let n be Nat;
(|.seq.|).0 = |.(seq.0).| by VALUED_1:18;
then
A7: 0 <=(|.seq.|).0 by COMPLEX1:46;
n=n+0 & Partial_Sums(|.seq.|).0 = (|.seq.|).0 by SERIES_1:def 1;
hence thesis by A7,SEQM_3:5;
end;
Partial_Sums(|.seq.|).n1 >0
proof
now
per cases;
case
n1=0;
then Partial_Sums(|.seq.|).(n1) <> 0 by A5,SERIES_1:def 1;
hence thesis by A6;
end;
case
A8: n1<>0;
set nn=n1-1;
(|.seq.|).n1 = |.(seq.n1).| by VALUED_1:18;
then
A9: nn+1 =n1 & 0 <= (|.seq.|).n1 by COMPLEX1:46;
0 + 1 <= n1 by A8,INT_1:7;
then
A10: nn in NAT by INT_1:5;
then 0 <= Partial_Sums(|.seq.|).nn by A6;
then (|.seq.|).(n1)+0 <= (|.seq.|).(n1)+Partial_Sums(|.seq.|).nn by
XREAL_1:7;
hence thesis by A5,A10,A9,SERIES_1:def 1;
end;
end;
hence thesis;
end;
hence contradiction by A2,A3;
end;
for n be Nat holds seq.n =0c
proof
let n be Nat;
0 = (|.seq.|).n by A4
.= |.(seq.n).| by VALUED_1:18;
hence thesis by COMPLEX1:45;
end;
hence thesis;
end;
theorem
for seq being Complex_Sequence holds |.seq.| = |.seq*'.| by Lm18;
theorem
for c be Complex, seq be Complex_Sequence st seq is convergent for
rseq be Real_Sequence st (for m be Nat holds rseq .m = |.seq.m-c.|*
|.seq.m-c.|) holds rseq is convergent & lim rseq = |.lim seq-c.|*|.lim seq-c.|
by Lm22;
theorem
for c be Complex, seq1 be Real_Sequence, seq be Complex_Sequence st
seq is convergent & seq1 is convergent for rseq be Real_Sequence st (for i be
Nat holds rseq.i = |.seq.i-c.|*|.seq.i-c.|+seq1.i) holds rseq is
convergent & lim rseq = |.lim seq-c.|*|.lim seq-c.|+lim seq1 by Lm23;