:: Introduction to Banach and Hilbert spaces - Part III
:: by Jan Popio{\l}ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-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, BHSP_1, PRE_TOPC, REAL_1, NAT_1, ORDINAL2, SUBSET_1,
SUPINF_2, XXREAL_0, CARD_1, METRIC_1, FUNCT_1, ARYTM_3, NORMSP_1,
ARYTM_1, RELAT_1, COMPLEX1, SEQ_2, XXREAL_2, VALUED_0, REWRITE1, BHSP_3;
notations ORDINAL1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1,
XXREAL_0, NAT_1, VALUED_0, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1,
NORMSP_1, BHSP_1, BHSP_2;
constructors PARTFUN1, FUNCT_3, XXREAL_0, REAL_1, COMPLEX1, SEQM_3, BHSP_2,
VALUED_1, RECDEF_1, NAT_1, RELSET_1, VFUNCT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, STRUCT_0,
VALUED_0, VFUNCT_1, FUNCT_2, BHSP_2;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems NAT_1, SEQM_3, FUNCT_2, RLVECT_1, BHSP_1, BHSP_2, NORMSP_1, XCMPLX_0,
XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, VALUED_0;
schemes NAT_1;
begin
reserve X for RealUnitarySpace,
x, g, g1, h for Point of X,
a, p, r, M, M1, M2 for Real,
seq, seq1, seq2, seq3 for sequence of X,
Nseq for increasing sequence of NAT,
k, l, l1, l2, l3, n, m, m1, m2 for Nat;
deffunc 09(RealUnitarySpace) = 0.$1;
registration let X;
cluster constant for sequence of X;
existence
proof
take the constant sequence of X;
thus thesis;
end;
end;
definition
let X;
let seq;
attr seq is Cauchy means
:Def1:
for r st r > 0 ex k st for n, m st n >= k &
m >= k holds dist(seq.n, seq.m) < r;
end;
registration let X;
cluster constant -> Cauchy for sequence of X;
coherence
proof let seq be sequence of X;
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 BHSP_1:34;
hence thesis by A2;
end;
end;
::$CT
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 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 BHSP_1:def 5;
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 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 BHSP_1:def 5;
end;
hence thesis;
end;
registration let X; let seq1,seq2 be Cauchy sequence of X;
cluster seq1+seq2 -> Cauchy;
coherence
proof
let r;
assume r > 0;
then
A1: r/2 > 0 by XREAL_1:215;
then consider m1 such that
A2: for n, m st n >= m1 & m >= m1 holds dist((seq1.n), (seq1.m)) < r/2
by Def1;
consider m2 such that
A3: for n, m st n >= m2 & m >= m2 holds dist((seq2.n), (seq2.m)) < r/2
by A1,Def1;
take k = m1 + m2;
let n, m such that
A4: n >= k & m >= k;
k >= m2 by NAT_1:12;
then n >= m2 & m >= m2 by A4,XXREAL_0:2;
then
A5: dist((seq2.n), (seq2.m)) < r/2 by A3;
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
A6: dist((seq1 + seq2).n, (seq1 + seq2).m) <= dist((seq1.n), (seq1.m)) +
dist((seq2.n), (seq2.m)) by BHSP_1:40;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 & m >= m1 by A4,XXREAL_0:2;
then dist((seq1.n), (seq1.m)) < r/2 by A2;
then dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r/2 + r/2 by A5,
XREAL_1:8;
hence thesis by A6,XXREAL_0:2;
end;
end;
registration let X; let seq1,seq2 be Cauchy sequence of X;
cluster seq1-seq2 -> Cauchy;
coherence
proof
let r;
assume r > 0;
then
A1: r/2 > 0 by XREAL_1:215;
then consider m1 such that
A2: for n, m st n >= m1 & m >= m1 holds dist((seq1.n), (seq1.m)) < r/2
by Def1;
consider m2 such that
A3: for n, m st n >= m2 & m >= m2 holds dist((seq2.n), (seq2.m)) < r/2
by A1,Def1;
take k = m1 + m2;
let n, m such that
A4: n >= k & m >= k;
k >= m2 by NAT_1:12;
then n >= m2 & m >= m2 by A4,XXREAL_0:2;
then
A5: dist((seq2.n), (seq2.m)) < r/2 by A3;
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
A6: dist((seq1 - seq2).n, (seq1 - seq2).m) <= dist((seq1.n), (seq1.m)) +
dist((seq2.n), (seq2.m)) by BHSP_1:41;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 & m >= m1 by A4,XXREAL_0:2;
then dist((seq1.n), (seq1.m)) < r/2 by A2;
then dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r/2 + r/2 by A5,
XREAL_1:8;
hence thesis by A6,XXREAL_0:2;
end;
end;
registration let X,a; let seq be Cauchy sequence of X;
cluster a * seq -> Cauchy;
coherence
proof
A1: now
A2: 0/|.a.| = 0;
assume
A3: a <> 0;
then
A4: |.a.| > 0 by COMPLEX1:47;
let r;
assume r > 0;
then r/|.a.| > 0 by A4,A2,XREAL_1:74;
then consider m1 such that
A5: for n, m st n >= m1 & m >= m1 holds dist(seq.n, seq.m) < r/|.a.|
by Def1;
take k = m1;
let n, m;
assume n >= k & m >= k;
then
A6: dist(seq.n, seq.m) < r/|.a.| by A5;
A7: |.a.| <> 0 by A3,COMPLEX1:47;
A8: |.a.| * (r/|.a.|) = |.a.| * (|.a.|" * r) by XCMPLX_0:def 9
.= |.a.| *|.a.|" * r
.= 1 * r by A7,XCMPLX_0:def 7
.= r;
dist(a * (seq.n), a * (seq.m)) = ||.(a * (seq.n)) - (a * (seq.m)).||
by BHSP_1:def 5
.= ||.a * ((seq.n) - (seq.m)).|| by RLVECT_1:34
.= |.a.| * ||.(seq.n) - (seq.m).|| by BHSP_1:27
.= |.a.| * dist(seq.n, seq.m) by BHSP_1:def 5;
then dist((a * (seq.n)), (a * (seq.m))) < r by A4,A6,A8,XREAL_1:68;
then dist((a * seq).n, (a * (seq.m))) < r by NORMSP_1:def 5;
hence dist((a * seq).n, (a * seq).m) < r by NORMSP_1:def 5;
end;
now
assume
A9: a = 0;
let r;
assume r > 0;
then consider m1 such that
A10: for n, m st n >= m1 & m >= m1 holds dist((seq.n), (seq.m)) < r by Def1;
take k = m1;
let n, m;
assume n >= k & m >= k;
then
A11: dist((seq.n), (seq.m)) < r by A10;
dist(a * (seq.n), a * (seq.m)) = dist(09(X), 0 * (seq.m)) by A9,
RLVECT_1:10
.= dist(09(X), 09(X)) by RLVECT_1:10
.= 0 by BHSP_1:34;
then dist(a * (seq.n), a * (seq.m)) < r by A11,BHSP_1:37;
then dist((a * seq).n, a * (seq.m)) < r by NORMSP_1:def 5;
hence dist((a * seq).n, (a * seq).m) < r by NORMSP_1:def 5;
end;
hence thesis by A1;
end;
end;
registration let X; let seq be Cauchy sequence of X;
cluster - seq -> Cauchy;
coherence
proof
(-1) * seq is Cauchy;
hence thesis by BHSP_1:55;
end;
end;
registration let X,x; let seq be Cauchy sequence of X;
cluster seq + x -> Cauchy;
coherence
proof
let r;
assume r > 0;
then consider m1 such that
A1: for n, m st n >= m1 & m >= m1 holds dist((seq.n), (seq.m)) < r by Def1;
take k = m1;
let n, m;
dist((seq.n) + x, (seq.m) + x) <= dist((seq.n), (seq.m)) + dist(x, x) by
BHSP_1:40;
then
A2: dist((seq.n) + x, (seq.m) + x) <= dist((seq.n), (seq.m)) + 0 by BHSP_1:34;
assume n >= k & m >= k;
then dist((seq.n), (seq.m)) < r by A1;
then dist((seq.n) + x, (seq.m) + x) < r by A2,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;
end;
registration let X,x; let seq be Cauchy sequence of X;
cluster seq - x -> Cauchy;
coherence
proof
seq + (-x) is Cauchy;
hence thesis by BHSP_1:56;
end;
end;
registration let X;
cluster convergent -> Cauchy for sequence of X;
coherence
proof let seq be sequence of X;
assume seq is convergent;
then consider h such that
A1: for r st r > 0
ex k being Nat st for n being Nat st n >= k holds dist((seq.n), h) < r by
BHSP_2:def 1;
let r;
assume r > 0;
then consider m1 being Nat such that
A2: for n being Nat st n >= m1 holds dist((seq.n), h) < r/2 by A1,XREAL_1:215;
reconsider k = m1 as Nat;
take k;
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 BHSP_1:35,XREAL_1:8;
hence thesis by XXREAL_0:2;
end;
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;
reflexivity
proof let seq1;
let r such that
A1: r > 0;
take m = 0;
let n such that
n >= m;
thus thesis by A1,BHSP_1:34;
end;
symmetry
proof let seq1,seq2;
assume
A2: for r st r > 0 ex m st for n st n >= m holds dist(seq1.n, seq2.n) < r;
let r;
assume r > 0;
then consider k such that
A3: for n st n >= k holds dist((seq1.n), (seq2.n)) < r by A2;
take m = k;
let n;
assume n >= m;
hence thesis by A3;
end;
end;
::$CT 9
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 such that
A4: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < r/2 by A1;
consider m2 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 BHSP_1:35;
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 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 BHSP_1:def 5;
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 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 BHSP_1:def 5;
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 BHSP_1:34;
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 such that
A4: for n, m st n >= m1 & m >= m1 holds dist((seq1.n), (seq1.m)) < r/3
by A1;
consider m2 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 BHSP_1:35;
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 BHSP_1:35;
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 being Nat such that
A4: for n being Nat st n >= m1 holds dist((seq1.n), (lim seq1)) < r/2
by A1,BHSP_2:def 2;
consider m2 such that
A5: for n st n >= m2 holds dist((seq1.n), (seq2.n)) < r/2 by A2,A3;
reconsider m = m1 + m2 as Nat;
take m;
let n being Nat 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 BHSP_1:35;
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 by BHSP_2:def 1;
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 being Nat such that
A5: for n being Nat st n >= m1 holds dist((seq1.n), g) < r/2
by A1,BHSP_2:def 2;
consider m2 such that
A6: for n st n >= m2 holds dist((seq1.n), (seq2.n)) < r/2 by A2,A4;
reconsider m = m1 + m2 as Nat;
take m;
let n being Nat 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
BHSP_1:35;
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 by BHSP_2:def 1;
hence thesis by A3,BHSP_2:def 2;
end;
definition
let X;
let seq;
attr seq is bounded means
:Def3:
ex M st M > 0 & for n holds ||.seq.n.|| <= M;
end;
registration let X;
cluster constant -> bounded for sequence of X;
coherence
proof let seq be sequence of X;
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;
reconsider M as Real;
assume
A4: x = 09(X);
for n holds ||.seq.n.|| <= M by A3,A1,A4,BHSP_1:26;
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,BHSP_1:28;
hence thesis by A5;
end;
hence thesis by A2;
end;
end;
registration let X; let seq1, seq2 be bounded sequence of X;
cluster seq1 + seq2 -> bounded;
coherence
proof
consider M2 such that
A1: M2 > 0 and
A2: for n holds ||.seq2.n.|| <= M2 by Def3;
consider M1 such that
A3: M1 > 0 and
A4: for n holds ||.seq1.n.|| <= M1 by Def3;
now
let n;
||.(seq1 + seq2).n.|| = ||.seq1.n + seq2.n.|| by NORMSP_1:def 2;
then
A5: ||.(seq1 + seq2).n.|| <= ||.seq1.n.|| + ||.seq2.n.|| by BHSP_1:30;
||.seq1.n.|| <= M1 & ||.seq2.n.|| <= M2 by A4,A2;
then ||.seq1.n.|| + ||.seq2.n.|| <= M1 + M2 by XREAL_1:7;
hence ||.(seq1 + seq2).n.|| <= M1 + M2 by A5,XXREAL_0:2;
end;
hence thesis by A3,A1;
end;
end;
registration let X; let seq be bounded sequence of X;
cluster -seq -> bounded;
coherence
proof
consider M such that
A1: M > 0 and
A2: for n holds ||.seq.n.|| <= M by Def3;
now
let n;
||.(- seq).n.|| = ||.- (seq.n).|| by BHSP_1:44
.= ||.seq.n.|| by BHSP_1:31;
hence ||.(- seq).n.|| <= M by A2;
end;
hence thesis by A1;
end;
end;
registration let X; let seq1, seq2 be bounded sequence of X;
cluster seq1 - seq2 -> bounded;
coherence
proof
A1: seq1 - seq2 = seq1 + (- seq2) by BHSP_1:49;
thus thesis by A1;
end;
end;
registration let X,a; let seq be bounded sequence of X;
cluster a * seq -> bounded;
coherence
proof
consider M such that
A1: M > 0 and
A2: for n holds ||.seq.n.|| <= M by Def3;
A3: a <> 0 implies a * seq is bounded
proof
A4: now
let n;
A5: |.a.| >= 0 by COMPLEX1:46;
||.(a * seq).n.|| = ||.a * (seq.n).|| by NORMSP_1:def 5
.= |.a.| * ||.seq.n.|| by BHSP_1:27;
hence ||.(a * seq).n.|| <= |.a.| * M by A2,A5,XREAL_1:64;
end;
assume a <> 0;
then |.a.| > 0 by COMPLEX1:47;
then |.a.| * M > 0 by A1,XREAL_1:129;
hence thesis by A4;
end;
a = 0 implies a * seq is bounded
proof
assume
A6: a = 0;
now
let n;
||.(a * seq).n.|| = ||.0 * (seq.n).|| by A6,NORMSP_1:def 5
.= ||.09(X).|| by RLVECT_1:10
.= 0 by BHSP_1:26;
hence ||.(a * seq).n.|| <= M by A1;
end;
hence thesis by A1;
end;
hence thesis by A3;
end;
end;
::$CT 5
theorem Th8:
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 BHSP_1:28,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 BHSP_1:28,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;
registration let X;
cluster convergent -> bounded for sequence of X;
coherence
proof let seq;
assume seq is convergent;
then consider g such that
A1: for r st r > 0 ex m being Nat st
for n being Nat st n >= m holds ||.seq.n - g.|| < r by
BHSP_2:9;
consider m1 being Nat such that
A2: for n being Nat st n >= m1 holds ||.seq.n - g.|| < 1 by A1;
A3: now
take p = ||.g.|| + 1;
0 + 0 < p by BHSP_1:28,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 BHSP_1:32;
then ||.seq.n.|| - ||.g.|| < 1 by A4,XXREAL_0:2;
hence ||.seq.n.|| < p by XREAL_1:19;
end;
now
reconsider m1 as Nat;
consider M2 such that
A5: M2 > 0 and
A6: for n st n <= m1 holds ||.seq.n.|| < M2 by Th8;
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;
end;
::$CT
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 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 BHSP_1:def 5;
||.seq2.n.|| - ||.seq1.n.|| <= ||.seq2.n - seq1.n.|| by BHSP_1:32;
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 Th8;
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;
registration let X; let seq be bounded sequence of X;
cluster -> bounded for subsequence of seq;
coherence
proof let seq1 be subsequence of seq;
consider Nseq such that
A1: seq1 = seq * Nseq by VALUED_0:def 17;
consider M1 such that
A2: M1 > 0 and
A3: for n holds ||.seq.n.|| <= M1 by Def3;
take M = M1;
now
let n;
A4: n in NAT by ORDINAL1:def 12;
seq1.n = seq.(Nseq.n) by A1,FUNCT_2:15,A4;
hence ||.seq1.n.|| <= M by A3;
end;
hence thesis by A2;
end;
end;
registration let X; let seq be convergent sequence of X;
cluster -> convergent for subsequence of seq;
coherence
proof let seq1 be subsequence of seq;
consider g1 such that
A1: for r st r > 0
ex m being Nat st for n being Nat st n >= m holds ||.(seq.n) - g1.|| < r
by BHSP_2:9;
consider Nseq such that
A2: seq1 = seq * Nseq by VALUED_0:def 17;
now
let r;
assume r > 0;
then consider m1 being Nat such that
A3: for n being Nat st n >= m1 holds ||.(seq.n) - g1.|| < r by A1;
take m = m1;
let n be Nat such that
A4: n >= m;
A5: n in NAT by ORDINAL1:def 12;
Nseq.n >= n by SEQM_3:14;
then
A6: Nseq.n >= m by A4,XXREAL_0:2;
seq1.n = seq.(Nseq.n) by A2,FUNCT_2:15,A5;
hence ||.(seq1.n) - g1.|| < r by A3,A6;
end;
hence thesis by BHSP_2:9;
end;
end;
::$CT 2
theorem Th10:
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 being Nat such that
A5: for n being Nat st n >= m1 holds dist((seq.n), (lim seq)) < r
by A2,BHSP_2:def 2;
take m = m1;
let n be Nat such that
A6: n >= m;
A7: n in NAT by ORDINAL1:def 12;
Nseq.n >= n by SEQM_3:14;
then
A8: Nseq.n >= m by A6,XXREAL_0:2;
seq1.n = seq.(Nseq.n) by A3,FUNCT_2:15,A7;
hence dist((seq1.n), (lim seq)) < r by A5,A8;
end;
seq1 is convergent by A1,A2;
hence thesis by A4,BHSP_2:def 2;
end;
registration let X; let seq be Cauchy sequence of X;
cluster -> Cauchy for subsequence of seq;
coherence
proof
let seq1 be subsequence of seq;
consider Nseq such that
A1: seq1 = seq * Nseq by VALUED_0:def 17;
now
let r;
assume r > 0;
then consider l such that
A2: for n, m st n >= l & m >= l holds dist((seq.n), (seq.m)) < r by Def1;
take k = l;
let n, m such that
A3: n >= k and
A4: m >= k;
Nseq.n >= n by SEQM_3:14;
then
A5: Nseq.n >= k by A3,XXREAL_0:2;
Nseq.m >= m by SEQM_3:14;
then
A6: Nseq.m >= k by A4,XXREAL_0:2;
A7: n in NAT & m in NAT by ORDINAL1:def 12;
seq1.n = seq.(Nseq.n) & seq1.m = seq.(Nseq.m) by A1,FUNCT_2:15,A7;
hence dist((seq1.n), (seq1.m)) < r by A2,A5,A6;
end;
hence thesis;
end;
end;
::$CT
theorem
(seq ^\k)^\m = (seq ^\m)^\k
proof
now
let n be Element of NAT;
thus ((seq ^\k)^\m).n = (seq ^\k).(n + m) by NAT_1:def 3
.= seq.(n + m + k) by NAT_1:def 3
.= seq.(n + k + m)
.= (seq ^\m).(n + k) by NAT_1:def 3
.= ((seq ^\m)^\k).n by NAT_1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq ^\k)^\m=seq ^\(k + m)
proof
now
let n be Element of NAT;
thus ((seq ^\k)^\m).n = (seq ^\k).(n + m) by NAT_1:def 3
.= seq.(n + m + k) by NAT_1:def 3
.= seq.(n + (k + m))
.= (seq ^\(k + m)).n by NAT_1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th13:
(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 Th14:
(-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 BHSP_1:49
.= (seq1 ^\k) + ((-seq2) ^\k) by Th13
.= (seq1 ^\k) + -(seq2 ^\k) by Th14
.= (seq1 ^\k) - (seq2 ^\k) by BHSP_1:49;
end;
theorem
(a * seq) ^\k = a * (seq ^\k)
proof
now
let n be Element of NAT;
thus ((a * seq) ^\k).n = (a * seq).(n + k) by NAT_1:def 3
.= a * (seq.(n + k)) by NORMSP_1:def 5
.= a * ((seq ^\k).n) by NAT_1:def 3
.= (a * (seq ^\k)).n by NORMSP_1:def 5;
end;
hence thesis by FUNCT_2:63;
end;
theorem
seq is convergent implies (seq ^\k) is convergent & lim (seq ^\k)=lim
seq by Th10;
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 being Nat st for n being Nat st n >= m holds ||.seq.n - g1.|| < r
by A1,BHSP_2:9;
now
take g = g1;
let r;
assume r > 0;
then consider m1 being Nat such that
A5: for n being Nat st n >= m1 holds ||.seq.n - g.|| < r by A4;
reconsider m = m1 + k as Nat;
take m;
let n be Nat;
assume
A6: n >= m;
then consider m2 being 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 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 BHSP_2:9;
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 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 being 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 such that
A8: l2 = n - k;
consider m2 being 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 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;
::$CT
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 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;
definition
let X;
attr X is complete means
for seq holds seq is Cauchy implies seq is convergent;
end;
::$CT 2
theorem
X is complete & seq is Cauchy implies seq is bounded
proof
assume X is complete & seq is Cauchy;
then seq is convergent;
hence thesis;
end;