Copyright (c) 2003 Association of Mizar Users
environ
vocabulary PRE_TOPC, NORMSP_1, RLVECT_1, FUNCT_1, ARYTM, ARYTM_1, ARYTM_3,
RELAT_1, ABSVALUE, ORDINAL2, SQUARE_1, PROB_1, SEQ_1, SEQ_2, SEQM_3,
SERIES_1, PROB_2, BHSP_1, BHSP_3, SUPINF_2, RSSPACE;
notation TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, STRUCT_0,
XREAL_0, REAL_1, NAT_1, RELAT_1, PARTFUN1, FUNCT_1, FUNCT_2, PRE_TOPC,
RLVECT_1, ABSVALUE, NORMSP_1, BHSP_1, BHSP_2, BHSP_3, SQUARE_1, SEQ_1,
SEQ_2, SEQM_3, SERIES_1, RSSPACE;
constructors REAL_1, NAT_1, DOMAIN_1, SQUARE_1, SEQ_2, SERIES_1, PREPOWER,
PARTFUN1, RLSUB_1, BHSP_2, BHSP_3, RSSPACE, MEMBERED;
clusters RELSET_1, XREAL_0, STRUCT_0, SEQ_1, RSSPACE, MEMBERED, NUMBERS,
ORDINAL2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
theorems XCMPLX_0, RELAT_1, SQUARE_1, AXIOMS, ABSVALUE, ZFMISC_1, REAL_1,
SEQ_1, SEQ_2, SEQM_3, SERIES_1, INT_1, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1,
RLSUB_1, BHSP_1, BHSP_2, BHSP_3, SEQ_4, RSSPACE, XREAL_0, XCMPLX_1;
schemes NAT_1, SEQ_1, FUNCT_2;
begin :: Hilbert Space of Real Sequences
theorem Th1:
( the carrier of l2_Space = the_set_of_l2RealSequences) &
(for x be set holds x is Element of l2_Space
iff x is Real_Sequence & seq_id(x)(#)seq_id(x) is summable) &
(for x be set holds x is VECTOR of l2_Space
iff x is Real_Sequence & seq_id(x)(#)seq_id(x) is summable) &
0.l2_Space = Zeroseq &
(for u be VECTOR of l2_Space holds u =seq_id(u)) &
(for u,v be VECTOR of l2_Space holds u+v =seq_id(u)+seq_id(v)) &
(for r be Real for u be VECTOR of l2_Space holds r*u =r(#)seq_id(u)) &
(for u be VECTOR of l2_Space holds -u =-seq_id(u) & seq_id(-u)=-seq_id(u)) &
(for u,v be VECTOR of l2_Space holds u-v =seq_id(u)-seq_id(v)) &
for v,w be VECTOR of l2_Space holds seq_id(v)(#)seq_id(w) is summable &
for v,w be VECTOR of l2_Space holds v.|.w = Sum(seq_id(v)(#)seq_id(w))
proof
A1:for x be set holds x is Element of l2_Space
iff x is Real_Sequence & seq_id(x)(#)seq_id(x) is summable
proof
let x be set;
x in the_set_of_RealSequences iff x is Real_Sequence by RSSPACE:def 1;
hence thesis by RSSPACE:def 11,def 13;
end;
A2:for u be VECTOR of l2_Space holds u =seq_id u
proof
let u be VECTOR of l2_Space;
u is VECTOR of Linear_Space_of_RealSequences
by RLSUB_1:18,RSSPACE:15,def 13;
hence thesis by RSSPACE:17;
end;
A3:for u,v be VECTOR of l2_Space holds u+v =seq_id(u)+seq_id(v)
proof
let u,v be VECTOR of l2_Space;
reconsider u1=u,v1=v as VECTOR of Linear_Space_of_RealSequences
by RLSUB_1:18,RSSPACE:15,def 13;
set L1 = Linear_Space_of_RealSequences;
set W = the_set_of_l2RealSequences;
A4: [:W,W:] c= [:the carrier of L1,the carrier of L1:] by ZFMISC_1:119;
dom (the add of L1)
= [:the carrier of L1,the carrier of L1:] by FUNCT_2:def 1;
then dom ((the add of Linear_Space_of_RealSequences) | [:W,W:])
=[:W,W:] by A4,RELAT_1:91;
then A5: [u,v] in dom ((the add of Linear_Space_of_RealSequences)|[:W,W:])
by RSSPACE:def 13,ZFMISC_1:106;
u+v =(the add of l2_Space).[u,v] by RLVECT_1:def 3
.=((the add of Linear_Space_of_RealSequences)|[:W,W:]).[u,v]
by RSSPACE:14,def 8,def 13
.=(the add of Linear_Space_of_RealSequences).[u,v]
by A5,FUNCT_1:70
.=u1+v1 by RLVECT_1:def 3;
hence thesis by RSSPACE:17;
end;
A6:for r be Real for u be VECTOR of l2_Space holds r*u =r(#)seq_id(u)
proof
let r be Real;
let u be VECTOR of l2_Space;
reconsider u1=u as VECTOR of Linear_Space_of_RealSequences
by RLSUB_1:18,RSSPACE:15,def 13;
set L1=Linear_Space_of_RealSequences;
set W = the_set_of_l2RealSequences;
A7: [:REAL,W:] c= [:REAL,the carrier of L1:] by ZFMISC_1:119;
dom (the Mult of L1) = [:REAL,the carrier of L1:] by FUNCT_2:def 1;
then dom ((the Mult of Linear_Space_of_RealSequences) | [:REAL,W:])
=[:REAL,W:] by A7,RELAT_1:91;
then A8: [r,u] in dom ((the Mult of Linear_Space_of_RealSequences)|[:REAL,W:])
by RSSPACE:def 13,ZFMISC_1:106;
r*u =(the Mult of l2_Space).[r,u] by RLVECT_1:def 4
.=((the Mult of Linear_Space_of_RealSequences)|[:REAL,W:]).[r,u]
by RSSPACE:14,def 9,def 13
.=(the Mult of Linear_Space_of_RealSequences).[r,u]
by A8,FUNCT_1:70
.=r*u1 by RLVECT_1:def 4;
hence thesis by RSSPACE:17;
end;
A9:for u be VECTOR of l2_Space holds (-u =-seq_id(u) & seq_id(-u)=-seq_id(u))
proof
let u be VECTOR of l2_Space;
-u = (-1)*u by RLVECT_1:29
.= (-1)(#)seq_id(u) by A6
.= -seq_id(u) by SEQ_1:25;
hence thesis by A2;
end;
A10:for u,v be VECTOR of l2_Space holds u-v =seq_id(u)-seq_id(v)
proof
let u,v be VECTOR of l2_Space;
thus u-v = u+(-v) by RLVECT_1:def 11
.= seq_id(u)+seq_id(-v) by A3
.= seq_id(u)+(-seq_id(v)) by A9
.= seq_id(u)-seq_id(v) by SEQ_1:15;
end;
A11:0.l2_Space = Zeroseq
proof
set W = the_set_of_l2RealSequences;
thus 0.l2_Space = Zero_(W,Linear_Space_of_RealSequences)
by RLVECT_1:def 2,RSSPACE:def 13
.= 0.Linear_Space_of_RealSequences by RSSPACE:14,def 10
.= Zeroseq by RLVECT_1:def 2,RSSPACE:def 7;
end;
A12:for u,v be VECTOR of l2_Space holds seq_id(u)(#)seq_id(v) is summable
proof
let u,v be VECTOR of l2_Space;
A13:(seq_id(v))(#)(seq_id(v)) is summable by RSSPACE:def 11,def 13;
A14:(seq_id(u))(#)(seq_id(u)) is summable by RSSPACE:def 11,def 13;
set p = (seq_id(v))(#)(seq_id(v));
set q = (seq_id(u))(#)(seq_id(u));
set r = abs( (seq_id(u))(#)(seq_id(v)));
A15:p+q is summable by A13,A14,SERIES_1:10;
A16:for n be Nat holds 0<=(2(#)r).n
proof
let n be Nat;
set rr=(seq_id(u))(#)(seq_id(v));
A17: (2(#)r).n = 2*r.n by SEQ_1:13
.= 2*abs(rr.n) by SEQ_1:16;
reconsider tt=abs(rr.n) as Real;
0 <= 2 & 0 <= tt by ABSVALUE:5;
hence thesis by A17,SQUARE_1:19;
end;
for n be Nat holds (2(#)r).n <=(p+q).n
proof
let n be Nat;
set s = seq_id v, t = seq_id u;
reconsider sn=s.n,tn=t.n as Real;
reconsider ss=abs sn,tt=abs tn as Real;
A18: (2(#)r).n =2*r.n by SEQ_1:13
.=2*abs( ((seq_id(u))(#)(seq_id(v))).n ) by SEQ_1:16
.=2*(abs((seq_id(u)).n * (seq_id(v)).n)) by SEQ_1:12
.= 2*(ss*tt) by ABSVALUE:10
.= 2*abs(sn)*abs(tn) by XCMPLX_1:4;
(p+q).n = p.n +q.n by SEQ_1:11
.= (s.n*s.n) + q.n by SEQ_1:12
.= (s.n*s.n) + (t.n*t.n) by SEQ_1:12
.= sn^2 + (t.n*t.n) by SQUARE_1:def 3
.= sn^2 + tn^2 by SQUARE_1:def 3
.=(abs(sn))^2 + tn^2 by SQUARE_1:62
.=(abs(sn))^2 + (abs(tn))^2 by SQUARE_1:62;
then A19: (p+q).n - (2(#)r).n
= (abs(sn))^2 - 2*abs(sn)*abs(tn) + (abs(tn))^2 by A18,XCMPLX_1:29
.= (abs(sn)-abs(tn))^2 by SQUARE_1:64;
0 <= (abs(sn)-abs(tn))^2 by SQUARE_1:72;
then 0 + (2(#)r).n <= (p+q).n - (2(#)r).n + (2(#)r).n by A19,REAL_1:55
;
then (2(#)r).n <= (p+q).n - ((2(#)r).n - (2(#)r).n) by XCMPLX_1:37;
hence thesis by XCMPLX_1:17;
end;
then A20: 2(#)r is summable by A15,A16,SERIES_1:24;
set q0 = 1/2;
q0(#)(2(#)r)=(q0*2)(#)r by SEQ_1:31 .=r by SEQ_1:35;
then r is summable by A20,SERIES_1:13;
then (seq_id(u))(#)(seq_id(v)) is absolutely_summable by SERIES_1:def 5;
hence thesis by SERIES_1:40;
end;
for v,w be VECTOR of l2_Space holds v.|.w = Sum(seq_id(v)(#)seq_id(w))
proof
let v,w be VECTOR of l2_Space;
thus v.|.w = (the scalar of l2_Space).[v,w] by BHSP_1:def 1
.= Sum(seq_id(v)(#)seq_id(w)) by RSSPACE:def 12,def 13;
end;
hence thesis by A1,A2,A3,A6,A9,A10,A11,A12,RSSPACE:def 13;
end;
theorem Th2:
for x, y, z being Point of l2_Space for a be Real holds
( x .|. x = 0 iff x = 0.l2_Space ) &
0 <= x .|. x &
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 l2_Space;
let a be Real;
A1:now assume
A2: x .|. x = 0;
A3: x .|. x = (the scalar of l2_Space).[x,x] by BHSP_1:def 1
.= Sum(seq_id(x)(#)seq_id(x)) by RSSPACE:def 12,def 13;
A4: for n be Nat holds 0 <= (seq_id(x)(#)seq_id(x)).n
proof
let n be Nat;
(seq_id(x)(#)seq_id(x)).n
=(seq_id(x)).n * (seq_id(x)).n by SEQ_1:12;
hence thesis by REAL_1:93;
end;
A5: seq_id(x)(#)seq_id(x) is summable by Th1;
A6: for n be Nat holds 0 = (seq_id(x)).n
proof
let n be Nat;
0 = (seq_id(x)(#)seq_id(x)).n by A2,A3,A4,A5,RSSPACE:21
.= ((seq_id(x)).n)*((seq_id(x)).n) by SEQ_1:12;
hence thesis by XCMPLX_1:6;
end;
x is Element of the_set_of_RealSequences by RSSPACE:def 11,def 13;
hence x=0.l2_Space by A6,Th1,RSSPACE:def 6;
end;
A7:now assume
A8:x=0.l2_Space;
A9: 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 SEQ_1:12
.=(seq_id(x)).n * 0 by A8,Th1,RSSPACE:def 6
.= 0;
end;
thus x .|. x = (the scalar of l2_Space).[x,x] by BHSP_1:def 1
.= Sum(seq_id(x)(#)seq_id(x)) by RSSPACE:def 12,def 13
.=0 by A9,RSSPACE:20;
end;
A10:for n be Nat holds 0 <= (seq_id(x)(#)seq_id(x)).n
proof
let n be Nat;
(seq_id(x)(#)seq_id(x)).n =(seq_id(x)).n * (seq_id(x)).n by SEQ_1:12;
hence thesis by REAL_1:93;
end;
A11:seq_id(x)(#)seq_id(x) is summable by Th1;
A12:x .|. x = (the scalar of l2_Space).[x,x] by BHSP_1:def 1
.= Sum(seq_id(x)(#)seq_id(x)) by RSSPACE:def 12,def 13;
A13:x .|. y = (the scalar of l2_Space).[x,y] by BHSP_1:def 1
.= Sum(seq_id(x)(#)seq_id(y)) by RSSPACE:def 12,def 13
.= (the scalar of l2_Space).[y,x] by RSSPACE:def 12,def 13
.=y .|. x by BHSP_1:def 1;
A14:seq_id(x)(#)seq_id(z) is summable by Th1;
A15:seq_id(y)(#)seq_id(z) is summable by Th1;
A16:(x+y) .|. z =(the scalar of l2_Space).[x+y,z] by BHSP_1:def 1
.= Sum(seq_id(x+y)(#)seq_id(z)) by RSSPACE:def 12,def 13
.= Sum(seq_id(seq_id(x)+seq_id(y))(#)seq_id(z)) by Th1
.= Sum((seq_id(x)+seq_id(y))(#)seq_id(z)) by RSSPACE:3
.= Sum(seq_id(x)(#)seq_id(z)+seq_id(y)(#)seq_id(z)) by SEQ_1:24
.= Sum(seq_id(x)(#)seq_id(z))+Sum(seq_id(y)(#)seq_id(z))
by A14,A15,SERIES_1:10
.=(the scalar of l2_Space).[x,z]+Sum(seq_id(y)(#)seq_id(z))
by RSSPACE:def 12,def 13
.=(the scalar of l2_Space).[x,z]
+(the scalar of l2_Space).[y,z] by RSSPACE:def 12,def 13
.=x .|. z +(the scalar of l2_Space).[y,z] by BHSP_1:def 1
.= x .|. z + y .|. z by BHSP_1:def 1;
A17:seq_id(x)(#)seq_id(y) is summable by Th1;
(a*x) .|. y = (the scalar of l2_Space).[a*x,y] by BHSP_1:def 1
.=Sum(seq_id(a*x)(#)seq_id(y)) by RSSPACE:def 12,def 13
.=Sum(seq_id(a(#)seq_id(x))(#)seq_id(y)) by Th1
.=Sum(a(#)seq_id(x)(#)seq_id(y)) by RSSPACE:3
.=Sum(a(#)(seq_id(x)(#)seq_id(y))) by SEQ_1:26
.=a*Sum(seq_id(x)(#)seq_id(y)) by A17,SERIES_1:13
.=a*(the scalar of l2_Space).[x,y] by RSSPACE:def 12,def 13
.=a * ( x .|. y ) by BHSP_1:def 1;
hence thesis by A1,A7,A10,A11,A12,A13,A16,SERIES_1:21;
end;
definition
cluster l2_Space -> RealUnitarySpace-like;
coherence by Th2,BHSP_1:def 2;
end;
Lm1:for rseq be Real_Sequence st
((for n be Nat holds 0 <= rseq.n) & rseq is summable) holds
( for n be Nat holds rseq.n <= (Partial_Sums rseq).n ) &
( for n be Nat holds 0 <= (Partial_Sums rseq).n ) &
( for n be Nat holds (Partial_Sums rseq).n <= Sum rseq) &
( for n be Nat holds rseq.n <= Sum rseq )
proof
let rseq be Real_Sequence such that
A1:for n be Nat holds 0 <= rseq.n and
A2:rseq is summable;
A3:Partial_Sums rseq is non-decreasing by A1,SERIES_1:19;
A4:Partial_Sums rseq is bounded_above by A1,A2,SERIES_1:20;
A5:for n be Nat holds (Partial_Sums rseq).n <= Sum rseq
proof
let n be Nat;
(Partial_Sums(rseq)).n <= lim Partial_Sums(rseq) by A3,A4,SEQ_4:54;
hence (Partial_Sums(rseq)).n <=Sum rseq by SERIES_1:def 3;
end;
A6:for n be Nat holds 0 <= Partial_Sums(rseq).n
proof
let n be Nat;
A7: n=n+0;
A8: Partial_Sums(rseq).0 = rseq.0 by SERIES_1:def 1;
0 <=rseq.0 by A1;
hence 0 <=Partial_Sums(rseq).n by A3,A7,A8,SEQM_3:11;
end;
A9:for n be Nat holds rseq.n <= Partial_Sums(rseq).n
proof
let n be Nat;
now per cases;
case n=0;
hence rseq.n <= Partial_Sums(rseq).n by SERIES_1:def 1;
case
A10: n<>0;
0 <= n by NAT_1:18;
then A11: 0 + 1 <= n by A10,INT_1:20;
set nn=n-1;
A12: nn is Nat by A11,INT_1:18;
A13: nn+1 = n-(1-1) by XCMPLX_1:37 .=n;
0 <= Partial_Sums(rseq).nn by A6,A12;
then rseq.n+0 <= rseq.n+Partial_Sums(rseq).nn by REAL_1:55;
hence rseq.n<=Partial_Sums(rseq).n by A12,A13,SERIES_1:def 1;
end;
hence thesis;
end;
for n be Nat holds rseq.n <= Sum rseq
proof
let n be Nat;
A14: (Partial_Sums(rseq)).n <= Sum rseq by A5;
rseq.n <= Partial_Sums(rseq).n by A9;
hence rseq.n <= Sum rseq by A14,AXIOMS:22;
end;
hence thesis by A5,A6,A9;
end;
Lm2:
(for x,y be Real holds (x+y)*(x+y) <= 2*x*x + 2*y*y) &
(for x,y be Real holds x*x <= 2*(x-y)*(x-y) + 2*y*y)
proof
A1:now
let x,y be Real;
A2: (x+y)*(x+y) =(x+y)^2 by SQUARE_1:def 3
.= x^2 + 2*x*y + y^2 by SQUARE_1:63;
2*x*x+2*y*y = 2*(x*x) + 2*y*y by XCMPLX_1:4
.= 2*(x*x) + 2*(y*y) by XCMPLX_1:4
.= 2*x^2 + 2*(y*y) by SQUARE_1:def 3
.= 2*x^2 + 2*y^2 by SQUARE_1:def 3;
then A3: 2*x*x+2*y*y - (x+y)*(x+y)
= 2*x^2 + 2*y^2 - (x^2 + 2*x*y) - y^2 by A2,XCMPLX_1:36
.= 2*x^2 + 2*y^2 - x^2 - 2*x*y - y^2 by XCMPLX_1:36
.= 2*x^2 - x^2 + 2*y^2 - 2*x*y - y^2 by XCMPLX_1:29
.= x^2 + x^2 - x^2 + 2*y^2 - 2*x*y - y^2 by XCMPLX_1:11
.= x^2 + 2*y^2 - 2*x*y - y^2 by XCMPLX_1:26
.= x^2 - 2*x*y + 2*y^2 - y^2 by XCMPLX_1:29
.= x^2 - 2*x*y + (2*y^2 - y^2) by XCMPLX_1:29
.= x^2 - 2*x*y + (y^2 + y^2 - y^2) by XCMPLX_1:11
.= x^2 - 2 * x * y + y^2 by XCMPLX_1:26
.= (x-y)^2 by SQUARE_1:64;
0 <= (x-y)^2 by SQUARE_1:72;
then 0 + (x+y)*(x+y) <= 2*x*x+2*y*y - (x+y)*(x+y)
+ (x+y)*(x+y) by A3,REAL_1:55;
then (x+y)*(x+y) <= 2*x*x+2*y*y
- ((x+y)*(x+y) - (x+y)*(x+y)) by XCMPLX_1:37;
hence (x+y)*(x+y) <=2*x*x+2*y*y by XCMPLX_1:17;
end;
now
let x,y be Real;
(x-y)+y=x by XCMPLX_1:27;
hence x*x <= 2*(x-y)*(x-y)+2*y*y by A1;
end;
hence thesis by A1;
end;
Lm3:
for e be Real
for seq be Real_Sequence st
(seq is convergent &
ex k be Nat st (for i be Nat st k <= i holds seq.i <=e ))
holds lim seq <=e
proof
let e be Real;
let seq be Real_Sequence such that
A1: seq is convergent
and
A2:ex k be Nat st (for i be Nat st k <= i holds seq.i <=e );
deffunc F(set)=e;
consider cseq be Real_Sequence such that
A3:for n be Nat holds cseq.n=F(n) from ExRealSeq;
A4:cseq is constant by A3,SEQM_3:def 6;
then A5:cseq is convergent by SEQ_4:39;
consider k be Nat such that
A6:for i be Nat st k <= i holds seq.i <=e by A2;
A7:(seq ^\k) is convergent by A1,SEQ_4:33;
A8:lim (seq ^\k)=lim seq by A1,SEQ_4:33;
A9:now let i be Nat;
A10: (seq ^\k).i = seq.(k+i) by SEQM_3:def 9;
k <= k+i by NAT_1:29;
then seq.(k+i) <=e by A6;
hence (seq ^\k) .i <= cseq.i by A3,A10;
end;
lim cseq = cseq.0 by A4,SEQ_4:41 .= e by A3;
hence thesis by A5,A7,A8,A9,SEQ_2:32;
end;
Lm4:
for c be Real, seq be Real_Sequence st seq is convergent
for rseq be Real_Sequence st
(for i be Nat holds rseq .i = (seq.i-c)*(seq.i-c))
holds (rseq is convergent & lim rseq = (lim seq-c)*(lim seq-c) )
proof
let c be Real;
let seq be Real_Sequence such that
A1:seq is convergent;
let rseq be Real_Sequence such that
A2:for i be Nat holds rseq .i = (seq.i-c)*(seq.i-c);
deffunc F(set)=c;
consider cseq be Real_Sequence such that
A3:for n be Nat holds cseq.n=F(n) from ExRealSeq;
now let i be Nat;
thus rseq.i=(seq.i-c)*(seq.i-c) by A2
.=(seq.i-(cseq.i))*(seq.i-c) by A3
.=(seq.i-(cseq.i))*(seq.i-(cseq.i)) by A3
.=(seq.i-(cseq.i))*(seq.i+-(cseq.i)) by XCMPLX_0:def 8
.=(seq.i+-(cseq.i))*(seq.i+-(cseq.i)) by XCMPLX_0:def 8
.=(seq.i+(-cseq).i)*(seq.i+-(cseq.i)) by SEQ_1:14
.=(seq.i+(-cseq).i)*(seq.i+(-cseq).i) by SEQ_1:14
.=(( seq+(-cseq)).i)*(seq.i+(-cseq).i) by SEQ_1:11
.=((seq+(-cseq)).i)*((seq+(-cseq)).i) by SEQ_1:11
.=( ( seq -cseq ).i)*(( seq + (-cseq) ).i) by SEQ_1:15
.=(( seq -cseq ).i)*((seq -cseq).i) by SEQ_1:15
.=((seq -cseq) (#) (seq -cseq)).i by SEQ_1:12;
end;
then A4:for x be set st x in NAT holds
rseq.x =((seq -cseq) (#) (seq -cseq)).x;
A5:cseq is constant by A3,SEQM_3:def 6;
then A6:cseq is convergent by SEQ_4:39;
then A7:seq -cseq is convergent by A1,SEQ_2:25;
then A8:(seq -cseq)(#)(seq -cseq) is convergent by SEQ_2:28;
lim ((seq -cseq)(#)(seq -cseq))
= (lim ((seq -cseq)))*(lim ((seq -cseq))) by A7,SEQ_2:29
.= ((lim seq) - (lim cseq))*(lim ((seq -cseq))) by A1,A6,SEQ_2:26
.= ((lim seq) - (lim cseq))*((lim seq) - (lim cseq)) by A1,A6,SEQ_2:26
.= ((lim seq) - (cseq.0))*((lim seq) - (lim cseq)) by A5,SEQ_4:41
.= ((lim seq) - (cseq.0))*((lim seq) - (cseq.0)) by A5,SEQ_4:41
.= ((lim seq) - c)*((lim seq) - (cseq.0)) by A3
.= ((lim seq) - c)*((lim seq) - c) by A3;
hence thesis by A4,A8,SEQ_1:8;
end;
Lm5:
for c be Real, seq,seq1 be Real_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 Real;
let seq,seq1 be Real_Sequence such that
A1:seq is convergent and
A2:seq1 is convergent;
let rseq be Real_Sequence such that
A3:for i be Nat holds rseq .i = (seq.i-c)*(seq.i-c)+seq1.i;
deffunc F(set)= c;
consider cseq be Real_Sequence such that
A4:for n be Nat holds cseq.n=F(n) from ExRealSeq;
now let i be Nat;
thus rseq.i=(seq.i-c)*(seq.i-c) +seq1.i by A3
.=(seq.i-(cseq.i))*(seq.i-c) +seq1.i by A4
.=(seq.i-(cseq.i))*(seq.i-(cseq.i)) +seq1.i by A4
.=(seq.i-(cseq.i))*(seq.i+-(cseq.i)) +seq1.i by XCMPLX_0:def 8
.=(seq.i+-(cseq.i))*(seq.i+-(cseq.i)) +seq1.i by XCMPLX_0:def 8
.=(seq.i+(-cseq).i)*(seq.i+-(cseq.i)) +seq1.i by SEQ_1:14
.=(seq.i+(-cseq).i)*(seq.i+(-cseq).i) +seq1.i by SEQ_1:14
.=(( seq+(-cseq)).i)*(seq.i+(-cseq).i) +seq1.i by SEQ_1:11
.=((seq+(-cseq)).i)*((seq+(-cseq)).i) +seq1.i by SEQ_1:11
.=( ( seq -cseq ).i)*(( seq + (-cseq) ).i) +seq1.i by SEQ_1:15
.=(( seq -cseq ).i)*((seq -cseq).i) +seq1.i by SEQ_1:15
.=((seq -cseq) (#) (seq -cseq)).i +seq1.i by SEQ_1:12
.=((seq -cseq) (#) (seq -cseq) +seq1).i by SEQ_1:11;
end;
then for x be set st x in NAT holds
rseq.x =((seq -cseq) (#) (seq -cseq)+seq1).x;
then A5:rseq = ((seq -cseq) (#) (seq -cseq)+seq1) by SEQ_1:8;
A6:cseq is constant by A4,SEQM_3:def 6;
then A7:cseq is convergent by SEQ_4:39;
then A8:seq -cseq is convergent by A1,SEQ_2:25;
then A9:(seq -cseq)(#)(seq -cseq) is convergent by SEQ_2:28;
lim ((seq -cseq)(#)(seq -cseq))
= (lim ((seq -cseq)))*(lim ((seq -cseq))) by A8,SEQ_2:29
.= ((lim seq) - (lim cseq))*(lim ((seq -cseq))) by A1,A7,SEQ_2:26
.= ((lim seq) - (lim cseq))*((lim seq) - (lim cseq)) by A1,A7,SEQ_2:26
.= ((lim seq) - (cseq.0))*((lim seq) - (lim cseq)) by A6,SEQ_4:41
.= ((lim seq) - (cseq.0))*((lim seq) - (cseq.0)) by A6,SEQ_4:41
.= ((lim seq) - c)*((lim seq) - (cseq.0)) by A4
.= ((lim seq) - c)*((lim seq) - c) by A4;
hence thesis by A2,A5,A9,SEQ_2:19,20;
end;
theorem
for vseq be sequence of l2_Space st vseq is_Cauchy_sequence holds
vseq is convergent
proof
let vseq be sequence of l2_Space such that
A1:vseq is_Cauchy_sequence;
defpred P[set,set] means ex i be Nat st $1=i
& ex rseqi be Real_Sequence
st ( for n be Nat holds rseqi.n=(seq_id(vseq.n)).i )
& rseqi is convergent
& $2=lim rseqi;
A2:for x be set st x in NAT ex y be set st
y in REAL & P[x,y]
proof
let x be set such that
A3: x in NAT;
reconsider i=x as Nat by A3;
deffunc F(set)=(seq_id(vseq.$1)).i;
consider rseqi be Real_Sequence such that
A4: for n be Nat holds rseqi.n=F(n) from ExRealSeq;
A5: rseqi is convergent
proof
now
let e be real number such that
A6: e > 0;
thus ex k be Nat st for m be Nat st
k<=m holds abs(rseqi.m -rseqi.k) < e
proof
e is Real by XREAL_0:def 1;
then consider k be Nat such that
A7: for n, m be Nat st ( n >= k & m >= k ) holds
||.(vseq.n) - (vseq.m).|| < e by A1,A6,BHSP_3:2;
now
let m be Nat such that
A8: k<=m;
||.(vseq.m) - (vseq.k).|| < e by A7,A8;
then A9: sqrt (((vseq.m) - (vseq.k)) .|.((vseq.m) - (vseq.k))) < e
by BHSP_1:def 4;
reconsider e1=e as Real by XREAL_0:def 1;
A10: seq_id(((vseq.m) - (vseq.k)))(#)seq_id(((vseq.m) - (vseq.k)))
is summable by RSSPACE:def 11,def 13;
A11: for i be Nat holds
0 <= (seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))).i
proof
let i be Nat;
(seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))).i
=(seq_id(((vseq.m) - (vseq.k)))).i
*(seq_id(((vseq.m) - (vseq.k)))).i by SEQ_1:12;
hence thesis by REAL_1:93;
end;
then A12: 0<= Sum(seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))) by A10,SERIES_1:21;
then A13: 0 <= sqrt ( Sum(seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))) )
by SQUARE_1:def 4;
sqrt ( Sum(seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))) ) < e by A9,Th1;
then (sqrt ( Sum(seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))) ) )^2 < e1^2
by A13,SQUARE_1:78;
then (sqrt ( Sum(seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))) ) )^2 < e*e
by SQUARE_1:def 3;
then A14: Sum(seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))) < e*e by A12,SQUARE_1:def 4;
A15: abs(rseqi.m-rseqi.k)*abs(rseqi.m-rseqi.k)
= (seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))).i
proof
seq_id((vseq.m) - (vseq.k))
=seq_id(seq_id((vseq.m))-seq_id((vseq.k))) by Th1
.= seq_id((vseq.m))-seq_id((vseq.k)) by RSSPACE:3
.= seq_id((vseq.m))+-seq_id((vseq.k)) by SEQ_1:15;
then (seq_id((vseq.m) - (vseq.k))).i
=(seq_id((vseq.m))).i+(-seq_id((vseq.k))).i by SEQ_1:11
.=(seq_id((vseq.m))).i+(-(seq_id((vseq.k))).i) by SEQ_1:14
.=(seq_id((vseq.m))).i-(seq_id((vseq.k))).i by XCMPLX_0:def 8
.=rseqi.m -(seq_id((vseq.k))).i by A4
.=rseqi.m - rseqi.k by A4;
then ((seq_id((vseq.m) - (vseq.k))).i)
*((seq_id((vseq.m) - (vseq.k))).i)
=((rseqi.m - rseqi.k))^2 by SQUARE_1:def 3
.= (abs((rseqi.m - rseqi.k)))^2 by SQUARE_1:62
.=abs((rseqi.m - rseqi.k))*abs((rseqi.m - rseqi.k))
by SQUARE_1:def 3;
hence thesis by SEQ_1:12;
end;
A16: (seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))).i
<= Sum(seq_id(((vseq.m) - (vseq.k)))
(#)seq_id(((vseq.m) - (vseq.k)))) by A10,A11,Lm1;
A17: 0 <= abs(rseqi.m-rseqi.k) by ABSVALUE:5;
then A18: 0 <= abs(rseqi.m-rseqi.k)*abs(rseqi.m-rseqi.k) by SQUARE_1:19;
A19: abs(rseqi.m-rseqi.k)*abs(rseqi.m-rseqi.k)
< e*e by A14,A15,A16,AXIOMS:22;
A20: sqrt (abs(rseqi.m-rseqi.k)*abs(rseqi.m-rseqi.k))
=sqrt ((abs(rseqi.m-rseqi.k))^2) by SQUARE_1:def 3
.=abs(rseqi.m-rseqi.k) by A17,SQUARE_1:89;
sqrt (e*e)=sqrt (e1^2) by SQUARE_1:def 3
.=e by A6,SQUARE_1:89;
hence abs(rseqi.m-rseqi.k) < e by A18,A19,A20,SQUARE_1:95;
end;
hence thesis;
end;
end;
hence thesis by SEQ_4:58;
end;
take lim rseqi;
thus thesis by A4,A5;
end;
consider f be Function of NAT,REAL such that
A21: for x be set st x in NAT holds P[x,f.x] from FuncEx1(A2);
reconsider tseq=f as Real_Sequence;
A22: now let i be Nat;
reconsider x=i as set;
ex i0 be Nat st x=i0
& ex rseqi be Real_Sequence
st ( for n be Nat holds rseqi.n=(seq_id(vseq.n)).i0 )
& rseqi is convergent & f.x=lim rseqi by A21;
hence ex rseqi be Real_Sequence
st ( for n be Nat holds rseqi.n=(seq_id(vseq.n)).i )
& rseqi is convergent & tseq.i=lim rseqi;
end;
A23:for e be Real st e >0
ex k be Nat st for n be Nat st n >= k holds
( (seq_id(tseq)-seq_id(vseq.n))(#)(seq_id(tseq)-seq_id(vseq.n))
is summable &
Sum((seq_id(tseq)-seq_id(vseq.n)) (#)( seq_id(tseq)-seq_id(vseq.n)))
< e *e )
proof
let e1 be Real such that
A24: e1 >0;
set e=e1/2;
A25: e > 0 by A24,SEQ_2:3;
e < e1 by A24,SEQ_2:4;
then A26:e*e < e1*e1 by A25,SEQ_4:6;
consider k be Nat such that
A27: for n, m be Nat st ( n >= k & m >= k )
holds ||.(vseq.n) - (vseq.m).|| < e by A1,A25,BHSP_3:2;
A28: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 such that
A29: n >= k & m >= k;
||.(vseq.n) - (vseq.m).|| < e by A27,A29;
then A30:sqrt (((vseq.n) - (vseq.m)) .|.((vseq.n) - (vseq.m)))
< e by BHSP_1:def 4;
A31: seq_id(((vseq.n) - (vseq.m)))(#)seq_id(((vseq.n) - (vseq.m)))
is summable by RSSPACE:def 11,def 13;
A32: 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)))).i
*(seq_id(((vseq.n) - (vseq.m)))).i by SEQ_1:12;
hence thesis by REAL_1:93;
end;
then A33:0<= Sum(seq_id(((vseq.n) - (vseq.m)))
(#)seq_id(((vseq.n) - (vseq.m)))) by A31,SERIES_1:21;
then A34:0 <= sqrt ( Sum(seq_id(((vseq.n) - (vseq.m)))
(#)seq_id(((vseq.n) - (vseq.m)))) ) by SQUARE_1:def 4;
sqrt ( Sum(seq_id(((vseq.n) - (vseq.m)))
(#)seq_id(((vseq.n) - (vseq.m)))) ) < e by A30,Th1;
then (sqrt ( Sum(seq_id(((vseq.n) - (vseq.m)))
(#)seq_id(((vseq.n) - (vseq.m)))) ) )^2 < e^2
by A34,SQUARE_1:78;
then (sqrt ( Sum(seq_id(((vseq.n) - (vseq.m)))
(#)seq_id(((vseq.n) - (vseq.m)))) ) )^2 < e*e
by SQUARE_1:def 3;
hence thesis by A32,A33,RSSPACE:def 11,def 13,SQUARE_1:def 4;
end;
A35: for n be Nat
for 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((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).i )
proof
let n be Nat;
A36: for m,k be Nat holds
seq_id((vseq.m) - (vseq.k))=seq_id((vseq.m))-seq_id((vseq.k))
proof
let m,k be Nat;
thus seq_id((vseq.m) - (vseq.k))
=seq_id(seq_id((vseq.m))-seq_id((vseq.k))) by Th1
.= seq_id((vseq.m))-seq_id((vseq.k)) by RSSPACE:3;
end;
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((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).$1);
A37: P[0]
proof
now
let rseq be Real_Sequence such that
A38: ( 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((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).0
proof
consider rseq0 be Real_Sequence such that
A39: ( for m be Nat holds rseq0.m=(seq_id(vseq.m)).0 )
& rseq0 is convergent & tseq.0=lim rseq0 by A22;
A40:now let m be Nat;
thus
rseq.m=Partial_Sums(seq_id(((vseq.m) - (vseq.n)))
(#)seq_id(((vseq.m) - (vseq.n)))).0 by A38
.=(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 A36
.=( (seq_id((vseq.m))-seq_id((vseq.n)) )
(#)(seq_id((vseq.m))-seq_id((vseq.n)) ) ).0 by A36
.= (seq_id((vseq.m))-seq_id((vseq.n)) ).0 *
(seq_id((vseq.m))-seq_id((vseq.n)) ).0 by SEQ_1:12
.= (seq_id((vseq.m))+-seq_id((vseq.n)) ).0 *
(seq_id((vseq.m))-seq_id((vseq.n)) ).0 by SEQ_1:15
.= (seq_id((vseq.m))+-seq_id((vseq.n)) ).0 *
(seq_id((vseq.m))+-seq_id((vseq.n)) ).0 by SEQ_1:15
.= ((seq_id((vseq.m))).0+(-seq_id((vseq.n))).0 ) *
(seq_id((vseq.m))+-seq_id((vseq.n)) ).0 by SEQ_1:11
.= ((seq_id((vseq.m))).0+(-seq_id((vseq.n))).0 ) *
((seq_id((vseq.m))).0+(-seq_id((vseq.n))).0 ) by SEQ_1:11
.= ((seq_id((vseq.m))).0+-(seq_id((vseq.n))).0 ) *
((seq_id((vseq.m))).0+(-seq_id((vseq.n))).0 ) by SEQ_1:14
.= ((seq_id((vseq.m))).0-(seq_id((vseq.n))).0 ) *
((seq_id((vseq.m))).0+(-seq_id((vseq.n))).0 )
by XCMPLX_0:def 8
.= ((seq_id((vseq.m))).0-(seq_id((vseq.n))).0 ) *
((seq_id((vseq.m))).0+-(seq_id((vseq.n))).0 ) by SEQ_1:14
.= ((seq_id((vseq.m))).0-(seq_id((vseq.n))).0 ) *
((seq_id((vseq.m))).0-(seq_id((vseq.n))).0 )
by XCMPLX_0:def 8
.= (rseq0.m-(seq_id((vseq.n))).0 ) *
((seq_id((vseq.m))).0-(seq_id((vseq.n))).0 ) by A39
.= (rseq0.m-(seq_id((vseq.n))).0 ) *
(rseq0.m-(seq_id((vseq.n))).0 ) by A39;
end;
then lim rseq = ( tseq.0-(seq_id((vseq.n))).0 ) *
( tseq.0-(seq_id((vseq.n))).0 ) by A39,Lm4
.= ( tseq.0+-(seq_id((vseq.n))).0 ) *
( tseq.0-(seq_id((vseq.n))).0 ) by XCMPLX_0:def 8
.= ( tseq.0+-(seq_id((vseq.n))).0 ) *
( tseq.0+-(seq_id((vseq.n))).0 ) by XCMPLX_0:def 8
.= ( tseq.0+(-seq_id((vseq.n))).0 ) *
( tseq.0+-(seq_id((vseq.n))).0 ) by SEQ_1:14
.= ( tseq.0+(-seq_id((vseq.n))).0 ) *
( tseq.0+(-seq_id((vseq.n))).0 ) by SEQ_1:14
.= ( tseq+(-seq_id((vseq.n)))).0 *
( tseq.0+(-seq_id((vseq.n))).0 ) by SEQ_1:11
.= ( tseq+(-seq_id((vseq.n)))).0 *
( tseq+(-seq_id((vseq.n)))).0 by SEQ_1:11
.= ( tseq-seq_id( (vseq.n) ) ).0 *
( tseq+(-seq_id((vseq.n)))).0 by SEQ_1:15
.= ( tseq-seq_id((vseq.n))).0 *
( tseq-seq_id((vseq.n))).0 by SEQ_1:15
.= ((tseq-seq_id((vseq.n)))
(#)(tseq-seq_id((vseq.n)))).0 by SEQ_1:12
.=Partial_Sums( (tseq-seq_id((vseq.n)))
(#)(tseq-seq_id((vseq.n))) ).0
by SERIES_1:def 1
.=Partial_Sums(( seq_id(tseq)-seq_id((vseq.n)) )
(#)(tseq-seq_id((vseq.n)) ) ).0 by RSSPACE:3
.=Partial_Sums(( seq_id(tseq)-seq_id((vseq.n)) )
(#)(seq_id(tseq)-seq_id((vseq.n)) ) ).0
by RSSPACE:3;
hence thesis by A39,A40,Lm4;
end;
end;
hence thesis;
end;
A41: for i be Nat st P[i] holds P[i+1]
proof
now let i be Nat such that
A42: 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((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-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((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).(i+1) )
proof
let rseq be Real_Sequence such that
A43:
for m be Nat holds rseq.m=Partial_Sums(seq_id(((vseq.m) - (vseq.n)))
(#)seq_id(((vseq.m) - (vseq.n)))).(i+1);
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
A44: for m be Nat holds rseqb.m = F(m) from ExRealSeq;
A45:rseqb is convergent
& lim rseqb =Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).i by A42,A44;
consider rseq0 be Real_Sequence such that
A46: ( for m be Nat holds rseq0.m=(seq_id(vseq.m)).(i+1) )
& rseq0 is convergent
& tseq.(i+1)=lim rseq0 by A22;
A47: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 A43
.=(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 A36
.=( (seq_id((vseq.m))-seq_id((vseq.n)) )
(#)(seq_id(((vseq.m) - (vseq.n))))).(i+1)
+rseqb.m by A44
.=( (seq_id((vseq.m))-seq_id((vseq.n)) )
(#)(seq_id((vseq.m))-seq_id((vseq.n)) ) ).(i+1)
+rseqb.m by A36
.= (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:12
.= (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:15
.= (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:15
.= ((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 SEQ_1:11
.= ((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 SEQ_1:11
.= ((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 SEQ_1:14
.= ((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 XCMPLX_0:def 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 SEQ_1:14
.= ((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 XCMPLX_0:def 8
.= (rseq0.m-(seq_id((vseq.n))).(i+1) ) *
((seq_id((vseq.m))).(i+1)-(seq_id((vseq.n))).(i+1) )
+rseqb.m by A46
.= (rseq0.m-(seq_id((vseq.n))).(i+1) ) *
(rseq0.m-(seq_id((vseq.n))).(i+1) )
+rseqb.m by A46;
end;
then lim rseq = ( lim (rseq0)-(seq_id((vseq.n))).(i+1) ) *
( lim (rseq0)-(seq_id((vseq.n))).(i+1) )
+ lim rseqb
by A45,A46,Lm5
.= ( tseq.(i+1)+-(seq_id((vseq.n))).(i+1) ) *
( tseq.(i+1)-(seq_id((vseq.n))).(i+1) )
+lim rseqb by A46,XCMPLX_0:def 8
.= ( tseq.(i+1)+-(seq_id((vseq.n))).(i+1) ) *
( tseq.(i+1)+-(seq_id((vseq.n))).(i+1) )
+lim rseqb by XCMPLX_0:def 8
.= ( tseq.(i+1)+(-seq_id((vseq.n))).(i+1) ) *
( tseq.(i+1)+-(seq_id((vseq.n))).(i+1) )
+ lim rseqb by SEQ_1:14
.= ( tseq.(i+1)+(-seq_id((vseq.n))).(i+1) ) *
( tseq.(i+1)+(-seq_id((vseq.n))).(i+1) )
+ lim rseqb by SEQ_1:14
.= ( tseq+(-seq_id((vseq.n)))).(i+1) *
( tseq.(i+1)+(-seq_id((vseq.n))).(i+1) )
+ lim rseqb by SEQ_1:11
.= ( tseq+(-seq_id((vseq.n)))).(i+1) *
( tseq+(-seq_id((vseq.n)))).(i+1)
+ lim rseqb by SEQ_1:11
.= ( tseq-seq_id( (vseq.n) ) ).(i+1) *
( tseq+(-seq_id((vseq.n)))).(i+1)
+ lim rseqb by SEQ_1:15
.= ( tseq-seq_id((vseq.n))).(i+1) *
( tseq-seq_id((vseq.n))).(i+1)
+ lim rseqb by SEQ_1:15
.= ( (tseq-seq_id((vseq.n)))
(#)(tseq-seq_id((vseq.n)))).(i+1)
+ lim rseqb by SEQ_1:12
.= ( (tseq-seq_id((vseq.n)))
(#)(tseq-seq_id((vseq.n)))).(i+1)
+ Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).i by A42,A44
.= ( (tseq-seq_id((vseq.n)))
(#)(seq_id(tseq)-seq_id((vseq.n))) ).(i+1)
+ Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).i by RSSPACE:3
.= ( (seq_id(tseq)-seq_id((vseq.n)))
(#)(seq_id(tseq)-seq_id((vseq.n))) ).(i+1)
+ Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).i by RSSPACE:3
.=Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).(i+1)
by SERIES_1:def 1;
hence thesis by A45,A46,A47,Lm5;
end;
end;
hence thesis;
end;
for i be Nat holds P[i] from Ind(A37,A41);
hence thesis;
end;
for n be Nat st n >= k holds
( (seq_id(tseq)-seq_id(vseq.n))(#)(seq_id(tseq)-seq_id(vseq.n))
is summable &
Sum((seq_id(tseq)-seq_id(vseq.n)) (#)( seq_id(tseq)-seq_id(vseq.n)))
< e1*e1 )
proof
let n be Nat such that
A48: n >= k;
A49:for i be Nat st 0 <= i holds
Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-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
A50: for m be Nat holds rseq.m=F(m) from ExRealSeq;
A51:rseq is convergent by A35,A50;
A52:lim rseq
=Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).i by A35,A50;
for m be Nat st m >= k holds rseq.m <= e*e
proof
let m be Nat such that
A53: m >= k;
A54: rseq.m=Partial_Sums(seq_id(((vseq.m) - (vseq.n)))
(#)seq_id(((vseq.m) - (vseq.n)))).i by A50;
A55: seq_id((vseq.m) - (vseq.n))(#)
seq_id((vseq.m) -(vseq.n)) is summable &
Sum(seq_id(((vseq.m) - (vseq.n)))
(#)seq_id(((vseq.m) - (vseq.n)))) < e*e
&for i be Nat holds
0 <= ( seq_id((vseq.m) - (vseq.n))
(#)seq_id((vseq.m) - (vseq.n)) ).i
by A28,A48,A53;
then 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 Lm1;
hence thesis by A54,A55,AXIOMS:22;
end;
hence (Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)))).i <=e*e by A51,A52,Lm3;
end;
A56:for i be Nat holds
0 <= ( (seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n))) .i
proof
let i be Nat;
((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n))).i
=(seq_id(tseq)-seq_id(vseq.n)).i
*(seq_id(tseq)-seq_id(vseq.n)).i by SEQ_1:12;
hence thesis by REAL_1:93;
end;
A57:Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ) is bounded_above
proof
now let i be Nat;
0 <= i by NAT_1:18;
then Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).i <=e*e by A49;
hence Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ).i < e1*e1 by A26,AXIOMS:22;
end;
hence thesis by SEQ_2:def 3;
end;
then (seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) is summable
by A56,SERIES_1:20;
then A58: Partial_Sums( (seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) ) is convergent
by SERIES_1:def 2;
A59: Sum((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)))
= lim Partial_Sums( (seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) )
by SERIES_1:def 3;
lim Partial_Sums((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)))
<=e*e by A49,A58,Lm3;
hence thesis by A26,A56,A57,A59,AXIOMS:22,SERIES_1:20;
end;
hence thesis;
end;
A60:seq_id(tseq)(#)seq_id(tseq) is summable
proof
A61: 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:12;
hence thesis by REAL_1:93;
end;
consider m be Nat such that
A62: for n be Nat st n >= m holds
( (seq_id(tseq)-seq_id(vseq.n))(#)( seq_id(tseq)-seq_id(vseq.n))
is summable &
Sum((seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n))) < 1*1 ) by A23;
A63: (seq_id(tseq)-seq_id(vseq.m))
(#)( seq_id(tseq)-seq_id(vseq.m)) is summable by A62;
A64: seq_id( (vseq.m) )(#)seq_id( (vseq.m) )
is summable by RSSPACE:def 11,def 13;
set a =(seq_id(tseq)-seq_id(vseq.m))(#)(seq_id(tseq)-seq_id(vseq.m));
set b=seq_id( (vseq.m) )(#)seq_id( (vseq.m) );
set d=seq_id(tseq)(#)seq_id(tseq);
A65:2(#)a is summable by A63,SERIES_1:13;
2(#)b is summable by A64,SERIES_1:13;
then A66:2(#)a + 2(#)b is summable by A65,SERIES_1:10;
for i be Nat holds d.i <= (2(#)a + 2(#)b).i
proof
let i be Nat;
A67: d.i=((seq_id(tseq)).i) * ((seq_id(tseq)).i) by SEQ_1:12;
A68: (2(#)a + 2(#)b).i = (2(#)a).i + (2(#)b).i by SEQ_1:11
.=2*(a.i)+ (2(#)b).i by SEQ_1:13
.=2*(a.i)+ 2*(b.i) by SEQ_1:13;
(seq_id(tseq)-seq_id(vseq.m)).i
= (seq_id(tseq)+-seq_id(vseq.m)).i by SEQ_1:15
.= (seq_id(tseq)).i+(-seq_id(vseq.m)).i by SEQ_1:11
.= (seq_id(tseq)).i+(-(seq_id(vseq.m)).i) by SEQ_1:14
.= (seq_id(tseq)).i-(seq_id(vseq.m)).i by XCMPLX_0:def 8;
then A69: a.i = ((seq_id(tseq)).i-(seq_id(vseq.m)).i)
*((seq_id(tseq)).i-(seq_id(vseq.m)).i) by SEQ_1:12;
set x=(seq_id(tseq)).i;
set y=(seq_id( (vseq.m) )).i;
A70:2*(a.i)=2*(x-y)*(x-y) by A69,XCMPLX_1:4;
2*(b.i)=2*(y*y) by SEQ_1:12
.=2*y*y by XCMPLX_1:4;
hence thesis by A67,A68,A70,Lm2;
end;
hence d is summable by A61,A66,SERIES_1:24;
end;
tseq in the_set_of_RealSequences by RSSPACE:def 1;
then reconsider tv=tseq as Point of l2_Space by A60,RSSPACE:def 11,def 13;
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
A71: e > 0;
consider m be Nat such that
A72:for n be Nat st n >= m holds
( (seq_id(tseq)-seq_id(vseq.n))
(#)(seq_id(tseq)-seq_id(vseq.n)) is summable &
Sum((seq_id(tseq)-seq_id(vseq.n))
(#)( seq_id(tseq)-seq_id(vseq.n))) < e *e ) by A23,A71;
now let n be Nat such that
A73:n >= m;
A74: Sum((seq_id(tseq)-seq_id(vseq.n))
(#)( seq_id(tseq)-seq_id(vseq.n))) < e*e by A72,A73;
tseq in the_set_of_RealSequences by RSSPACE:def 1;
then reconsider u=tseq as VECTOR of l2_Space by A60,RSSPACE:def 11,def 13;
reconsider v=vseq.n as VECTOR of l2_Space;
seq_id(u-v) = u-v by Th1;
then seq_id(u-v)=seq_id(tseq)-seq_id(vseq.n) by Th1;
then A75:(u-v).|.(u-v) < e*e by A74,Th1;
0 <= ((u-v).|.(u-v)) by BHSP_1:def 2;
then sqrt ((u-v).|.(u-v)) < sqrt (e*e) by A75,SQUARE_1:95;
then A76: sqrt ((u-v).|.(u-v)) < sqrt (e^2) by SQUARE_1:def 3;
||.(vseq.n) - tv.||
=||.(vseq.n) +(-tv).|| by RLVECT_1:def 11
.=||.-(tv-(vseq.n)).|| by RLVECT_1:47
.=||.tv-(vseq.n).|| by BHSP_1:37
.=sqrt ((u-v).|.(u-v)) by BHSP_1:def 4;
hence ||.(vseq.n) - tv.|| < e by A71,A76,SQUARE_1:89;
end;
hence thesis;
end;
hence thesis by BHSP_2:9;
end;
then Lm6: l2_Space is complete by BHSP_3:def 6;
definition
cluster l2_Space -> Hilbert complete;
coherence by Lm6,BHSP_3:def 7;
end;
begin :: Miscellaneous
theorem
for rseq be Real_Sequence st
((for n be Nat holds 0 <= rseq.n) & rseq is summable) holds
( for n be Nat holds rseq.n <= (Partial_Sums rseq).n ) &
( for n be Nat holds 0 <= (Partial_Sums rseq).n ) &
( for n be Nat holds (Partial_Sums(rseq)).n <= Sum rseq ) &
( for n be Nat holds rseq.n <= Sum(rseq) ) by Lm1;
theorem
(for x,y be Real holds (x+y)*(x+y) <= 2*x*x + 2*y*y) &
(for x,y be Real holds x*x <= 2*(x-y)*(x-y) + 2*y*y) by Lm2;
theorem
for e being Real, seq being Real_Sequence st
(seq is convergent &
ex k being Nat st (for i being Nat st k <= i holds seq.i <=e))
holds lim seq <=e by Lm3;
theorem
for c being Real, seq being Real_Sequence st seq is convergent
for rseq be Real_Sequence st
(for i be Nat holds rseq.i = (seq.i-c)*(seq.i-c)) holds
rseq is convergent & lim rseq = (lim seq-c)*(lim seq-c) by Lm4;
theorem
for c being Real, seq,seq1 being Real_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 Lm5;