:: Convergent Sequences in Complex Unitary Space
:: by Noboru Endou
::
:: Received February 10, 2004
:: Copyright (c) 2004-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, CSSPACE, PRE_TOPC, XCMPLX_0, REAL_1, NAT_1, SUBSET_1,
ORDINAL2, SUPINF_2, SEQ_2, XXREAL_0, CARD_1, METRIC_1, FUNCT_1, ARYTM_3,
ARYTM_1, RELAT_1, COMPLEX1, NORMSP_1, SEQ_1, TARSKI, STRUCT_0, XBOOLE_0,
BHSP_3, XXREAL_2, VALUED_0, REWRITE1;
notations TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, RELAT_1, NAT_1, SEQ_1, VALUED_0, STRUCT_0, PRE_TOPC,
RLVECT_1, VFUNCT_1, NORMSP_1, BHSP_1, SEQ_2, CLVECT_1, CSSPACE, RECDEF_1;
constructors REAL_1, COMPLEX1, SEQ_2, BHSP_3, CSSPACE, VALUED_1, RECDEF_1,
RELSET_1, VFUNCT_1, COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, MEMBERED,
STRUCT_0, VALUED_0, VFUNCT_1, FUNCT_2;
requirements SUBSET, REAL, NUMERALS, ARITHM;
theorems XBOOLE_0, TARSKI, ABSVALUE, SEQ_2, SEQM_3, FUNCT_1, NAT_1, FUNCT_2,
RLVECT_1, XCMPLX_0, XBOOLE_1, CLVECT_1, COMPLEX1, NORMSP_1, CSSPACE,
SUBSET_1, XREAL_1, XXREAL_0, ORDINAL1, BHSP_1, VALUED_0;
schemes SEQ_1, FRAENKEL, NAT_1;
begin :: Convergence in complex unitary space
reserve X for ComplexUnitarySpace;
reserve x, y, w, g, g1, g2 for Point of X;
reserve z for Complex;
reserve p, q, r, M, M1, M2 for Real;
reserve seq, seq1, seq2, seq3 for sequence of X;
reserve k,n,m for Nat;
reserve Nseq for increasing sequence of NAT;
deffunc 09(ComplexUnitarySpace) = 0. $1;
definition
let X, seq;
attr seq is convergent means
ex g st for r st r > 0 ex m st for n st n >= m holds dist(seq.n, g) < r;
end;
theorem Th1:
seq is constant implies seq is convergent
proof
assume seq is constant;
then consider x such that
A1: for n being Nat holds seq.n = x by VALUED_0:def 18;
take g = x;
let r such that
A2: r > 0;
take m = 0;
let n such that n >= m;
dist((seq.n) , g) = dist(x, g) by A1
.= 0 by CSSPACE:50;
hence thesis by A2;
end;
theorem Th2:
seq1 is convergent & (ex k st for n st k <= n holds seq2.n = seq1
.n) implies seq2 is convergent
proof
assume that
A1: seq1 is convergent and
A2: ex k st for n st k <= n holds seq2.n = seq1.n;
consider k such that
A3: for n st n >= k holds seq2.n = seq1.n by A2;
consider g such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq1.n) , g) < r
by A1;
take h = g;
let r;
assume r > 0;
then consider m1 be Nat such that
A5: for n st n >= m1 holds dist((seq1.n) , h) < r by A4;
A6: now
assume
A7: m1 <= k;
take m = k;
let n;
assume
A8: n >= m;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq1.n) , g) < r by A5;
hence dist((seq2.n) , h) < r by A3,A8;
end;
now
assume
A9: k <= m1;
take m = m1;
let n;
assume
A10: n >= m;
then seq2.n = seq1.n by A3,A9,XXREAL_0:2;
hence dist((seq2.n) , h) < r by A5,A10;
end;
hence thesis by A6;
end;
theorem Th3:
seq1 is convergent & seq2 is convergent implies seq1 + seq2 is convergent
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
consider g1 such that
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq1.n) , g1) < r
by A1;
consider g2 be Point of X such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq2.n) , g2) < r
by A2;
take g = g1 + g2;
let r;
assume
A5: r > 0;
then consider m1 be Nat such that
A6: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A3,XREAL_1:215;
consider m2 be Nat such that
A7: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A4,A5,XREAL_1:215;
take k = m1 + m2;
let n such that
A8: n >= k;
k >= m2 by NAT_1:12;
then n >= m2 by A8,XXREAL_0:2;
then
A9: dist((seq2.n) , g2) < r/2 by A7;
dist((seq1 + seq2).n, g) = dist((seq1.n) + (seq2.n) , (g1 + g2)) by
NORMSP_1:def 2;
then
A10: dist((seq1 + seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
by CSSPACE:56;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A8,XXREAL_0:2;
then dist((seq1.n) , g1) < r/2 by A6;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A9,XREAL_1:8;
hence thesis by A10,XXREAL_0:2;
end;
theorem Th4:
seq1 is convergent & seq2 is convergent implies seq1 - seq2 is convergent
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
consider g1 such that
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq1.n) , g1) < r
by A1;
consider g2 be Point of X such that
A4: for r st r > 0 ex m st for n st n >= m holds dist((seq2.n) , g2) < r
by A2;
take g = g1 - g2;
let r;
assume
A5: r > 0;
then consider m1 be Nat such that
A6: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A3,XREAL_1:215;
consider m2 be Nat such that
A7: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A4,A5,XREAL_1:215;
take k = m1 + m2;
let n such that
A8: n >= k;
k >= m2 by NAT_1:12;
then n >= m2 by A8,XXREAL_0:2;
then
A9: dist((seq2.n) , g2) < r/2 by A7;
dist((seq1 - seq2).n, g) = dist((seq1.n) - (seq2.n) , (g1 - g2)) by
NORMSP_1:def 3;
then
A10: dist((seq1 - seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
by CSSPACE:57;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A8,XXREAL_0:2;
then dist((seq1.n) , g1) < r/2 by A6;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A9,XREAL_1:8;
hence thesis by A10,XXREAL_0:2;
end;
theorem Th5:
seq is convergent implies z * seq is convergent
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , g) < r;
take h = z * g;
A2: now
A3: 0/|.z.| = 0;
assume
A4: z <> 0;
then
A5: |.z.| > 0 by COMPLEX1:47;
let r;
assume r > 0;
then consider m1 be Nat such that
A6: for n st n >= m1 holds dist((seq.n) , g) < r/|.z.| by A1,A5,A3,XREAL_1:74;
take k = m1;
let n;
assume n >= k;
then
A7: dist((seq.n) , g) < r/|.z.| by A6;
A8: |.z.| <> 0 by A4,COMPLEX1:47;
A9: |.z.| * (r/|.z.|) = |.z.| * (|.z.|" * r) by XCMPLX_0:def 9
.= |.z.| *|.z.|" * r
.= 1 * r by A8,XCMPLX_0:def 7
.= r;
dist(z * (seq.n) , z * g) = ||.(z * (seq.n)) - (z * g).|| by CSSPACE:def 16
.= ||.z * ((seq.n) - g).|| by CLVECT_1:9
.= |.z.| * ||.(seq.n) - g.|| by CSSPACE:43
.= |.z.| * dist((seq.n) , g) by CSSPACE:def 16;
then dist((z *(seq.n)) , h) < r by A5,A7,A9,XREAL_1:68;
hence dist((z * seq).n, h) < r by CLVECT_1:def 14;
end;
now
assume
A10: z = 0;
let r;
assume r > 0;
then consider m1 be Nat such that
A11: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n;
assume n >= k;
then
A12: dist((seq.n) , g) < r by A11;
dist(z * (seq.n) , z * g) = dist(0c * (seq.n) , 09(X)) by A10,CLVECT_1:1
.= dist(09(X) , 09(X)) by CLVECT_1:1
.= 0 by CSSPACE:50;
then dist(z * (seq.n) , h) < r by A12,CSSPACE:53;
hence dist((z * seq).n, h) < r by CLVECT_1:def 14;
end;
hence thesis by A2;
end;
theorem Th6:
seq is convergent implies - seq is convergent
proof
assume seq is convergent;
then (-1r) * seq is convergent by Th5;
hence thesis by CSSPACE:70;
end;
theorem Th7:
seq is convergent implies seq + x is convergent
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , g) < r;
take g + x;
let r;
assume r > 0;
then consider m1 be Nat such that
A2: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n;
dist((seq.n)+x,g+x) <= dist((seq.n),g) + dist(x,x) by CSSPACE:56;
then
A3: dist((seq.n) + x, g + x) <= dist((seq.n) , g) + 0 by CSSPACE:50;
assume n >= k;
then dist((seq.n) , g) < r by A2;
then dist((seq.n) + x, g + x) < r by A3,XXREAL_0:2;
hence thesis by BHSP_1:def 6;
end;
theorem Th8:
seq is convergent implies seq - x is convergent
proof
assume seq is convergent;
then seq + (-x) is convergent by Th7;
hence thesis by CSSPACE:71;
end;
theorem Th9:
seq is convergent iff ex g st for r st r > 0 ex m st for n st n
>= m holds ||.(seq.n) - g.|| < r
proof
thus seq is convergent implies ex g st for r st r > 0 ex m st for n st n >=
m holds ||.(seq.n) - g.|| < r
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , g) < r;
take g;
let r;
assume r > 0;
then consider m1 be Nat such that
A2: for n st n >= m1 holds dist((seq.n) , g) < r by A1;
take k = m1;
let n;
assume n >= k;
then dist((seq.n) , g) < r by A2;
hence thesis by CSSPACE:def 16;
end;
( ex g st for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.||
< r ) implies seq is convergent
proof
given g such that
A3: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r;
take g;
let r;
assume r > 0;
then consider m1 be Nat such that
A4: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A3;
take k = m1;
let n;
assume n >= k;
then ||.(seq.n) - g.|| < r by A4;
hence thesis by CSSPACE:def 16;
end;
hence thesis;
end;
definition
let X, seq;
assume
A1: seq is convergent;
func lim seq -> Point of X means
:Def2:
for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , it) < r;
existence by A1;
uniqueness
proof
for x, y st ( for r st r > 0 ex m st for n st n >= m holds dist((seq.n
) , x) < r ) & ( for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , y)
< r ) holds x = y
proof
given x, y such that
A2: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , x) < r and
A3: for r st r > 0 ex m st for n st n >= m holds dist((seq.n) , y) < r and
A4: x <> y;
A5: dist(x, y) > 0 by A4,CSSPACE:54;
then
A6: dist(x, y)/4 > 0/4 by XREAL_1:74;
then consider m1 be Nat such that
A7: for n st n >= m1 holds dist((seq.n) , x) < dist(x, y)/4 by A2;
consider m2 be Nat such that
A8: for n st n >= m2 holds dist((seq.n) , y) < dist(x, y)/4 by A3,A6;
A9: now
assume m1 >= m2;
then
A10: dist((seq.m1) , y) < dist(x, y)/4 by A8;
dist(x, y) = dist(x - (seq.m1) , y - (seq.m1)) by CSSPACE:58;
then
A11: dist(x, y) <= dist((seq.m1) , x) + dist((seq.m1) , y) by CSSPACE:59;
dist((seq.m1) , x) < dist(x, y)/4 by A7;
then dist((seq.m1) , x) + dist((seq.m1) , y) < dist(x, y)/4 + dist(x,
y) /4 by A10,XREAL_1:8;
then dist(x, y) <= dist(x, y)/2 by A11,XXREAL_0:2;
hence contradiction by A5,XREAL_1:216;
end;
now
assume m1 <= m2;
then
A12: dist((seq.m2) , x) < dist(x, y)/4 by A7;
dist(x, y) = dist(x - (seq.m2) , y - (seq.m2)) by CSSPACE:58;
then
A13: dist(x, y) <= dist((seq.m2) , x) + dist((seq.m2) , y) by CSSPACE:59;
dist((seq.m2) , y) < dist(x, y)/4 by A8;
then dist((seq.m2) , x) + dist((seq.m2) , y) < dist(x, y)/4 + dist(x,
y)/4 by A12,XREAL_1:8;
then dist(x, y) <= dist(x, y)/2 by A13,XXREAL_0:2;
hence contradiction by A5,XREAL_1:216;
end;
hence contradiction by A9;
end;
hence thesis;
end;
end;
theorem Th10:
seq is constant & x in rng seq implies lim seq = x
proof
assume that
A1: seq is constant and
A2: x in rng seq;
consider y such that
A3: rng seq = {y} by A1,FUNCT_2:111;
consider w such that
A4: for n being Nat holds seq.n = w by A1,VALUED_0:def 18;
A5: x = y by A2,A3,TARSKI:def 1;
A6: now
let r such that
A7: r > 0;
reconsider m = 0 as Nat;
take m;
let n such that
n >= m;
n in NAT by ORDINAL1:def 12;
then n in dom seq by NORMSP_1:12;
then seq.n in rng seq by FUNCT_1:def 3;
then w in rng seq by A4;
then w = x by A3,A5,TARSKI:def 1;
then seq.n = x by A4;
hence dist((seq.n) , x) < r by A7,CSSPACE:50;
end;
seq is convergent by A1,Th1;
hence thesis by A6,Def2;
end;
theorem
seq is constant & (ex n st seq.n = x) implies lim seq = x
proof
assume that
A1: seq is constant and
A2: ex n st seq.n = x;
consider n such that
A3: seq.n = x by A2;
n in NAT by ORDINAL1:def 12;
then n in dom seq by NORMSP_1:12;
then x in rng seq by A3,FUNCT_1:def 3;
hence thesis by A1,Th10;
end;
theorem
seq1 is convergent & (ex k st for n st n >= k holds seq2.n = seq1.n)
implies lim seq1 = lim seq2
proof
assume that
A1: seq1 is convergent and
A2: ex k st for n st n >= k holds seq2.n = seq1.n;
consider k such that
A3: for n st n >= k holds seq2.n = seq1.n by A2;
A4: now
let r;
assume r > 0;
then consider m1 be Nat such that
A5: for n st n >= m1 holds dist((seq1.n) , (lim seq1)) < r by A1,Def2;
A6: now
assume
A7: m1 <= k;
take m = k;
let n;
assume
A8: n >= m;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq1.n) , (lim seq1)) < r by A5;
hence dist((seq2.n) , (lim seq1)) < r by A3,A8;
end;
now
assume
A9: k <= m1;
take m = m1;
let n;
assume
A10: n >= m;
then seq2.n = seq1.n by A3,A9,XXREAL_0:2;
hence dist((seq2.n) , (lim seq1)) < r by A5,A10;
end;
hence ex m st for n st n >= m holds dist((seq2.n) , (lim seq1)) < r by A6;
end;
seq2 is convergent by A1,A2,Th2;
hence thesis by A4,Def2;
end;
theorem Th13:
seq1 is convergent & seq2 is convergent implies lim (seq1 + seq2
) = (lim seq1) + (lim seq2)
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
set g2 = lim seq2;
set g1 = lim seq1;
set g = g1 + g2;
A3: now
let r;
assume r > 0;
then
A4: r/2 > 0 by XREAL_1:215;
then consider m1 be Nat such that
A5: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A1,Def2;
consider m2 be Nat such that
A6: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A2,A4,Def2;
take k = m1 + m2;
let n such that
A7: n >= k;
k >= m2 by NAT_1:12;
then n >= m2 by A7,XXREAL_0:2;
then
A8: dist((seq2.n) , g2) < r/2 by A6;
dist((seq1 + seq2).n, g) = dist((seq1.n) + (seq2.n) , g1 + g2) by
NORMSP_1:def 2;
then
A9: dist((seq1 + seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
by CSSPACE:56;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq1.n) , g1) < r/2 by A5;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A8,XREAL_1:8;
hence dist((seq1 + seq2).n, g) < r by A9,XXREAL_0:2;
end;
seq1 + seq2 is convergent by A1,A2,Th3;
hence thesis by A3,Def2;
end;
theorem Th14:
seq1 is convergent & seq2 is convergent implies lim (seq1 - seq2
) = (lim seq1) - (lim seq2)
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent;
set g2 = lim seq2;
set g1 = lim seq1;
set g = g1 - g2;
A3: now
let r;
assume r > 0; then
A4: r/2 > 0 by XREAL_1:215;
then consider m1 be Nat such that
A5: for n st n >= m1 holds dist((seq1.n) , g1) < r/2 by A1,Def2;
consider m2 be Nat such that
A6: for n st n >= m2 holds dist((seq2.n) , g2) < r/2 by A2,A4,Def2;
take k = m1 + m2;
let n such that
A7: n >= k;
k >= m2 by NAT_1:12;
then n >= m2 by A7,XXREAL_0:2;
then
A8: dist((seq2.n) , g2) < r/2 by A6;
dist((seq1 - seq2).n, g) = dist((seq1.n) - (seq2.n) , g1 - g2) by
NORMSP_1:def 3;
then
A9: dist((seq1 - seq2).n, g) <= dist((seq1.n) , g1) + dist((seq2.n) , g2)
by CSSPACE:57;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq1.n) , g1) < r/2 by A5;
then dist((seq1.n) , g1) + dist((seq2.n) , g2) < r/2 + r/2 by A8,XREAL_1:8;
hence dist((seq1 - seq2).n, g) < r by A9,XXREAL_0:2;
end;
seq1 - seq2 is convergent by A1,A2,Th4;
hence thesis by A3,Def2;
end;
theorem Th15:
seq is convergent implies lim (z * seq) = z * (lim seq)
proof
set g = lim seq;
set h = z * g;
A1: now
set m1 = the Nat;
assume
A2: z = 0;
let r;
assume
A3: r > 0;
take k = m1;
let n;
assume n >= k;
dist(z*(seq.n), z*g) = dist(0c*(seq.n), 09(X)) by A2,CLVECT_1:1
.= dist(09(X), 09(X)) by CLVECT_1:1
.= 0 by CSSPACE:50;
hence dist((z * seq).n, h) < r by A3,CLVECT_1:def 14;
end;
assume
A4: seq is convergent;
A5: now
A6: 0/|.z.| =0;
assume
A7: z <> 0;
then
A8: |.z.| > 0 by COMPLEX1:47;
let r;
assume r > 0;
then r/|.z.| > 0 by A8,A6,XREAL_1:74;
then consider m1 be Nat such that
A9: for n st n >= m1 holds dist((seq.n),g) < r/|.z.| by A4,Def2;
take k = m1;
let n;
assume n >= k;
then
A10: dist((seq.n) , g) < r/|.z.| by A9;
A11: |.z.| <> 0 by A7,COMPLEX1:47;
A12: |.z.| * (r/|.z.|) = |.z.| * (|.z.|" * r) by XCMPLX_0:def 9
.= |.z.| *|.z.|" * r
.= 1 * r by A11,XCMPLX_0:def 7
.= r;
dist(z*(seq.n), z*g) = ||.(z*(seq.n)) - (z*g).|| by CSSPACE:def 16
.= ||.z * ((seq.n) - g).|| by CLVECT_1:9
.= |.z.| * ||.(seq.n) - g.|| by CSSPACE:43
.= |.z.| * dist((seq.n) , g) by CSSPACE:def 16;
then dist(z * (seq.n) , h) < r by A8,A10,A12,XREAL_1:68;
hence dist((z * seq).n, h) < r by CLVECT_1:def 14;
end;
z * seq is convergent by A4,Th5;
hence thesis by A1,A5,Def2;
end;
theorem Th16:
seq is convergent implies lim (- seq) = - (lim seq)
proof
assume seq is convergent;
then lim ((-1r) * seq) = (-1r) * (lim seq) by Th15;
then lim (- seq) = (-1r) * (lim seq) by CSSPACE:70;
hence thesis by CLVECT_1:3;
end;
theorem Th17:
seq is convergent implies lim (seq + x) = (lim seq) + x
proof
set g = lim seq;
assume
A1: seq is convergent;
A2: now
let r;
assume r > 0;
then consider m1 be Nat such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,Def2;
take k = m1;
let n;
assume n >= k; then
A4: dist((seq.n) , g) < r by A3;
dist((seq.n) , g) = dist((seq.n) - (-x) , g - (-x)) by CSSPACE:58
.= dist((seq.n) + (-(-x)) , g - (-x)) by RLVECT_1:def 11
.= dist((seq.n) + x, g - (-x)) by RLVECT_1:17
.= dist((seq.n) + x, g + (-(-x))) by RLVECT_1:def 11
.= dist((seq.n) + x, g + x) by RLVECT_1:17;
hence dist((seq + x).n, (g + x)) < r by A4,BHSP_1:def 6;
end;
seq + x is convergent by A1,Th7;
hence thesis by A2,Def2;
end;
theorem
seq is convergent implies lim (seq - x) = (lim seq) - x
proof
assume seq is convergent;
then lim (seq + (-x)) = (lim seq) + (-x) by Th17;
then lim (seq - x) = (lim seq) + (-x) by CSSPACE:71;
hence thesis by RLVECT_1:def 11;
end;
theorem Th19:
seq is convergent implies (lim seq = g iff for r st r > 0 ex m
st for n st n >= m holds ||.(seq.n) - g.|| < r)
proof
assume
A1: seq is convergent;
thus lim seq = g implies for r st r > 0 ex m st for n st n >= m holds ||.(
seq.n) - g.|| < r
proof
assume
A2: lim seq = g;
let r;
assume r > 0;
then consider m1 be Nat such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,Def2;
take k = m1;
let n;
assume n >= k;
then dist((seq.n) , g) < r by A3;
hence thesis by CSSPACE:def 16;
end;
( for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r )
implies lim seq = g
proof
assume
A4: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r;
now
let r;
assume r > 0;
then consider m1 be Nat such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A4;
take k = m1;
let n;
assume n >= k;
then ||.(seq.n) - g.|| < r by A5;
hence dist((seq.n) , g) < r by CSSPACE:def 16;
end;
hence thesis by A1,Def2;
end;
hence thesis;
end;
definition
let X, seq;
func ||.seq.|| -> Real_Sequence means
:Def3:
for n holds it.n =||.(seq.n).||;
existence
proof
deffunc F(Nat) = ||.(seq.$1).||;
consider s being Real_Sequence such that
A1: for n holds s.n = F(n) from SEQ_1:sch 1;
take s;
thus thesis by A1;
end;
uniqueness
proof
let s,t be Real_Sequence;
assume that
A2: for n holds s.n = ||.(seq.n).|| and
A3: for n holds t.n = ||.(seq.n).||;
now
let n be Element of NAT;
s.n = ||.(seq.n).|| by A2;
hence s.n = t.n by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th20:
seq is convergent implies ||.seq.|| is convergent
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g.|| < r by Th9;
now
let r be Real;
assume
A2: r > 0;
consider m1 be Nat such that
A3: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2;
take k = m1;
now
let n;
assume n >= k; then
A4: ||.(seq.n) - g.|| < r by A3;
|.||.(seq.n).|| - ||.g.||.| <= ||.(seq.n) - g.|| by CSSPACE:49;
then |.||.(seq.n).|| - ||.g.||.| < r by A4,XXREAL_0:2;
hence |.||.seq.||.n - ||.g.||.| < r by Def3;
end;
hence for n st k <= n holds |.||.seq.||.n - ||.g.||.| < r;
end;
hence thesis by SEQ_2:def 6;
end;
theorem Th21:
seq is convergent & lim seq = g implies ||.seq.|| is convergent
& lim ||.seq.|| = ||.g.||
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: now
let r be Real;
assume
A4: r > 0;
consider m1 be Nat such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4,Th19;
take k = m1;
now
let n;
assume n >= k;
then
A6: ||.(seq.n) - g.|| < r by A5;
|.||.(seq.n).|| - ||.g.||.| <= ||.(seq.n) - g.|| by CSSPACE:49;
then |.||.(seq.n).|| - ||.g.||.| < r by A6,XXREAL_0:2;
hence |.||.seq.||.n - ||.g.||.| < r by Def3;
end;
hence for n st k <= n holds |.||.seq.||.n - ||.g.||.| < r;
end;
||.seq.|| is convergent by A1,Th20;
hence thesis by A3,SEQ_2:def 7;
end;
theorem Th22:
seq is convergent & lim seq = g implies ||.seq - g.|| is
convergent & lim ||.seq - g.|| = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = g;
A3: now
let r be Real;
assume
A4: r > 0;
consider m1 be Nat such that
A5: for n st n >= m1 holds ||.(seq.n) - g.|| < r by A1,A2,A4,Th19;
take k = m1;
let n;
assume n >= k;
then ||.(seq.n) - g.|| < r by A5;
then
A6: ||.((seq.n) - g ) - 09(X).|| < r by RLVECT_1:13;
|.||.(seq.n) - g.|| - ||.09(X).||.| <= ||.((seq.n) - g ) - 09( X )
.|| by CSSPACE:49;
then |.||.(seq.n) - g.|| - ||.09(X).||.| < r by A6,XXREAL_0:2;
then |.(||.(seq.n) - g.|| - 0).| < r by CSSPACE:42;
then |.(||.(seq - g).n.|| - 0).| < r by NORMSP_1:def 4;
hence |.(||.seq - g.||.n - 0).| < r by Def3;
end;
||.seq - g.|| is convergent by A1,Th8,Th20;
hence thesis by A3,SEQ_2:def 7;
end;
definition
let X, seq, x;
func dist(seq, x) -> Real_Sequence means
:Def4:
for n holds it.n =dist((seq. n) , x);
existence
proof
deffunc F(Nat) = dist((seq.$1) , x);
consider s being Real_Sequence such that
A1: for n holds s.n = F(n) from SEQ_1:sch 1;
take s;
thus thesis by A1;
end;
uniqueness
proof
let s,t be Real_Sequence;
assume that
A2: for n holds s.n = dist((seq.n) , x) and
A3: for n holds t.n = dist((seq.n) , x);
now
let n be Element of NAT;
s.n = dist((seq.n) , x) by A2;
hence s.n = t.n by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th23:
seq is convergent & lim seq = g implies dist(seq,g) is convergent
proof
assume
A1: seq is convergent & lim seq = g;
now
let r be Real;
assume
A2: r > 0;
consider m1 be Nat such that
A3: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A2,Def2;
take k = m1;
now
let n;
dist((seq.n) , g) >= 0 by CSSPACE:53;
then
A4: |.(dist((seq.n) , g) - 0).| = dist((seq.n) , g) by ABSVALUE:def 1;
assume n >= k;
then dist((seq.n) , g) < r by A3;
hence |.(dist(seq, g).n - 0).| < r by A4,Def4;
end;
hence for n st k <= n holds |.(dist(seq, g).n - 0).| < r;
end;
hence thesis by SEQ_2:def 6;
end;
theorem Th24:
seq is convergent & lim seq = g implies dist(seq,g) is
convergent & lim dist(seq,g) = 0
proof
assume
A1: seq is convergent & lim seq = g;
A2: now
let r be Real;
assume
A3: r > 0;
consider m1 be Nat such that
A4: for n st n >= m1 holds dist((seq.n) , g) < r by A1,A3,Def2;
take k = m1;
let n;
dist((seq.n) , g) >= 0 by CSSPACE:53;
then
A5: |.(dist((seq.n) , g) - 0).| = dist((seq.n) , g) by ABSVALUE:def 1;
assume n >= k;
then dist((seq.n) , g) < r by A4;
hence |.(dist(seq, g).n - 0).| < r by A5,Def4;
end;
dist(seq, g) is convergent by A1,Th23;
hence thesis by A2,SEQ_2:def 7;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.seq1 + seq2.|| is convergent & lim ||.seq1 + seq2.|| = ||.g1 + g2
.||
proof
assume seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2;
then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
hence thesis by Th21;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.(seq1 + seq2) - (g1 + g2).|| is convergent & lim ||.(seq1 + seq2)
- (g1 + g2).|| = 0
proof
assume seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2;
then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
hence thesis by Th22;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.seq1 - seq2.|| is convergent & lim ||.seq1 - seq2.|| = ||.g1 - g2
.||
proof
assume seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2;
then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
hence thesis by Th21;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies ||.(seq1 - seq2) - (g1 - g2).|| is convergent & lim ||.(seq1 - seq2)
- (g1 - g2).|| = 0
proof
assume seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2;
then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
hence thesis by Th22;
end;
theorem
seq is convergent & lim seq = g implies ||.z * seq.|| is convergent &
lim ||.z * seq.|| = ||.z * g.||
proof
assume seq is convergent & lim seq = g;
then z * seq is convergent & lim (z * seq) = z * g by Th5,Th15;
hence thesis by Th21;
end;
theorem
seq is convergent & lim seq = g implies ||.(z * seq) - (z * g).|| is
convergent & lim ||.(z * seq) - (z * g).|| = 0
proof
assume seq is convergent & lim seq = g;
then z * seq is convergent & lim (z * seq) = z * g by Th5,Th15;
hence thesis by Th22;
end;
theorem
seq is convergent & lim seq = g implies ||.- seq.|| is convergent &
lim ||.- seq.|| = ||.- g.||
proof
assume seq is convergent & lim seq = g;
then - seq is convergent & lim (- seq) = - g by Th6,Th16;
hence thesis by Th21;
end;
theorem
seq is convergent & lim seq = g implies ||.(- seq) - (- g).|| is
convergent & lim ||.(- seq) - (- g).|| = 0
proof
assume seq is convergent & lim seq = g;
then - seq is convergent & lim (- seq) = - g by Th6,Th16;
hence thesis by Th22;
end;
Lm1: seq is convergent & lim seq = g implies ||.seq + x.|| is convergent & lim
||.seq + x.|| = ||.g + x.||
proof
assume seq is convergent & lim seq = g;
then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
hence thesis by Th21;
end;
theorem Th33:
seq is convergent & lim seq = g implies ||.(seq + x) - (g + x)
.|| is convergent & lim ||.(seq + x) - (g + x).|| = 0
proof
assume seq is convergent & lim seq = g;
then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
hence thesis by Th22;
end;
theorem
seq is convergent & lim seq = g implies ||.seq - x.|| is convergent &
lim ||.seq - x.|| = ||.g - x.||
proof
assume
A1: seq is convergent & lim seq = g;
then lim ||.seq + (-x).|| = ||.g + (-x).|| by Lm1;
then
A2: lim ||.seq - x.|| = ||.g + (-x).|| by CSSPACE:71;
||.seq + (-x).|| is convergent by A1,Lm1;
hence thesis by A2,CSSPACE:71,RLVECT_1:def 11;
end;
theorem
seq is convergent & lim seq = g implies ||.(seq - x) - (g - x).|| is
convergent & lim ||.(seq - x) - (g - x).|| = 0
proof
assume
A1: seq is convergent & lim seq = g;
then lim ||.(seq + (-x)) - (g + (-x)).|| = 0 by Th33;
then
A2: lim ||.(seq - x) - (g + (-x)).|| = 0 by CSSPACE:71;
||.(seq + (-x)) - (g + (-x)).|| is convergent by A1,Th33;
then ||.(seq - x) - (g + (-x)).|| is convergent by CSSPACE:71;
hence thesis by A2,RLVECT_1:def 11;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies dist((seq1 + seq2) , (g1 + g2)) is convergent & lim dist((seq1 +
seq2) , (g1 + g2)) = 0
proof
assume seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2;
then seq1 + seq2 is convergent & lim (seq1 + seq2) = g1 + g2 by Th3,Th13;
hence thesis by Th24;
end;
theorem
seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2 implies dist((seq1 - seq2) , (g1 - g2)) is convergent & lim dist((seq1 -
seq2) , (g1 - g2)) = 0
proof
assume seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 =
g2;
then seq1 - seq2 is convergent & lim (seq1 - seq2) = g1 - g2 by Th4,Th14;
hence thesis by Th24;
end;
theorem
seq is convergent & lim seq = g implies dist((z * seq) , (z * g)) is
convergent & lim dist((z * seq) , (z * g)) = 0
proof
assume seq is convergent & lim seq = g;
then z * seq is convergent & lim (z * seq) = z * g by Th5,Th15;
hence thesis by Th24;
end;
theorem
seq is convergent & lim seq = g implies dist((seq + x) , (g + x)) is
convergent & lim dist((seq + x) , (g + x)) = 0
proof
assume seq is convergent & lim seq = g;
then seq + x is convergent & lim (seq + x) = g + x by Th7,Th17;
hence thesis by Th24;
end;
definition
let X, x, r;
func Ball(x,r) -> Subset of X equals
{y where y is Point of X : ||.x - y.||
< r};
coherence
proof
defpred P[Point of X] means ||.x - $1.|| < r;
{y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
10;
hence thesis;
end;
func cl_Ball(x,r) -> Subset of X equals
{y where y is Point of X : ||.x - y
.|| <= r};
coherence
proof
defpred P[Point of X] means ||.x - $1.|| <= r;
{y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
10;
hence thesis;
end;
func Sphere(x,r) -> Subset of X equals
{y where y is Point of X : ||.x - y
.|| = r};
coherence
proof
defpred P[Point of X] means ||.x - $1.|| = r;
{y where y is Point of X : P[y]} c= the carrier of X from FRAENKEL:sch
10;
hence thesis;
end;
end;
theorem Th40:
w in Ball(x,r) iff ||.x - w.|| < r
proof
thus w in Ball(x,r) implies ||.x - w.|| < r
proof
assume w in Ball(x,r);
then ex y be Point of X st w = y & ||.x - y.|| < r;
hence thesis;
end;
thus thesis;
end;
theorem Th41:
w in Ball(x,r) iff dist(x,w) < r
proof
thus w in Ball(x,r) implies dist(x,w) < r
proof
assume w in Ball(x,r);
then ||.x - w.|| < r by Th40;
hence thesis by CSSPACE:def 16;
end;
assume dist(x,w) < r;
then ||.x - w.|| < r by CSSPACE:def 16;
hence thesis;
end;
theorem
r > 0 implies x in Ball(x,r)
proof
A1: dist(x,x) = 0 by CSSPACE:50;
assume r > 0;
hence thesis by A1,Th41;
end;
theorem
y in Ball(x,r) & w in Ball(x,r) implies dist(y,w) < 2 * r
proof
assume that
A1: y in Ball(x,r) and
A2: w in Ball(x,r);
dist(x,w) < r by A2,Th41;
then
A3: r + dist(x,w) < r + r by XREAL_1:6;
A4: dist(y,w) <= dist(y,x) + dist(x,w) by CSSPACE:51;
dist(x,y) < r by A1,Th41;
then dist(x,y) + dist(x,w) < r + dist(x,w) by XREAL_1:6;
then dist(x,y) + dist(x,w) < 2 * r by A3,XXREAL_0:2;
hence thesis by A4,XXREAL_0:2;
end;
theorem
y in Ball(x,r) implies y - w in Ball(x - w,r)
proof
assume y in Ball(x,r); then
A1: dist(x,y) < r by Th41;
dist(x - w,y - w) = dist(x,y) by CSSPACE:58;
hence thesis by A1,Th41;
end;
theorem
y in Ball(x,r) implies (y - x) in Ball (0.(X),r)
proof
assume y in Ball(x,r);
then ||.x - y.|| < r by Th40;
then ||.(-y) + x.|| < r by RLVECT_1:def 11;
then ||.-(y - x).|| < r by RLVECT_1:33;
then ||.09(X) - (y - x).|| < r by RLVECT_1:14;
hence thesis;
end;
theorem
y in Ball(x,r) & r <= q implies y in Ball(x,q)
proof
assume that
A1: y in Ball(x,r) and
A2: r <= q;
||.x - y.|| < r by A1,Th40;
then ||.x - y.|| < q by A2,XXREAL_0:2;
hence thesis;
end;
theorem Th47:
w in cl_Ball(x,r) iff ||.x - w.|| <= r
proof
thus w in cl_Ball(x,r) implies ||.x - w.|| <= r
proof
assume w in cl_Ball(x,r);
then ex y be Point of X st w = y & ||.x - y.|| <= r;
hence thesis;
end;
assume ||.x - w.|| <= r;
hence thesis;
end;
theorem Th48:
w in cl_Ball(x,r) iff dist(x,w) <= r
proof
thus w in cl_Ball(x,r) implies dist(x,w) <= r
proof
assume w in cl_Ball(x,r);
then ||.x - w.|| <= r by Th47;
hence thesis by CSSPACE:def 16;
end;
assume dist(x,w) <= r;
then ||.x - w.|| <= r by CSSPACE:def 16;
hence thesis;
end;
theorem
r >= 0 implies x in cl_Ball(x,r)
proof
assume r >= 0;
then dist(x,x) <= r by CSSPACE:50;
hence thesis by Th48;
end;
theorem Th50:
y in Ball(x,r) implies y in cl_Ball(x,r)
proof
assume y in Ball(x,r);
then ||.x - y.|| <= r by Th40;
hence thesis;
end;
theorem Th51:
w in Sphere(x,r) iff ||.x - w.|| = r
proof
thus w in Sphere(x,r) implies ||.x - w.|| = r
proof
assume w in Sphere(x,r);
then ex y be Point of X st w = y & ||.x - y.|| = r;
hence thesis;
end;
assume ||.x - w.|| = r;
hence thesis;
end;
theorem
w in Sphere(x,r) iff dist(x,w) = r
proof
thus w in Sphere(x,r) implies dist(x,w) = r
proof
assume w in Sphere(x,r);
then ||.x - w.|| = r by Th51;
hence thesis by CSSPACE:def 16;
end;
assume dist(x,w) = r;
then ||.x - w.|| = r by CSSPACE:def 16;
hence thesis;
end;
theorem
y in Sphere(x,r) implies y in cl_Ball(x,r)
proof
assume y in Sphere(x,r);
then ||.x - y.|| = r by Th51;
hence thesis;
end;
theorem Th54:
Ball(x,r) c= cl_Ball(x,r)
proof
for y holds y in Ball(x,r) implies y in cl_Ball(x,r) by Th50;
hence thesis by SUBSET_1:2;
end;
theorem Th55:
Sphere(x,r) c= cl_Ball(x,r)
proof
now
let y;
assume y in Sphere(x,r);
then ||.x - y.|| = r by Th51;
hence y in cl_Ball(x,r);
end;
hence thesis by SUBSET_1:2;
end;
theorem
Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r)
proof
now
let y;
assume y in cl_Ball(x,r);
then
A1: ||.x - y.|| <= r by Th47;
now
per cases by A1,XXREAL_0:1;
case
||.x - y.|| < r;
hence y in Ball(x,r);
end;
case
||.x - y.|| = r;
hence y in Sphere(x,r);
end;
end;
hence y in Ball(x,r) \/ Sphere(x,r) by XBOOLE_0:def 3;
end;
then
A2: cl_Ball(x,r) c= Ball(x,r) \/ Sphere(x,r) by SUBSET_1:2;
Ball(x,r) c= cl_Ball(x,r) & Sphere(x,r) c= cl_Ball(x,r) by Th54,Th55;
then Ball(x,r) \/ Sphere(x,r) c= cl_Ball(x,r) by XBOOLE_1:8;
hence thesis by A2,XBOOLE_0:def 10;
end;
begin :: Cauchy sequence and Hilbert space with complex coefficient
deffunc 09(ComplexUnitarySpace) = 0.$1;
definition
let X;
let seq;
attr seq is Cauchy means
for r st r > 0 ex k st for n, m st n >= k &
m >= k holds dist((seq.n), (seq.m)) < r;
end;
theorem
seq is constant implies seq is Cauchy
proof
assume
A1: seq is constant;
let r such that
A2: r > 0;
take k = 0;
let n, m such that
n >= k and
m >= k;
dist((seq.n), (seq.m)) = dist((seq.n), (seq.n)) by A1,VALUED_0:23
.= 0 by CSSPACE:50;
hence thesis by A2;
end;
theorem
seq is Cauchy iff for r st r > 0 ex k st for n, m st n >= k & m >= k
holds ||.(seq.n) - (seq.m).|| < r
proof
thus seq is Cauchy implies for r st r > 0 ex k st for n, m st n >= k & m >=
k holds ||.(seq.n) - (seq.m).|| < r
proof
assume
A1: seq is Cauchy;
let r;
assume r > 0;
then consider l being Nat such that
A2: for n, m st n >= l & m >= l holds dist((seq.n), (seq.m)) < r by A1;
take k = l;
let n, m;
assume n >= k & m >= k;
then dist((seq.n), (seq.m)) < r by A2;
hence thesis by CSSPACE:def 16;
end;
( for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds ||.(seq.n
) - (seq.m).|| < r ) implies seq is Cauchy
proof
assume
A3: for r st r > 0 ex k st for n, m st n >= k & m >= k holds ||.(seq.n
) - (seq.m).|| < r;
let r;
assume r > 0;
then consider l being Nat such that
A4: for n, m st n >= l & m >= l holds ||.(seq.n) - (seq.m).|| < r by A3;
take k = l;
let n, m;
assume n >= k & m >= k;
then ||.(seq.n) - (seq.m).|| < r by A4;
hence thesis by CSSPACE:def 16;
end;
hence thesis;
end;
theorem
seq1 is Cauchy & seq2 is Cauchy implies seq1 + seq2 is Cauchy
proof
assume that
A1: seq1 is Cauchy and
A2: seq2 is Cauchy;
let r;
assume r > 0;
then
A3: r/2 > 0 by XREAL_1:215;
then consider m1 be Nat such that
A4: for n, m st n >= m1 & m >= m1 holds dist((seq1.n), (seq1.m)) < r/2
by A1;
consider m2 be Nat such that
A5: for n, m st n >= m2 & m >= m2 holds dist((seq2.n), (seq2.m)) < r/2
by A2,A3;
take k = m1 + m2;
let n, m such that
A6: n >= k & m >= k;
k >= m2 by NAT_1:12;
then n >= m2 & m >= m2 by A6,XXREAL_0:2;
then
A7: dist((seq2.n), (seq2.m)) < r/2 by A5;
dist((seq1 + seq2).n, (seq1 + seq2).m) = dist((seq1.n) + (seq2.n), (
seq1 + seq2).m) by NORMSP_1:def 2
.= dist((seq1.n) + (seq2.n), (seq1.m) + (seq2.m)) by NORMSP_1:def 2;
then
A8: dist((seq1 + seq2).n, (seq1 + seq2).m) <= dist((seq1.n), (seq1.m)) +
dist((seq2.n), (seq2.m)) by CSSPACE:56;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 & m >= m1 by A6,XXREAL_0:2;
then dist((seq1.n), (seq1.m)) < r/2 by A4;
then dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r/2 + r/2 by A7,
XREAL_1:8;
hence thesis by A8,XXREAL_0:2;
end;
theorem
seq1 is Cauchy & seq2 is Cauchy implies seq1 - seq2 is Cauchy
proof
assume that
A1: seq1 is Cauchy and
A2: seq2 is Cauchy;
let r;
assume r > 0;
then
A3: r/2 > 0 by XREAL_1:215;
then consider m1 be Nat such that
A4: for n, m st n >= m1 & m >= m1 holds dist((seq1.n), (seq1.m)) < r/2
by A1;
consider m2 be Nat such that
A5: for n, m st n >= m2 & m >= m2 holds dist((seq2.n), (seq2.m)) < r/2
by A2,A3;
take k = m1 + m2;
let n, m such that
A6: n >= k & m >= k;
k >= m2 by NAT_1:12;
then n >= m2 & m >= m2 by A6,XXREAL_0:2;
then
A7: dist((seq2.n), (seq2.m)) < r/2 by A5;
dist((seq1 - seq2).n, (seq1 - seq2).m) = dist((seq1.n) - (seq2.n), (
seq1 - seq2).m) by NORMSP_1:def 3
.= dist((seq1.n) - (seq2.n), (seq1.m) - (seq2.m)) by NORMSP_1:def 3;
then
A8: dist((seq1 - seq2).n, (seq1 - seq2).m) <= dist((seq1.n), (seq1.m)) +
dist((seq2.n), (seq2.m)) by CSSPACE:57;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 & m >= m1 by A6,XXREAL_0:2;
then dist((seq1.n), (seq1.m)) < r/2 by A4;
then dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r/2 + r/2 by A7,
XREAL_1:8;
hence thesis by A8,XXREAL_0:2;
end;
theorem Th61:
seq is Cauchy implies z * seq is Cauchy
proof
assume
A1: seq is Cauchy;
A2: now
A3: 0/|.z.| = 0;
assume
A4: z <> 0;
then
A5: |.z.| > 0 by COMPLEX1:47;
let r;
assume r > 0;
then r/|.z.| > 0 by A5,A3,XREAL_1:74;
then consider m1 be Nat such that
A6: for n, m st n >= m1 & m >= m1 holds dist((seq.n), (seq.m)) < r/|.
z.| by A1;
take k = m1;
let n, m;
assume n >= k & m >= k;
then
A7: dist((seq.n), (seq.m)) < r/|.z.| by A6;
A8: |.z.| <> 0 by A4,COMPLEX1:47;
A9: |.z.| * (r/|.z.|) = |.z.| * (|.z.|" * r) by XCMPLX_0:def 9
.= |.z.| *|.z.|" * r
.= 1 * r by A8,XCMPLX_0:def 7
.= r;
dist(z * (seq.n), z * (seq.m)) = ||.(z * (seq.n)) - (z * (seq.m)).||
by CSSPACE:def 16
.= ||.z * ((seq.n) - (seq.m)).|| by CLVECT_1:9
.= |.z.| * ||.(seq.n) - (seq.m).|| by CSSPACE:43
.= |.z.| * dist((seq.n), (seq.m)) by CSSPACE:def 16;
then dist((z * (seq.n)), (z * (seq.m))) < r by A5,A7,A9,XREAL_1:68;
then dist((z * seq).n, (z * (seq.m))) < r by CLVECT_1:def 14;
hence dist((z * seq).n, (z * seq).m) < r by CLVECT_1:def 14;
end;
now
assume
A10: z = 0;
let r;
assume r > 0;
then consider m1 be Nat such that
A11: for n, m st n >= m1 & m >= m1 holds dist((seq.n), (seq.m)) < r by A1;
take k = m1;
let n, m;
assume n >= k & m >= k;
then
A12: dist((seq.n), (seq.m)) < r by A11;
dist(z * (seq.n), z * (seq.m)) = dist(09(X), 0c * (seq.m)) by A10,
CLVECT_1:1
.= dist(09(X), 09(X)) by CLVECT_1:1
.= 0 by CSSPACE:50;
then dist(z * (seq.n), z * (seq.m)) < r by A12,CSSPACE:53;
then dist((z * seq).n, z * (seq.m)) < r by CLVECT_1:def 14;
hence dist((z * seq).n, (z * seq).m) < r by CLVECT_1:def 14;
end;
hence thesis by A2;
end;
theorem
seq is Cauchy implies - seq is Cauchy
proof
assume seq is Cauchy;
then (-1r) * seq is Cauchy by Th61;
hence thesis by CSSPACE:70;
end;
theorem Th63:
seq is Cauchy implies seq + x is Cauchy
proof
assume
A1: seq is Cauchy;
let r;
assume r > 0;
then consider m1 be Nat such that
A2: for n, m st n >= m1 & m >= m1 holds dist((seq.n), (seq.m)) < r by A1;
take k = m1;
let n, m;
dist((seq.n) + x, (seq.m) + x) <= dist((seq.n), (seq.m)) + dist(x, x) by
CSSPACE:56;
then
A3: dist((seq.n) + x, (seq.m) + x) <= dist((seq.n), (seq.m)) + 0 by CSSPACE:50;
assume n >= k & m >= k;
then dist((seq.n), (seq.m)) < r by A2;
then dist((seq.n) + x, (seq.m) + x) < r by A3,XXREAL_0:2;
then dist((seq + x).n, (seq.m) + x) < r by BHSP_1:def 6;
hence thesis by BHSP_1:def 6;
end;
theorem
seq is Cauchy implies seq - x is Cauchy
proof
assume seq is Cauchy;
then seq + (-x) is Cauchy by Th63;
hence thesis by CSSPACE:71;
end;
theorem
seq is convergent implies seq is Cauchy
proof
assume seq is convergent;
then consider h be Point of X such that
A1: for r st r > 0 ex k st for n st n >= k holds dist((seq.n), h) < r;
let r;
assume r > 0;
then consider m1 be Nat such that
A2: for n st n >= m1 holds dist((seq.n), h) < r/2 by A1,XREAL_1:215;
take k = m1;
let n, m;
assume n >= k & m >= k;
then dist((seq.n), h) < r/2 & dist((seq.m), h) < r/2 by A2;
then dist((seq.n), (seq.m)) <= dist((seq.n), h) + dist(h, (seq.m)) & dist((
seq.n) , h) + dist(h, (seq.m)) < r/2 + r/2 by CSSPACE:51,XREAL_1:8;
hence thesis by XXREAL_0:2;
end;
definition
let X;
let seq1, seq2;
pred seq1 is_compared_to seq2 means
for r st r > 0 ex m st for n st n >= m holds dist(seq1.n, seq2.n) < r;
end;
theorem Th66:
seq is_compared_to seq
proof
let r such that
A1: r > 0;
take m = 0;
let n such that
n >= m;
thus thesis by A1,CSSPACE:50;
end;
theorem Th67:
seq1 is_compared_to seq2 implies seq2 is_compared_to seq1
proof
assume
A1: seq1 is_compared_to seq2;
let r;
assume r > 0;
then consider k such that
A2: for n st n >= k holds dist((seq1.n), (seq2.n)) < r by A1;
take m = k;
let n;
assume n >= m;
hence thesis by A2;
end;
definition
let X;
let seq1, seq2;
redefine pred seq1 is_compared_to seq2; :: redefines is_compared_to (CLVECT_2, definition)
reflexivity by Th66;
symmetry by Th67;
end;
theorem
seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies seq1
is_compared_to seq3
proof
assume that
A1: seq1 is_compared_to seq2 and
A2: seq2 is_compared_to seq3;
let r;
assume r > 0;
then
A3: r/2 > 0 by XREAL_1:215;
then consider m1 be Nat such that
A4: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < r/2 by A1;
consider m2 be Nat such that
A5: for n st n >= m2 holds dist((seq2.n), (seq3.n)) < r/2 by A2,A3;
take m = m1 + m2;
let n such that
A6: n >= m;
m >= m2 by NAT_1:12;
then n >= m2 by A6,XXREAL_0:2;
then
A7: dist((seq2.n), (seq3.n)) < r/2 by A5;
A8: dist((seq1.n), (seq3.n)) <= dist((seq1.n), (seq2.n)) + dist((seq2.n), (
seq3.n)) by CSSPACE:51;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A6,XXREAL_0:2;
then dist((seq1.n), (seq2.n)) < r/2 by A4;
then dist((seq1.n), (seq2.n)) + dist((seq2.n), (seq3.n)) < r/2 + r/2 by A7,
XREAL_1:8;
hence thesis by A8,XXREAL_0:2;
end;
theorem
seq1 is_compared_to seq2 iff for r st r > 0 ex m st for n st n >= m
holds ||.(seq1.n) - (seq2.n).|| < r
proof
thus seq1 is_compared_to seq2 implies for r st r > 0 ex m st for n st n >= m
holds ||.(seq1.n) - (seq2.n).|| < r
proof
assume
A1: seq1 is_compared_to seq2;
let r;
assume r > 0;
then consider m1 be Nat such that
A2: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < r by A1;
take m = m1;
let n;
assume n >= m;
then dist((seq1.n), (seq2.n)) < r by A2;
hence thesis by CSSPACE:def 16;
end;
( for r st r > 0 ex m st for n st n >= m holds ||.(seq1.n) - (seq2.n).||
< r ) implies seq1 is_compared_to seq2
proof
assume
A3: for r st r > 0 ex m st for n st n >= m holds ||.(seq1.n) - (seq2.n
).|| < r;
let r;
assume r > 0;
then consider m1 be Nat such that
A4: for n st n >= m1 holds ||.(seq1.n) - (seq2.n).|| < r by A3;
take m = m1;
let n;
assume n >= m;
then ||.(seq1.n) - (seq2.n).|| < r by A4;
hence thesis by CSSPACE:def 16;
end;
hence thesis;
end;
theorem
( ex k st for n st n >= k holds seq1.n = seq2.n ) implies seq1
is_compared_to seq2
proof
assume ex k st for n st n >= k holds seq1.n = seq2.n;
then consider m such that
A1: for n st n >= m holds seq1.n = seq2.n;
let r such that
A2: r > 0;
take k = m;
let n;
assume n >= k;
then dist((seq1.n), (seq2.n)) = dist((seq1.n), (seq1.n)) by A1
.= 0 by CSSPACE:50;
hence thesis by A2;
end;
theorem
seq1 is Cauchy & seq1 is_compared_to seq2 implies seq2 is Cauchy
proof
assume that
A1: seq1 is Cauchy and
A2: seq1 is_compared_to seq2;
let r;
assume r > 0;
then
A3: r/3 > 0 by XREAL_1:222;
then consider m1 be Nat such that
A4: for n, m st n >= m1 & m >= m1 holds dist((seq1.n), (seq1.m)) < r/3
by A1;
consider m2 be Nat such that
A5: for n st n >= m2 holds dist((seq1.n), (seq2.n)) < r/3 by A2,A3;
take k = m1 + m2;
let n, m such that
A6: n >= k and
A7: m >= k;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 & m >= m1 by A6,A7,XXREAL_0:2;
then
A8: dist((seq1.n), (seq1.m)) < r/3 by A4;
A9: dist((seq2.n), (seq1.m)) <= dist((seq2.n), (seq1.n)) + dist((seq1.n), (
seq1.m)) by CSSPACE:51;
A10: k >= m2 by NAT_1:12;
then n >= m2 by A6,XXREAL_0:2;
then dist((seq1.n), (seq2.n)) < r/3 by A5;
then
dist((seq2.n), (seq1.n)) + dist((seq1.n), (seq1.m)) < r/3 + r/3 by A8,
XREAL_1:8;
then
A11: dist((seq2.n), (seq1.m)) < r/3 + r/3 by A9,XXREAL_0:2;
A12: dist((seq2.n), (seq2.m)) <= dist((seq2.n), (seq1.m)) + dist((seq1.m), (
seq2.m)) by CSSPACE:51;
m >= m2 by A7,A10,XXREAL_0:2;
then dist((seq1.m), (seq2.m)) < r/3 by A5;
then dist((seq2.n), (seq1.m)) + dist((seq1.m), (seq2.m)) < r/3 + r/3 + r/3
by A11,XREAL_1:8;
hence thesis by A12,XXREAL_0:2;
end;
theorem
seq1 is convergent & seq1 is_compared_to seq2 implies seq2 is convergent
proof
assume that
A1: seq1 is convergent and
A2: seq1 is_compared_to seq2;
now
let r;
assume r > 0;
then
A3: r/2 > 0 by XREAL_1:215;
then consider m1 be Nat such that
A4: for n st n >= m1 holds dist((seq1.n), (lim seq1)) < r/2 by A1,Def2;
consider m2 be Nat such that
A5: for n st n >= m2 holds dist((seq1.n), (seq2.n)) < r/2 by A2,A3;
take m = m1 + m2;
let n such that
A6: n >= m;
m >= m2 by NAT_1:12;
then n >= m2 by A6,XXREAL_0:2;
then
A7: dist((seq1.n), (seq2.n)) < r/2 by A5;
A8: dist((seq2.n), (lim seq1)) <= dist((seq2.n), (seq1.n)) + dist((seq1.n
), (lim seq1)) by CSSPACE:51;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A6,XXREAL_0:2;
then dist((seq1.n), (lim seq1)) < r/2 by A4;
then dist((seq2.n), (seq1.n)) + dist((seq1.n), (lim seq1)) < r/2 + r/2 by
A7,XREAL_1:8;
hence dist((seq2.n), (lim seq1)) < r by A8,XXREAL_0:2;
end;
hence thesis;
end;
theorem
seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 implies
seq2 is convergent & lim seq2 = g
proof
assume that
A1: seq1 is convergent & lim seq1 = g and
A2: seq1 is_compared_to seq2;
A3: now
let r;
assume r > 0;
then
A4: r/2 > 0 by XREAL_1:215;
then consider m1 be Nat such that
A5: for n st n >= m1 holds dist((seq1.n), g) < r/2 by A1,Def2;
consider m2 be Nat such that
A6: for n st n >= m2 holds dist((seq1.n), (seq2.n)) < r/2 by A2,A4;
take m = m1 + m2;
let n such that
A7: n >= m;
m >= m2 by NAT_1:12;
then n >= m2 by A7,XXREAL_0:2;
then
A8: dist((seq1.n), (seq2.n)) < r/2 by A6;
A9: dist((seq2.n), g) <= dist((seq2.n), (seq1.n)) + dist((seq1.n), g) by
CSSPACE:51;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A7,XXREAL_0:2;
then dist((seq1.n), g) < r/2 by A5;
then dist((seq2.n), (seq1.n)) + dist((seq1.n), g) < r/2 + r/2 by A8,
XREAL_1:8;
hence dist((seq2.n), g) < r by A9,XXREAL_0:2;
end;
then seq2 is convergent;
hence thesis by A3,Def2;
end;
definition
let X;
let seq;
attr seq is bounded means
ex M st M > 0 & for n holds ||.seq.n.|| <= M;
end;
theorem Th74:
seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded
proof
assume that
A1: seq1 is bounded and
A2: seq2 is bounded;
consider M2 such that
A3: M2 > 0 and
A4: for n holds ||.seq2.n.|| <= M2 by A2;
consider M1 such that
A5: M1 > 0 and
A6: for n holds ||.seq1.n.|| <= M1 by A1;
now
let n;
||.(seq1 + seq2).n.|| = ||.seq1.n + seq2.n.|| by NORMSP_1:def 2;
then
A7: ||.(seq1 + seq2).n.|| <= ||.seq1.n.|| + ||.seq2.n.|| by CSSPACE:46;
||.seq1.n.|| <= M1 & ||.seq2.n.|| <= M2 by A6,A4;
then ||.seq1.n.|| + ||.seq2.n.|| <= M1 + M2 by XREAL_1:7;
hence ||.(seq1 + seq2).n.|| <= M1 + M2 by A7,XXREAL_0:2;
end;
hence thesis by A5,A3;
end;
theorem Th75:
seq is bounded implies -seq is bounded
proof
assume seq is bounded;
then consider M such that
A1: M > 0 and
A2: for n holds ||.seq.n.|| <= M;
now
let n;
||.(- seq).n.|| = ||.- (seq.n).|| by BHSP_1:44
.= ||.seq.n.|| by CSSPACE:47;
hence ||.(- seq).n.|| <= M by A2;
end;
hence thesis by A1;
end;
theorem
seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded
proof
assume that
A1: seq1 is bounded and
A2: seq2 is bounded;
A3: seq1 - seq2 = seq1 + (- seq2) by CSSPACE:64;
- seq2 is bounded by A2,Th75;
hence thesis by A1,A3,Th74;
end;
theorem
seq is bounded implies z * seq is bounded
proof
assume seq is bounded;
then consider M such that
A1: M > 0 and
A2: for n holds ||.seq.n.|| <= M;
A3: z <> 0 implies z * seq is bounded
proof
A4: now
let n;
A5: |.z.| >= 0 by COMPLEX1:46;
||.(z * seq).n.|| = ||.z * (seq.n).|| by CLVECT_1:def 14
.= |.z.| * ||.seq.n.|| by CSSPACE:43;
hence ||.(z * seq).n.|| <= |.z.| * M by A2,A5,XREAL_1:64;
end;
assume z <> 0;
then |.z.| > 0 by COMPLEX1:47;
then |.z.| * M > 0 by A1,XREAL_1:129;
hence thesis by A4;
end;
z = 0 implies z * seq is bounded
proof
assume
A6: z = 0;
now
let n;
||.(z * seq).n.|| = ||.0c * (seq.n).|| by A6,CLVECT_1:def 14
.= ||.09(X).|| by CLVECT_1:1
.= 0 by CSSPACE:42;
hence ||.(z * seq).n.|| <= M by A1;
end;
hence thesis by A1;
end;
hence thesis by A3;
end;
theorem
seq is constant implies seq is bounded
proof
assume seq is constant;
then consider x such that
A1: for n being Nat holds seq.n = x by VALUED_0:def 18;
A2: x = 09(X) implies seq is bounded
proof
consider M being Real such that
A3: M > 0 by XREAL_1:1;
assume
A4: x = 09(X);
for n holds ||.seq.n.|| <= M by A3,CSSPACE:42,A1,A4;
hence thesis by A3;
end;
x <> 09(X) implies seq is bounded
proof
assume x <> 09(X);
consider M being Real such that
A5: ||.x.|| < M by XREAL_1:1;
reconsider M as Real;
||.x.|| >= 0 & for n holds ||.seq.n.|| <= M by A1,A5,CSSPACE:44;
hence thesis by A5;
end;
hence thesis by A2;
end;
theorem Th79:
for m ex M st ( M > 0 & for n st n <= m holds ||.seq.n.|| < M )
proof
defpred P[Nat] means
ex M st ( M > 0 & for n st n <= $1 holds ||.seq.n.|| < M );
A1: for m st P[m] holds P[m+1]
proof
let m;
given M1 such that
A2: M1 > 0 and
A3: for n st n <= m holds ||.seq.n.|| < M1;
A4: now
assume
A5: ||.seq.(m+1).|| >= M1;
take M = ||.seq.(m+1).|| + 1;
M > 0 + 0 by CSSPACE:44,XREAL_1:8;
hence M > 0;
let n such that
A6: n <= m + 1;
A7: now
assume m >= n;
then ||.seq.n.|| < M1 by A3;
then ||.seq.n.|| < ||.seq.(m+1).|| by A5,XXREAL_0:2;
then ||.seq.n.|| + 0 < M by XREAL_1:8;
hence ||.seq.n.|| < M;
end;
now
assume n = m + 1;
then ||.seq.n.|| + 0 < M by XREAL_1:8;
hence ||.seq.n.|| < M;
end;
hence ||.seq.n.|| < M by A6,A7,NAT_1:8;
end;
now
assume
A8: ||.seq.(m+1).|| <= M1;
take M = M1 + 1;
thus M > 0 by A2;
let n such that
A9: n <= m + 1;
A10: now
assume m >= n;
then
A11: ||.seq.n.|| < M1 by A3;
M > M1 + 0 by XREAL_1:8;
hence ||.seq.n.|| < M by A11,XXREAL_0:2;
end;
now
A12: M > M1 + 0 by XREAL_1:8;
assume n = m + 1;
hence ||.seq.n.|| < M by A8,A12,XXREAL_0:2;
end;
hence ||.seq.n.|| < M by A9,A10,NAT_1:8;
end;
hence thesis by A4;
end;
A13: P[0]
proof
take M = ||.(seq.0).|| + 1;
||.(seq.0).|| + 1 > 0 + 0 by CSSPACE:44,XREAL_1:8;
hence M > 0;
let n;
assume n <= 0;
then n = 0;
then ||.seq.n.|| + 0 < M by XREAL_1:8;
hence thesis;
end;
thus for m holds P[m] from NAT_1:sch 2(A13,A1);
end;
theorem Th80:
seq is convergent implies seq is bounded
proof
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m st for n st n >= m holds ||.seq.n - g.|| < r by Th9;
consider m1 be Nat such that
A2: for n st n >= m1 holds ||.seq.n - g.|| < 1 by A1;
A3: now
take p = ||.g.|| + 1;
0 + 0 < p by CSSPACE:44,XREAL_1:8;
hence p > 0;
let n;
assume n >= m1;
then
A4: ||.seq.n - g.|| < 1 by A2;
||.seq.n.|| - ||.g.|| <= ||.seq.n - g.|| by CSSPACE:48;
then ||.seq.n.|| - ||.g.|| < 1 by A4,XXREAL_0:2;
hence ||.seq.n.|| < p by XREAL_1:19;
end;
now
consider M2 such that
A5: M2 > 0 and
A6: for n st n <= m1 holds ||.seq.n.|| < M2 by Th79;
consider M1 such that
A7: M1 > 0 and
A8: for n st n >= m1 holds ||.seq.n.|| < M1 by A3;
take M = M1 + M2;
thus M > 0 by A7,A5;
let n;
A9: M > 0 + M2 by A7,XREAL_1:8;
A10: now
assume n <= m1;
then ||.seq.n.|| < M2 by A6;
hence ||.seq.n.|| <= M by A9,XXREAL_0:2;
end;
A11: M > M1 + 0 by A5,XREAL_1:8;
now
assume n >= m1;
then ||.seq.n.|| < M1 by A8;
hence ||.seq.n.|| <= M by A11,XXREAL_0:2;
end;
hence ||.seq.n.|| <= M by A10;
end;
hence thesis;
end;
theorem
seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded
proof
assume that
A1: seq1 is bounded and
A2: seq1 is_compared_to seq2;
consider m1 be Nat such that
A3: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < 1 by A2;
consider p such that
A4: p > 0 and
A5: for n holds ||.seq1.n.|| <= p by A1;
A6: ex M st ( M > 0 & for n st n >= m1 holds ||.seq2.n.|| < M )
proof
take M = p + 1;
now
let n;
assume n >= m1;
then dist((seq1.n), (seq2.n)) < 1 by A3;
then
A7: ||.seq2.n - seq1.n.|| < 1 by CSSPACE:def 16;
||.seq2.n.|| - ||.seq1.n.|| <= ||.seq2.n - seq1.n.|| by CSSPACE:48;
then ||.seq2.n.|| - ||.seq1.n.|| < 1 by A7,XXREAL_0:2;
then
A8: ||.seq2.n.|| < ||.seq1.n.|| + 1 by XREAL_1:19;
||.seq1.n.|| <= p by A5;
then ||.seq1.n.|| + 1 <= p + 1 by XREAL_1:6;
hence ||.seq2.n.|| < M by A8,XXREAL_0:2;
end;
hence thesis by A4;
end;
now
consider M2 such that
A9: M2 > 0 and
A10: for n st n <= m1 holds ||.seq2.n.|| < M2 by Th79;
consider M1 such that
A11: M1 > 0 and
A12: for n st n >= m1 holds ||.seq2.n.|| < M1 by A6;
take M = M1 + M2;
thus M > 0 by A11,A9;
let n;
A13: M > 0 + M2 by A11,XREAL_1:8;
A14: now
assume n <= m1;
then ||.seq2.n.|| < M2 by A10;
hence ||.seq2.n.|| <= M by A13,XXREAL_0:2;
end;
A15: M > M1 + 0 by A9,XREAL_1:8;
now
assume n >= m1;
then ||.seq2.n.|| < M1 by A12;
hence ||.seq2.n.|| <= M by A15,XXREAL_0:2;
end;
hence ||.seq2.n.|| <= M by A14;
end;
hence thesis;
end;
theorem Th82:
seq is bounded & seq1 is subsequence of seq implies seq1 is bounded
proof
assume that
A1: seq is bounded and
A2: seq1 is subsequence of seq;
consider Nseq such that
A3: seq1 = seq * Nseq by A2,VALUED_0:def 17;
consider M1 such that
A4: M1 > 0 and
A5: for n holds ||.seq.n.|| <= M1 by A1;
take M = M1;
now
let n;
n in NAT by ORDINAL1:def 12;
then seq1.n = seq.(Nseq.n) by A3,FUNCT_2:15;
hence ||.seq1.n.|| <= M by A5;
end;
hence thesis by A4;
end;
theorem Th83:
seq is convergent & seq1 is subsequence of seq implies seq1 is convergent
proof
assume that
A1: seq is convergent and
A2: seq1 is subsequence of seq;
consider Nseq such that
A3: seq1 = seq * Nseq by A2,VALUED_0:def 17;
consider g1 such that
A4: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g1.|| < r
by A1,Th9;
now
let r;
assume r > 0;
then consider m1 be Nat such that
A5: for n st n >= m1 holds ||.(seq.n) - g1.|| < r by A4;
take m = m1;
let n such that
A6: n >= m;
Nseq.n >= n by SEQM_3:14;
then
A7: Nseq.n >= m by A6,XXREAL_0:2;
n in NAT by ORDINAL1:def 12;
then seq1.n = seq.(Nseq.n) by A3,FUNCT_2:15;
hence ||.(seq1.n) - g1.|| < r by A5,A7;
end;
hence thesis by Th9;
end;
theorem Th84:
seq1 is subsequence of seq & seq is convergent implies lim seq1= lim seq
proof
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent;
consider Nseq such that
A3: seq1 = seq * Nseq by A1,VALUED_0:def 17;
A4: now
let r;
assume r > 0;
then consider m1 be Nat such that
A5: for n st n >= m1 holds dist((seq.n), (lim seq)) < r by A2,Def2;
take m = m1;
let n such that
A6: n >= m;
Nseq.n >= n by SEQM_3:14;
then
A7: Nseq.n >= m by A6,XXREAL_0:2;
n in NAT by ORDINAL1:def 12;
then seq1.n = seq.(Nseq.n) by A3,FUNCT_2:15;
hence dist((seq1.n), (lim seq)) < r by A5,A7;
end;
seq1 is convergent by A1,A2,Th83;
hence thesis by A4,Def2;
end;
theorem Th85:
seq is Cauchy & seq1 is subsequence of seq implies seq1 is Cauchy
proof
assume that
A1: seq is Cauchy and
A2: seq1 is subsequence of seq;
consider Nseq such that
A3: seq1 = seq * Nseq by A2,VALUED_0:def 17;
now
let r;
assume r > 0;
then consider l be Nat such that
A4: for n, m st n >= l & m >= l holds dist((seq.n), (seq.m)) < r by A1;
take k = l;
let n, m such that
A5: n >= k and
A6: m >= k;
A7: n in NAT & m in NAT by ORDINAL1:def 12;
Nseq.n >= n by SEQM_3:14;
then
A8: Nseq.n >= k by A5,XXREAL_0:2;
Nseq.m >= m by SEQM_3:14;
then
A9: Nseq.m >= k by A6,XXREAL_0:2;
seq1.n = seq.(Nseq.n) & seq1.m = seq.(Nseq.m) by A3,FUNCT_2:15,A7;
hence dist((seq1.n), (seq1.m)) < r by A4,A8,A9;
end;
hence thesis;
end;
theorem Th86:
(seq1 + seq2) ^\k = (seq1 ^\k) + (seq2 ^\k)
proof
now
let n be Element of NAT;
thus ((seq1 + seq2) ^\k).n = (seq1 + seq2).(n + k) by NAT_1:def 3
.= seq1.(n + k) + seq2.(n + k) by NORMSP_1:def 2
.= (seq1 ^\k).n + seq2.(n + k) by NAT_1:def 3
.= (seq1 ^\k).n + (seq2 ^\k).n by NAT_1:def 3
.= ((seq1 ^\k) + (seq2 ^\k)).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th87:
(-seq) ^\k = -(seq ^\k)
proof
now
let n be Element of NAT;
thus ((-seq) ^\k).n = (-seq).(n + k) by NAT_1:def 3
.= -(seq.(n + k)) by BHSP_1:44
.= -((seq ^\ k).n) by NAT_1:def 3
.= (-(seq ^\k)).n by BHSP_1:44;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq1 - seq2) ^\k = (seq1 ^\k) - (seq2 ^\k)
proof
thus (seq1 - seq2) ^\k = (seq1 + (-seq2)) ^\k by CSSPACE:64
.= (seq1 ^\k) + ((-seq2) ^\k) by Th86
.= (seq1 ^\k) + -(seq2 ^\k) by Th87
.= (seq1 ^\k) - (seq2 ^\k) by CSSPACE:64;
end;
theorem
(z * seq) ^\k = z * (seq ^\k)
proof
now
let n be Element of NAT;
thus ((z * seq) ^\k).n = (z * seq).(n + k) by NAT_1:def 3
.= z * (seq.(n + k)) by CLVECT_1:def 14
.= z * ((seq ^\k).n) by NAT_1:def 3
.= (z * (seq ^\k)).n by CLVECT_1:def 14;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq is convergent implies (seq ^\k) is convergent & lim (seq ^\k)=lim
seq by Th83,Th84;
theorem
seq is convergent & (ex k st seq = seq1 ^\k) implies seq1 is convergent
proof
assume that
A1: seq is convergent and
A2: ex k st seq = seq1 ^\k;
consider k such that
A3: seq = seq1 ^\k by A2;
consider g1 such that
A4: for r st r > 0 ex m st for n st n >= m holds ||.seq.n - g1.|| < r by A1,Th9
;
now
take g = g1;
let r;
assume r > 0;
then consider m1 be Nat such that
A5: for n st n >= m1 holds ||.seq.n - g.|| < r by A4;
take m = m1 + k;
let n;
assume
A6: n >= m;
then consider m2 be Nat such that
A7: n = m1 + k + m2 by NAT_1:10;
reconsider m2 as Nat;
n - k = m1 + m2 by A7;
then consider l being Nat such that
A8: l = n - k;
now
assume l < m1;
then l + k < m1 + k by XREAL_1:6;
hence contradiction by A6,A8;
end;
then
A9: ||.seq.l - g.|| < r by A5;
l + k = n by A8;
hence ||.seq1.n - g.|| < r by A3,A9,NAT_1:def 3;
end;
hence thesis by Th9;
end;
theorem
seq is Cauchy & (ex k st seq = seq1 ^\k) implies seq1 is Cauchy
proof
assume that
A1: seq is Cauchy and
A2: ex k st seq = seq1 ^\k;
consider k such that
A3: seq = seq1 ^\k by A2;
let r;
assume r > 0;
then consider l1 being Nat such that
A4: for n, m st n >= l1 & m >= l1 holds dist((seq.n), (seq.m)) < r by A1;
take l = l1 + k;
let n, m;
assume that
A5: n >= l and
A6: m >= l;
consider m1 be Nat such that
A7: n = l1 + k + m1 by A5,NAT_1:10;
reconsider m1 as Nat;
n - k = l1 + m1 by A7;
then consider l2 being Nat such that
A8: l2 = n - k;
consider m2 be Nat such that
A9: m = l1 + k + m2 by A6,NAT_1:10;
reconsider m2 as Nat;
m - k = l1 + m2 by A9;
then consider l3 being Nat such that
A10: l3 = m - k;
A11: now
assume l2 < l1;
then l2 + k < l1 + k by XREAL_1:6;
hence contradiction by A5,A8;
end;
A12: l2 + k = n by A8;
now
assume l3 < l1;
then l3 + k < l1 + k by XREAL_1:6;
hence contradiction by A6,A10;
end;
then dist((seq.l2), (seq.l3)) < r by A4,A11;
then
A13: dist((seq1.n), (seq.l3)) < r by A3,A12,NAT_1:def 3;
l3 + k = m by A10;
hence thesis by A3,A13,NAT_1:def 3;
end;
theorem
seq is Cauchy implies (seq ^\k) is Cauchy by Th85;
theorem
seq1 is_compared_to seq2 implies (seq1 ^\k) is_compared_to (seq2 ^\k)
proof
assume
A1: seq1 is_compared_to seq2;
let r;
assume r > 0;
then consider m1 be Nat such that
A2: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < r by A1;
take m = m1;
let n such that
A3: n >= m;
n + k >= n by NAT_1:11;
then n + k >= m by A3,XXREAL_0:2;
then dist((seq1.(n + k)), (seq2.(n + k))) < r by A2;
then dist((seq1 ^\k).n, (seq2.(n + k))) < r by NAT_1:def 3;
hence thesis by NAT_1:def 3;
end;
theorem
seq is bounded implies (seq ^\k) is bounded by Th82;
theorem
seq is constant implies (seq ^\k) is constant;
definition
let X;
attr X is complete means
for seq holds seq is Cauchy implies seq is convergent;
end;
theorem
X is complete & seq is Cauchy implies seq is bounded
by Th80;