:: Banach Space of Absolute Summable Complex Sequences :: by Noboru Endou :: :: Received February 24, 2004 :: Copyright (c) 2004-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, CSSPACE, RSSPACE, SERIES_1, TARSKI, XCMPLX_0, COMSEQ_1, SEQ_1, SEQ_2, FUNCT_1, COMPLEX1, ARYTM_1, ORDINAL2, FUNCOP_1, ARYTM_3, XBOOLE_0, RLSUB_1, RLVECT_1, CARD_1, XXREAL_0, RELAT_1, VALUED_1, CLVECT_1, ALGSTR_0, CARD_3, BINOP_1, ZFMISC_1, STRUCT_0, SUPINF_2, NORMSP_1, REALSET1, PRE_TOPC, METRIC_1, REAL_1, NAT_1, RSSPACE3, XXREAL_2, CSSPACE3, NORMSP_0, RELAT_2; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0, COMPLEX1, NAT_1, STRUCT_0, ALGSTR_0, RELAT_1, BINOP_1, REALSET1, DOMAIN_1, PARTFUN1, FUNCT_1, XXREAL_0, FUNCT_2, FUNCOP_1, PRE_TOPC, RLVECT_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, NORMSP_0, CLVECT_1, CSSPACE; constructors BINOP_1, FUNCOP_1, REAL_1, COMSEQ_2, COMSEQ_3, REALSET1, CSSPACE, SEQ_2, RELSET_1, CFUNCDOM; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, COMSEQ_2, REALSET1, STRUCT_0, CLVECT_1, CSSPACE, VALUED_1, VALUED_0, XCMPLX_0, SEQ_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; equalities REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, VALUED_1, NORMSP_0, CSSPACE, CFUNCDOM; expansions NORMSP_0; theorems RELAT_1, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SERIES_1, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, CSSPACE, CLVECT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, COMPLEX1, TARSKI, XBOOLE_0, RSSPACE2, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, XCMPLX_0, XREAL_0, CSSPACE2, ORDINAL1; schemes NAT_1, SEQ_1, FUNCT_2, COMSEQ_1, XBOOLE_0; begin :: Complex_l1_Space:The Space of Absolute Summable Complex Sequences definition func the_set_of_l1ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def1: for x being object holds x in it iff x in the_set_of_ComplexSequences & 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_ComplexSequences & P[x] from XBOOLE_0:sch 1; for x be object st x in IT holds x in the_set_of_ComplexSequences by A1; then IT is Subset of the_set_of_ComplexSequences by TARSKI:def 3; hence thesis by A1; end; uniqueness proof let X1,X2 be Subset of Linear_Space_of_ComplexSequences; assume that A2: for x being object holds x in X1 iff x in the_set_of_ComplexSequences & seq_id(x) is absolutely_summable and A3: for x being object holds x in X2 iff x in the_set_of_ComplexSequences & 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_ComplexSequences & 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_ComplexSequences & 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 Complex, seq be Complex_Sequence, rseq be Real_Sequence st seq is convergent & ( for i be Nat holds rseq.i = |.(seq.i-c).| ) holds rseq is convergent & lim rseq = |.(lim seq-c).| proof let c be Complex; let seq be Complex_Sequence; let rseq be Real_Sequence; assume that A1: seq is convergent and A2: for i be Nat holds rseq.i = |.(seq.i-c).|; reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2; reconsider cseq = NAT --> c1 as Complex_Sequence; A3: for n be Nat holds cseq.n=c by ORDINAL1:def 12,FUNCOP_1:7; then A4: cseq is convergent by COMSEQ_2:9; then reconsider seq9 = seq-cseq as convergent Complex_Sequence by A1; seq -cseq is convergent by A1,A4; then A5: lim |.(seq -cseq).| = |.(lim(seq-cseq)).| by SEQ_2:27 .=|.(lim seq-lim cseq).| by A1,A4,COMSEQ_2:26 .=|.(lim seq-c).| by A3,COMSEQ_2:10; now let i be Nat; A6: i in NAT by ORDINAL1:def 12; thus rseq.i=|.(seq.i-c).| by A2 .=|.(seq.i-(cseq.i)).|by FUNCOP_1:7,A6 .=|.(seq.i+-(cseq.i)).| .=|.(seq.i+(-cseq).i).| by VALUED_1:8 .=|.(seq -cseq).i .| by VALUED_1:1,A6 .=|. seq-cseq .| .i by VALUED_1:18; end; then A7: for x be object st x in NAT holds rseq.x = |.(seq -cseq).| .x; |.seq9.| is convergent; hence thesis by A7,A5,FUNCT_2:12; end; registration cluster the_set_of_l1ComplexSequences -> non empty; coherence proof seq_id CZeroseq is absolutely_summable proof reconsider cseq=seq_id CZeroseq as Complex_Sequence; for n being Nat holds cseq.n = 0c by CSSPACE:4; hence thesis by COMSEQ_3:51; end; hence thesis by Def1; end; end; registration cluster the_set_of_l1ComplexSequences -> linearly-closed; coherence proof set W = the_set_of_l1ComplexSequences; A1: for v,u be VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l1ComplexSequences & u in the_set_of_l1ComplexSequences holds v + u in the_set_of_l1ComplexSequences proof let v,u be VECTOR of Linear_Space_of_ComplexSequences such that A2: v in W and A3: u in W; seq_id(v+u) is absolutely_summable proof set r = |.seq_id(v+u).|; set q = |.seq_id u.|; set p = |.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 VALUED_1:18; hence thesis by COMPLEX1:46; end; A5: for n be Nat holds r.n <=(p+q).n proof let n be Nat; A6: n in NAT by ORDINAL1:def 12; A7: |.((seq_id v).n).|+|.((seq_id u).n).| = |.(seq_id v).| .n + |.( (seq_id u).n).| by VALUED_1:18 .= |.(seq_id v).| .n+ |.(seq_id u).| .n by VALUED_1:18 .= (p + q).n by SEQ_1:7; r.n=|.((seq_id(v+u)).n).| by VALUED_1:18 .=|.((seq_id(seq_id(v) + seq_id(u))).n).| by CSSPACE:2 .=|.((seq_id v).n + (seq_id u).n).| by VALUED_1:1,A6; hence thesis by A7,COMPLEX1:56; end; seq_id u is absolutely_summable by A3,Def1; then A8: q is summable by COMSEQ_3:def 9; seq_id v is absolutely_summable by A2,Def1; then p is summable by COMSEQ_3:def 9; then p+q is summable by A8,SERIES_1:7; then r is summable by A4,A5,SERIES_1:20; hence thesis by COMSEQ_3:def 9; end; hence thesis by Def1; end; for a be Complex, v be VECTOR of Linear_Space_of_ComplexSequences st v in W holds a * v in W proof let a be Complex; let v be VECTOR of Linear_Space_of_ComplexSequences such that A9: v in W; seq_id(a*v) is absolutely_summable proof set r1 = ((|.a.|)(#)|.(seq_id v).|); set q1 = |.seq_id(a*v).|; A10: for n be Nat holds 0<=q1.n proof let n be Nat; q1.n=|.((seq_id(a*v)).n).| by VALUED_1:18; hence thesis by COMPLEX1:46; end; A11: for n be Nat holds q1.n <=r1.n proof let n be Nat; q1.n=|.((seq_id(a*v)).n).| by VALUED_1:18 .=|.((seq_id(a(#)seq_id v)).n).| by CSSPACE:3 .=|.(a(#)seq_id v).| .n by VALUED_1:18; hence thesis by COMSEQ_1:50; end; seq_id v is absolutely_summable by A9,Def1; then |. seq_id v .| is summable by COMSEQ_3:def 9; then r1 is summable by SERIES_1:10; then q1 is summable by A10,A11,SERIES_1:20; hence thesis by COMSEQ_3:def 9; end; hence thesis by Def1; end; hence thesis by A1,CLVECT_1:def 7; end; end; Lm1: CLSStruct (# the_set_of_l1ComplexSequences, Zero_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Add_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Mult_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences) #) is Subspace of Linear_Space_of_ComplexSequences by CSSPACE:11; registration cluster CLSStruct (# the_set_of_l1ComplexSequences, Zero_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Add_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences), Mult_( the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; coherence by CSSPACE:11; end; definition func cl_norm -> Function of the_set_of_l1ComplexSequences, REAL means :Def2: for x be object st x in the_set_of_l1ComplexSequences holds it.x = Sum |.seq_id x.|; existence proof deffunc F(object) = Sum |.seq_id $1.|; A1: for z be object st z in the_set_of_l1ComplexSequences holds F(z) in REAL by XREAL_0:def 1; ex f being Function of the_set_of_l1ComplexSequences,REAL st for x being object st x in the_set_of_l1ComplexSequences 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_l1ComplexSequences, REAL such that A2: for x be object st x in the_set_of_l1ComplexSequences holds NORM1.x = Sum |.seq_id x.| and A3: for x be object st x in the_set_of_l1ComplexSequences holds NORM2.x = Sum |.seq_id x.|; A4: for z be object st z in the_set_of_l1ComplexSequences holds NORM1.z = NORM2. z proof let z be object such that A5: z in the_set_of_l1ComplexSequences; NORM1.z = Sum |.seq_id z.| by A2,A5; hence thesis by A3,A5; end; dom NORM1 = the_set_of_l1ComplexSequences & dom NORM2 = the_set_of_l1ComplexSequences 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 [:COMPLEX, X:], X, N be Function of X, REAL; cluster CNORMSTR (# X, Z, A, M, N #) -> non empty; coherence; end; theorem for l be CNORMSTR st the CLSStruct of l is ComplexLinearSpace holds l is ComplexLinearSpace by CSSPACE:79; theorem Th3: for cseq be Complex_Sequence st (for n be Nat holds cseq.n=0c) holds cseq is absolutely_summable & Sum |.cseq.| = 0 proof let cseq be Complex_Sequence such that A1: for n be Nat holds cseq.n=0c; A2: for n be Nat holds (|.cseq.|).n=0 proof let n be Nat; cseq.n=0c by A1; hence thesis by COMPLEX1:44,VALUED_1:18; end; A3: for m be Nat holds Partial_Sums (|.cseq.|).m = 0 proof defpred P[Nat] means (|.cseq.|).$1 = (Partial_Sums |.cseq.|).$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: (|.cseq.|).k = (Partial_Sums (|.cseq.|)).k; thus (|.cseq.|).(k+1) = 0 + (|.cseq.|).(k+1) .= (|.cseq.|).k + (|.cseq.|).(k+1) by A2 .= (Partial_Sums |.cseq.|).(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 |.cseq.|).m = (|.cseq.|).m .= 0 by A2; end; A7: for p be Real st 0
non empty CNORMSTR equals CNORMSTR (# the_set_of_l1ComplexSequences, Zero_(the_set_of_l1ComplexSequences, Linear_Space_of_ComplexSequences), Add_(the_set_of_l1ComplexSequences, Linear_Space_of_ComplexSequences), Mult_(the_set_of_l1ComplexSequences, Linear_Space_of_ComplexSequences), cl_norm #); coherence; end; ::$CT theorem Th4: Complex_l1_Space is ComplexLinearSpace by Lm2,CSSPACE:79; begin :: Complex_l1_Space is Banach theorem Th5: the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & ( for x be set holds x is VECTOR of Complex_l1_Space iff x is Complex_Sequence & seq_id x is absolutely_summable ) & 0.Complex_l1_Space = CZeroseq & ( for u be VECTOR of Complex_l1_Space holds u =seq_id u ) & ( for u,v be VECTOR of Complex_l1_Space holds u+v =seq_id(u)+seq_id(v) ) & ( for p be Complex for u be VECTOR of Complex_l1_Space holds p*u =p(#)seq_id(u) ) & ( for u be VECTOR of Complex_l1_Space holds -u = -seq_id u & seq_id(-u) = -seq_id(u) ) & ( for u,v be VECTOR of Complex_l1_Space holds u-v =seq_id(u)-seq_id v ) & ( for v be VECTOR of Complex_l1_Space holds seq_id v is absolutely_summable ) & for v be VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.seq_id v.| proof set l1 =Complex_l1_Space; A1: for x be set holds x is Element of l1 iff x is Complex_Sequence & seq_id x is absolutely_summable proof let x be set; x in the_set_of_ComplexSequences iff x is Complex_Sequence by FUNCT_2:8,66; hence thesis by 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_ComplexSequences by Lm1, CLVECT_1:29; set L1=Linear_Space_of_ComplexSequences; set W = the_set_of_l1ComplexSequences; dom (the addF of L1) = [:the carrier of L1,the carrier of L1:] by FUNCT_2:def 1; then A3: dom ((the addF of Linear_Space_of_ComplexSequences)||W) =[:W,W:] by RELAT_1:62,ZFMISC_1:96; u+v =((the addF of Linear_Space_of_ComplexSequences)||W).[u,v] by CSSPACE:def 8 .=u1+v1 by A3,FUNCT_1:47; hence thesis by CSSPACE:2; end; A4: for p be Complex for u be VECTOR of l1 holds p*u =p(#)seq_id(u) proof let p be Complex; let u be VECTOR of l1; reconsider u1=u as VECTOR of Linear_Space_of_ComplexSequences by Lm1, CLVECT_1:29; set L1=Linear_Space_of_ComplexSequences; set W = the_set_of_l1ComplexSequences; dom (the Mult of L1) = [:COMPLEX,the carrier of L1:] by FUNCT_2:def 1; then A5: dom ((the Mult of Linear_Space_of_ComplexSequences) | [:COMPLEX,W :]) =[:COMPLEX,W:] by RELAT_1:62,ZFMISC_1:96; reconsider p as Element of COMPLEX by XCMPLX_0:def 2; p*u =(the Mult of l1).[p,u] by CLVECT_1:def 1 .=((the Mult of Linear_Space_of_ComplexSequences)|[:COMPLEX,W:]).[p,u] by CSSPACE:def 9 .=(the Mult of Linear_Space_of_ComplexSequences).[p,u] by A5,FUNCT_1:47 .=p*u1 by CLVECT_1:def 1; hence thesis by CSSPACE: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_ComplexSequences by Lm1,CLVECT_1:29; 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 = (-1r)*u by Th4,CLVECT_1:3 .= (-1r)(#)seq_id(u) by A4 .= -seq_id(u) by COMSEQ_1:11; 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; end; A9: for v be VECTOR of l1 holds ||.v.|| = Sum |.seq_id v.| by Def2; 0.l1 = 0.Linear_Space_of_ComplexSequences by CSSPACE:def 10 .= CZeroseq; hence thesis by A1,A6,A2,A4,A7,A8,A9; end; theorem Th6: for x, y being Point of Complex_l1_Space, p be Complex holds ( ||.x.|| = 0 iff x = 0.Complex_l1_Space ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| & ||. p*x .|| = |.p.| * ||.x.|| proof let x, y be Point of Complex_l1_Space; let p be Complex; A1: for n be Nat holds 0 <= (|.seq_id x.|).n proof let n be Nat; 0 <= |.((seq_id x).n).| by COMPLEX1:46; hence thesis by VALUED_1:18; end; A2: now let n be Nat; (|.seq_id(x+y).|).n = |.((seq_id(x+y)).n).| by VALUED_1:18; hence 0 <= (|.seq_id(x+y).|).n by COMPLEX1:46; end; A3: for n be Nat holds (|.seq_id(x+y).|).n = |.(((seq_id x).n) + ((seq_id y).n)).| proof let n be Nat; A4: n in NAT by ORDINAL1:def 12; (|.seq_id(x+y).|).n = (|.(seq_id(seq_id(x)+seq_id y)).|).n by Th5 .= |.((seq_id x+seq_id y).n).| by VALUED_1:18 .= |.(((seq_id x).n)+((seq_id y).n)).| by VALUED_1:1,A4; hence thesis; end; A5: for n be Nat holds (|.seq_id(x+y).|).n <= (|.seq_id x.|).n + (|.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 (|.(seq_id(x+y)).|) .n <= |.((seq_id x).n).| + |.((seq_id y).n).| by A3; then (|.(seq_id(x+y)).|) .n <= (|.(seq_id x).|).n + |.((seq_id y).n).| by VALUED_1:18; hence thesis by VALUED_1:18; end; A6: for n being Nat holds (|.seq_id(x+y).|).n <= (|.seq_id x.| + |.seq_id y.|).n proof let n be Nat; (|.seq_id x.|).n + (|.seq_id y.|).n =((|.seq_id x.|) + (|.seq_id y.|) ).n by SEQ_1:7; hence thesis by A5; end; seq_id y is absolutely_summable by Def1; then A7: |.seq_id y.| is summable by COMSEQ_3:def 9; seq_id x is absolutely_summable by Def1; then |.seq_id x.| is summable by COMSEQ_3:def 9; then |.seq_id x.| + |.seq_id y.| is summable by A7,SERIES_1:7; then A8: Sum(|.seq_id(x+y).|) <= Sum(|.seq_id x.| + |.seq_id y.|) by A6,A2, SERIES_1:20; A9: now assume x=0.Complex_l1_Space; then A10: for n be Nat holds (seq_id x).n=0 by Th5,CSSPACE:4; thus ||.x.|| = Sum |.seq_id x.| by Def2 .= 0 by A10,Th3; end; A11: Sum |.seq_id(x+y).| = ||.x + y.|| by Th5; A12: now A13: x in the_set_of_ComplexSequences by Def1; assume A14: ||.x.|| = 0; ||.x.|| = Sum |.seq_id x.| & seq_id(x) is absolutely_summable by Th5; then for n be Nat holds 0 = (seq_id x).n by A14,CSSPACE2:13; hence x=0.Complex_l1_Space by A13,Th5,CSSPACE:5; end; A15: ||.x.|| = Sum |.seq_id x.| & ||.y.|| = Sum |.seq_id y.| by Th5; A16: for n be Nat holds (|.p(#)seq_id(x).|).n =|.p.|*(|.seq_id x .| .n) proof let n be Nat; reconsider p as Element of COMPLEX by XCMPLX_0:def 2; (|.(p(#)seq_id(x)).|).n =|.((p(#)seq_id(x)).n).| by VALUED_1:18 .=|.(p*((seq_id x).n)).| by VALUED_1:6 .=(|.p.|)*(|.((seq_id x).n).|) by COMPLEX1:65 .=(|.p.|)*((|.seq_id x.|).n) by VALUED_1:18; hence thesis; end; seq_id x is absolutely_summable by Def1; then A17: |.seq_id x.| is summable by COMSEQ_3:def 9; seq_id x is absolutely_summable by Def1; then A18: |.seq_id x.| is summable by COMSEQ_3:def 9; ||.(p*x).|| =Sum(|.seq_id(p*x).|) by Th5 .=Sum(|.seq_id(p(#)seq_id(x)).|) by Th5 .=Sum(|.p.|(#)|.seq_id x.|) by A16,SEQ_1:9 .=|.p.|*Sum(|.seq_id x.|) by A17,SERIES_1:10 .=|.p.|*||.x.|| by Th5; hence thesis by A12,A9,A1,A18,A15,A11,A7,A8,SERIES_1:7,18; end; registration cluster Complex_l1_Space -> reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; coherence by Lm2,Th6,CLVECT_1:def 13,CSSPACE:79; end; Lm3: for c be Complex, seq be Complex_Sequence, 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 Complex; let seq be Complex_Sequence; let seq1 be Real_Sequence; assume that A1: seq is convergent and A2: seq1 is convergent; reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def 2; reconsider cseq = NAT --> c1 as Complex_Sequence; A3: for n be Nat holds cseq.n=c by ORDINAL1:def 12,FUNCOP_1:7; then A4: lim cseq = c by COMSEQ_2:10 .= cseq.0 by FUNCOP_1:7; A5: cseq is convergent by A3,COMSEQ_2:9; then seq -cseq is convergent by A1; then A6: lim |.(seq-cseq).| = |.(lim(seq-cseq)).| by SEQ_2:27 .= |.(lim seq - (cseq.0)).| by A1,A4,A5,COMSEQ_2:26 .= |.(lim seq - c).| by FUNCOP_1:7; let rseq be Real_Sequence such that A7: 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 A7 .=|.(seq.i-cseq.i).|+seq1.i by FUNCOP_1:7 .=|.(seq.i+(-cseq.i)).|+seq1.i .=|.(seq.i+(-cseq).i).|+seq1.i by VALUED_1:8 .=|.((seq-cseq).i).| + seq1.i by VALUED_1:1 .=|.(seq-cseq).| .i + seq1.i by VALUED_1:18 .=(|.(seq-cseq).| + seq1).i by SEQ_1:7; end; then A8: rseq = (|.(seq-(cseq)).| + seq1) by FUNCT_2:63; reconsider seq1=seq-cseq as convergent Complex_Sequence by A1,A5; |.seq1.| is convergent; hence thesis by A2,A8,A6,SEQ_2:6; end; definition let X be non empty CNORMSTR, x, y be Point of X; func dist(x,y) -> Real equals ||.x - y.||; coherence; end; definition let CNRM be non empty CNORMSTR; let seqt be sequence of CNRM; 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 CNRM be non empty CNORMSTR; let seq be sequence of CNRM; synonym seq is Cauchy_sequence_by_Norm for seq is CCauchy; end; reserve NRM for non empty ComplexNormSpace; reserve seq for sequence of NRM; theorem Th7: 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; thus (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) implies seq is Cauchy_sequence_by_Norm proof 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 being 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; end; theorem for vseq be sequence of Complex_l1_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent proof let vseq be sequence of Complex_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 Complex_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 COMPLEX & P[x,y] proof let x be object; assume x in NAT; then reconsider i=x as Element of NAT; deffunc F(Nat) = (seq_id(vseq.$1)).i; consider rseqi be Complex_Sequence such that A3: for n be Nat holds rseqi.n= F(n) from COMSEQ_1:sch 1; take lim rseqi; thus lim rseqi in COMPLEX by XCMPLX_0:def 2; now let e be Real such that A4: e > 0; thus ex k be Nat st for m be Nat st k <= m holds |.(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,Th7; 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 VALUED_1:18; end; seq_id((vseq.m)-(vseq.k)) is absolutely_summable by Def1; then |.(seq_id((vseq.m)-(vseq.k))).| is summable by COMSEQ_3:def 9; then A8: |.(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 Th5 .= seq_id((vseq.m))+-seq_id((vseq.k)); then (seq_id((vseq.m) - (vseq.k))).i =(seq_id((vseq.m))).i+(-seq_id( (vseq.k))).i by VALUED_1:1 .=(seq_id((vseq.m))).i+(-(seq_id((vseq.k))).i) by VALUED_1:8 .=(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).| = |.(seq_id((vseq.m) - (vseq.k))).| .i by VALUED_1:18; ||.(vseq.m) - (vseq.k).|| =Sum(|.(seq_id((vseq.m) - (vseq.k))) .|) by Th5; 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 COMSEQ_3:46; hence thesis by A3; end; consider f be sequence of COMPLEX 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 Complex_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 Complex_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 Complex_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 |.(seq_id tseq-seq_id(vseq.n)).| is summable & Sum(|.(seq_id tseq-seq_id(vseq.n)).|) < e proof let e1 be Real such that A13: e1 >0; 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,Th7; A16: for m,n be Nat st n >= k & m >= k holds ( |.(seq_id((vseq. n) - (vseq.m))).| is summable & Sum(|.(seq_id((vseq.n) - (vseq.m))).|) < e & for i be Nat holds 0 <= |.(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 Complex_l1_Space).(vseq.n-vseq.m) < e; A18: for i be Nat holds 0 <= |.(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 VALUED_1:18; end; seq_id(vseq.n-vseq.m) is absolutely_summable by Def1; hence thesis by A17,A18,Def2,COMSEQ_3:def 9; 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(|.seq_id( vseq.m-vseq.n).|).i ) holds rseq is convergent & lim rseq = Partial_Sums(|.( 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).|).$1 holds rseq is convergent & lim rseq = Partial_Sums(|.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 Th5; 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(|.seq_id(vseq.m-vseq.n).|).i ) holds rseq is convergent & lim rseq = Partial_Sums(|.((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).|).(i+1) ) holds rseq is convergent & lim rseq =Partial_Sums(|.((seq_id tseq-seq_id(vseq.n))).|).(i+1) proof deffunc F(Nat) = Partial_Sums(|.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 Complex_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(|. seq_id(vseq.m-vseq.n).|).(i+1); A27: now let m be Nat; thus rseq.m = Partial_Sums(|.(seq_id(vseq.m-vseq.n)).|).(i+1) by A26 .=|.(seq_id(vseq.m-vseq.n)).| .(i+1) +Partial_Sums(|.seq_id( vseq.m-vseq.n).|).i by SERIES_1:def 1 .=|.seq_id(vseq.m)-seq_id(vseq.n).| .(i+1) +Partial_Sums(|. seq_id(vseq.m-vseq.n).|).i by A20 .=|.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 VALUED_1:18 .=|.((seq_id(vseq.m)).(i+1)+(-seq_id(vseq.n)).(i+1)).| + rseqb .m by VALUED_1:1 .=|.((seq_id(vseq.m)).(i+1)+-(seq_id(vseq.n)).(i+1)).| + rseqb .m by VALUED_1:8 .= |.((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 VALUED_1:8 .= |.((tseq-(seq_id(vseq.n))).(i+1) ).| + lim rseqb by VALUED_1:1 .= |.(tseq-(seq_id(vseq.n))).| .(i+1) + lim rseqb by VALUED_1:18 .= |.(tseq-(seq_id(vseq.n))).| .(i+1) + Partial_Sums(|.((seq_id tseq -seq_id(vseq.n))).|).i by A21,A22 .= Partial_Sums (|.((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(|.seq_id( vseq.m-vseq.n).|).0; thus rseq is convergent & lim rseq = Partial_Sums(|.seq_id tseq-seq_id (vseq.n).|).0 proof consider rseq0 be Complex_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(|.seq_id(vseq.m-vseq.n).|).0 by A30 .=(|.seq_id(vseq.m-vseq.n).|).0 by SERIES_1:def 1 .=(|.seq_id(vseq.m)-seq_id(vseq.n).|).0 by A20 .=|.((seq_id(vseq.m)+-seq_id(vseq.n)).0).| by VALUED_1:18 .=|.((seq_id(vseq.m)).0+(-seq_id(vseq.n)).0).| by VALUED_1:1 .=|.((seq_id(vseq.m)).0+-(seq_id(vseq.n)).0).| by VALUED_1:8 .=|.((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 VALUED_1:8 .= |.((tseq-(seq_id((vseq.n)))).0).| by VALUED_1:1 .= |.(seq_id tseq-(seq_id(vseq.n))).| .0 by VALUED_1:18 .=Partial_Sums(|.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 |.(seq_id tseq-seq_id(vseq.n) ).| is summable & Sum |.(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(|.((seq_id tseq -seq_id(vseq.n))).|).i <=e proof let i be Nat such that 0 <=i; deffunc F(Nat)= Partial_Sums(|.(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(|.(seq_id(vseq.m-vseq.n)).|).i by A38; assume A41: m >= k; then |.(seq_id((vseq.m) - (vseq.n))).| is summable & for i be Nat holds 0 <= |.seq_id(vseq.m-vseq.n).| .i by A16,A36; then A42: Partial_Sums(|.(seq_id((vseq.m) - (vseq.n))).|).i <=Sum(|.( seq_id((vseq.m) - (vseq.n))).|) by RSSPACE2:3; Sum(|.(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(|.(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(|.((seq_id tseq -seq_id(vseq.n))).|).i <=e by A37,NAT_1:2; hence Partial_Sums(|.((seq_id tseq -seq_id(vseq.n))).|).i < e1 by A14, XXREAL_0:2; end; then A43: Partial_Sums(|.((seq_id tseq -seq_id(vseq.n))).|) is bounded_above by SEQ_2:def 3; A44: for i be Nat holds 0 <= |.(seq_id tseq-seq_id(vseq.n)).| .i proof let i be Nat; |.(seq_id tseq -seq_id(vseq.n)).| .i =|.((seq_id tseq -seq_id( vseq.n)).i).| by VALUED_1:18; hence thesis by COMPLEX1:46; end; then |.((seq_id tseq-seq_id(vseq.n))).| is summable by A43,SERIES_1:17; then Partial_Sums(|.((seq_id tseq -seq_id(vseq.n))).|) is convergent by SERIES_1:def 2; then Sum(|.((seq_id tseq -seq_id(vseq.n))).|) = lim Partial_Sums(|.(( seq_id tseq - seq_id(vseq.n))).|) & lim Partial_Sums(|.((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; |.seq_id tseq.| is summable proof set d=|.seq_id tseq.|; A45: for i be Nat holds 0 <= |.(seq_id tseq).| .i proof let i be Nat; |.(seq_id tseq).| .i = |.((seq_id tseq).i).| by VALUED_1:18; hence thesis by COMPLEX1:46; end; reconsider jj=1 as Real; consider m be Nat such that A46: for n be Nat st n >= m holds |.((seq_id tseq -seq_id( vseq.n))).| is summable & Sum(|.((seq_id tseq -seq_id(vseq.n))).|) < 1 by A12; set b=|.seq_id(vseq.m).|; set a=|.(seq_id tseq -seq_id(vseq.m)).|; seq_id(vseq.m) is absolutely_summable by Def1; then A47: |.(seq_id(vseq.m)).| is summable by COMSEQ_3:def 9; A48: for i be Nat holds d.i <= (a+b).i proof let i be Nat; A49: i in NAT by ORDINAL1:def 12; A50: b.i=|.((seq_id(vseq.m)).i).| & d.i=|.((seq_id tseq).i).| by VALUED_1:18; a.i = |.((seq_id tseq+-seq_id(vseq.m)).i).| by VALUED_1:18 .= |.((seq_id tseq).i+(-seq_id(vseq.m)).i).| by VALUED_1:1,A49 .= |.((seq_id tseq).i+(-(seq_id(vseq.m)).i)).| by VALUED_1:8 .=|.((seq_id tseq).i-(seq_id(vseq.m)).i).|; then d.i-b.i <= a.i by A50,COMPLEX1:59; then d.i-b.i+b.i<= a.i + b.i by XREAL_1:6; hence thesis by SEQ_1:7; end; |.((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 A51: seq_id tseq is absolutely_summable by COMSEQ_3:def 9; A52: tseq in the_set_of_ComplexSequences by FUNCT_2:8; then reconsider tv=tseq as Point of Complex_l1_Space by A51,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 A53: for n be Nat st n >= m holds |.(seq_id tseq-seq_id( vseq.n)).| is summable & Sum(|.(seq_id tseq-seq_id(vseq.n)).|) < e by A12; now reconsider u=tseq as VECTOR of Complex_l1_Space by A51,A52,Def1; let n be Nat; assume n >= m; then A54: Sum |.(seq_id tseq-seq_id(vseq.n)).| < e by A53; reconsider v=vseq.n as VECTOR of Complex_l1_Space; seq_id(u-v) = u-v by Th5; then Sum |. seq_id(u-v).| = Sum |.(seq_id tseq-seq_id(vseq.n)).| by Th5; then A55: (the normF of Complex_l1_Space).(u-v) < e by A54,Def2; ||.(vseq.n) - tv.|| =||.-(tv-(vseq.n)).|| by RLVECT_1:33 .=||.tv-(vseq.n).|| by CLVECT_1:103; hence ||.(vseq.n) - tv.|| < e by A55; end; hence thesis; end; hence thesis by CLVECT_1:def 15; end;