:: Sequences in $R^n$
:: by Agnieszka Sakowicz , Jaros{\l}aw Gryko and Adam Grabowski
::
:: Received May 10, 1994
:: Copyright (c) 1994-2017 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, SEQ_1, NAT_1, EUCLID, REAL_1, PRE_TOPC,
FUNCT_1, RELAT_1, VALUED_0, TARSKI, STRUCT_0, SUPINF_2, ARYTM_3, ARYTM_1,
COMPLEX1, VALUED_1, CARD_1, XXREAL_0, XXREAL_2, SEQ_2, ORDINAL2,
XBOOLE_0, PARTFUN1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1,
VALUED_1, PARTFUN1, COMPLEX1, REAL_1, PRE_TOPC, XXREAL_0, XCMPLX_0,
XREAL_0, NAT_1, SEQ_1, STRUCT_0, RLVECT_1, VFUNCT_1, EUCLID;
constructors REAL_1, COMPLEX1, MONOID_0, EUCLID, RELSET_1, BINOP_2, VFUNCT_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0,
MONOID_0, EUCLID, XBOOLE_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FUNCT_2;
equalities STRUCT_0, RLVECT_1;
theorems FUNCT_1, FUNCT_2, TARSKI, EUCLID, SEQ_1, NAT_1, XBOOLE_0, NORMSP_1,
XCMPLX_0, XREAL_1, COMPLEX1, XXREAL_0, VFUNCT_1, ORDINAL1, RLVECT_1;
schemes SEQ_1, NAT_1;
begin
definition
let N be Nat;
mode Real_Sequence of N is sequence of TOP-REAL N;
end;
reserve N for Nat;
reserve n,m,n1,n2 for Nat;
reserve q,r,r1,r2 for Real;
reserve x,y for set;
reserve w,w1,w2,g,g1,g2 for Point of TOP-REAL N;
reserve seq,seq1,seq2,seq3,seq9 for Real_Sequence of N;
theorem Th1:
for f being Function holds f is Real_Sequence of N iff (dom f=NAT
& for n holds f.n is Point of TOP-REAL N)
proof
let f be Function;
thus f is Real_Sequence of N implies
(dom f=NAT & for n being Nat holds f.n is Point
of TOP-REAL N)
by NORMSP_1:12,ORDINAL1:def 12;
assume that
A1: dom f=NAT and
A2: for n holds f.n is Point of TOP-REAL N;
for x holds x in NAT implies f.x is Point of TOP-REAL N by A2;
hence thesis by A1,NORMSP_1:12;
end;
definition
let N;
let IT be Real_Sequence of N;
attr IT is non-zero means
rng IT c= NonZero TOP-REAL N;
end;
theorem Th2:
seq is non-zero iff for x st x in NAT holds seq.x<>0.TOP-REAL N
proof
thus seq is non-zero implies for x st x in NAT holds seq.x<>0.TOP-REAL N
proof
assume seq is non-zero;
then
A1: rng seq c= NonZero TOP-REAL N;
let x;
assume x in NAT;
then x in dom seq by Th1;
then seq.x in rng seq by FUNCT_1:def 3;
then not seq.x in {0.TOP-REAL N} by A1,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
assume
A2: for x st x in NAT holds seq.x<>0.TOP-REAL N;
now
let y be object;
assume y in rng seq;
then consider x being object such that
A3: x in dom seq and
A4: seq.x=y by FUNCT_1:def 3;
A5: x in NAT by A3,NORMSP_1:12;
then y<>0.TOP-REAL N by A2,A4;
then
A6: not y in {0.TOP-REAL N} by TARSKI:def 1;
y is Point of TOP-REAL N by A4,A5,NORMSP_1:12;
hence y in NonZero TOP-REAL N by A6,XBOOLE_0:def 5;
end;
then rng seq c= NonZero TOP-REAL N by TARSKI:def 3;
hence thesis;
end;
theorem Th3:
seq is non-zero iff for n holds seq.n<>0.TOP-REAL N
proof
thus seq is non-zero implies for n holds seq.n<>0.TOP-REAL N
by ORDINAL1:def 12,Th2;
assume for n holds seq.n<>0.TOP-REAL N;
then for x holds x in NAT implies seq.x<>0.TOP-REAL N;
hence thesis by Th2;
end;
definition
let N be Nat,seq1,seq2 be Real_Sequence of N;
func seq1 + seq2 -> Real_Sequence of N equals
seq1 + seq2;
coherence
proof
A1: dom seq1 = NAT & dom seq2 = NAT by FUNCT_2:def 1;
dom (seq1+seq2) = dom seq1 /\ dom seq2 by VFUNCT_1:def 1;
hence thesis by A1,FUNCT_2:67;
end;
end;
definition
let r be Real;
let N be Nat,seq be Real_Sequence of N;
func r * seq -> Real_Sequence of N equals
r(#)seq;
coherence
proof
A1: dom seq = NAT by FUNCT_2:def 1;
dom (r(#)seq) = dom seq by VFUNCT_1:def 4;
hence thesis by A1,FUNCT_2:67;
end;
end;
definition
let N be Nat,seq be Real_Sequence of N;
func - seq -> Real_Sequence of N equals
- seq;
coherence
proof
A1: dom seq = NAT by FUNCT_2:def 1;
dom (-seq) = dom seq by VFUNCT_1:def 5;
hence thesis by A1,FUNCT_2:67;
end;
end;
definition
let N be Nat,seq1,seq2 be Real_Sequence of N;
func seq1 - seq2 -> Real_Sequence of N equals
seq1 +- seq2;
correctness;
end;
definition
let N be Nat,seq be Real_Sequence of N;
func |.seq.| -> Real_Sequence means
:Def6:
for n being Nat holds it.n = |.seq.n.|;
existence
proof
deffunc U(Nat) = |.seq.$1.|;
thus ex s being Real_Sequence st
for n being Nat holds s.n= U(n) from SEQ_1:sch 1;
end;
uniqueness
proof
let seq8,seq9 be Real_Sequence such that
A1: for n being Nat holds seq8.n=|.seq.n.| and
A2: for n being Nat holds seq9.n=|.seq.n.|;
let n be Element of NAT;
seq9.n=|.seq.n.| by A2;
hence seq8.n=seq9.n by A1;
end;
end;
theorem Th4:
for N,n be Nat,seq1,seq2 be Real_Sequence of N holds
(seq1+seq2).n = seq1.n + seq2.n
proof
let N,n be Nat,seq1,seq2 be Real_Sequence of N;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(seq1+seq2) = NAT by FUNCT_2:def 1;
thus (seq1+seq2).n = (seq1+seq2)/.m
.= seq1/.m + seq2/.m by A1,VFUNCT_1:def 1
.= seq1.n + seq2.n;
end;
theorem Th5:
for N,n be Nat,seq be Real_Sequence of N holds
(r*seq).n = r*seq.n
proof
let N,n be Nat,seq be Real_Sequence of N;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(r*seq) = NAT by FUNCT_2:def 1;
thus (r*seq).n = (r*seq)/.m
.= r*seq/.m by A1,VFUNCT_1:def 4
.= r*seq.n;
end;
theorem Th6:
for N,n be Nat,seq be Real_Sequence of N holds
(-seq).n = -seq.n
proof
let N,n be Nat,seq be Real_Sequence of N;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom(-seq) = NAT by FUNCT_2:def 1;
thus (-seq).n = (-seq)/.m
.= -seq/.m by A1,VFUNCT_1:def 5
.= -seq.n;
end;
theorem Th7:
|.r.|*|.w.| = |.r*w.| by EUCLID:11;
theorem
|.r*seq.| = |.r.|(#)|.seq.|
proof
let n be Element of NAT;
thus |.r*seq.|.n=|.(r*seq).n.| by Def6
.=|.r*(seq.n).| by Th5
.=|.r.|*|.seq.n.| by Th7
.=|.r.|*(|.seq.|).n by Def6
.=(|.r.|(#)|.seq.|).n by SEQ_1:9;
end;
theorem
seq1 + seq2 = seq2 + seq1
proof
let n be Element of NAT;
thus (seq1+seq2).n = seq1.n + seq2.n by Th4
.= (seq2 + seq1).n by Th4;
end;
theorem Th10:
(seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proof
let n be Element of NAT;
thus ((seq1+seq2)+seq3).n = (seq1+seq2).n+ seq3.n by Th4
.= seq1.n+seq2.n+seq3.n by Th4
.=seq1.n+(seq2.n+seq3.n) by RLVECT_1:def 3
.=seq1.n+(seq2+seq3).n by Th4
.=(seq1+(seq2+seq3)).n by Th4;
end;
theorem Th11:
-seq = (-1)*seq
proof
let n be Element of NAT;
thus ((-1)*seq).n=(-1)*seq.n by Th5
.=-seq.n by RLVECT_1:16
.=(-seq).n by Th6;
end;
theorem Th12:
r*(seq1 + seq2) = r*seq1 + r*seq2
proof
let n be Element of NAT;
thus (r*(seq1 + seq2)).n=r*(seq1+seq2).n by Th5
.=r*(seq1.n+seq2.n) by Th4
.=r*seq1.n+r*seq2.n by RLVECT_1:def 5
.=(r*seq1).n+r*seq2.n by Th5
.=(r*seq1).n+(r*seq2).n by Th5
.=((r*seq1)+(r*seq2)).n by Th4;
end;
theorem Th13:
(r*q)*seq = r*(q*seq)
proof
let n be Element of NAT;
thus ((r*q)*seq).n=(r*q)*seq.n by Th5
.=r*(q*seq.n) by RLVECT_1:def 7
.=r*(q*seq).n by Th5
.=(r*(q*seq)).n by Th5;
end;
theorem Th14:
r*(seq1 - seq2) = r*seq1 - r*seq2
proof
thus r*(seq1-seq2)=r*seq1+r*(-seq2) by Th12
.=r*seq1+r*((-1)*seq2) by Th11
.=r*seq1+((-1)*r)*seq2 by Th13
.=r*seq1+(-1)*(r*seq2) by Th13
.=r*seq1-(r*seq2) by Th11;
end;
theorem
seq1 - (seq2 + seq3) = seq1 - seq2 - seq3
proof
thus seq1-(seq2+seq3)=seq1+(-1)*(seq2+seq3) by Th11
.=seq1+((-1)*seq2+(-1)*seq3) by Th12
.=seq1+(-seq2+(-1)*seq3) by Th11
.=seq1+(-seq2+-seq3) by Th11
.=seq1-seq2-seq3 by Th10;
end;
theorem Th16:
1*seq=seq
proof
let n be Element of NAT;
thus (1*seq).n=1*seq.n by Th5
.=seq.n by RLVECT_1:def 8;
end;
theorem Th17:
-(-seq) = seq
proof
thus -(-seq)=(-1)*(-seq) by Th11
.=(-1)*((-1)*seq) by Th11
.=((-1)*(-1))*seq by Th13
.=seq by Th16;
end;
theorem
seq1 - (-seq2) = seq1 + seq2 by Th17;
theorem
seq1 - (seq2 - seq3) = seq1 - seq2 + seq3
proof
thus seq1-(seq2-seq3)=seq1+(-1)*(seq2-seq3) by Th11
.=seq1+((-1)*seq2-((-1)*seq3)) by Th14
.=seq1+(-seq2-((-1)*seq3)) by Th11
.=seq1+(-seq2-(-seq3)) by Th11
.=seq1+(-seq2+seq3) by Th17
.=seq1-seq2+seq3 by Th10;
end;
theorem
seq1 + (seq2 - seq3) = seq1 + seq2 - seq3 by Th10;
theorem Th21:
r <> 0 & seq is non-zero implies r*seq is non-zero
proof
assume that
A1: r<>0 and
A2: seq is non-zero and
A3: not r*seq is non-zero;
consider n1 such that
A4: (r*seq).n1=0.TOP-REAL N by A3,Th3;
A5: seq.n1 <> 0.TOP-REAL N by A2,Th3;
r*seq.n1=0.TOP-REAL N by A4,Th5;
hence contradiction by A1,A5,RLVECT_1:11;
end;
theorem
seq is non-zero implies -seq is non-zero
proof
assume seq is non-zero;
then (-1)*seq is non-zero by Th21;
hence thesis by Th11;
end;
theorem Th23:
|.0.TOP-REAL N.| = 0
proof
thus |.0.TOP-REAL N.| = |.0*N.| by EUCLID:70
.= 0 by EUCLID:7;
end;
theorem Th24:
|.w.| = 0 implies w = 0.TOP-REAL N
proof
reconsider s = w as Element of REAL N by EUCLID:22;
assume |.w.| = 0;
then s = 0*N by EUCLID:8
.= 0.TOP-REAL N by EUCLID:70;
hence thesis;
end;
theorem
|.w.| >= 0;
theorem
|.-w.| = |.w.| by EUCLID:71;
theorem Th27:
|.w1 - w2.| = |.w2 - w1.|
proof
thus |.w1 - w2.| = |.-(w1 - w2).| by EUCLID:71
.= |.w2 - w1.| by RLVECT_1:33;
end;
Lm1: |.w1 - w2.| = 0 implies w1 = w2
proof
assume |.w1 - w2.| = 0;
then w1 - w2 = 0.TOP-REAL N by Th24;
hence thesis by RLVECT_1:21;
end;
Lm2: w1 = w2 implies |.w1 - w2.| = 0
proof
assume w1 = w2;
then |.w1 - w2.| = |.0.TOP-REAL N.| by RLVECT_1:5
.= 0 by Th23;
hence thesis;
end;
theorem
|.w1 - w2.| = 0 iff w1 = w2 by Lm1,Lm2;
theorem Th29:
|.w1 + w2.| <= |.w1.| + |.w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
w1 + w2 = s1 + s2;
hence thesis by EUCLID:12;
end;
theorem
|.w1 - w2.| <= |.w1.| + |.w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
w1 - w2 = s1 - s2;
hence thesis by EUCLID:13;
end;
theorem
|.w1.| - |.w2.| <= |.w1 + w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
w1 + w2 = s1 + s2;
hence thesis by EUCLID:14;
end;
theorem Th32:
|.w1.| - |.w2.| <= |.w1 - w2.|
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
w1 - w2 = s1 - s2;
hence thesis by EUCLID:15;
end;
theorem
w1 <> w2 implies |.w1 - w2.| > 0
proof
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
s1 - s2 = w1 - w2;
hence thesis by EUCLID:17;
end;
theorem
|.w1 - w2.| <= |.w1 - w.| + |.w - w2.|
proof
0.TOP-REAL N = w - w by RLVECT_1:5
.= -w + w;
then |.w1 - w2.| = |.w1 + ((-w) + w) - w2.| by RLVECT_1:4
.= |.w1 + (-w) + w - w2.| by RLVECT_1:def 3
.= |.(w1 - w) + w - w2.|
.= |.(w1 - w) + (w - w2).| by RLVECT_1:def 3;
hence thesis by Th29;
end;
definition
let N;
let IT be Real_Sequence of N;
attr IT is bounded means
ex r st for n holds |.IT.n.| < r;
end;
theorem Th35:
for n ex r st (0 Point of TOP-REAL N means
:Def9:
for r st 0g2;
A5: now
assume |.g1-g2.|=0;
then 0.TOP-REAL N+g2=g1-g2+g2 by Th24;
then g2=g1-g2+g2 by RLVECT_1:4
.=g1-(g2-g2) by RLVECT_1:29
.=g1-0.TOP-REAL N by RLVECT_1:5
.=g1+ -0.TOP-REAL N
.=g1+(-1)*0.TOP-REAL N by RLVECT_1:16
.=g1+0.TOP-REAL N by RLVECT_1:10
.=g1 by RLVECT_1:4;
hence contradiction by A4;
end;
then consider n1 such that
A6: for m st n1<=m holds |.seq.m-g1.|<|.g1-g2.|/4 by A2,XREAL_1:224;
consider n2 such that
A7: for m st n2<=m holds |.seq.m-g2.|<|.g1-g2.|/4 by A3,A5,XREAL_1:224;
A8: |.seq.(n1+n2)-g2.|<|.g1-g2.|/4 by A7,NAT_1:12;
|.seq.(n1+n2)-g1.|<|.g1-g2.|/4 by A6,NAT_1:12;
then
A9: |.seq.(n1+n2)-g2.|+|.seq.(n1+n2)-g1.|<|.g1-g2.|/4+|.g1-g2.|/4 by A8,
XREAL_1:8;
|.g1-g2.|=|.g1-g2+0.TOP-REAL N.| by RLVECT_1:4
.=|.g1-g2+(-1)*0.TOP-REAL N.| by RLVECT_1:10
.= |.g1-g2+-0.TOP-REAL N.| by RLVECT_1:16
.= |.g1-g2-0.TOP-REAL N.|
.=|.g1-g2-(seq.(n1+n2)-seq.(n1+n2)).| by RLVECT_1:5
.=|.g1-g2-seq.(n1+n2)+seq.(n1+n2).| by RLVECT_1:29
.=|.g1-(seq.(n1+n2)+g2)+seq.(n1+n2).| by RLVECT_1:27
.=|.g1-seq.(n1+n2)-g2+seq.(n1+n2).| by RLVECT_1:27
.=|.g1-seq.(n1+n2)-(g2-seq.(n1+n2)).| by RLVECT_1:29
.=|.g1-seq.(n1+n2)+-(g2-seq.(n1+n2)).|
.=|.g1-seq.(n1+n2)+(seq.(n1+n2)-g2).| by RLVECT_1:33
.=|.-(seq.(n1+n2)-g1)+(seq.(n1+n2)-g2).| by RLVECT_1:33;
then |.g1-g2.|<=|.-(seq.(n1+n2)-g1).|+|.seq.(n1+n2)-g2.| by Th29;
then
A10: |.g1-g2.|<=|.seq.(n1+n2)-g1.|+|.seq.(n1+n2)-g2.| by EUCLID:71;
|.g1-g2.|/2 <|.g1-g2.| by A5,XREAL_1:216;
hence contradiction by A9,A10,XXREAL_0:2;
end;
end;
theorem Th36:
seq is convergent & seq9 is convergent implies seq + seq9 is convergent
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent;
consider g1 such that
A3: for r st 00;
then
A5: 0<|.r.| by COMPLEX1:47;
let q;
assume 00;
then
A8: 0<|.r.| by COMPLEX1:47;
let q;
assume 0|.r.| by A7,COMPLEX1:47;
A12: |.r.|*(q/|.r.|)=|.r.|*(|.r.|"*q) by XCMPLX_0:def 9
.=|.r.|*|.r.|"*q
.=1*q by A11,XCMPLX_0:def 7
.=q;
|.((r*seq).m)-r*(lim seq).|=|.r*seq.m-r*(lim seq).| by Th5
.=|.r*(seq.m-(lim seq)).| by RLVECT_1:34
.=|.r.|*|.seq.m-(lim seq).| by Th7;
hence |.((r*seq).m)-r*(lim seq).| 0.TOP-REAL N implies ex n st
for m st n<=m holds |.(lim seq).|/2 < |.seq.m.|)
proof
assume that
A1: seq is convergent and
A2: (lim seq)<>0.TOP-REAL N;
0 <> |.(lim seq).| by A2,Th24;
then 0<|.(lim seq).|/2 by XREAL_1:215;
then consider n1 such that
A3: for m st n1<=m holds |.seq.m-(lim seq).|<|.(lim seq).|/2 by A1,Def9;
take n=n1;
let m;
assume n<=m;
then
A4: |.seq.m-(lim seq).|<|.(lim seq).|/2 by A3;
|.(lim seq).|-|.seq.m.|<=|.(lim seq)-seq.m.| & |.(lim seq)-seq.m.|=|.seq
.m-( lim seq).| by Th27,Th32;
then
A5: |.(lim seq).|-|.seq.m.|<|.(lim seq).|/2 by A4,XXREAL_0:2;
|.(lim seq).|/2+(|.seq.m.|-|.(lim seq).|/2) =|.seq.m.| & |.(lim seq).|-
|.seq .m.|+(|.seq.m.|-|.(lim seq).|/2) =|.(lim seq).|/2;
hence thesis by A5,XREAL_1:6;
end;