:: Banach Space of Absolute Summable Real Sequences :: by Yasumasa Suzuki, Noboru Endou and Yasunari Shidama :: :: Received August 8, 2003 :: Copyright (c) 2003-2021 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
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;