:: Hilbert Space of Real Sequences
:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003-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, STRUCT_0, RSSPACE, RLVECT_1, SEQ_1, VALUED_1, SERIES_1,
SUPINF_2, ARYTM_3, REAL_1, RELAT_1, ARYTM_1, PROB_2, CARD_3, COMPLEX1,
SUBSET_1, CARD_1, XXREAL_0, FUNCT_1, SQUARE_1, BHSP_1, ALGSTR_0,
ZFMISC_1, REALSET1, PRE_TOPC, VALUED_0, XXREAL_2, ORDINAL2, SEQ_2, NAT_1,
BHSP_3, NORMSP_1, REWRITE1, RSSPACE2, ASYMPT_1;
notations TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, BINOP_1, REALSET1, RELAT_1,
PARTFUN1, FUNCT_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1,
REAL_1, NAT_1, VALUED_1, SQUARE_1, SEQ_1, SERIES_1, COMSEQ_2, SEQ_2,
STRUCT_0, ALGSTR_0, XREAL_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3,
FUNCSDOM, RSSPACE;
constructors PARTFUN1, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D,
SEQ_2, SERIES_1, REALSET1, RLSUB_1, BHSP_2, BHSP_3, RSSPACE, VALUED_1,
RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, FUNCSDOM;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, REALSET1, RSSPACE, VALUED_1, FUNCT_2, VALUED_0, NAT_1, SEQ_4,
SERIES_1, SQUARE_1, SEQ_1, SEQ_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions BHSP_3;
equalities SQUARE_1, BINOP_1, REALSET1, RLVECT_1, STRUCT_0, ALGSTR_0, RSSPACE,
FUNCSDOM, SEQ_1;
theorems RELAT_1, SQUARE_1, ZFMISC_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, COMPLEX1, XREAL_1, XXREAL_0, ORDINAL1;
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 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
thus the carrier of l2_Space = the_set_of_l2RealSequences;
thus 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 FUNCT_2:8,66;
hence thesis by RSSPACE:def 11;
end;
thus 0.l2_Space = 0.Linear_Space_of_RealSequences by RSSPACE:def 10
.= Zeroseq;
thus for u be VECTOR of l2_Space holds u = seq_id(u);
set W = the_set_of_l2RealSequences;
set L1 = Linear_Space_of_RealSequences;
thus
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;
reconsider u1=u,v1=v as VECTOR of Linear_Space_of_RealSequences by
RLSUB_1:10,RSSPACE:12;
dom (the addF of L1) = [:the carrier of L1,the carrier of L1:] by
FUNCT_2:def 1;
then dom ((the addF of Linear_Space_of_RealSequences)||W) =[:W,W:] by
RELAT_1:62,ZFMISC_1:96;
then
A11: [u,v] in dom ((the addF of Linear_Space_of_RealSequences)||W)
by ZFMISC_1:87;
u+v =((the addF of Linear_Space_of_RealSequences)||W).[u,v] by
RSSPACE:def 8
.=u1+v1 by A11,FUNCT_1:47;
hence thesis by RSSPACE:2;
end;
thus
A12: for r be Real for u be VECTOR of l2_Space holds r*u =r(#)seq_id(u)
proof
let r be Real;
reconsider r as Element of REAL by XREAL_0:def 1;
let u be VECTOR of l2_Space;
reconsider u1=u as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10
,RSSPACE:12;
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 RELAT_1:62,ZFMISC_1:96;
then
A13: [r,u] in dom ((the Mult of Linear_Space_of_RealSequences)|[:REAL,W :]
) by ZFMISC_1:87;
r*u =((the Mult of Linear_Space_of_RealSequences)|[:REAL,W:]).[r,u]
by RSSPACE:def 9
.=r*u1 by A13,FUNCT_1:47;
hence thesis by RSSPACE:3;
end;
thus
A15: 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:16
.= (-1)(#)seq_id(u) by A12
.= -seq_id(u) by SEQ_1:17;
hence thesis;
end;
thus 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 = seq_id(u)+seq_id(-v) by A10
.= seq_id(u)+(-seq_id(v)) by A15
.= seq_id(u)-seq_id(v) by SEQ_1:11;
end;
thus for u,v be VECTOR of l2_Space holds seq_id(u)(#)seq_id(v) is summable
proof
set q0 = 1/2;
let u,v be VECTOR of l2_Space;
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)));
A2: for n be Nat holds 0<=(2(#)r).n
proof
set rr=(seq_id u)(#)(seq_id v);
let n be Nat;
reconsider tt=|.rr.n.| as Real;
A3: 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 A3;
end;
A4: 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;
reconsider sn=s.n,tn=t.n as Real;
reconsider ss=|.sn.|,tt=|.tn.| as Real;
A5: (p+q).n = p.n +q.n by SEQ_1:7
.= (s.n*s.n) + q.n by SEQ_1:8
.= sn^2 + (t.n*t.n) by SEQ_1:8
.=(|.sn.|)^2 + tn^2 by COMPLEX1:75
.=(|.sn.|)^2 + (|.tn.|)^2 by COMPLEX1:75;
A6: 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*(ss*tt) by COMPLEX1:65
.= 2*|.sn.|*|.tn.|;
then 0 + (2(#)r).n <= (p+q).n - (2(#)r).n + (2(#)r).n by A5,A6,XREAL_1:7;
hence thesis;
end;
A7: 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 RSSPACE:def 11;
then p+q is summable by SERIES_1:7;
then 2(#)r is summable by A2,A4,SERIES_1:20;
then r is summable by A7,SERIES_1:10;
then (seq_id(u))(#)(seq_id(v)) is absolutely_summable by SERIES_1:def 4;
hence thesis;
end;
thus 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;
end;
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: 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:8;
hence thesis by XREAL_1:63;
end;
A2: seq_id(x)(#)seq_id(x) is summable & x .|. x = Sum(seq_id(x)(#)seq_id(x)
) by Th1;
A3: now
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:8;
hence thesis by XREAL_1:63;
end;
assume
A5: x .|. x = 0;
A6: x .|. x = Sum(seq_id(x)(#)seq_id(x)) & seq_id(x)(#)seq_id(x) is
summable by Th1;
A7: for n be Nat holds 0 = (seq_id x).n
proof
let n be Nat;
0 = (seq_id(x)(#)seq_id(x)).n by A5,A4,A6,RSSPACE:17
.= ((seq_id(x)).n)*((seq_id(x)).n) by SEQ_1:8;
hence thesis by XCMPLX_1:6;
end;
x is Element of the_set_of_RealSequences by RSSPACE:def 11;
hence x=0.l2_Space by A7,Th1,RSSPACE:5;
end;
A8: x .|. y = Sum(seq_id(x)(#)seq_id(y)) by Th1
.=y .|. x by Th1;
A9: now
assume
A10: x=0.l2_Space;
A11: 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:8
.=(seq_id(x)).n * 0 by A10,Th1
.= 0;
end;
thus x .|. x = Sum(seq_id(x)(#)seq_id(x)) by Th1
.=0 by A11,RSSPACE:16;
end;
A12: seq_id(x)(#)seq_id(y) is summable by Th1;
A13: (a*x) .|. y =Sum(seq_id(a*x)(#)seq_id(y)) by Th1
.=Sum(a(#)seq_id(x)(#)seq_id(y)) by Th1
.=Sum(a(#)(seq_id(x)(#)seq_id(y))) by SEQ_1:18
.=a*Sum(seq_id(x)(#)seq_id(y)) by A12,SERIES_1:10
.=a * ( x .|. y ) by Th1;
A14: seq_id(x)(#)seq_id(z) is summable & seq_id(y)(#)seq_id(z) is summable
by Th1;
(x+y) .|. z = Sum(seq_id(x+y)(#)seq_id(z)) by Th1
.= Sum((seq_id(x)+seq_id(y))(#)seq_id(z)) by Th1
.= Sum(seq_id(x)(#)seq_id(z)+seq_id(y)(#)seq_id(z)) by SEQ_1:16
.= Sum(seq_id(x)(#)seq_id(z))+Sum(seq_id(y)(#)seq_id(z)) by A14,SERIES_1:7
.= x .|. z + Sum(seq_id(y)(#)seq_id(z)) by Th1
.= x .|. z + y .|. z by Th1;
hence thesis by A3,A9,A1,A2,A8,A13,SERIES_1:18;
end;
registration
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)
holds ( for n be Nat holds 0 <= (Partial_Sums rseq).n ) & ( for n be
Nat holds rseq.n <= (Partial_Sums rseq).n ) & (rseq is summable
implies ( 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;
A2: Partial_Sums rseq is non-decreasing by A1,SERIES_1:16;
thus
A3: for n be Nat holds 0 <= Partial_Sums(rseq).n
proof
let n be Nat;
A4: n=n+0 & Partial_Sums(rseq).0 = rseq.0 by SERIES_1:def 1;
0 <= rseq.0 by A1;
hence thesis by A2,A4,SEQM_3:5;
end;
thus
A5: for n be Nat holds rseq.n <= Partial_Sums(rseq).n
proof
let n be Nat;
now
per cases;
case
n=0;
hence thesis by SERIES_1:def 1;
end;
case
A6: n<>0;
A7: n in NAT by ORDINAL1:def 12;
set nn=n-1;
0 + 1 <= n by A6,INT_1:7,A7;
then
A8: nn in NAT by INT_1:5,A7;
then 0 <= Partial_Sums(rseq).nn by A3;
then nn+1 =n & rseq.n+0 <= rseq.n+Partial_Sums(rseq).nn by XREAL_1:7;
hence thesis by A8,SERIES_1:def 1;
end;
end;
hence thesis;
end;
assume rseq is summable;
then
A9: Partial_Sums rseq is bounded_above by A1,SERIES_1:17;
thus
A10: 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 A1,A9,SEQ_4:37
,SERIES_1:16;
hence thesis by SERIES_1:def 3;
end;
let n be Nat;
A11: rseq.n <= Partial_Sums(rseq).n by A5;
(Partial_Sums(rseq)).n <= Sum rseq by A10;
hence thesis by A11,XXREAL_0:2;
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;
0 <= (x-y)^2 by XREAL_1:63;
then 0 + (x+y)*(x+y) <= 2*x*x+2*y*y - (x+y)*(x+y) + (x+y)*(x+y) by
XREAL_1:7;
hence (x+y)*(x+y) <=2*x*x+2*y*y;
end;
now
let x,y be Real;
(x-y)+y=x;
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;
consider k be Nat such that
A3: for i be Nat st k <= i holds seq.i <=e by A2;
reconsider ee=e as Element of REAL by XREAL_0:def 1;
set cseq = seq_const e;
A4: lim cseq = cseq.0 by SEQ_4:26
.= e by SEQ_1:57;
A5: now
let i be Nat;
(seq ^\k).i = seq.(k+i) & seq.(k+i) <=e by A3,NAT_1:11,def 3;
hence (seq ^\k) .i <= cseq.i by SEQ_1:57;
end;
lim (seq ^\k)=lim seq by A1,SEQ_4:20;
hence thesis by A1,A5,A4,SEQ_2:18;
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;
reconsider cc = c as Element of REAL by XREAL_0:def 1;
set cseq = seq_const c;
let seq be Real_Sequence such that
A1: seq is convergent;
A2: seq -cseq is convergent by A1;
then
A3: (seq -cseq)(#)(seq -cseq) is convergent;
let rseq be Real_Sequence such that
A4: for i be Nat holds rseq .i = (seq.i-c)*(seq.i-c);
now
let i be Element of NAT;
thus rseq.i=(seq.i-c)*(seq.i-c) by A4
.=(seq.i-(cseq.i))*(seq.i-c) by SEQ_1:57
.=(seq.i-(cseq.i))*(seq.i+-(cseq.i)) by SEQ_1:57
.=(seq.i+(-cseq).i)*(seq.i+-(cseq.i)) by SEQ_1:10
.=(seq.i+(-cseq).i)*(seq.i+(-cseq).i) by SEQ_1:10
.=(( seq+(-cseq)).i)*(seq.i+(-cseq).i) by SEQ_1:7
.=( ( seq -cseq ).i)*(( seq + (-cseq) ).i) by SEQ_1:7,11
.=(( seq -cseq ).i)*((seq -cseq).i) by SEQ_1:11
.=((seq -cseq) (#) (seq -cseq)).i by SEQ_1:8;
end;
then
A5: for x be object st x in NAT
holds rseq.x =((seq -cseq) (#) (seq -cseq)) .x;
lim ((seq -cseq)(#)(seq -cseq)) = (lim ((seq -cseq)))*(lim ((seq -cseq))
) by A2,SEQ_2:15
.= ((lim seq) - (lim cseq))*(lim ((seq -cseq))) by A1,SEQ_2:12
.= ((lim seq) - (lim cseq))*((lim seq) - (lim cseq)) by A1,SEQ_2:12
.= ((lim seq) - (cseq.0))*((lim seq) - (lim cseq)) by SEQ_4:26
.= ((lim seq) - (cseq.0))*((lim seq) - (cseq.0)) by SEQ_4:26
.= ((lim seq) - c)*((lim seq) - (cseq.0)) by SEQ_1:57
.= ((lim seq) - c)*((lim seq) - c) by SEQ_1:57;
hence thesis by A5,A3,FUNCT_2:12;
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;
reconsider cc = c as Element of REAL by XREAL_0:def 1;
set cseq = seq_const c;
A3: seq -cseq is convergent by A1;
then
A4: (seq -cseq)(#)(seq -cseq) is convergent;
let rseq be Real_Sequence such that
A5: 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 A5
.=(seq.i-(cseq.i))*(seq.i-c) +seq1.i by SEQ_1:57
.=(seq.i-(cseq.i))*(seq.i+-(cseq.i)) +seq1.i by SEQ_1:57
.=(seq.i+(-cseq).i)*(seq.i+-(cseq.i)) +seq1.i by SEQ_1:10
.=(seq.i+(-cseq).i)*(seq.i+(-cseq).i) +seq1.i by SEQ_1:10
.=(( seq+(-cseq)).i)*(seq.i+(-cseq).i) +seq1.i by SEQ_1:7
.=( ( seq -cseq ).i)*(( seq + (-cseq) ).i) +seq1.i by SEQ_1:7,11
.=(( seq -cseq ).i)*((seq -cseq).i) +seq1.i by SEQ_1:11
.=((seq -cseq) (#) (seq -cseq)).i +seq1.i by SEQ_1:8
.=((seq -cseq) (#) (seq -cseq) +seq1).i by SEQ_1:7;
end;
then
A6: rseq = ((seq -cseq) (#) (seq -cseq)+seq1) by FUNCT_2:63;
lim ((seq -cseq)(#)(seq -cseq)) = (lim ((seq -cseq)))*(lim ((seq -cseq))
) by A3,SEQ_2:15
.= ((lim seq) - (lim cseq))*(lim ((seq -cseq))) by A1,SEQ_2:12
.= ((lim seq) - (lim cseq))*((lim seq) - (lim cseq)) by A1,SEQ_2:12
.= ((lim seq) - (cseq.0))*((lim seq) - (lim cseq)) by SEQ_4:26
.= ((lim seq) - (cseq.0))*((lim seq) - (cseq.0)) by SEQ_4:26
.= ((lim seq) - c)*((lim seq) - (cseq.0)) by SEQ_1:57
.= ((lim seq) - c)*((lim seq) - c) by SEQ_1:57;
hence thesis by A2,A6,A4,SEQ_2:6;
end;
registration
cluster l2_Space -> complete;
coherence
proof
let vseq be sequence of l2_Space such that
A1: vseq is Cauchy;
defpred P[object,object] 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 object st x in NAT ex y be object st y in REAL & P[x,y]
proof
let x be object;
assume
x in NAT;
then reconsider i=x as Element of NAT;
deffunc F(set)=(seq_id(vseq.$1)).i;
consider rseqi be Real_Sequence such that
A3: for n be Nat holds rseqi.n=F(n) from SEQ_1:sch 1;
reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr;
now
let e be Real such that
A4: e > 0;
thus ex k be Nat st for m be Nat st k<=m holds
|.rseqi.m -rseqi.k.| < e
proof
consider k be Nat such that
A5: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n
) - (vseq.m).|| < e by A1,A4,BHSP_3:2;
now
let m be Nat;
assume k<=m;
then ||.(vseq.m) - (vseq.k).|| < e by A5;
then sqrt (((vseq.m) - (vseq.k)) .|.((vseq.m) - (vseq.k ))) < e by
BHSP_1:def 4;
then
A6: sqrt ( Sum(seq_id(((vseq.m) - (vseq.k))) (#)seq_id(((vseq.m) -
(vseq.k)))) ) < e by Th1;
reconsider e1=e as Real;
A7: sqrt (|.rseqi.m-rseqi.k.|*|.rseqi.m-rseqi.k.|) =sqrt ((|.
rseqi.m-rseqi.k.|)^2)
.=|.rseqi.m-rseqi.k.| by COMPLEX1:46,SQUARE_1:22;
seq_id((vseq.m) - (vseq.k)) = seq_id(vseq.m)-seq_id(vseq.k) by Th1
.= seq_id(vseq.m)+-seq_id(vseq.k) by SEQ_1:11;
then (seq_id((vseq.m) - (vseq.k))).i =(seq_id(vseq.m)).i+(-seq_id(
vseq.k)).i by SEQ_1:7
.=(seq_id(vseq.m)).i+(-(seq_id(vseq.k)).i) by SEQ_1:10
.=(seq_id(vseq.m)).i-(seq_id(vseq.k)).i
.=rseqi.m -(seq_id(vseq.k)).i by A3
.=rseqi.m - rseqi.k by A3;
then
((seq_id((vseq.m) - (vseq.k))).i) *((seq_id((vseq.m) - (vseq.k)
)).i) =((rseqi.m - rseqi.k))^2
.= (|.(rseqi.m - rseqi.k).|)^2 by COMPLEX1:75
.=|.(rseqi.m - rseqi.k).|*|.(rseqi.m - rseqi.k).|;
then
A8: |.rseqi.m-rseqi.k.|*|.rseqi.m-rseqi.k.| = (seq_id(((vseq.m) -
(vseq.k))) (#)seq_id(((vseq.m) - (vseq.k)))).i by SEQ_1:8;
A9: 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:8;
hence thesis by XREAL_1:63;
end;
A10: seq_id(((vseq.m) - (vseq.k)))(#)seq_id(((vseq.m) - (vseq.k)))
is summable by RSSPACE:def 11;
then
A11: 0<= Sum(seq_id(((vseq.m) - (vseq.k))) (#)seq_id(((vseq.m) - (
vseq.k)))) by A9,SERIES_1:18;
then
0 <= sqrt ( Sum(seq_id(((vseq.m) - (vseq.k))) (#)seq_id(((vseq.
m) - (vseq.k)))) ) by SQUARE_1:def 2;
then
(sqrt ( Sum(seq_id(((vseq.m) - (vseq.k))) (#)seq_id(((vseq.m) -
(vseq.k)))) ) )^2 < e1^2 by A6,SQUARE_1:16;
then
A12: Sum(seq_id(((vseq.m) - (vseq.k))) (#)seq_id(((vseq.m) - (vseq.k
)))) < e*e by A11,SQUARE_1:def 2;
(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,A9,Lm1;
then
A13: 0 <= |.rseqi.m-rseqi.k.| & |.rseqi.m-rseqi.k.|*|.rseqi.m-
rseqi.k.| < e*e by A12,A8,COMPLEX1:46,XXREAL_0:2;
sqrt (e*e)=sqrt (e1^2) .=e by A4,SQUARE_1:22;
hence |.rseqi.m-rseqi.k.| < e by A13,A7,SQUARE_1:27;
end;
hence thesis;
end;
end;
then rseqi is convergent by SEQ_4:41;
hence thesis by A3;
end;
consider f be sequence of REAL such that
A14: for x be object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A2);
reconsider tseq=f as Real_Sequence;
A15: now
let i be Nat;
i in NAT by ORDINAL1:def 12;
then
ex i0 be Nat st i=i0 & ex rseqi be Real_Sequence st ( for
n be Nat holds rseqi.n=(seq_id(vseq.n)).i0 ) & rseqi is convergent &
f.i=lim rseqi by A14;
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;
A16: 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
A17: e1 >0;
set e=e1/2;
A18: e > 0 by A17,XREAL_1:215;
then consider k be Nat such that
A19: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A1,BHSP_3:2;
e < e1 by A17,XREAL_1:216;
then
A20: e*e < e1*e1 by A18,XREAL_1:97;
A21: 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 A19;
then sqrt (((vseq.n) - (vseq.m)) .|.((vseq.n) - (vseq.m))) < e by
BHSP_1:def 4;
then
A22: sqrt ( Sum(seq_id(((vseq.n) - (vseq.m))) (#)seq_id(((vseq.n) - (
vseq.m)))) ) < e by Th1;
A23: for i being 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:8;
hence thesis by XREAL_1:63;
end;
seq_id(((vseq.n) - (vseq.m)))(#)seq_id(((vseq.n) - (vseq.m))) is
summable by RSSPACE:def 11;
then
A24: 0<= Sum(seq_id(((vseq.n) - (vseq.m))) (#)seq_id(((vseq.n) - (vseq.m
)))) by A23,SERIES_1:18;
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 A22,SQUARE_1:16;
hence thesis by A23,A24,RSSPACE:def 11,SQUARE_1:def 2;
end;
A25: for n,i be Nat holds for rseq be Real_Sequence st
( for m being 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;
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);
A26: for m,k be Nat holds seq_id((vseq.m) - (vseq.k))=seq_id(
(vseq.m))-seq_id((vseq.k)) by Th1;
for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A27: 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
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
A28: for m be Nat holds rseqb.m = F(m) from SEQ_1:sch 1;
consider rseq0 be Real_Sequence such that
A29: for m be Nat holds rseq0.m=(seq_id(vseq.m)).(i+1 ) and
A30: rseq0 is convergent and
A31: tseq.(i+1)=lim rseq0 by A15;
let rseq be Real_Sequence such that
A32: for m be Nat holds rseq.m=Partial_Sums(seq_id(((
vseq.m) - (vseq.n))) (#)seq_id(((vseq.m) - (vseq.n)))).(i+1);
A33: 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 A32
.=(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 A26
.=( (seq_id(vseq.m)-seq_id(vseq.n) ) (#)(seq_id(((vseq.m) - (
vseq.n))))).(i+1) +rseqb.m by A28
.=( (seq_id(vseq.m)-seq_id(vseq.n) ) (#)(seq_id(vseq.m)-seq_id
(vseq.n) ) ).(i+1) +rseqb.m by A26
.= (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 SEQ_1:11
.= ((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:7,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:7
.= ((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:10
.= ((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:10
.= (rseq0.m-(seq_id(vseq.n)).(i+1) ) * ((seq_id(vseq.m)).(i+1)
-(seq_id(vseq.n)).(i+1) ) +rseqb.m by A29
.= (rseq0.m-(seq_id(vseq.n)).(i+1) ) * (rseq0.m-(seq_id(vseq.n
)).(i+1) ) +rseqb.m by A29;
end;
A34: rseqb is convergent by A27,A28;
then
lim rseq = ( tseq.(i+1)+-(seq_id(vseq.n)).(i+1) ) * ( tseq.(i+1
)-(seq_id(vseq.n)).(i+1) ) +lim rseqb by A30,A31,A33,Lm5
.= ( tseq.(i+1)+(-seq_id(vseq.n)).(i+1) ) * ( tseq.(i+1)+-(
seq_id(vseq.n)).(i+1) ) + lim rseqb by SEQ_1:10
.= ( tseq.(i+1)+(-seq_id(vseq.n)).(i+1) ) * ( tseq.(i+1)+(-
seq_id(vseq.n)).(i+1) ) + lim rseqb by SEQ_1:10
.= ( tseq+(-seq_id(vseq.n))).(i+1) * ( tseq.(i+1)+(-seq_id(vseq.
n)).(i+1) ) + lim rseqb by SEQ_1:7
.= ( tseq-seq_id(vseq.n)).(i+1) * ( tseq+(-seq_id(vseq.n))).(i+1
) + lim rseqb by SEQ_1:7,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)) (#)(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((seq_id tseq-seq_id(vseq.n)) (#)(seq_id tseq-seq_id(vseq.n)) ).i
by A27,A28
.=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 A34,A30,A33,Lm5;
end;
end;
then
A35: for i be Nat st P[i] holds P[i+1];
now
let rseq be Real_Sequence such that
A36: 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
A37: for m be Nat holds rseq0.m=(seq_id(vseq.m)).0 and
A38: rseq0 is convergent and
A39: tseq.0=lim rseq0 by A15;
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 A36
.=(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 A26
.=( (seq_id(vseq.m)-seq_id(vseq.n) ) (#)(seq_id(vseq.m)-seq_id
(vseq.n) ) ).0 by A26
.= (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 SEQ_1:11
.= ((seq_id(vseq.m)).0+(-seq_id(vseq.n)).0 ) * (seq_id(vseq.m)
+-seq_id(vseq.n) ).0 by SEQ_1:7,11
.= ((seq_id(vseq.m)).0+(-seq_id(vseq.n)).0 ) * ((seq_id(vseq.m
)).0+(-seq_id(vseq.n)).0 ) by SEQ_1:7
.= ((seq_id(vseq.m)).0+-(seq_id(vseq.n)).0 ) * ((seq_id(vseq.m
)).0+(-seq_id(vseq.n)).0 ) by SEQ_1:10
.= ((seq_id(vseq.m)).0-(seq_id(vseq.n)).0 ) * ((seq_id(vseq.m)
).0+-(seq_id(vseq.n)).0 ) by SEQ_1:10
.= (rseq0.m-(seq_id(vseq.n)).0 ) * ((seq_id(vseq.m)).0-(seq_id
(vseq.n)).0 ) by A37
.= (rseq0.m-(seq_id(vseq.n)).0 ) * (rseq0.m-(seq_id(vseq.n)).0
) by A37;
end;
then lim rseq = ( tseq.0+-(seq_id(vseq.n)).0 ) * ( tseq.0-(seq_id(
vseq.n)).0 ) by A38,A39,Lm4
.= ( tseq.0+(-seq_id(vseq.n)).0 ) * ( tseq.0+-(seq_id(vseq.n)).0
) by SEQ_1:10
.= ( tseq.0+(-seq_id(vseq.n)).0 ) * ( tseq.0+(-seq_id(vseq.n)).0
) by SEQ_1:10
.= ( tseq+(-seq_id(vseq.n))).0 * ( tseq.0+(-seq_id(vseq.n)).0 )
by SEQ_1:7
.= ( tseq-seq_id(vseq.n) ).0 * ( tseq+(-seq_id(vseq.n))).0 by
SEQ_1:7,11
.= ( tseq-seq_id(vseq.n)).0 * ( tseq-seq_id(vseq.n)).0 by SEQ_1:11
.= ((tseq-seq_id(vseq.n)) (#)(tseq-seq_id(vseq.n))).0 by SEQ_1:8
.=Partial_Sums(( seq_id tseq-seq_id(vseq.n) ) (#)(seq_id tseq-
seq_id(vseq.n) ) ).0 by SERIES_1:def 1;
hence thesis by A38,A40,Lm4;
end;
end;
then
A41: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A41,A35);
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
A42: n >= k;
A43: 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
A44: for m be Nat holds rseq.m=F(m) from SEQ_1:sch 1;
A45: for m be Nat st m >= k holds rseq.m <= e*e
proof
let m be Nat such that
A46: 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 A21,A42,A46;
then
A47: 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;
A48: rseq.m=Partial_Sums(seq_id(((vseq.m) - (vseq.n))) (#)seq_id(((
vseq.m) - (vseq.n)))).i by A44;
Sum(seq_id(((vseq.m) - (vseq.n))) (#)seq_id(((vseq.m) - (vseq.n
)))) < e*e by A21,A42,A46;
hence thesis by A48,A47,XXREAL_0:2;
end;
rseq is convergent & lim rseq =Partial_Sums((seq_id tseq-seq_id(
vseq.n)) (#) (seq_id tseq-seq_id(vseq.n)) ).i by A25,A44;
hence thesis by A45,Lm3;
end;
now
let i be Nat;
Partial_Sums((seq_id tseq-seq_id(vseq.n)) (#)(seq_id tseq-seq_id(
vseq.n)) ).i <=e*e by A43;
hence
Partial_Sums((seq_id tseq -seq_id(vseq.n)) (#)(seq_id tseq-seq_id
(vseq.n)) ).i < e1*e1 by A20,XXREAL_0:2;
end;
then
A49: Partial_Sums((seq_id tseq-seq_id(vseq.n)) (#)(seq_id tseq-seq_id(
vseq.n)) ) is bounded_above by SEQ_2:def 3;
A50: 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:8;
hence thesis by XREAL_1:63;
end;
then (seq_id tseq-seq_id(vseq.n)) (#)(seq_id tseq-seq_id(vseq.n)) is
summable by A49,SERIES_1:17;
then Partial_Sums( (seq_id tseq-seq_id(vseq.n)) (#)(seq_id tseq-seq_id(
vseq.n)) ) is convergent by SERIES_1:def 2;
then
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)
) ) & lim Partial_Sums((seq_id tseq-seq_id(vseq.n)) (#)(seq_id tseq -seq_id(
vseq.n ))) <=e*e by A43,Lm3,SERIES_1:def 3;
hence thesis by A20,A50,A49,SERIES_1:17,XXREAL_0:2;
end;
hence thesis;
end;
A51: seq_id tseq(#)seq_id tseq is summable
proof
set d=seq_id tseq(#)seq_id tseq;
A52: 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
A53: 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 A16;
set b=seq_id(vseq.m)(#)seq_id(vseq.m);
set a =(seq_id tseq-seq_id(vseq.m))(#)(seq_id tseq-seq_id(vseq.m));
seq_id(vseq.m)(#)seq_id(vseq.m) is summable by RSSPACE:def 11;
then
A54: 2(#)b is summable by SERIES_1:10;
A55: for i be Nat holds d.i <= (2(#)a + 2(#)b).i
proof
let i be Nat;
set x=(seq_id tseq).i;
set y=(seq_id(vseq.m)).i;
A56: 2*(b.i)=2*(y*y) by SEQ_1:8
.=2*y*y;
(seq_id tseq-seq_id(vseq.m)).i = (seq_id tseq+-seq_id(vseq.m)).i
by SEQ_1:11
.= (seq_id tseq).i+(-seq_id(vseq.m)).i by SEQ_1:7
.= (seq_id tseq).i+(-(seq_id(vseq.m)).i) by SEQ_1:10
.= (seq_id tseq).i-(seq_id(vseq.m)).i;
then a.i = ((seq_id tseq).i-(seq_id(vseq.m)).i) *((seq_id tseq).i-(
seq_id(vseq.m)).i) by SEQ_1:8;
then
A57: d.i=((seq_id tseq).i) * ((seq_id tseq).i) & 2*(a.i)=2*(x-y)*(x-y)
by SEQ_1:8;
(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;
hence thesis by A57,A56,Lm2;
end;
(seq_id tseq-seq_id(vseq.m)) (#)( seq_id tseq-seq_id(vseq.m)) is
summable by A53;
then 2(#)a is summable by SERIES_1:10;
then 2(#)a + 2(#)b is summable by A54,SERIES_1:7;
hence thesis by A52,A55,SERIES_1:20;
end;
tseq in the_set_of_RealSequences by FUNCT_2:8;
then reconsider tv=tseq as Point of l2_Space by A51,RSSPACE: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
A58: e > 0;
consider m be Nat such that
A59: 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 A16,A58;
now
tseq in the_set_of_RealSequences by FUNCT_2:8;
then reconsider u=tseq as VECTOR of l2_Space by A51,RSSPACE:def 11;
let n be Nat;
assume n >= m;
then
A60: Sum((seq_id tseq-seq_id(vseq.n)) (#)( seq_id tseq-seq_id(vseq.n)))
< e*e by A59;
reconsider v=vseq.n as VECTOR of l2_Space;
seq_id(u-v)=seq_id tseq-seq_id(vseq.n) by Th1;
then
A61: (u-v).|.(u-v) < e*e by A60,Th1;
A62: ||.(vseq.n) - tv.|| =||.-(tv-(vseq.n)).|| by RLVECT_1:33
.=||.tv-(vseq.n).|| by BHSP_1:31
.=sqrt ((u-v).|.(u-v)) by BHSP_1:def 4;
0 <= (u-v).|.(u-v) by BHSP_1:def 2;
then sqrt ((u-v).|.(u-v)) < sqrt (e^2) by A61,SQUARE_1:27;
hence ||.(vseq.n) - tv.|| < e by A58,A62,SQUARE_1:22;
end;
hence thesis;
end;
hence thesis by BHSP_2:9;
end;
end;
registration
cluster complete for RealUnitarySpace;
existence
proof
take l2_Space;
thus thesis;
end;
end;
definition
mode RealHilbertSpace is complete RealUnitarySpace;
end;
begin :: Miscellaneous
theorem
for r be Real_Sequence st (for n be Nat holds 0 <= r.n)
holds ( for n be Nat holds 0 <= (Partial_Sums r).n ) & ( for n be
Nat holds r.n <= (Partial_Sums r).n ) & ( r is summable implies (
for n be Nat holds (Partial_Sums r).n <= Sum r) &
for n be Nat holds r.n <= Sum r ) 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, s being Real_Sequence st
(s is convergent & ex k
being Nat st for i being Nat st k <= i holds s.i <= e )
holds lim s <=e by Lm3;
theorem
for c being Real, s being Real_Sequence st s is convergent
for r be
Real_Sequence st (for i be Nat holds r.i = (s.i-c)*(s.i-c)) holds r
is convergent & lim r = (lim s-c)*(lim s-c) by Lm4;
theorem
for c being Real, s,s1 being Real_Sequence st s is convergent & s1 is
convergent for r be Real_Sequence st (for i be Nat holds r.i = (s.i-
c)*(s.i-c)+s1.i) holds r is convergent & lim r = (lim s-c)*(lim s-c)+lim s1 by
Lm5;