:: Real Linear Space of Real Sequences
:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, 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<p ex n be Nat
st for m being Nat st n<=m holds |.(Partial_Sums rseq).m-0 .|<p
proof
let p be Real such that
A7: 0<p;
take 0;
let m be Nat such that
0<=m;
|.(Partial_Sums rseq).m-0 .| = |.0-0 .| by A2
.= 0 by ABSVALUE:def 1;
hence thesis by A7;
end;
then
A8: Partial_Sums rseq is convergent by SEQ_2:def 6;
then lim (Partial_Sums rseq) = 0 by A6,SEQ_2:def 7;
hence thesis by A8,SERIES_1:def 2,def 3;
end;
theorem
for rseq be Real_Sequence st (for n be Nat holds 0 <= rseq.n) &
rseq is summable & Sum rseq=0 holds for n be Nat holds rseq.n = 0
proof
let rseq be Real_Sequence such that
A1: for n be Nat holds 0 <= rseq.n and
A2: rseq is summable and
A3: Sum rseq=0;
A4: Partial_Sums rseq is bounded_above by A1,A2,SERIES_1:17;
A5: for n be Nat holds (Partial_Sums rseq).n <= Sum rseq
proof
let n be Nat;
(Partial_Sums(rseq)).n <= lim Partial_Sums rseq by A1,A4,SEQ_4:37
,SERIES_1:16;
hence thesis by SERIES_1:def 3;
end;
A6: Partial_Sums rseq is non-decreasing by A1,SERIES_1:16;
now
given n1 be Nat such that
A7: rseq.n1 <> 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;