:: Real Linear Space of Real Sequences :: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama :: :: Received April 3, 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, XBOOLE_0, SEQ_1, FUNCT_2, TARSKI, REAL_1, BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, CARD_1, NAT_1, RLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, RLSUB_1, REALSET1, SERIES_1, XXREAL_0, SQUARE_1, CARD_3, BHSP_1, COMPLEX1, SEQ_2, ORDINAL2, XXREAL_2, VALUED_0, RSSPACE, ASYMPT_1, FUNCSDOM; notations TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, REALSET1, FUNCOP_1, RLVECT_1, RLSUB_1, BHSP_1, SQUARE_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, BINOP_1, FUNCSDOM; constructors PARTFUN1, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_2, SEQM_3, SERIES_1, REALSET1, RLSUB_1, BHSP_1, VALUED_1, RELSET_1, COMSEQ_2, SEQ_1, FUNCSDOM; registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, BHSP_1, ALGSTR_0, VALUED_1, FUNCT_2, VALUED_0, SERIES_1, SQUARE_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions TARSKI, XBOOLE_0, FUNCT_2, RLVECT_1, ALGSTR_0, RLSUB_1; equalities SQUARE_1, BINOP_1, RLVECT_1, XBOOLE_0, REALSET1, STRUCT_0, SEQ_1, ALGSTR_0, FUNCSDOM, ORDINAL1; expansions BINOP_1, RLSUB_1; theorems RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, COMSEQ_3, INT_1, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, RLSUB_1, SEQ_4, XREAL_1, ORDINAL1, ALGSTR_0, XREAL_0, FUNCOP_1, FUNCSDOM, VALUED_1; schemes NAT_1, BINOP_1, XBOOLE_0; begin definition func the_set_of_RealSequences -> non empty set equals Funcs(NAT,REAL); coherence; end; definition let a be object such that A1: a in the_set_of_RealSequences; func seq_id(a) -> Real_Sequence equals :Def2: a; coherence by A1,FUNCT_2:66; end; definition ::$CD 3 func Zeroseq -> Element of the_set_of_RealSequences equals seq_const 0; coherence by FUNCT_2:8; end; registration let x be Element of the_set_of_RealSequences; reduce seq_id x to x; reducibility by Def2; end; registration let x be Real_Sequence; reduce seq_id x to x; reducibility proof x in the_set_of_RealSequences by FUNCT_2:8; hence thesis by Def2; end; end; theorem for x be Real_Sequence holds seq_id x = x; definition func Linear_Space_of_RealSequences -> strict RLSStruct equals RealVectSpace(NAT); coherence; end; registration let x be Element of Linear_Space_of_RealSequences; reduce seq_id x to x; reducibility by Def2; end; registration cluster Linear_Space_of_RealSequences -> non empty; coherence; end; theorem for v,w being VECTOR of Linear_Space_of_RealSequences holds v + w = seq_id(v) + seq_id(w) proof let v,w be VECTOR of Linear_Space_of_RealSequences; reconsider v1 = v, w1 = w as Element of Funcs(NAT,REAL); (RealFuncAdd NAT).(v1,w1) = seq_id(v)+seq_id(w) proof let n be Element of NAT; thus (RealFuncAdd NAT).(v1,w1).n = v1.n+w1.n by FUNCSDOM:1 .= (seq_id(v)+seq_id(w)).n by VALUED_1:1; end; hence thesis; end; theorem Th3: for r being Real, v being VECTOR of Linear_Space_of_RealSequences holds r * v = r (#) seq_id(v) proof let r be Real; let v be VECTOR of Linear_Space_of_RealSequences; reconsider r1 = r as Element of REAL by XREAL_0:def 1; reconsider v1 = v as Element of Funcs(NAT,REAL); reconsider h = (RealFuncExtMult NAT).(r1,v1) as Real_Sequence by FUNCT_2:66; h = r(#)seq_id(v) proof let n be Element of NAT; thus h.n = r*(v1.n) by FUNCSDOM:4 .= (r(#)seq_id(v)).n by VALUED_1:6; end; hence thesis; end; registration cluster Linear_Space_of_RealSequences -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; coherence; end; definition let X be RealLinearSpace; let X1 be Subset of X such that A1: X1 is linearly-closed non empty; func Add_(X1,X) -> BinOp of X1 equals :Def5: (the addF of X)||X1; correctness proof A2: dom (the addF of X) = [:the carrier of X,the carrier of X:] by FUNCT_2:def 1; A3: for z be object st z in [:X1,X1:] holds ((the addF of X)||X1).z in X1 proof let z be object such that A4: z in [:X1,X1:]; consider r,x be object such that A5: r in X1 & x in X1 and A6: z=[r,x] by A4,ZFMISC_1:def 2; reconsider y=x,r1=r as VECTOR of X by A5; [r,x] in dom ((the addF of X)||X1) by A2,A4,A6,RELAT_1:62,ZFMISC_1:96; then ((the addF of X)||X1).z = r1+y by A6,FUNCT_1:47; hence thesis by A1,A5; end; dom ((the addF of X)||X1) =[:X1,X1:] by A2,RELAT_1:62,ZFMISC_1:96; hence thesis by A3,FUNCT_2:3; end; end; definition let X be RealLinearSpace; let X1 be Subset of X such that A1: X1 is linearly-closed non empty; func Mult_(X1,X) -> Function of [:REAL,X1:], X1 equals :Def6: (the Mult of X) | [:REAL,X1:]; correctness proof A2: [:REAL,X1:] c= [:REAL,the carrier of X:] & dom (the Mult of X) = [: REAL,the carrier of X:] by FUNCT_2:def 1,ZFMISC_1:95; A3: for z be object st z in [:REAL,X1:] holds ((the Mult of X) | [:REAL,X1:]) .z in X1 proof let z be object such that A4: z in [:REAL,X1:]; consider r,x be object such that A5: r in REAL and A6: x in X1 and A7: z=[r,x] by A4,ZFMISC_1:def 2; reconsider r as Real by A5; reconsider y=x as VECTOR of X by A6; [r,x] in dom ((the Mult of X) | [:REAL,X1:]) by A2,A4,A7,RELAT_1:62; then ((the Mult of X) | [:REAL,X1:]).z = r*y by A7,FUNCT_1:47; hence thesis by A1,A6; end; dom ((the Mult of X) | [:REAL,X1:]) =[:REAL,X1:] by A2,RELAT_1:62; hence thesis by A3,FUNCT_2:3; end; end; definition let X be RealLinearSpace, X1 be Subset of X such that A1: X1 is linearly-closed non empty; func Zero_(X1,X) -> Element of X1 equals :Def7: 0.X; correctness proof set v = the Element of X1; v in X1 by A1; then reconsider v as Element of X; v-v=0.X by RLVECT_1:15; hence thesis by A1,RLSUB_1:3; end; end; theorem for n being object holds (seq_id Zeroseq).n = 0 proof set f = seq_id Zeroseq; let n be object; per cases; suppose A1: n in dom f; dom f = NAT by FUNCT_2:def 1; hence thesis by A1,FUNCOP_1:7; end; suppose not n in dom f; hence thesis by FUNCT_1:def 2; end; end; theorem for f being Element of the_set_of_RealSequences st for n being Nat holds (seq_id f).n = 0 holds f = Zeroseq proof let f be Element of the_set_of_RealSequences; set g = seq_id f; assume A1: for n being Nat holds g.n = 0; A2: dom g = NAT by FUNCT_2:def 1; for z being object st z in dom g holds g.z = 0 by A1; hence f = Zeroseq by A2,FUNCOP_1:11; end; ::$CT 5 theorem Th4: for V be RealLinearSpace, V1 be Subset of V st V1 is linearly-closed non empty holds RLSStruct (# V1,Zero_(V1,V), Add_(V1,V),Mult_(V1,V) #) is Subspace of V proof let V be RealLinearSpace; let V1 be Subset of V such that A1: V1 is linearly-closed non empty; A2: Mult_(V1,V) = (the Mult of V) | [:REAL,V1:] by A1,Def6; Zero_(V1,V) = 0.V & Add_(V1,V)= (the addF of V)||V1 by A1,Def5,Def7; hence thesis by A1,A2,RLSUB_1:24; end; definition func the_set_of_l2RealSequences -> Subset of Linear_Space_of_RealSequences means :Def8: for x being object holds x in it iff x in the_set_of_RealSequences & seq_id(x) (#) seq_id(x) is summable; existence proof defpred P[object] means seq_id($1)(#)seq_id($1) is 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)(#)seq_id(x) is summable and A3: for x being object holds x in X2 iff x in the_set_of_RealSequences & seq_id(x)(#)seq_id(x) is summable; thus X1 c= X2 proof let x be object; assume A4: x in X1; then seq_id(x)(#)seq_id(x) is summable by A2; hence thesis by A3,A4; end; let x be object; assume A5: x in X2; then seq_id(x)(#)seq_id(x) is summable by A3; hence thesis by A2,A5; end; end; registration cluster the_set_of_l2RealSequences -> linearly-closed non empty; coherence proof set W = the_set_of_l2RealSequences; hereby let v,u be VECTOR of Linear_Space_of_RealSequences such that A4: v in W and A5: u in W; (seq_id(v+u))(#)(seq_id(v+u)) is summable proof set r = (seq_id(v+u))(#)(seq_id(v+u)); set q = (seq_id(u))(#)(seq_id(u)); set p = (seq_id(v))(#)(seq_id(v)); A6: for n be Nat holds 0<=r.n proof let n be Nat; r.n=(seq_id(v+u)).n * (seq_id(v+u)).n by SEQ_1:8; hence thesis by XREAL_1:63; end; A7: for n be Nat holds r.n <=(2(#)p+2(#)q).n proof set s = seq_id v, t = seq_id u; let n be Nat; reconsider sn=s.n, tn=t.n as Real; A8: (2(#)p+2(#)q).n=(2(#)p).n +(2(#)q).n by SEQ_1:7 .= 2*p.n + (2(#)q).n by SEQ_1:9 .= 2*p.n + 2*q.n by SEQ_1:9 .= 2*(s.n*s.n) + 2*q.n by SEQ_1:8 .= 2*sn^2 + 2*tn^2 by SEQ_1:8; A9: 0 <= (sn-tn)^2 by XREAL_1:63; reconsider vu = v+u as Element of Funcs(NAT,REAL); n in NAT by ORDINAL1:def 12; then vu.n = s.n+t.n by FUNCSDOM:1; then r.n=((s.n)+(t.n))^2 by SEQ_1:8 .= sn^2 + 2*sn*tn + tn^2; then 0 + r.n <= (2(#)p+2(#)q).n - r.n + r.n by A8,A9,XREAL_1:7; hence thesis; end; (seq_id u)(#)(seq_id u) is summable by A5,Def8; then A10: 2(#)q is summable by SERIES_1:10; (seq_id v)(#)(seq_id v) is summable by A4,Def8; then 2(#)p is summable by SERIES_1:10; then 2(#)p+2(#)q is summable by A10,SERIES_1:7; hence thesis by A6,A7,SERIES_1:20; end; hence v+u in W by Def8; end; hereby let a be Real; let v be VECTOR of Linear_Space_of_RealSequences; assume v in W; then A2: (seq_id(v))(#)(seq_id(v)) is summable by Def8; a*v = a(#)seq_id(v) by Th3; then (seq_id(a*v))(#)(seq_id(a*v)) = a(#)((a(#)seq_id(v))(#) seq_id(v)) by SEQ_1:19 .=a(#)(a(#)( seq_id(v)(#)seq_id(v))) by SEQ_1:18 .=(a*a)(#)(seq_id(v)(#)seq_id(v)) by SEQ_1:23; then (seq_id(a*v))(#)(seq_id(a*v)) is summable by A2,SERIES_1:10; hence a*v in W by Def8; end; seq_id Zeroseq (#)seq_id Zeroseq is absolutely_summable proof reconsider rseq=(seq_id(Zeroseq)(#)seq_id Zeroseq) as Real_Sequence; now let n be Nat; thus rseq.n =((seq_id Zeroseq).n ) * ((seq_id Zeroseq).n) by SEQ_1:8 .=((seq_id Zeroseq).n ) * 0 by FUNCOP_1:7,ORDINAL1:def 12 .=0; end; hence thesis by COMSEQ_3:3; end; hence thesis by Def8; end; end; theorem RLSStruct(# the_set_of_l2RealSequences, Zero_( the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_( the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_( the_set_of_l2RealSequences,Linear_Space_of_RealSequences) #) is Subspace of Linear_Space_of_RealSequences by Th4; theorem Th6: RLSStruct (# the_set_of_l2RealSequences, Zero_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences) #) is RealLinearSpace by Th4; ::$CT definition func l_scalar -> Function of [:the_set_of_l2RealSequences, the_set_of_l2RealSequences:], REAL means for x,y be object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds it.(x,y) = Sum(seq_id(x)(#)seq_id(y)); existence proof deffunc F(object,object) = Sum(seq_id($1)(#)seq_id($2)); set X = the_set_of_l2RealSequences; A1: for x,y being object st x in X & y in X holds F(x,y) in REAL by XREAL_0:def 1; ex f being Function of [:X,X:],REAL st for x,y being object st x in X & y in X holds f.(x,y) = F(x,y) from BINOP_1:sch 2(A1); hence thesis; end; uniqueness proof set X = the_set_of_l2RealSequences; let scalar1, scalar2 be Function of [: X, X :], REAL such that A2: for x,y be object st x in X & y in X holds scalar1.(x,y) = Sum(seq_id (x)(#)seq_id(y)) and A3: for x,y be object st x in X & y in X holds scalar2.(x,y) = Sum(seq_id (x)(#)seq_id(y)); for x, y be set st x in X & y in X holds scalar1.(x,y) = scalar2.(x,y) proof let x,y be set such that A4: x in X & y in X; thus scalar1.(x,y) = Sum(seq_id(x)(#)seq_id(y)) by A2,A4 .= scalar2.(x,y) by A3,A4; end; hence thesis; end; end; definition func l2_Space -> non empty UNITSTR equals UNITSTR (# the_set_of_l2RealSequences, Zero_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_(the_set_of_l2RealSequences,Linear_Space_of_RealSequences), l_scalar #); coherence; end; registration let x be Element of l2_Space; reduce seq_id x to x; reducibility proof x in the_set_of_RealSequences by Def8; hence thesis by Def2; end; end; theorem Th7: for l being RLSStruct st the RLSStruct of l is RealLinearSpace holds l is RealLinearSpace proof let l be RLSStruct such that A1: the RLSStruct of l is RealLinearSpace; reconsider l as non empty RLSStruct by A1; reconsider l0=RLSStruct (# the carrier of l, 0.l, the addF of l, the Mult of l #) as RealLinearSpace by A1; A2: l is Abelian proof let v,w be VECTOR of l; reconsider v1=v as VECTOR of l0; reconsider w1=w as VECTOR of l0; thus v+w =v1+w1 .= w1+v1 .= w +v; end; A3: l is right_zeroed proof let v be VECTOR of l; reconsider v1=v as VECTOR of l0; thus v+0.l= v1 + 0.l0 .= v; end; A4: l is right_complementable proof let v be VECTOR of l; reconsider v1=v as VECTOR of l0; consider w1 being VECTOR of l0 such that A5: v1 + w1 = 0.l0 by ALGSTR_0:def 11; reconsider w = w1 as VECTOR of l; take w; thus thesis by A5; end; A6: for v being VECTOR of l holds 1 * v = v proof let v be VECTOR of l; reconsider v1=v as VECTOR of l0; thus 1*v= 1*v1 .= v by RLVECT_1:def 8; end; A7: for a,b be Real for v being VECTOR of l holds (a * b) * v = a * (b * v) proof let a,b be Real; let v be VECTOR of l; reconsider v1=v as VECTOR of l0; thus (a*b)*v =(a*b)*v1 .=a*(b*v1) by RLVECT_1:def 7 .= a*(b*v); end; A8: for a,b be Real for v being VECTOR of l holds (a + b) * v = a * v + b * v proof let a,b be Real; let v be VECTOR of l; reconsider v1=v as VECTOR of l0; thus (a+b)*v =(a+b)*v1 .=a*v1+b*v1 by RLVECT_1:def 6 .= a*v +b*v; end; A9: for a be Real for v,w being VECTOR of l holds a * (v + w) = a * v + a * w proof let a be Real; let v,w be VECTOR of l; reconsider v1=v, w1=w as VECTOR of l0; thus a*(v+w) =a*(v1+w1) .=a*v1+a*w1 by RLVECT_1:def 5 .= a*v +a*w; end; l is add-associative proof let u,v,w be VECTOR of l; reconsider u1=u, v1=v, w1=w as VECTOR of l0; thus (u + v) + w = (u1+v1)+w1 .= u1+(v1+w1) by RLVECT_1:def 3 .= u+(v+w); end; hence thesis by A2,A3,A4,A9,A8,A7,A6,RLVECT_1:def 5,def 6,def 7,def 8; end; theorem for rseq be Real_Sequence st (for n be Nat holds rseq.n=0) holds rseq is summable & Sum rseq = 0 proof let rseq be Real_Sequence such that A1: for n be Nat holds rseq.n=0; A2: for m be Nat holds Partial_Sums (rseq).m = 0 proof defpred P[Nat] means rseq.$1 = (Partial_Sums rseq).$1; let m be Nat; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A4: rseq.k = (Partial_Sums (rseq)).k; thus rseq.(k+1) = 0 + (rseq).(k+1) .= rseq.k + rseq.(k+1) by A1 .= (Partial_Sums rseq).(k+1) by A4,SERIES_1:def 1; end; A5: P[0] by SERIES_1:def 1; for n be Nat holds P[n] from NAT_1:sch 2(A5,A3); hence (Partial_Sums rseq).m = rseq.m .= 0 by A1; end; A6: for p be Real st 0
0; A8: for n be Nat holds 0 <= Partial_Sums(rseq).n proof let n be Nat; A9: n=n+0 & Partial_Sums(rseq).0 = rseq.0 by SERIES_1:def 1; 0 <=rseq.0 by A1; hence thesis by A6,A9,SEQM_3:5; end; Partial_Sums(rseq).n1 >0 proof now per cases; case A10: n1=0; then Partial_Sums(rseq).n1=rseq.0 by SERIES_1:def 1; hence thesis by A1,A7,A10; end; case A11: n1<>0; set nn=n1-1; A12: nn+1 =n1 & 0 <= rseq.n1 by A1; A13: n1 in NAT by ORDINAL1:def 12; 0 <= n1 by NAT_1:2; then 0 + 1 <= n1 by A11,INT_1:7,A13; then A14: nn in NAT by INT_1:5,A13; then A15: Partial_Sums(rseq).(nn+1) = Partial_Sums(rseq).nn + rseq.(nn+1) by SERIES_1:def 1; 0 <= Partial_Sums(rseq).nn by A8,A14; hence thesis by A7,A12,A15; end; end; hence thesis; end; hence contradiction by A3,A5; end; hence thesis; end; registration cluster l2_Space -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; coherence by Th6,Th7; end;