:: Banach Space of Absolute Summable Real Sequences
:: by Yasumasa Suzuki, Noboru Endou and Yasunari Shidama
::
:: Received August 8, 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, SUBSET_1, RSSPACE, SERIES_1, TARSKI, REAL_1, SEQ_1,
SEQ_2, FUNCT_1, COMPLEX1, ARYTM_1, ORDINAL2, ARYTM_3, CARD_1, XBOOLE_0,
RLSUB_1, RLVECT_1, XXREAL_0, RELAT_1, VALUED_1, ALGSTR_0, CARD_3,
BINOP_1, ZFMISC_1, NORMSP_1, STRUCT_0, SUPINF_2, REALSET1, PRE_TOPC,
METRIC_1, NAT_1, XXREAL_2, RSSPACE3, NORMSP_0, RELAT_2, ASYMPT_1;
notations TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, REALSET1, NUMBERS,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, STRUCT_0, ALGSTR_0, FUNCT_1,
FUNCT_2, RELAT_1, BINOP_1, FUNCOP_1, PRE_TOPC, RLVECT_1, RLSUB_1,
NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SERIES_1, PARTFUN1,
FUNCSDOM, RSSPACE, XXREAL_0;
constructors PARTFUN1, BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1,
SEQ_2, SERIES_1, REALSET1, RLSUB_1, RSSPACE, VALUED_1, RELSET_1, BINOP_2,
RVSUM_1, COMSEQ_2, SEQ_1, FUNCSDOM;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, REALSET1,
STRUCT_0, RLVECT_1, NORMSP_1, RSSPACE, VALUED_1, FUNCT_2, SEQ_4,
VALUED_0, SEQ_1, SEQ_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities BINOP_1, REALSET1, RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0, RSSPACE,
SEQ_1, FUNCSDOM;
expansions NORMSP_0;
theorems XBOOLE_0, RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2,
SERIES_1, COMSEQ_3, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, RLSUB_1, NORMSP_1,
XREAL_0, SEQ_4, RSSPACE, RSSPACE2, COMPLEX1, XREAL_1, XXREAL_0, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2, XBOOLE_0;
begin :: l1_Space:The Space of Absolute Summable Real Sequences
definition
func the_set_of_l1RealSequences -> Subset of Linear_Space_of_RealSequences
means
:Def1:
for x being object holds x in it iff x in the_set_of_RealSequences &
seq_id(x) is absolutely_summable;
existence
proof
defpred P[object] means seq_id($1) is absolutely_summable;
consider IT being set such that
A1: for x being object holds x in IT iff x in the_set_of_RealSequences &
P[x] from XBOOLE_0:sch 1;
for x be object st x in IT holds x in the_set_of_RealSequences by A1;
then IT is Subset of the_set_of_RealSequences by TARSKI:def 3;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of Linear_Space_of_RealSequences;
assume that
A2: for x being object holds x in X1 iff x in the_set_of_RealSequences &
seq_id(x) is absolutely_summable and
A3: for x being object holds x in X2 iff x in the_set_of_RealSequences &
seq_id(x) is absolutely_summable;
for x being object st x in X2 holds x in X1
proof
let x be object;
assume x in X2;
then
x in the_set_of_RealSequences & seq_id(x) is absolutely_summable by A3;
hence thesis by A2;
end;
then
A4: X2 c= X1 by TARSKI:def 3;
for x being object st x in X1 holds x in X2
proof
let x be object;
assume x in X1;
then
x in the_set_of_RealSequences & seq_id(x) is absolutely_summable by A2;
hence thesis by A3;
end;
then X1 c= X2 by TARSKI:def 3;
hence thesis by A4,XBOOLE_0:def 10;
end;
end;
theorem Th1:
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.| )
holds rseq is convergent & lim rseq = |.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: abs(seq -cseq) is convergent;
let rseq be Real_Sequence such that
A4: for i be Nat holds rseq .i = |.seq.i-c.|;
now
let i be Nat;
thus rseq.i=|.seq.i-c.| by A4
.=|.seq.i-(cseq.i).|by SEQ_1:57
.=|.seq.i+-(cseq.i).|
.=|.seq.i+(-cseq).i.| by SEQ_1:10
.=|.(seq+(-cseq)).i.| by SEQ_1:7
.=|.(seq -cseq ).i.| by SEQ_1:11
.=abs(seq -cseq).i by SEQ_1:12;
end;
then
A5: for x be object st x in NAT holds rseq.x = abs(seq -cseq).x;
lim abs(seq -cseq) = |.lim(seq-cseq).| by A2,SEQ_4:14
.=|.lim seq-lim cseq.| by A1,SEQ_2:12
.=|.lim seq-(cseq.0).| by SEQ_4:26
.=|.lim seq-c.| by SEQ_1:57;
hence thesis by A5,A3,FUNCT_2:12;
end;
registration
cluster the_set_of_l1RealSequences -> non empty;
coherence
proof
seq_id Zeroseq is absolutely_summable
proof
reconsider rseq=seq_id Zeroseq as Real_Sequence;
for n being Nat holds rseq.n = 0;
hence thesis by COMSEQ_3:3;
end;
hence thesis by Def1;
end;
end;
registration
cluster the_set_of_l1RealSequences -> linearly-closed;
coherence
proof
set W = the_set_of_l1RealSequences;
A1: for v,u be VECTOR of Linear_Space_of_RealSequences st v in
the_set_of_l1RealSequences & u in the_set_of_l1RealSequences holds v + u in
the_set_of_l1RealSequences
proof
let v,u be VECTOR of Linear_Space_of_RealSequences such that
A2: v in W and
A3: u in W;
seq_id(v+u) is absolutely_summable
proof
set r = abs seq_id(v+u);
set q = abs seq_id u;
set p = abs seq_id v;
A4: for n be Nat holds 0<=r.n
proof
let n be Nat;
r.n=|.(seq_id(v+u)).n.| by SEQ_1:12;
hence thesis by COMPLEX1:46;
end;
A5: for n be Nat holds r.n <=(p+q).n
proof
let n be Nat;
A6: |.(seq_id v).n.|+|.(seq_id u).n.| = abs(seq_id v).n + |.(
seq_id u).n.| by SEQ_1:12
.= abs(seq_id v).n+ abs(seq_id u).n by SEQ_1:12
.= (p + q).n by SEQ_1:7;
r.n=|.(seq_id(v+u)).n.| by SEQ_1:12
.=|.(seq_id(seq_id(v) + seq_id(u))).n.| by RSSPACE:2
.=|.(seq_id v).n + (seq_id u).n.| by SEQ_1:7;
hence thesis by A6,COMPLEX1:56;
end;
seq_id u is absolutely_summable by A3,Def1;
then
A7: q is summable by SERIES_1:def 4;
seq_id v is absolutely_summable by A2,Def1;
then p is summable by SERIES_1:def 4;
then p+q is summable by A7,SERIES_1:7;
then r is summable by A4,A5,SERIES_1:20;
hence thesis by SERIES_1:def 4;
end;
hence thesis by Def1;
end;
for a be Real
for v be VECTOR of Linear_Space_of_RealSequences st v
in W holds a * v in W
proof
let a be Real;
let v be VECTOR of Linear_Space_of_RealSequences such that
A8: v in W;
seq_id(a*v) is absolutely_summable
proof
set r1 = |.a.|(#)abs(seq_id v);
set q1 = abs seq_id(a*v);
A9: for n be Nat holds 0<=q1.n
proof
let n be Nat;
q1.n=|.(seq_id(a*v)).n.| by SEQ_1:12;
hence thesis by COMPLEX1:46;
end;
A10: for n be Nat holds q1.n <=r1.n
proof
let n be Nat;
q1.n=|.(seq_id(a*v)).n.| by SEQ_1:12
.=|.(seq_id(a(#)seq_id v)).n.| by RSSPACE:3
.=abs(a(#)seq_id v).n by SEQ_1:12;
hence thesis by SEQ_1:56;
end;
seq_id v is absolutely_summable by A8,Def1;
then abs seq_id v is summable by SERIES_1:def 4;
then r1 is summable by SERIES_1:10;
then q1 is summable by A9,A10,SERIES_1:20;
hence thesis by SERIES_1:def 4;
end;
hence thesis by Def1;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
end;
Lm1: RLSStruct (# the_set_of_l1RealSequences, Zero_(the_set_of_l1RealSequences
,Linear_Space_of_RealSequences), Add_(the_set_of_l1RealSequences,
Linear_Space_of_RealSequences), Mult_(the_set_of_l1RealSequences,
Linear_Space_of_RealSequences) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:11;
registration
cluster RLSStruct (# the_set_of_l1RealSequences, Zero_(
the_set_of_l1RealSequences,Linear_Space_of_RealSequences), Add_(
the_set_of_l1RealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_l1RealSequences,Linear_Space_of_RealSequences) #) -> Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by RSSPACE:11;
end;
Lm2: RLSStruct (# the_set_of_l1RealSequences, Zero_(the_set_of_l1RealSequences
,Linear_Space_of_RealSequences), Add_(the_set_of_l1RealSequences,
Linear_Space_of_RealSequences), Mult_(the_set_of_l1RealSequences,
Linear_Space_of_RealSequences) #) is RealLinearSpace;
definition
func l_norm -> Function of the_set_of_l1RealSequences, REAL means
:Def2:
for x be object st x in the_set_of_l1RealSequences
holds it.x = Sum abs seq_id x;
existence
proof
deffunc F(object) = Sum abs seq_id $1;
A1: for z be object st z in the_set_of_l1RealSequences holds F(z) in REAL
by XREAL_0:def 1;
ex f being Function of the_set_of_l1RealSequences,REAL st for x being
object st x in the_set_of_l1RealSequences holds f.x = F(x)
from FUNCT_2:sch 2(A1);
hence thesis;
end;
uniqueness
proof
let NORM1,NORM2 be Function of the_set_of_l1RealSequences, REAL such that
A2: for x be object st x in the_set_of_l1RealSequences holds NORM1.x =
Sum abs seq_id x and
A3: for x be object st x in the_set_of_l1RealSequences holds NORM2.x =
Sum abs seq_id x;
A4: for z be object st z in the_set_of_l1RealSequences
holds NORM1.z = NORM2. z
proof
let z be object such that
A5: z in the_set_of_l1RealSequences;
NORM1.z = Sum abs seq_id z by A2,A5;
hence thesis by A3,A5;
end;
dom NORM1 = the_set_of_l1RealSequences & dom NORM2 =
the_set_of_l1RealSequences by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:2;
end;
end;
registration
let X be non empty set, Z be Element of X, A be BinOp of X, M be Function of
[:REAL, X:], X, N be Function of X, REAL;
cluster NORMSTR (# X, Z, A, M, N #) -> non empty;
coherence;
end;
theorem
for l be NORMSTR st the RLSStruct of l is RealLinearSpace holds l is
RealLinearSpace by RSSPACE:15;
theorem Th3:
for rseq be Real_Sequence st (for n be Nat holds rseq.
n=0) holds rseq is absolutely_summable & Sum abs rseq = 0
proof
let rseq be Real_Sequence such that
A1: for n be Nat holds rseq.n=0;
A2: for n be Nat holds (abs rseq).n=0
proof
let n be Nat;
rseq.n=0 & (abs rseq).n = |.rseq.n.| by A1,SEQ_1:12;
hence thesis by ABSVALUE:2;
end;
A3: for m be Nat holds Partial_Sums (abs(rseq)).m = 0
proof
defpred P[Nat] means
(abs rseq).$1 = (Partial_Sums abs rseq).$1;
let m be Nat;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: (abs rseq).k = (Partial_Sums (abs rseq)).k;
thus (abs rseq).(k+1) = 0 + (abs rseq).(k+1)
.= (abs rseq).k + (abs rseq).(k+1) by A2
.= (Partial_Sums abs rseq).(k+1) by A5,SERIES_1:def 1;
end;
A6: P[0] by SERIES_1:def 1;
for n be Nat holds P[n] from NAT_1:sch 2(A6,A4);
hence (Partial_Sums abs rseq).m = (abs rseq).m .= 0 by A2;
end;
A7: for p be Real st 0<p ex n be Nat st
for m be Nat st n<=m holds |.(Partial_Sums abs rseq).m-0 .|<p
proof
let p be Real such that
A8: 0<p;
take 0;
let m be Nat such that
0<=m;
|.(Partial_Sums abs rseq).m-0 .| = |.0-0 .| by A3
.= 0 by ABSVALUE:def 1;
hence thesis by A8;
end;
then
A9: Partial_Sums abs rseq is convergent by SEQ_2:def 6;
then
A10: abs rseq is summable by SERIES_1:def 2;
lim Partial_Sums abs rseq =0 by A7,A9,SEQ_2:def 7;
hence thesis by A10,SERIES_1:def 3,def 4;
end;
theorem Th4:
for rseq be Real_Sequence st rseq is absolutely_summable & Sum
abs rseq=0 holds for n be Nat holds rseq.n =0
proof
let rseq being Real_Sequence such that
A1: rseq is absolutely_summable and
A2: Sum abs rseq=0;
reconsider arseq = abs rseq as Real_Sequence;
A3: for n be Nat holds 0 <= (abs rseq).n
proof
let n be Nat;
0 <= |.rseq.n.| by COMPLEX1:46;
hence thesis by SEQ_1:12;
end;
A4: arseq is summable by A1,SERIES_1:def 4;
let n be Nat;
(abs rseq).n =0 by A2,A4,A3,RSSPACE:17;
then |.rseq.n.|=0 by SEQ_1:12;
hence thesis by ABSVALUE:2;
end;
theorem Th5:
NORMSTR (# the_set_of_l1RealSequences, Zero_(
the_set_of_l1RealSequences,Linear_Space_of_RealSequences), Add_(
the_set_of_l1RealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_l1RealSequences,Linear_Space_of_RealSequences), l_norm #) is
RealLinearSpace by Lm2,RSSPACE:15;
definition
func l1_Space -> non empty NORMSTR equals
NORMSTR (#
the_set_of_l1RealSequences, Zero_(the_set_of_l1RealSequences,
Linear_Space_of_RealSequences), Add_(the_set_of_l1RealSequences,
Linear_Space_of_RealSequences), Mult_(the_set_of_l1RealSequences,
Linear_Space_of_RealSequences), l_norm #);
coherence;
end;
begin :: l1_Space is Banach
theorem Th6:
the carrier of l1_Space = the_set_of_l1RealSequences & ( for x be
set holds x is VECTOR of l1_Space iff x is Real_Sequence & seq_id x is
absolutely_summable ) & 0.l1_Space = Zeroseq & ( for u be VECTOR of l1_Space
holds u =seq_id u ) & ( for u,v be VECTOR of l1_Space holds u+v =seq_id(u)+
seq_id(v) ) &
( for r be Real for u be VECTOR of l1_Space holds r*u =r(#)seq_id
(u) ) & ( for u be VECTOR of l1_Space holds -u = -seq_id u & seq_id(-u) = -
seq_id(u) ) & ( for u,v be VECTOR of l1_Space holds u-v =seq_id(u)-seq_id v ) &
( for v be VECTOR of l1_Space holds seq_id v is absolutely_summable ) & for v
be VECTOR of l1_Space holds ||.v.|| = Sum abs seq_id v
proof
set l1 =l1_Space;
A1: for x be set holds x is Element of l1 iff x is Real_Sequence & seq_id x
is absolutely_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 Def1;
end;
A2: for u,v be VECTOR of l1 holds u+v =seq_id(u)+seq_id(v)
proof
let u,v be VECTOR of l1;
reconsider u1=u, v1=v as VECTOR of Linear_Space_of_RealSequences by Lm1,
RLSUB_1:10;
set L1=Linear_Space_of_RealSequences;
set W = the_set_of_l1RealSequences;
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
A3: [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 A3,FUNCT_1:47;
hence thesis by RSSPACE:2;
end;
A4: for r be Real for u be VECTOR of l1 holds r*u =r(#)seq_id(u)
proof
let r be Real;
let u be VECTOR of l1;
reconsider r as Element of REAL by XREAL_0:def 1;
reconsider u1=u as VECTOR of Linear_Space_of_RealSequences by Lm1,
RLSUB_1:10;
set L1=Linear_Space_of_RealSequences;
set W = the_set_of_l1RealSequences;
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
A5: [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 A5,FUNCT_1:47;
hence thesis by RSSPACE:3;
end;
A6: for u be VECTOR of l1 holds u =seq_id u
proof
let u be VECTOR of l1;
u is VECTOR of Linear_Space_of_RealSequences by Lm1,RLSUB_1:10;
hence thesis;
end;
A7: for u be VECTOR of l1 holds -u =-seq_id u & seq_id(-u)=-seq_id u
proof
let u be VECTOR of l1;
-u = (-1)*u by Th5,RLVECT_1:16
.= (-1)(#)seq_id(u) by A4
.= -seq_id(u) by SEQ_1:17;
hence thesis;
end;
A8: for u,v be VECTOR of l1 holds u-v =seq_id(u)-seq_id(v)
proof
let u,v be VECTOR of l1;
thus u-v = seq_id(u)+seq_id(-v) by A2
.= seq_id(u)+(-seq_id(v)) by A7
.= seq_id(u)-seq_id(v) by SEQ_1:11;
end;
A9: for v be VECTOR of l1 holds ||.v.|| = Sum abs seq_id v
by Def2;
0.l1 = 0.Linear_Space_of_RealSequences by RSSPACE:def 10
.= Zeroseq;
hence thesis by A1,A6,A2,A4,A7,A8,A9;
end;
theorem Th7:
for x, y being Point of l1_Space, a be Real holds ( ||.x.|| = 0
iff x = 0.l1_Space ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| & ||. a*x
.|| = |.a.| * ||.x.||
proof
let x, y be Point of l1_Space;
let a be Real;
A1: for n be Nat holds 0 <= abs(seq_id x).n
proof
let n be Nat;
0 <= |.(seq_id x).n.| by COMPLEX1:46;
hence thesis by SEQ_1:12;
end;
A2: now
let n be Nat;
(abs(seq_id(x+y))).n = |.(seq_id(x+y)).n.| by SEQ_1:12;
hence 0 <= (abs(seq_id(x+y))).n by COMPLEX1:46;
end;
A3: for n be Nat holds (abs seq_id(x+y)).n = |.((seq_id x).n)
+ ((seq_id y).n).|
proof
let n be Nat;
(abs seq_id(x+y)).n = (abs(seq_id(seq_id(x)+seq_id y))).n by Th6
.= |.(seq_id x+seq_id y).n.| by SEQ_1:12
.= |.((seq_id x).n)+((seq_id y).n).| by SEQ_1:7;
hence thesis;
end;
A4: for n be Nat holds (abs seq_id(x+y)).n <= (abs seq_id x).n +
(abs seq_id y).n
proof
let n be Nat;
(|.((seq_id x).n)+ ((seq_id y).n).|) <= |.(seq_id x).n.| + |.(
seq_id y).n.| by COMPLEX1:56;
then
(abs(seq_id(x+y))) .n <= |.(seq_id x).n.| + |.(seq_id y).n.| by A3;
then
(abs(seq_id(x+y))) .n <= (abs(seq_id x)).n + |.(seq_id y).n.| by SEQ_1:12;
hence thesis by SEQ_1:12;
end;
A5: for n being Nat holds (abs(seq_id(x+y))).n <= ((abs seq_id x
) + (abs seq_id y)).n
proof
let n be Nat;
(abs seq_id x).n + (abs seq_id y).n =((abs seq_id x) + (abs seq_id y)
).n by SEQ_1:7;
hence thesis by A4;
end;
seq_id y is absolutely_summable by Def1;
then
A6: abs seq_id y is summable by SERIES_1:def 4;
seq_id x is absolutely_summable by Def1;
then abs seq_id x is summable by SERIES_1:def 4;
then (abs seq_id x) + (abs seq_id y) is summable by A6,SERIES_1:7;
then
A7: Sum(abs(seq_id(x+y))) <= Sum((abs seq_id x) + (abs seq_id y)) by A5,A2,
SERIES_1:20;
A8: now
assume x=0.l1_Space;
then
A9: for n be Nat holds (seq_id x).n=0 by Th6;
thus ||.x.|| = Sum abs seq_id x by Def2
.= 0 by A9,Th3;
end;
A10: Sum abs seq_id(x+y) = ||.x + y.|| by Th6;
A11: now
A12: x in the_set_of_RealSequences by Def1;
assume
A13: ||.x.|| = 0;
||.x.|| = Sum abs seq_id x & seq_id(x) is absolutely_summable by Th6;
then for n be Nat holds 0 = (seq_id x).n by A13,Th4;
hence x=0.l1_Space by A12,Th6,RSSPACE:5;
end;
A14: ||.x.|| = Sum abs seq_id x & ||.y.|| = Sum abs seq_id y by Th6;
A15: for n be Nat holds (abs(a(#)seq_id(x))).n =|.a.|*(abs(
seq_id x).n)
proof
let n be Nat;
(abs(a(#)seq_id(x))).n =|.(a(#)seq_id(x)).n.| by SEQ_1:12
.=|.a*((seq_id x).n).| by SEQ_1:9
.=|.a.|*(|.(seq_id x).n.|) by COMPLEX1:65
.=|.a.|*(abs(seq_id x).n) by SEQ_1:12;
hence thesis;
end;
seq_id x is absolutely_summable by Def1;
then
A16: abs seq_id x is summable by SERIES_1:def 4;
seq_id x is absolutely_summable by Def1;
then
A17: abs seq_id x is summable by SERIES_1:def 4;
||.(a*x).|| =Sum(abs(seq_id(a*x))) by Th6
.=Sum(|.seq_id(a(#)seq_id(x)).|) by Th6
.=Sum(|.a.| (#) (abs seq_id x)) by A15,SEQ_1:9
.=|.a.|*Sum(abs seq_id x) by A16,SERIES_1:10
.=|.a.|*||.x.|| by Th6;
hence thesis by A11,A8,A1,A17,A14,A10,A6,A7,SERIES_1:7,18;
end;
registration
cluster l1_Space -> reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence
by Th7,Lm2,NORMSP_1:def 1,RSSPACE:15;
end;
Lm3: 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.|+seq1.i) holds rseq is convergent & lim rseq =|.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: abs(seq- cseq) is convergent;
let rseq be Real_Sequence such that
A5: for i be Nat holds rseq .i = |.seq.i-c.|+seq1.i;
now
let i be Element of NAT;
thus rseq.i=|.seq.i-c.|+seq1.i by A5
.=|.seq.i-cseq.i.|+seq1.i by SEQ_1:57
.=|.seq.i+(-cseq.i).|+seq1.i
.=|.seq.i+(-cseq).i.|+seq1.i by SEQ_1:10
.=|.(seq+ -cseq).i.| + seq1.i by SEQ_1:7
.=|.(seq-cseq).i.| + seq1.i by SEQ_1:11
.=abs(seq-cseq).i + seq1.i by SEQ_1:12
.=(abs(seq-cseq) + seq1).i by SEQ_1:7;
end;
then
A6: rseq = (abs(seq-(cseq)) + seq1) by FUNCT_2:63;
lim abs(seq-cseq) = |.lim(seq-cseq).| by A3,SEQ_4:14
.= |.lim seq - lim cseq.| by A1,SEQ_2:12
.= |.lim seq - (cseq.0).| by SEQ_4:26
.= |.lim seq - c.| by SEQ_1:57;
hence thesis by A2,A6,A4,SEQ_2:6;
end;
definition
let X be non empty NORMSTR, x, y be Point of X;
func dist(x,y) -> Real equals
||.x - y.||;
coherence;
end;
reserve NRM for non empty RealNormSpace;
reserve seq for sequence of NRM;
definition
let NRM be non empty NORMSTR;
let seqt be sequence of NRM;
attr seqt is CCauchy means
for r1 be Real st r1 > 0
ex k1 be Nat st
for n1, m1 be Nat st n1 >= k1 & m1 >= k1 holds dist(seqt.n1, seqt.m1) < r1;
end;
notation
let NRM be non empty NORMSTR;
let seqt be sequence of NRM;
synonym seqt is Cauchy_sequence_by_Norm for seqt is CCauchy;
end;
theorem Th8:
seq is Cauchy_sequence_by_Norm iff for r be Real st r > 0
ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.(
seq.n) - (seq.m).|| < r
proof
thus seq is Cauchy_sequence_by_Norm implies
for r be Real st r > 0
ex k be Nat st for n, m be Nat st n >= k & m >= k holds ||.(seq.n
) - (seq.m).|| < r
proof
assume
A1: seq is Cauchy_sequence_by_Norm;
let r be Real;
assume r > 0;
then consider k be Nat such that
A2: for n, m be Nat st n >= k & m >= k holds dist(seq.n,
seq.m) < r by A1;
for n, m be Nat st n >= k & m >= k holds ||.(seq.n) - (seq.
m).|| < r
proof
let n,m be Nat;
assume n >= k & m >= k;
then dist(seq.n, seq.m) < r by A2;
hence thesis;
end;
hence thesis;
end;
assume
A3: for r be Real st r > 0 ex k be Nat st for n, m be
Nat st n >= k & m >= k holds ||.(seq.n) - (seq.m).|| < r;
now
let r be Real;
assume
A4: r > 0;
now
consider k be Nat such that
A5: for n, m be Nat st n >= k & m >= k holds ||.(seq.n
) - (seq.m).|| < r by A3,A4;
for n,m be Nat st n >= k & m >= k holds dist(seq.n,
seq.m) < r by A5;
hence ex k be Nat st for n, m be Nat st n >= k &
m >= k holds dist(seq.n, seq.m) < r;
end;
hence ex k be Nat st for n, m be Nat st n >= k & m
>= k holds dist(seq.n, seq.m) < r;
end;
hence thesis;
end;
theorem
for vseq be sequence of l1_Space st vseq is Cauchy_sequence_by_Norm
holds vseq is convergent
proof
let vseq be sequence of l1_Space such that
A1: vseq is Cauchy_sequence_by_Norm;
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 Nat;
deffunc F(Nat) = (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,Th8;
for m being Nat st k <= m holds |.rseqi.m-rseqi.k.| < e
proof
let m be Nat such that
A6: k<=m;
A7: for i be Nat holds 0 <= |.seq_id((vseq.m) - (vseq.
k)).|. i
proof
let i be Nat;
0 <= |.(seq_id((vseq.m) - (vseq.k))).i.| by COMPLEX1:46;
hence thesis by SEQ_1:12;
end;
seq_id((vseq.m)-(vseq.k)) is absolutely_summable by Def1;
then abs(seq_id((vseq.m)-(vseq.k))) is summable by SERIES_1:def 4;
then
A8: abs(seq_id((vseq.m) - (vseq.k))).i <= Sum(|.seq_id((vseq.m) -
(vseq.k)).|) by A7,RSSPACE2:3;
seq_id((vseq.m) - (vseq.k)) =seq_id(seq_id((vseq.m))-seq_id((
vseq.k))) by Th6
.= 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
A9: |.rseqi.m-rseqi.k.| = abs(seq_id((vseq.m) - (vseq.k))).i by SEQ_1:12;
||.(vseq.m) - (vseq.k).|| =Sum(|.seq_id((vseq.m) - (vseq.k)).|
) by Th6;
then Sum(|.seq_id((vseq.m) - (vseq.k)).|) < e by A5,A6;
hence thesis by A8,A9,XXREAL_0:2;
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
A10: 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;
A11: 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 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 A10;
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;
A12: for e be Real
st e >0 ex k be Nat st for n be Nat
st n >= k holds abs(seq_id tseq-seq_id(vseq.n)) is summable & Sum(abs(seq_id
tseq-seq_id(vseq.n))) < e
proof
let e1 be Real such that
A13: e1 >0;
reconsider e1 as Real;
set e=e1/2;
A14: e < e1 by A13,XREAL_1:216;
e > 0 by A13,XREAL_1:215;
then consider k be Nat such that
A15: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A1,Th8;
A16: for m,n be Nat st n >= k & m >= k holds ( abs(seq_id((vseq
.n) - (vseq.m))) is summable & Sum(abs(seq_id((vseq.n) - (vseq.m)))) < e & for
i be Nat holds 0 <= abs(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 A15;
then
A17: (the normF of l1_Space).((vseq.n) - (vseq.m)) < e;
A18: for i be Nat holds 0 <= abs(seq_id((vseq.n) - (vseq.m))) .i
proof
let i be Nat;
0 <= |.(seq_id((vseq.n) - (vseq.m))).i.| by COMPLEX1:46;
hence thesis by SEQ_1:12;
end;
seq_id(((vseq.n) - (vseq.m))) is absolutely_summable by Def1;
hence thesis by A17,A18,Def2,SERIES_1:def 4;
end;
A19: for n be Nat for i be Nat holds for rseq be
Real_Sequence st ( for m be Nat holds rseq.m=Partial_Sums(abs(seq_id
((vseq.m)-(vseq.n)))).i ) holds rseq is convergent & lim rseq = Partial_Sums(
abs(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(abs(seq_id((vseq.m) - (vseq.n)))).$1
holds rseq is convergent & lim rseq = Partial_Sums(abs(seq_id tseq-seq_id(vseq.
n))).$1;
A20: 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;
seq_id((vseq.m) - (vseq.k)) = seq_id(seq_id((vseq.m))-seq_id((
vseq.k))) by Th6;
hence thesis;
end;
now
let i be Nat such that
A21: for rseq be Real_Sequence st ( for m be Nat holds
rseq.m= Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).i ) holds rseq is
convergent & lim rseq = Partial_Sums(abs((seq_id tseq - seq_id(vseq.n)))).i;
thus for rseq be Real_Sequence st ( for m be Nat holds rseq
.m = Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).(i+1) ) holds rseq is
convergent & lim rseq =Partial_Sums(abs((seq_id tseq - seq_id(vseq.n)))).(i+1)
proof
deffunc F(Nat) = Partial_Sums(abs(seq_id((vseq.$1) - (
vseq.n)))).i;
consider rseqb be Real_Sequence such that
A22: for m be Nat holds rseqb.m = F(m) from SEQ_1:sch 1;
consider rseq0 be Real_Sequence such that
A23: for m be Nat holds rseq0.m=(seq_id(vseq.m)).(i+1 ) and
A24: rseq0 is convergent and
A25: tseq.(i+1)=lim rseq0 by A11;
let rseq be Real_Sequence such that
A26: for m be Nat holds rseq.m = Partial_Sums(abs(
seq_id((vseq.m) - (vseq.n)))).(i+1);
A27: now
let m be Nat;
thus rseq.m = Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).(i+1)
by A26
.=abs(seq_id((vseq.m) - (vseq.n))).(i+1) +Partial_Sums(abs(
seq_id((vseq.m) - (vseq.n)))).i by SERIES_1:def 1
.=abs(seq_id(vseq.m)-seq_id(vseq.n)).(i+1) +Partial_Sums(abs(
seq_id((vseq.m) - (vseq.n)))).i by A20
.=abs(seq_id(vseq.m)-seq_id(vseq.n)).(i+1) + rseqb.m by A22
.=|.(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).| + rseqb.m by
SEQ_1:11
.=|.(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).| + rseqb.
m by SEQ_1:10
.= |.(seq_id(vseq.m)).(i+1)-(seq_id(vseq.n)).(i+1).| + rseqb.
m
.= |.rseq0.m-(seq_id(vseq.n)).(i+1).| + rseqb.m by A23;
end;
A28: rseqb is convergent by A21,A22;
then lim rseq = |.lim(rseq0)-(seq_id(vseq.n)).(i+1).| + lim rseqb
by A24,A27,Lm3
.= |.tseq.(i+1)+-(seq_id(vseq.n)).(i+1).| + lim rseqb by A25
.= |.tseq.(i+1)+(-seq_id(vseq.n)).(i+1).| + lim rseqb by SEQ_1:10
.= |.(tseq+(-seq_id(vseq.n))).(i+1).| + lim rseqb by SEQ_1:7
.= |.(tseq-(seq_id(vseq.n))).(i+1).| + lim rseqb by SEQ_1:11
.= abs(tseq-(seq_id(vseq.n))).(i+1) + lim rseqb by SEQ_1:12
.= abs(tseq-(seq_id(vseq.n))).(i+1) + Partial_Sums(abs((seq_id
tseq -seq_id(vseq.n)))).i by A21,A22
.= Partial_Sums (abs((seq_id tseq -seq_id(vseq.n)))).(i+1) by
SERIES_1:def 1;
hence thesis by A28,A24,A27,Lm3;
end;
end;
then
A29: for i be Nat st P[i] holds P[i+1];
now
let rseq be Real_Sequence such that
A30: for m be Nat holds rseq.m=Partial_Sums(abs(seq_id(
(vseq.m) - (vseq.n)))).0;
thus rseq is convergent & lim rseq = Partial_Sums(abs(seq_id tseq-
seq_id(vseq.n))).0
proof
consider rseq0 be Real_Sequence such that
A31: for m be Nat holds rseq0.m=(seq_id(vseq.m)).0 and
A32: rseq0 is convergent and
A33: tseq.0=lim rseq0 by A11;
A34: for m being Nat holds rseq.m = |.rseq0.m-(seq_id((
vseq.n))).0 .|
proof
let m be Nat;
rseq.m=Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).0 by A30
.=(abs(seq_id((vseq.m) - (vseq.n)))).0 by SERIES_1:def 1
.=(abs(seq_id(vseq.m)-seq_id(vseq.n))).0 by A20
.=(abs(seq_id(vseq.m)+-seq_id(vseq.n))).0 by SEQ_1:11
.=|.(seq_id(vseq.m)+-seq_id(vseq.n)).0 .| by SEQ_1:12
.=|.(seq_id(vseq.m)).0+(-seq_id(vseq.n)).0 .| by SEQ_1:7
.=|.(seq_id(vseq.m)).0+-(seq_id(vseq.n)).0 .| by SEQ_1:10
.=|.(seq_id(vseq.m)).0-(seq_id(vseq.n)).0 .|;
hence thesis by A31;
end;
then lim rseq = |.lim(rseq0) -((seq_id(vseq.n)).0 ).| by A32,Th1
.= |.tseq.0+-((seq_id(vseq.n)).0).| by A33
.= |.tseq.0+(-(seq_id(vseq.n))).0 .| by SEQ_1:10
.= |.(tseq+(-seq_id((vseq.n)))).0 .| by SEQ_1:7
.= |.(tseq-(seq_id((vseq.n)))).0 .| by SEQ_1:11
.= abs(seq_id tseq-(seq_id(vseq.n))).0 by SEQ_1:12
.=Partial_Sums(abs(seq_id tseq-(seq_id(vseq.n)))).0 by
SERIES_1:def 1;
hence thesis by A32,A34,Th1;
end;
end;
then
A35: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A35,A29);
hence thesis;
end;
for n be Nat st n >= k holds abs(seq_id tseq-seq_id(vseq.n
)) is summable & Sum abs(seq_id tseq-seq_id(vseq.n)) < e1
proof
let n be Nat such that
A36: n >= k;
A37: for i be Nat st 0 <= i holds Partial_Sums(abs((seq_id
tseq -seq_id(vseq.n)))).i <=e
proof
let i be Nat such that
0 <=i;
deffunc F(Nat)= Partial_Sums(abs(seq_id((vseq.$1) - (vseq.n
)))).i;
consider rseq be Real_Sequence such that
A38: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
A39: for m be Nat st m >= k holds rseq.m <= e
proof
let m be Nat;
A40: rseq.m = Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).i by A38;
assume
A41: m >= k;
then
abs(seq_id((vseq.m) - (vseq.n))) is summable &
for i be Nat holds 0 <= abs(seq_id((vseq.m) - (vseq.n))).i
by A16,A36;
then
A42: Partial_Sums(abs(seq_id((vseq.m) - (vseq.n)))).i <=Sum(abs(
seq_id((vseq.m) - (vseq.n)))) by RSSPACE2:3;
Sum(abs(seq_id((vseq.m) - (vseq.n)))) < e by A16,A36,A41;
hence thesis by A42,A40,XXREAL_0:2;
end;
rseq is convergent & lim rseq = Partial_Sums(abs(seq_id tseq-
seq_id(vseq.n)) ).i by A19,A38;
hence thesis by A39,RSSPACE2:5;
end;
now
take e1;
let i be Nat;
Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))).i <=e by A37,NAT_1:2;
hence Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))).i < e1 by A14,
XXREAL_0:2;
end;
then
A43: Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))) is bounded_above
by SEQ_2:def 3;
A44: for i be Nat holds 0 <= abs(seq_id tseq-seq_id(vseq.n)). i
proof
let i be Nat;
abs(seq_id tseq -seq_id(vseq.n)).i =|.(seq_id tseq -seq_id(vseq
.n)).i.| by SEQ_1:12;
hence thesis by COMPLEX1:46;
end;
then abs((seq_id tseq-seq_id(vseq.n))) is summable by A43,SERIES_1:17;
then Partial_Sums(abs((seq_id tseq -seq_id(vseq.n)))) is convergent by
SERIES_1:def 2;
then Sum(abs((seq_id tseq -seq_id(vseq.n)))) = lim Partial_Sums(abs((
seq_id tseq - seq_id(vseq.n)))) & lim Partial_Sums(abs((seq_id tseq -seq_id(
vseq.n)))) <= e by A37,RSSPACE2:5,SERIES_1:def 3;
hence thesis by A14,A44,A43,SERIES_1:17,XXREAL_0:2;
end;
hence thesis;
end;
abs seq_id tseq is summable
proof
set d=abs seq_id tseq;
A45: for i be Nat holds 0 <= abs(seq_id tseq).i
proof
let i be Nat;
abs(seq_id tseq).i = |.(seq_id tseq).i.| by SEQ_1:12;
hence thesis by COMPLEX1:46;
end;
consider m be Nat such that
A46: for n be Nat st n >= m holds abs((seq_id tseq -seq_id(
vseq.n))) is summable & Sum(abs((seq_id tseq -seq_id(vseq.n)))) < 1 by A12;
set b=abs seq_id(vseq.m);
set a=abs(seq_id tseq -seq_id(vseq.m));
seq_id(vseq.m) is absolutely_summable by Def1;
then
A47: abs(seq_id(vseq.m)) is summable by SERIES_1:def 4;
A48: for i be Nat holds d.i <= (a+b).i
proof
let i be Nat;
A49: b.i=|.(seq_id(vseq.m)).i.| & d.i=|.(seq_id tseq).i.| by SEQ_1:12;
a.i = |.(seq_id tseq -seq_id(vseq.m)).i.| by SEQ_1:12
.= |.(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 d.i-b.i <= a.i by A49,COMPLEX1:59;
then d.i-b.i+b.i<= a.i + b.i by XREAL_1:6;
hence thesis by SEQ_1:7;
end;
abs((seq_id tseq -seq_id(vseq.m))) is summable by A46;
then a + b is summable by A47,SERIES_1:7;
hence thesis by A45,A48,SERIES_1:20;
end;
then
A50: seq_id tseq is absolutely_summable by SERIES_1:def 4;
A51: tseq in the_set_of_RealSequences by FUNCT_2:8;
then reconsider tv=tseq as Point of l1_Space by A50,Def1;
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;
assume e > 0;
then consider m be Nat such that
A52: for n be Nat st n >= m holds abs(seq_id tseq-seq_id(
vseq.n)) is summable & Sum(abs(seq_id tseq-seq_id(vseq.n))) < e by A12;
reconsider m as Element of NAT by ORDINAL1:def 12;
take m;
reconsider u=tseq as VECTOR of l1_Space by A50,A51,Def1;
let n be Nat;
assume n >= m;
then
A53: Sum abs(seq_id tseq-seq_id(vseq.n)) < e by A52;
reconsider v=vseq.n as VECTOR of l1_Space;
seq_id(u-v) = u-v by Th6;
then Sum abs seq_id(u-v) = Sum abs(seq_id tseq-seq_id(vseq.n)) by Th6;
then
A54: (the normF of l1_Space).(u-v) < e by A53,Def2;
||.(vseq.n) - tv.|| =||.-(tv-(vseq.n)).|| by RLVECT_1:33
.=||.tv-(vseq.n).|| by NORMSP_1:2;
hence ||.(vseq.n) - tv.|| < e by A54;
end;
hence thesis by NORMSP_1:def 6;
end;