:: Inferior Limit and Superior Limit of Sequences of Real Numbers
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 29, 2005
:: Copyright (c) 2005-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, SUBSET_1, SEQ_1, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1,
COMPLEX1, ORDINAL2, REAL_1, SEQ_4, RELAT_1, FUNCT_1, TARSKI, XXREAL_2,
XBOOLE_0, SUPINF_2, PARTFUN3, NAT_1, VALUED_1, VALUED_0, SEQ_2, RINFSUP1,
MEMBER_1;
notations ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1,
COMPLEX1, TARSKI, XXREAL_2, VALUED_0, FUNCT_1, SEQ_4, XBOOLE_0, SUBSET_1,
COMSEQ_2, SEQ_2, RELSET_1, FUNCT_2, MEASURE6, VALUED_1, SEQ_1, PARTFUN3,
MEMBER_1;
constructors REAL_1, NAT_1, COMPLEX1, SEQM_3, LIMFUNC1, PARTFUN3, PARTFUN1,
XXREAL_2, SEQ_4, RELSET_1, BINOP_2, SEQ_2, MEASURE6, MEMBER_1, SQUARE_1,
COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, RFUNCT_1, MEMBER_1, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, PARTFUN3, XXREAL_2;
equalities VALUED_1;
expansions TARSKI, XBOOLE_0, PARTFUN3, VALUED_1, XXREAL_2;
theorems FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, NAT_1, TARSKI, XREAL_0, SEQ_4,
SEQM_3, SETLIM_1, LIMFUNC1, PREPOWER, XREAL_1, XXREAL_0, ORDINAL1,
RELAT_1, XXREAL_2, VALUED_0, MEASURE6, MEMBER_1;
schemes FUNCT_2, NAT_1;
begin
reserve n,m,k,k1,k2 for Nat;
reserve r,r1,r2,s,t,p for Real;
reserve seq,seq1,seq2 for Real_Sequence;
reserve x,y for set;
Lm1: for s st 0 < s & r1 <= r2 holds r1 < r2 + s & r1 - s < r2
proof
let s such that
A1: 0<s;
assume r1 <= r2;
then r1 + 0 < r2 + s by A1,XREAL_1:8;
hence thesis by XREAL_1:19;
end;
theorem Th1:
s - r < t & s + r > t iff |.t-s.| < r
proof
thus s - r < t & s + r > t implies |.t-s.| < r
proof
assume that
A1: s - r < t and
A2: s + r > t;
-r + s < t by A1;
then
A3: -r < t - s by XREAL_1:20;
t - s < r by A2,XREAL_1:19;
hence thesis by A3,SEQ_2:1;
end;
assume
A4: |.t-s.| < r;
then -r < t - s by SEQ_2:1;
then
A5: s + -r < t by XREAL_1:20;
t - s < r by A4,SEQ_2:1;
hence thesis by A5,XREAL_1:19;
end;
definition
let seq be Real_Sequence;
func upper_bound seq -> Real equals
upper_bound rng seq;
coherence;
end;
definition
let seq be Real_Sequence;
func lower_bound seq -> Real equals
lower_bound rng seq;
coherence;
end;
theorem Th2:
seq1+seq2-seq2=seq1
proof
for n being Element of NAT holds (seq1+seq2-seq2).n = seq1.n
proof
let n be Element of NAT;
(seq1+seq2-seq2).n = (seq1+(seq2-seq2)).n by SEQ_1:31
.= seq1.n + (seq2+-seq2).n by SEQ_1:7
.= seq1.n + (seq2.n +(-seq2).n) by SEQ_1:7
.= seq1.n + (seq2.n +-seq2.n) by SEQ_1:10
.= seq1.n;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th3:
r in rng seq iff -r in rng(-seq)
proof
thus r in rng seq implies -r in rng(-seq)
proof
assume r in rng seq;
then consider n being Element of NAT such that
A1: r=seq.n by FUNCT_2:113;
-r=(-seq).n by A1,SEQ_1:10;
hence thesis by VALUED_0:28;
end;
assume -r in rng(-seq);
then consider n being Element of NAT such that
A2: -r=(-seq).n by FUNCT_2:113;
r=-(-seq).n by A2;
then r= - -seq.n by SEQ_1:10;
hence thesis by VALUED_0:28;
end;
theorem Th4:
rng (-seq) = -- rng seq
proof
thus rng (-seq) c= -- rng seq
proof
let x be object;
assume
A1: x in rng(-seq);
then reconsider r = x as Real;
-r in rng -(-seq) by A1,Th3;
then - -r in -- rng seq by MEASURE6:40;
hence thesis;
end;
let x be object;
assume
A2: x in -- rng seq;
then reconsider r = x as Real;
-r in -- -- rng seq by A2,MEMBER_1:12;
then - -r in rng (-seq) by Th3;
hence thesis;
end;
theorem Th5:
seq is bounded_above iff rng seq is bounded_above
proof
A1: seq is bounded_above implies rng seq is bounded_above
proof
assume seq is bounded_above;
then consider t such that
A2: for n holds seq.n<t by SEQ_2:def 3;
t is UpperBound of rng seq
proof
let r be ExtReal;
assume r in rng seq;
then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3;
hence r<=t by A2;
end;
hence thesis;
end;
rng seq is bounded_above implies seq is bounded_above
proof
assume rng seq is bounded_above;
then consider t such that
A3: t is UpperBound of rng seq;
A4: for r st r in rng seq holds r<=t by A3,XXREAL_2:def 1;
now
let n;
A5: n in NAT by ORDINAL1:def 12;
seq.n <= t by A4,FUNCT_2:4,A5;
hence seq.n < t+1 by Lm1;
end;
hence thesis by SEQ_2:def 3;
end;
hence thesis by A1;
end;
theorem Th6:
seq is bounded_below iff rng seq is bounded_below
proof
A1: seq is bounded_below implies rng seq is bounded_below
proof
assume seq is bounded_below;
then consider t such that
A2: for n holds t<seq.n by SEQ_2:def 4;
t is LowerBound of rng seq
proof
let r be ExtReal;
assume r in rng seq;
then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3;
hence t<=r by A2;
end;
hence thesis;
end;
rng seq is bounded_below implies seq is bounded_below
proof
assume rng seq is bounded_below;
then consider t such that
A3: t is LowerBound of rng seq;
A4: for r st r in rng seq holds t<=r by A3,XXREAL_2:def 2;
now
let n;
A5: n in NAT by ORDINAL1:def 12;
t <= seq.n by A4,FUNCT_2:4,A5;
hence t - 1 < seq.n by Lm1;
end;
hence thesis by SEQ_2:def 4;
end;
hence thesis by A1;
end;
theorem Th7:
seq is bounded_above implies ( r = upper_bound seq iff (for n holds seq.n
<= r) & for s st 0<s holds ex k st r-s < seq.k )
proof
set R = rng seq;
assume seq is bounded_above;
then
A1: rng seq is bounded_above by Th5;
A2: rng seq <> {} by RELAT_1:41;
A3: (for n holds seq.n <= r) & (for s st 0<s holds ex k st r-s<seq.k)
implies r = upper_bound seq
proof
assume that
A4: for n holds seq.n <= r and
A5: for s st 0<s holds ex k st r-s<seq.k;
A6: now
let s;
assume 0<s;
then consider k such that
A7: r-s< seq.k by A5;
A8: k in NAT by ORDINAL1:def 12;
consider r2 such that
A9: r2 in R & r2 = seq.k by FUNCT_2:4,A8;
take r2;
thus r2 in R & r-s < r2 by A7,A9;
end;
now
let r1;
assume r1 in R;
then ex n being object st n in dom seq & seq.n = r1 by FUNCT_1:def 3;
hence r1 <= r by A4;
end;
hence thesis by A1,A2,A6,SEQ_4:def 1;
end;
r = upper_bound seq implies (for n holds seq.n <= r) &
for s st 0<s holds ex k
st r-s<seq.k
proof
assume
A10: r = upper_bound seq;
A11: now
let s;
assume 0<s;
then consider r2 such that
A12: r2 in R and
A13: r-s<r2 by A1,A2,A10,SEQ_4:def 1;
consider k being Nat such that
A14: r2 = seq.k by A12,SETLIM_1:4;
reconsider k as Nat;
take k;
thus r-s < seq.k by A13,A14;
end;
now
let n;
A15: n in NAT by ORDINAL1:def 12;
seq.n in R by FUNCT_2:4,A15;
hence seq.n <= r by A1,A10,SEQ_4:def 1;
end;
hence thesis by A11;
end;
hence thesis by A3;
end;
theorem Th8:
seq is bounded_below implies (r = lower_bound seq iff (for n holds r <=
seq.n) & for s st 0<s holds ex k st seq.k < r+s )
proof
set R = rng seq;
assume seq is bounded_below;
then
A1: rng seq is bounded_below by Th6;
A2: rng seq <> {} by RELAT_1:41;
A3: (for n holds r <= seq.n) & (for s st 0<s holds ex k st seq.k<r+s)
implies r = lower_bound seq
proof
assume that
A4: for n holds r <= seq.n and
A5: for s st 0<s holds ex k st seq.k<r+s;
A6: now
let s;
assume 0<s;
then consider k such that
A7: seq.k < r+s by A5;
A8: k in NAT by ORDINAL1:def 12;
consider r2 such that
A9: r2 in R & r2 = seq.k by FUNCT_2:4,A8;
take r2;
thus r2 in R & r2 <r+s by A7,A9;
end;
now
let r1;
assume r1 in R;
then ex n being object st n in dom seq & seq.n = r1 by FUNCT_1:def 3;
hence r <= r1 by A4;
end;
hence thesis by A1,A2,A6,SEQ_4:def 2;
end;
r = lower_bound seq implies (for n holds r <= seq.n) &
for s st 0<s holds ex k
st seq.k<r+s
proof
assume
A10: r = lower_bound seq;
A11: now
let s;
assume 0<s;
then consider r2 such that
A12: r2 in R and
A13: r2<r+s by A1,A2,A10,SEQ_4:def 2;
consider k being Nat such that
A14: r2 = seq.k by A12,SETLIM_1:4;
reconsider k as Nat;
take k;
thus seq.k<r+s by A13,A14;
end;
now
let n;
n in NAT by ORDINAL1:def 12;
then seq.n in R by FUNCT_2:4;
hence r <= seq.n by A1,A10,SEQ_4:def 2;
end;
hence thesis by A11;
end;
hence thesis by A3;
end;
theorem Th9:
(for n holds seq.n <= r) iff seq is bounded_above & upper_bound seq <= r
proof
thus (for n holds seq.n <= r) implies seq is bounded_above &
upper_bound seq <= r
proof
assume
A1: for n holds seq.n <= r;
now
let m;
seq.m <= r by A1;
hence seq.m < r + 1 by Lm1;
end;
hence
A2: seq is bounded_above by SEQ_2:def 3;
now
set r1= (upper_bound seq) - r;
assume r < upper_bound seq;
then r1 > 0 by XREAL_1:50;
then ex k st (upper_bound seq) - r1 < seq.k by A2,Th7;
hence contradiction by A1;
end;
hence thesis;
end;
assume that
A3: seq is bounded_above and
A4: upper_bound seq <= r;
now
let n;
seq.n <= upper_bound seq by A3,Th7;
hence seq.n <= r by A4,XXREAL_0:2;
end;
hence thesis;
end;
theorem Th10:
(for n holds r <= seq.n) iff seq is bounded_below & r <= lower_bound seq
proof
thus (for n holds r <= seq.n) implies seq is bounded_below &
r <= lower_bound seq
proof
assume
A1: for n holds r <= seq.n;
now
let m;
r <= seq.m by A1;
hence r -1 < seq.m by Lm1;
end;
hence
A2: seq is bounded_below by SEQ_2:def 4;
now
set r1=r - (lower_bound seq);
assume r > lower_bound seq;
then r1 > 0 by XREAL_1:50;
then ex k st seq.k < (lower_bound seq) + r1 by A2,Th8;
hence contradiction by A1;
end;
hence thesis;
end;
assume that
A3: seq is bounded_below and
A4: r <= lower_bound seq;
now
let n;
lower_bound seq <= seq.n by A3,Th8;
hence r <= seq.n by A4,XXREAL_0:2;
end;
hence thesis;
end;
theorem
seq is bounded_above iff -seq is bounded_below
proof
set seq1=-seq;
thus seq is bounded_above implies -seq is bounded_below;
assume seq1 is bounded_below;
then consider t such that
A1: for n holds seq1.n>t by SEQ_2:def 4;
for n holds seq.n < -t
proof
let n;
seq1.n=-seq.n by SEQ_1:10;
then
A2: -seq1.n = seq.n;
seq1.n > t by A1;
hence thesis by A2,XREAL_1:24;
end;
hence thesis by SEQ_2:def 3;
end;
theorem
seq is bounded_below iff -seq is bounded_above
proof
- -seq = seq;
hence thesis;
end;
theorem Th13:
seq is bounded_above implies upper_bound seq = -lower_bound (-seq)
proof
assume seq is bounded_above;
then rng seq is non empty bounded_above by Th5,RELAT_1:41;
then upper_bound rng seq = - lower_bound (--(rng seq)) by MEASURE6:44
.= - lower_bound rng -seq by Th4;
hence thesis;
end;
theorem Th14:
seq is bounded_below implies lower_bound seq = -upper_bound (-seq)
proof
assume seq is bounded_below;
then rng seq is non empty bounded_below by Th6,RELAT_1:41;
then lower_bound rng seq = - upper_bound --(rng seq) by MEASURE6:43
.= - upper_bound rng -seq by Th4;
hence thesis;
end;
theorem Th15:
seq1 is bounded_below & seq2 is bounded_below implies lower_bound (seq1
+ seq2) >= lower_bound seq1 + lower_bound seq2
proof
assume that
A1: seq1 is bounded_below and
A2: seq2 is bounded_below;
for n holds (seq1 + seq2).n >= lower_bound seq1 + lower_bound seq2
proof
let n;
A3: seq2.n >= lower_bound seq2 by A2,Th8;
(seq1 + seq2).n = seq1.n + seq2.n & seq1.n >= lower_bound seq1
by A1,Th8,SEQ_1:7;
hence thesis by A3,XREAL_1:7;
end;
hence thesis by Th10;
end;
theorem Th16:
seq1 is bounded_above & seq2 is bounded_above implies upper_bound (seq1
+ seq2) <= upper_bound seq1 + upper_bound seq2
proof
assume that
A1: seq1 is bounded_above and
A2: seq2 is bounded_above;
for n holds (seq1 + seq2).n <= upper_bound seq1 + upper_bound seq2
proof
let n;
A3: seq2.n <= upper_bound seq2 by A2,Th7;
(seq1 + seq2).n = seq1.n + seq2.n & seq1.n <= upper_bound seq1
by A1,Th7,SEQ_1:7;
hence thesis by A3,XREAL_1:7;
end;
hence thesis by Th9;
end;
notation
let f be Real_Sequence;
synonym f is nonnegative for f is nonnegative-yielding;
end;
definition
let f be Real_Sequence;
redefine attr f is nonnegative means :: redefines nonnegative (RINFSUP1, synonym) → nonnegative-yielding (PARTFUN3, definition)
for n holds f.n >= 0;
compatibility
proof
thus f is nonnegative implies for n holds f.n >= 0 by VALUED_0:28;
assume
A1: for n holds f.n >= 0;
let r be Real;
assume r in rng f;
then ex x being Element of NAT st r = f.x by FUNCT_2:113;
hence thesis by A1;
end;
end;
theorem Th17:
seq is nonnegative implies seq ^\k is nonnegative
proof
assume
A1: seq is nonnegative;
for n holds (seq ^\k).n >= 0
proof
let n;
(seq ^\k).n = seq.(n+k) by NAT_1:def 3;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th18:
seq is bounded_below nonnegative implies lower_bound seq >= 0
by Th10;
theorem
seq is bounded_above nonnegative implies upper_bound seq >= 0
proof
assume
A1: seq is bounded_above nonnegative;
then
A2: seq.0 <= upper_bound seq by Th7;
0 <= seq.0 by A1;
hence thesis by A2;
end;
theorem Th20:
seq1 is bounded_below nonnegative & seq2 is bounded_below
nonnegative implies (seq1(#)seq2) is bounded_below &
lower_bound (seq1 (#) seq2) >= (
lower_bound seq1) * (lower_bound seq2)
proof
assume that
A1: seq1 is bounded_below nonnegative and
A2: seq2 is bounded_below nonnegative;
for n holds (seq1 (#) seq2).n >= (lower_bound seq1) * (lower_bound seq2)
proof
let n;
A3: (seq1 (#) seq2).n = seq1.n * seq2.n & seq1.n >=
lower_bound seq1 by A1,Th8,SEQ_1:8;
A4: lower_bound seq2 >= 0 by A2,Th18;
seq2.n >= lower_bound seq2 & lower_bound seq1 >= 0 by A1,A2,Th8,Th18;
hence thesis by A3,A4,XREAL_1:66;
end;
hence thesis by Th10;
end;
theorem Th21:
seq1 is bounded_above nonnegative & seq2 is bounded_above
nonnegative implies (seq1(#)seq2) is bounded_above &
upper_bound (seq1 (#) seq2) <= (
upper_bound seq1) * (upper_bound seq2)
proof
assume that
A1: seq1 is bounded_above nonnegative and
A2: seq2 is bounded_above nonnegative;
for n holds (seq1 (#) seq2).n <= (upper_bound seq1) * (upper_bound seq2)
proof
let n;
A3: (seq1 (#) seq2).n = seq1.n * seq2.n & seq1.n <= upper_bound seq1
by A1,Th7,SEQ_1:8;
A4: seq2.n >= 0 by A2;
seq2.n <= upper_bound seq2 & seq1.n >= 0 by A1,A2,Th7;
hence thesis by A3,A4,XREAL_1:66;
end;
hence thesis by Th9;
end;
theorem
seq is non-decreasing bounded_above implies seq is bounded;
theorem
seq is non-increasing bounded_below implies seq is bounded;
theorem Th24:
seq is non-decreasing bounded_above implies lim seq = upper_bound seq
proof
assume
A1: seq is non-decreasing bounded_above;
then for n holds seq.n <= lim seq by SEQ_4:37;
then
A2: upper_bound seq <= lim seq by Th9;
for n holds seq.n <= upper_bound seq by A1,Th7;
then lim seq <= upper_bound seq by A1,PREPOWER:2;
hence thesis by A2,XXREAL_0:1;
end;
theorem Th25:
seq is non-increasing bounded_below implies lim seq = lower_bound seq
proof
assume
A1: seq is non-increasing bounded_below;
then for n holds lim seq <= seq.n by SEQ_4:38;
then
A2: lim seq <= lower_bound seq by Th10;
for n holds lower_bound seq <= seq.n by A1,Th8;
then lower_bound seq <= lim seq by A1,PREPOWER:1;
hence thesis by A2,XXREAL_0:1;
end;
theorem
seq is bounded_above implies seq ^\k is bounded_above by SEQM_3:27;
theorem
seq is bounded_below implies seq ^\k is bounded_below by SEQM_3:28;
theorem
seq is bounded implies seq ^\k is bounded by SEQM_3:29;
theorem Th29:
for seq, n holds
{seq.k: n <= k} is Subset of REAL
proof
let seq, n;
set Y = {seq.k: n <= k};
now
let x be object;
assume x in Y;
then consider z1 be set such that
A1: z1 = x and
A2: z1 in Y;
consider k1 being Nat such that
A3: z1 = seq.k1 & n <= k1 by A2;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
z1 = seq.k1 by A3;
hence x in REAL by A1;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th30:
rng (seq ^\ k) = {seq.n where n: k <= n}
proof
set seq1 = seq ^\ k;
set Z = {seq.m where m: k <= m};
now
let x be object;
assume x in Z;
then consider k1 being Nat such that
A1: x=seq.k1 and
A2: k <= k1;
consider k2 being Nat such that
A3: k1 = k + k2 by A2,NAT_1:10;
reconsider k2 as Element of NAT by ORDINAL1:def 12;
x = seq1.k2 by A1,A3,NAT_1:def 3;
hence x in rng seq1 by FUNCT_2:4;
end;
then
A4: Z c= rng seq1;
A5: dom seq1 = NAT by FUNCT_2:def 1;
now
let y be object;
assume y in rng seq1;
then consider m1 be object such that
A6: m1 in NAT and
A7: y = seq1.m1 by A5,FUNCT_1:def 3;
reconsider m1 as Nat by A6;
reconsider km1 = k+m1 as Nat;
y = seq.(km1) by A7,NAT_1:def 3;
hence y in Z by SETLIM_1:1;
end;
then rng seq1 c= Z;
hence thesis by A4;
end;
theorem Th31:
seq is bounded_above implies for n for R being Subset of REAL st
R = {seq.k : n <= k} holds R is bounded_above
proof
assume
A1: seq is bounded_above;
let n;
set seq1 = seq ^\n;
seq1 is bounded_above by A1,SEQM_3:27;
then
A2: rng seq1 is bounded_above by Th5;
let R be Subset of REAL;
assume R = {seq.k : n <= k};
hence thesis by A2,Th30;
end;
theorem Th32:
seq is bounded_below implies for n for R being Subset of REAL st
R = {seq.k : n <= k} holds R is bounded_below
proof
assume
A1: seq is bounded_below;
let n;
set seq1 = seq ^\n;
seq1 is bounded_below by A1,SEQM_3:28;
then
A2: rng seq1 is bounded_below by Th6;
let R be Subset of REAL;
assume R = {seq.k : n <= k};
hence thesis by A2,Th30;
end;
theorem Th33:
seq is bounded implies for n for R being Subset of REAL st R = {
seq.k : n <= k} holds R is real-bounded
by Th31,Th32;
theorem Th34:
seq is non-decreasing implies for n for R being Subset of REAL
st R = {seq.k : n <= k} holds lower_bound R = seq.n
proof
assume
A1: seq is non-decreasing;
let n;
A2: now
let r;
assume r in {seq.k : n <= k};
then consider r1 being Real such that
A3: r = r1 & r1 in {seq.k : n <= k};
consider k1 such that
A4: r1 = seq.k1 and
A5: n <= k1 by A3;
consider k being Nat such that
A6: n + k =k1 by A5,NAT_1:10;
thus seq.n <= r by A1,A3,A4,A6,SEQM_3:5;
end;
let R be Subset of REAL;
A7: now
let s;
A8: seq.n in {seq.k : n <= k};
assume 0 < s;
hence ex r st r in {seq.k : n <= k} & r< seq.n + s by A8,XREAL_1:29;
end;
assume
A9: R = {seq.k : n <= k};
then
A10: R <> {} by SETLIM_1:1;
R is bounded_below by A1,A9,Th32,LIMFUNC1:1;
hence thesis by A9,A10,A2,A7,SEQ_4:def 2;
end;
theorem Th35:
seq is non-increasing implies for n for R being Subset of REAL
st R = {seq.k : n <= k} holds upper_bound R = seq.n
proof
assume
A1: seq is non-increasing;
let n;
A2: now
let r;
assume r in {seq.k : n <= k};
then consider r1 being Real such that
A3: r = r1 & r1 in {seq.k : n <= k};
consider k1 such that
A4: r1 = seq.k1 and
A5: n <= k1 by A3;
consider k being Nat such that
A6: n + k =k1 by A5,NAT_1:10;
thus r <= seq.n by A1,A3,A4,A6,SEQM_3:7;
end;
let R be Subset of REAL;
A7: now
let s;
A8: seq.n in {seq.k : n <= k};
assume 0 < s;
hence ex r st r in {seq.k : n <= k} & seq.n - s < r by A8,XREAL_1:44;
end;
assume
A9: R = {seq.k : n <= k};
then
A10: R <> {} by SETLIM_1:1;
R is bounded_above by A1,A9,Th31,LIMFUNC1:1;
hence thesis by A9,A10,A2,A7,SEQ_4:def 1;
end;
definition
let seq be Real_Sequence;
func inferior_realsequence seq -> Real_Sequence means
:Def4:
for n for Y being Subset of REAL st Y = {seq.k : n <= k}
holds it.n = lower_bound Y;
existence
proof
defpred P[Element of NAT, Element of REAL] means for Y being Subset of REAL
st Y = {seq.k: $1 <= k} holds $2 = lower_bound Y;
A1: for n being Element of NAT ex y being Element of REAL st P[n,y]
proof
let n be Element of NAT;
reconsider Y={seq.k: n <= k} as Subset of REAL by Th29;
reconsider y = lower_bound Y as Element of REAL by XREAL_0:def 1;
for Y being Subset of REAL st Y = {seq.k: n <= k} holds y = lower_bound Y;
hence thesis;
end;
consider f being sequence of REAL such that
A2: for n being Element of NAT holds P[n,f.n] from FUNCT_2:sch 3(A1);
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
uniqueness
proof
let seq1,seq2 be Real_Sequence such that
A3: for n for Y being Subset of REAL st Y = {seq.k : n <= k} holds
seq1.n = lower_bound Y and
A4: for m for Y being Subset of REAL st Y = {seq.k : m <= k} holds
seq2.m = lower_bound Y;
A5: for y being object st y in NAT holds seq1.y = seq2.y
proof
let y be object;
assume y in NAT;
then reconsider y as Element of NAT;
reconsider Y = {seq.k: y <= k} as Subset of REAL by Th29;
seq1.y = lower_bound Y by A3;
hence thesis by A4;
end;
NAT = dom seq1 & NAT = dom seq2 by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
definition
let seq be Real_Sequence;
func superior_realsequence seq -> Real_Sequence means
:Def5:
for n for Y
being Subset of REAL st Y = {seq.k : n <= k} holds it.n = upper_bound Y;
existence
proof
defpred P[Element of NAT, Element of REAL] means for Y being Subset of REAL
st Y = {seq.k: $1 <= k} holds $2 = upper_bound Y;
A1: for n being Element of NAT ex y being Element of REAL st P[n,y]
proof
let n be Element of NAT;
reconsider Y={seq.k: n <= k} as Subset of REAL by Th29;
reconsider y = upper_bound Y as Element of REAL by XREAL_0:def 1;
for Y being Subset of REAL st Y = {seq.k: n <= k} holds y = upper_bound Y;
hence thesis;
end;
consider f being sequence of REAL such that
A2: for n being Element of NAT holds P[n,
f.n] from FUNCT_2:sch 3(A1);
take f;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
uniqueness
proof
let seq1,seq2 be Real_Sequence such that
A3: for n for Y being Subset of REAL st Y = {seq.k : n <= k} holds
seq1.n = upper_bound Y and
A4: for m for Y being Subset of REAL st Y = {seq.k : m <= k} holds
seq2.m = upper_bound Y;
A5: for y being object st y in NAT holds seq1.y = seq2.y
proof
let y be object;
assume y in NAT;
then reconsider y as Element of NAT;
reconsider Y = {seq.k: y <= k} as Subset of REAL by Th29;
seq1.y = upper_bound Y by A3;
hence thesis by A4;
end;
NAT = dom seq1 & NAT = dom seq2 by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
theorem Th36:
(inferior_realsequence seq).n = lower_bound (seq ^\n)
proof
reconsider Y = {seq.k: n <= k} as Subset of REAL by Th29;
(inferior_realsequence seq).n = lower_bound Y by Def4
.= lower_bound rng (seq ^\ n) by Th30;
hence thesis;
end;
theorem Th37:
(superior_realsequence seq).n = upper_bound (seq ^\n)
proof
reconsider Y = {seq.k: n <= k} as Subset of REAL by Th29;
(superior_realsequence seq).n = upper_bound Y by Def5
.= upper_bound rng (seq ^\ n) by Th30;
hence thesis;
end;
theorem Th38:
seq is bounded_below implies (inferior_realsequence seq).0 = lower_bound seq
proof
reconsider Y1 = {seq.k : 0 <= k} as Subset of REAL by Th29;
(inferior_realsequence seq).0 = lower_bound Y1 by Def4
.= lower_bound seq by SETLIM_1:5;
hence thesis;
end;
theorem Th39:
seq is bounded_above implies (superior_realsequence seq).0 = upper_bound seq
proof
reconsider Y1 = {seq.k : 0 <= k} as Subset of REAL by Th29;
(superior_realsequence seq).0 = upper_bound Y1 by Def5
.= upper_bound seq by SETLIM_1:5;
hence thesis;
end;
theorem Th40:
seq is bounded_below implies (r = (inferior_realsequence seq).n
iff (for k holds r <= seq.(n+k)) & for s st 0<s ex k st seq.(n+k)<r+s)
proof
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
assume seq is bounded_below;
then
A1: Y1 is non empty bounded_below by Th32,SETLIM_1:1;
thus r = (inferior_realsequence seq).n implies (for k holds r<=seq.(n+k)) &
for s st 0<s ex k st seq.(n+k)<r+s
proof
assume r = (inferior_realsequence seq).n;
then
A2: r = lower_bound Y1 by Def4;
A3: for s st 0<s ex k st seq.(n+k)<r+s
proof
let s;
assume 0<s;
then consider r1 such that
A4: r1 in Y1 and
A5: r1<r+s by A1,A2,SEQ_4:def 2;
consider k1 such that
A6: r1=seq.k1 and
A7: n <= k1 by A4;
consider k2 being Nat such that
A8: k1 = n + k2 by A7,NAT_1:10;
thus thesis by A5,A6,A8;
end;
for k holds r<=seq.(n+k)
proof
let k;
seq.(n+k) in Y1 by SETLIM_1:1;
hence thesis by A1,A2,SEQ_4:def 2;
end;
hence thesis by A3;
end;
assume that
A9: for k holds r <= seq.(n+k) and
A10: for s st 0<s ex k st seq.(n+k)<r+s;
A11: for s st 0<s ex r1 st r1 in Y1 & r1<r+s
proof
let s;
assume 0<s;
then consider k such that
A12: seq.(n+k)<r+s by A10;
n + k >= n by NAT_1:11;
then seq.(n+k) in Y1;
hence thesis by A12;
end;
for r1 st r1 in Y1 holds r <= r1
proof
let r1;
assume r1 in Y1;
then consider k1 such that
A13: r1=seq.k1 and
A14: n <= k1;
consider k2 being Nat such that
A15: k1 = n + k2 by A14,NAT_1:10;
thus thesis by A9,A13,A15;
end;
then r=lower_bound Y1 by A1,A11,SEQ_4:def 2;
hence thesis by Def4;
end;
theorem Th41:
seq is bounded_above implies (r = (superior_realsequence seq).n
iff (for k holds seq.(n+k) <= r) & for s st 0<s ex k st r-s<seq.(n+k))
proof
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
assume seq is bounded_above;
then
A1: Y1 is non empty bounded_above by Th31,SETLIM_1:1;
thus r = (superior_realsequence seq).n implies (for k holds seq.(n+k) <= r)
& for s st 0<s ex k st r-s<seq.(n+k)
proof
assume r = (superior_realsequence seq).n;
then
A2: r = upper_bound Y1 by Def5;
A3: for s st 0<s ex k st r-s<seq.(n+k)
proof
let s;
assume 0<s;
then consider r1 such that
A4: r1 in Y1 and
A5: r-s<r1 by A1,A2,SEQ_4:def 1;
consider k1 such that
A6: r1=seq.k1 and
A7: n <= k1 by A4;
consider k2 being Nat such that
A8: k1 = n + k2 by A7,NAT_1:10;
thus thesis by A5,A6,A8;
end;
for k holds seq.(n+k) <= r
proof
let k;
seq.(n+k) in Y1 by SETLIM_1:1;
hence thesis by A1,A2,SEQ_4:def 1;
end;
hence thesis by A3;
end;
assume that
A9: for k holds seq.(n+k) <= r and
A10: for s st 0<s ex k st r-s<seq.(n+k);
A11: for s st 0<s ex r1 st r1 in Y1 & r-s<r1
proof
let s;
assume 0<s;
then consider k such that
A12: r-s<seq.(n+k) by A10;
n + k >= n by NAT_1:11;
then seq.(n+k) in Y1;
hence thesis by A12;
end;
for r1 st r1 in Y1 holds r1 <= r
proof
let r1;
assume r1 in Y1;
then consider k1 such that
A13: r1=seq.k1 and
A14: n <= k1;
consider k2 being Nat such that
A15: k1 = n + k2 by A14,NAT_1:10;
thus thesis by A9,A13,A15;
end;
then r=upper_bound Y1 by A1,A11,SEQ_4:def 1;
hence thesis by Def5;
end;
theorem Th42:
seq is bounded_below implies ((for k holds r <= seq.(n+k)) iff r
<= (inferior_realsequence seq).n)
proof
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
set seq1 = seq ^\n;
assume seq is bounded_below;
then
A1: seq1 is bounded_below by SEQM_3:28;
A2: rng seq1 = Y1 by Th30;
thus (for k holds r <= seq.(n+k)) implies r <= (inferior_realsequence seq).n
proof
assume
A3: for k holds r <= seq.(n+k);
now
let n1 being Nat;
n1 in NAT by ORDINAL1:def 12;
then seq1.n1 in rng seq1 by FUNCT_2:4;
then consider r1 such that
A4: seq1.n1= r1 and
A5: r1 in Y1 by A2;
consider k1 being Nat such that
A6: r1 = seq.k1 and
A7: n <= k1 by A5;
consider k2 being Nat such that
A8: k1 = n + k2 by A7,NAT_1:10;
thus r <= seq1.n1 by A3,A4,A6,A8;
end;
then r <= lower_bound seq1 by Th10;
then r <= lower_bound Y1 by Th30;
hence thesis by Def4;
end;
assume r <= (inferior_realsequence seq).n;
then r <= lower_bound Y1 by Def4;
then
A9: r <= lower_bound seq1 by Th30;
now
let m1 be Nat;
n <= n+m1 by NAT_1:11;
then seq.(n+m1) in Y1;
then seq.(n+m1) in rng seq1 by Th30;
then ex k being object st k in dom seq1 & seq1.k = seq.(n+m1)
by FUNCT_1:def 3;
hence r <= seq.(n+m1) by A1,A9,Th10;
end;
hence thesis;
end;
theorem Th43:
seq is bounded_below implies ((for m st n <= m holds r <= seq.m)
iff r <= (inferior_realsequence seq).n)
proof
assume
A1: seq is bounded_below;
thus (for m st n<=m holds r <= seq.m) implies r <= (inferior_realsequence
seq).n
proof
assume for m st n<=m holds r <= seq.m;
then for k holds r <= seq.(n+k) by NAT_1:11;
hence thesis by A1,Th42;
end;
assume
A2: r <= (inferior_realsequence seq).n;
now
let m;
assume n<=m;
then consider k being Nat such that
A3: m = n + k by NAT_1:10;
thus r <= seq.m by A1,A2,A3,Th42;
end;
hence thesis;
end;
theorem Th44:
seq is bounded_above implies ((for k holds seq.(n+k) <= r) iff (
superior_realsequence seq).n <= r)
proof
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
set seq1 = seq ^\n;
assume seq is bounded_above;
then
A1: seq1 is bounded_above by SEQM_3:27;
A2: rng seq1 = Y1 by Th30;
thus (for k holds seq.(n+k) <= r) implies (superior_realsequence seq).n <= r
proof
assume
A3: for k holds seq.(n+k) <= r;
now
let n1 being Nat;
n1 in NAT by ORDINAL1:def 12;
then seq1.n1 in rng seq1 by FUNCT_2:4;
then consider r1 such that
A4: seq1.n1= r1 and
A5: r1 in Y1 by A2;
consider k1 being Nat such that
A6: r1 = seq.k1 and
A7: n <= k1 by A5;
consider k2 being Nat such that
A8: k1 = n + k2 by A7,NAT_1:10;
thus seq1.n1 <= r by A3,A4,A6,A8;
end;
then upper_bound seq1 <= r by Th9;
then upper_bound Y1 <= r by Th30;
hence thesis by Def5;
end;
assume (superior_realsequence seq).n <= r;
then upper_bound Y1 <= r by Def5;
then
A9: upper_bound seq1 <= r by Th30;
now
let m1 being Nat;
n <= n+m1 by NAT_1:11;
then seq.(n+m1) in Y1;
then seq.(n+m1) in rng seq1 by Th30;
then ex k being object st k in dom seq1 & seq1.k = seq.(n+m1)
by FUNCT_1:def 3;
hence seq.(n+m1) <= r by A1,A9,Th9;
end;
hence thesis;
end;
theorem Th45:
seq is bounded_above implies ((for m st n<=m holds seq.m <= r)
iff (superior_realsequence seq).n <= r)
proof
assume
A1: seq is bounded_above;
thus (for m st n<=m holds seq.m <= r) implies (superior_realsequence seq).n
<= r
proof
assume for m st n<=m holds seq.m <= r;
then for k holds seq.(n+k) <= r by NAT_1:11;
hence thesis by A1,Th44;
end;
assume
A2: (superior_realsequence seq).n <= r;
now
let m;
assume n<=m;
then consider k being Nat such that
A3: m = n + k by NAT_1:10;
thus seq.m <= r by A1,A2,A3,Th44;
end;
hence thesis;
end;
theorem Th46:
seq is bounded_below implies (inferior_realsequence seq).n = min
((inferior_realsequence seq).(n+1),seq.n)
proof
reconsider Y2 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
reconsider Y3 = {seq.n} as Subset of REAL;
A1: (inferior_realsequence seq).(n+1) = lower_bound Y2 by Def4;
assume
A2: seq is bounded_below;
then
A3: Y2 <> {} & Y2 is bounded_below by Th32,SETLIM_1:1;
A4: Y3 is bounded_below
proof
consider t such that
A5: for m holds t<seq.m by A2,SEQ_2:def 4;
t is LowerBound of Y3
proof
let r be ExtReal;
assume r in Y3;
then r = seq.n by TARSKI:def 1;
hence t <= r by A5;
end;
hence thesis;
end;
(inferior_realsequence seq).n = lower_bound Y1 by Def4;
then (inferior_realsequence seq).n = lower_bound (Y2 \/ Y3) by SETLIM_1:2
.= min(lower_bound Y2,lower_bound Y3) by A3,A4,SEQ_4:142
.= min((inferior_realsequence seq).(n+1),seq.n) by A1,SEQ_4:9;
hence thesis;
end;
theorem Th47:
seq is bounded_above implies (superior_realsequence seq).n = max
((superior_realsequence seq).(n+1),seq.n)
proof
reconsider Y2 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
reconsider Y3 = {seq.n} as Subset of REAL;
A1: (superior_realsequence seq).(n+1) = upper_bound Y2 by Def5;
assume
A2: seq is bounded_above;
then
A3: Y2 <> {} & Y2 is bounded_above by Th31,SETLIM_1:1;
A4: Y3 is bounded_above
proof
consider t such that
A5: for m holds seq.m<t by A2,SEQ_2:def 3;
t is UpperBound of Y3
proof
let r be ExtReal;
assume r in Y3;
then r = seq.n by TARSKI:def 1;
hence r <=t by A5;
end;
hence thesis;
end;
(superior_realsequence seq).n = upper_bound Y1 by Def5;
then (superior_realsequence seq).n = upper_bound (Y2 \/ Y3) by SETLIM_1:2
.= max(upper_bound Y2,upper_bound Y3) by A3,A4,SEQ_4:143
.= max((superior_realsequence seq).(n+1),seq.n) by A1,SEQ_4:9;
hence thesis;
end;
theorem Th48:
seq is bounded_below implies (inferior_realsequence seq).n <= (
inferior_realsequence seq).(n+1)
proof
A1: min((inferior_realsequence seq).(n+1),seq.n) <= (inferior_realsequence
seq).(n+1) by XXREAL_0:17;
assume seq is bounded_below;
hence thesis by A1,Th46;
end;
theorem Th49:
seq is bounded_above implies (superior_realsequence seq).(n+1)
<= (superior_realsequence seq).n
proof
A1: (superior_realsequence seq).(n+1) <= max((superior_realsequence seq).(n+
1),seq.n) by XXREAL_0:25;
assume seq is bounded_above;
hence thesis by A1,Th47;
end;
theorem Th50:
seq is bounded_below implies inferior_realsequence seq is non-decreasing
by Th48;
theorem Th51:
seq is bounded_above implies superior_realsequence seq is non-increasing
by Th49;
theorem
seq is bounded implies (inferior_realsequence seq).n <= (
superior_realsequence seq).n
proof
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
assume
A1: seq is bounded;
A2: Y1 <> {} by SETLIM_1:1;
(superior_realsequence seq).n = upper_bound Y1 &
(inferior_realsequence seq).n =
lower_bound Y1 by Def4,Def5;
hence thesis by A1,A2,Th33,SEQ_4:11;
end;
theorem Th53:
seq is bounded implies (inferior_realsequence seq).n <= lower_bound (
superior_realsequence seq)
proof
reconsider Y2 = {seq.k2 : n <= k2} as Subset of REAL by Th29;
assume
A1: seq is bounded;
A2: now
let m;
reconsider Y1 = {seq.k1 : m <= k1} as Subset of REAL by Th29;
n <= n + m by NAT_1:11;
then
A3: seq.(n+m) in Y2;
Y2 is real-bounded by A1,Th33;
then Y2 is bounded_below;
then
A4: lower_bound Y2 <= seq.(n+m) by A3,SEQ_4:def 2;
m <= n + m by NAT_1:11;
then
A5: seq.(n+m) in Y1;
Y1 is real-bounded by A1,Th33;
then Y1 is bounded_above;
then
A6: seq.(n+m) <= upper_bound Y1 by A5,SEQ_4:def 1;
(superior_realsequence seq).m = upper_bound Y1 by Def5;
hence lower_bound Y2 <= (superior_realsequence seq).m by A6,A4,XXREAL_0:2;
end;
(inferior_realsequence seq).n = lower_bound Y2 by Def4;
hence thesis by A2,Th10;
end;
theorem Th54:
seq is bounded implies upper_bound(inferior_realsequence seq) <= (
superior_realsequence seq).n
proof
reconsider Y2 = {seq.k2 : n <= k2} as Subset of REAL by Th29;
assume
A1: seq is bounded;
A2: now
let m;
reconsider Y1 = {seq.k1 : m <= k1} as Subset of REAL by Th29;
n <= n + m by NAT_1:11;
then
A3: seq.(n+m) in Y2;
Y2 is real-bounded by A1,Th33;
then Y2 is bounded_above;
then
A4: upper_bound Y2 >= seq.(n+m) by A3,SEQ_4:def 1;
m <= n + m by NAT_1:11;
then
A5: seq.(n+m) in Y1;
Y1 is real-bounded by A1,Th33;
then Y1 is bounded_below;
then
A6: seq.(n+m) >= lower_bound Y1 by A5,SEQ_4:def 2;
(inferior_realsequence seq).m = lower_bound Y1 by Def4;
hence upper_bound Y2 >= (inferior_realsequence seq).m by A6,A4,XXREAL_0:2;
end;
(superior_realsequence seq).n = upper_bound Y2 by Def5;
hence thesis by A2,Th9;
end;
theorem Th55:
seq is bounded implies upper_bound(inferior_realsequence seq) <= lower_bound(
superior_realsequence seq)
proof
set seq1 = (inferior_realsequence seq);
set r = lower_bound(superior_realsequence seq);
assume seq is bounded;
then seq1.n <= r by Th53;
hence thesis by Th9;
end;
theorem Th56:
seq is bounded implies superior_realsequence seq is bounded &
inferior_realsequence seq is bounded
proof
assume
A1: seq is bounded;
then inferior_realsequence seq is non-decreasing by Th50;
then
A2: inferior_realsequence seq is bounded_below by LIMFUNC1:1;
now
let m;
upper_bound(inferior_realsequence seq) <= (superior_realsequence seq).m
by A1,Th54;
hence (upper_bound(inferior_realsequence seq)) - 1 <
(superior_realsequence seq).m
by Lm1;
end;
then
A3: (superior_realsequence seq) is bounded_below by SEQ_2:def 4;
now
let m;
(inferior_realsequence seq).m <= lower_bound (superior_realsequence seq)
by A1,Th53;
hence (inferior_realsequence seq).m <
(lower_bound (superior_realsequence seq)) +1
by Lm1;
end;
then
A4: (inferior_realsequence seq) is bounded_above by SEQ_2:def 3;
superior_realsequence seq is non-increasing by A1,Th51;
then superior_realsequence seq is bounded_above by LIMFUNC1:1;
hence thesis by A2,A4,A3;
end;
theorem Th57:
seq is bounded implies inferior_realsequence seq is convergent &
lim inferior_realsequence seq = upper_bound inferior_realsequence seq
proof
assume seq is bounded;
then
inferior_realsequence seq is non-decreasing & inferior_realsequence seq
is bounded by Th50,Th56;
hence thesis by Th24;
end;
theorem Th58:
seq is bounded implies superior_realsequence seq is convergent &
lim superior_realsequence seq = lower_bound superior_realsequence seq
proof
assume seq is bounded;
then
superior_realsequence seq is non-increasing & superior_realsequence seq
is bounded by Th51,Th56;
hence thesis by Th25;
end;
theorem Th59:
seq is bounded_below implies (inferior_realsequence seq).n = - (
superior_realsequence(-seq)).n
proof
assume
A1: seq is bounded_below;
(inferior_realsequence seq).n = lower_bound (seq ^\n) by Th36
.= - upper_bound -(seq ^\n) by A1,Th14,SEQM_3:28
.= - upper_bound ((-seq) ^\n) by SEQM_3:16;
hence thesis by Th37;
end;
theorem Th60:
seq is bounded_above implies (superior_realsequence seq).n = - (
inferior_realsequence(-seq)).n
proof
assume
A1: seq is bounded_above;
(superior_realsequence seq).n = upper_bound (seq ^\n) by Th37
.= - lower_bound -(seq ^\n) by A1,Th13,SEQM_3:27
.= - lower_bound ((-seq) ^\n) by SEQM_3:16;
hence thesis by Th36;
end;
theorem Th61:
seq is bounded_below implies (inferior_realsequence seq) = - (
superior_realsequence(-seq))
proof
assume seq is bounded_below;
then (inferior_realsequence seq).n = - (superior_realsequence(-seq)).n by
Th59;
hence thesis by SEQ_1:10;
end;
theorem Th62:
seq is bounded_above implies (superior_realsequence seq) = - (
inferior_realsequence(-seq))
proof
assume seq is bounded_above;
then (superior_realsequence seq).n = - (inferior_realsequence(-seq)).n by
Th60;
hence thesis by SEQ_1:10;
end;
theorem
seq is non-decreasing implies seq.n <= (inferior_realsequence seq).(n+ 1)
proof
reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: (inferior_realsequence seq).(n+1) = lower_bound Y1 by Def4;
assume
A2: seq is non-decreasing;
then lower_bound Y1 = seq.(n+1) by Th34;
hence thesis by A2,A1;
end;
Lm2: seq is non-decreasing implies (inferior_realsequence seq).n = seq.n
proof
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
assume
A1: seq is non-decreasing;
(inferior_realsequence seq).n = lower_bound Y1 by Def4;
hence thesis by A1,Th34;
end;
theorem
seq is non-decreasing implies inferior_realsequence seq = seq
proof
assume seq is non-decreasing;
then for n being Element of NAT holds
(inferior_realsequence seq).n = seq.n by Lm2;
hence thesis by FUNCT_2:63;
end;
theorem Th65:
seq is non-decreasing bounded_above implies seq.n <= (
superior_realsequence seq).(n+1)
proof
reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: seq.(n+1) in Y1;
assume
A2: seq is non-decreasing bounded_above;
then Y1 is bounded_above by Th31;
then
A3: seq.(n+1) <= upper_bound Y1 by A1,SEQ_4:def 1;
A4: (superior_realsequence seq).(n+1) = upper_bound Y1 by Def5;
seq.n <= seq.(n+1) by A2;
hence thesis by A4,A3,XXREAL_0:2;
end;
theorem Th66:
seq is non-decreasing bounded_above implies (
superior_realsequence seq).n = (superior_realsequence seq).(n+1)
proof
assume
A1: seq is non-decreasing bounded_above;
then seq.n <= (superior_realsequence seq).(n+1) by Th65;
then max((superior_realsequence seq).(n+1),seq.n) = (superior_realsequence
seq).(n+1) by XXREAL_0:def 10;
hence thesis by A1,Th47;
end;
theorem Th67:
seq is non-decreasing bounded_above implies (
superior_realsequence seq).n = upper_bound seq & (superior_realsequence seq)
is
constant
proof
reconsider ubs = upper_bound seq as Element of REAL by XREAL_0:def 1;
defpred P[Nat] means (superior_realsequence seq).$1 = ubs;
assume
A1: seq is non-decreasing bounded_above;
A2: for k being Nat st P[k] holds P[k+1]
by A1,Th66;
A3: P[0] by A1,Th39;
for k being Nat holds P[k] from NAT_1:sch 2(A3,A2);
hence thesis by VALUED_0:def 18;
end;
theorem
seq is non-decreasing bounded_above implies
lower_bound (superior_realsequence
seq) = upper_bound seq
proof
assume
A1: seq is non-decreasing bounded_above;
then (superior_realsequence seq) is constant by Th67;
then consider r1 being Element of REAL such that
A2: rng (superior_realsequence seq)={r1} by FUNCT_2:111;
r1 in rng (superior_realsequence seq) by A2,TARSKI:def 1;
then ex n being Element of NAT
st r1 = (superior_realsequence seq).n by FUNCT_2:113;
then rng (superior_realsequence seq)= {upper_bound seq} by A1,A2,Th67;
hence thesis by SEQ_4:9;
end;
theorem
seq is non-increasing implies (superior_realsequence seq).(n+1) <= seq .n
proof
reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: (superior_realsequence seq).(n+1) = upper_bound Y1 by Def5;
assume
A2: seq is non-increasing;
then upper_bound Y1 = seq.(n+1) by Th35;
hence thesis by A2,A1;
end;
Lm3: seq is non-increasing implies (superior_realsequence seq).n = seq.n
proof
reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
assume
A1: seq is non-increasing;
(superior_realsequence seq).n = upper_bound Y1 by Def5;
hence thesis by A1,Th35;
end;
theorem
seq is non-increasing implies superior_realsequence seq = seq
proof
assume seq is non-increasing;
then for n being Element of NAT holds
(superior_realsequence seq).n = seq.n by Lm3;
hence thesis by FUNCT_2:63;
end;
theorem Th71:
seq is non-increasing bounded_below implies (
inferior_realsequence seq).(n+1) <= seq.n
proof
reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: seq.(n+1) in Y1;
assume
A2: seq is non-increasing bounded_below;
then Y1 is bounded_below by Th32;
then
A3: lower_bound Y1 <= seq.(n+1) by A1,SEQ_4:def 2;
A4: (inferior_realsequence seq).(n+1) = lower_bound Y1 by Def4;
seq.(n+1) <= seq.n by A2;
hence thesis by A4,A3,XXREAL_0:2;
end;
theorem Th72:
seq is non-increasing bounded_below implies (
inferior_realsequence seq).n = (inferior_realsequence seq).(n+1)
proof
assume
A1: seq is non-increasing bounded_below;
then (inferior_realsequence seq).(n+1) <= seq.n by Th71;
then min((inferior_realsequence seq).(n+1),seq.n) = (inferior_realsequence
seq).(n+1) by XXREAL_0:def 9;
hence thesis by A1,Th46;
end;
theorem Th73:
seq is non-increasing & seq is bounded_below implies (
inferior_realsequence seq).n = lower_bound seq &
(inferior_realsequence seq) is
constant
proof
assume that
A1: seq is non-increasing and
A2: seq is bounded_below;
reconsider lbs = lower_bound seq as Element of REAL by XREAL_0:def 1;
defpred P[Nat] means (inferior_realsequence seq).$1 = lbs;
A3: for k being Nat st P[k] holds P[k+1]
by A1,A2,Th72;
A4: P[0] by A2,Th38;
for k being Nat holds P[k] from NAT_1:sch 2(A4,A3);
hence thesis by VALUED_0:def 18;
end;
theorem
seq is non-increasing bounded_below implies upper_bound inferior_realsequence
seq = lower_bound seq
proof
assume
A1: seq is non-increasing bounded_below;
then inferior_realsequence seq is constant by Th73;
then consider r1 being Element of REAL such that
A2: rng inferior_realsequence seq={r1} by FUNCT_2:111;
r1 in rng inferior_realsequence seq by A2,TARSKI:def 1;
then ex n being Element of NAT
st r1 = (inferior_realsequence seq).n by FUNCT_2:113;
then upper_bound inferior_realsequence seq =
upper_bound {lower_bound seq} by A1,A2,Th73
.= lower_bound seq by SEQ_4:9;
hence thesis;
end;
theorem Th75:
seq1 is bounded & seq2 is bounded & (for n holds seq1.n <= seq2.
n) implies (for n holds (superior_realsequence seq1).n <= (
superior_realsequence seq2).n) & for n holds (inferior_realsequence seq1).n <=
(inferior_realsequence seq2).n
proof
assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n holds seq1.n <= seq2.n;
now
let n;
reconsider Y2 = {seq2.k2 : n <= k2} as Subset of REAL by Th29;
reconsider Y1 = {seq1.k1 : n <= k1} as Subset of REAL by Th29;
A4: Y1 <> {} & Y2 <> {} by SETLIM_1:1;
A5: (inferior_realsequence seq1).n = lower_bound Y1 &
(inferior_realsequence seq2)
.n = lower_bound Y2 by Def4;
Y1 is real-bounded by A1,Th33;
then
A6: Y1 is bounded_below;
now
let r;
assume r in Y2;
then consider k such that
A7: r = seq2.k and
A8: n <= k;
seq1.k in Y1 by A8;
then
A9: lower_bound Y1 <= seq1.k by A6,SEQ_4:def 2;
seq1.k <= r by A3,A7;
hence lower_bound Y1 <= r by A9,XXREAL_0:2;
end;
then
A10: for r be Real st r in Y2 holds lower_bound Y1 <= r;
Y2 is real-bounded by A2,Th33;
then
A11: Y2 is bounded_above;
A12: now
let r be Real;
assume r in Y1;
then consider k such that
A13: r = seq1.k and
A14: n <= k;
seq2.k in Y2 by A14;
then
A15: seq2.k <= upper_bound Y2 by A11,SEQ_4:def 1;
r <= seq2.k by A3,A13;
hence r <= upper_bound Y2 by A15,XXREAL_0:2;
end;
(superior_realsequence seq1).n = upper_bound Y1 &
(superior_realsequence seq2)
.n = upper_bound Y2 by Def5;
hence (superior_realsequence seq1).n <= (superior_realsequence seq2).n & (
inferior_realsequence seq1).n <= (inferior_realsequence seq2).n
by A5,A4,A12,A10,SEQ_4:113,144;
end;
hence thesis;
end;
theorem
seq1 is bounded_below & seq2 is bounded_below implies (
inferior_realsequence(seq1+seq2)).n >= (inferior_realsequence seq1).n + (
inferior_realsequence seq2).n
proof
assume seq1 is bounded_below & seq2 is bounded_below;
then seq1 ^\n is bounded_below & seq2 ^\n is bounded_below by SEQM_3:28;
then lower_bound(seq1 ^\n + seq2 ^\n) >=
lower_bound(seq1 ^\n) + lower_bound(seq2 ^\n) by Th15;
then
A1: lower_bound((seq1+seq2) ^\n) >=
lower_bound(seq1 ^\n) + lower_bound(seq2 ^\n) by SEQM_3:15;
(inferior_realsequence seq1).n =
lower_bound(seq1 ^\n) & (inferior_realsequence
seq2 ).n = lower_bound(seq2 ^\n) by Th36;
hence thesis by A1,Th36;
end;
theorem
seq1 is bounded_above & seq2 is bounded_above implies (
superior_realsequence(seq1+seq2)).n <= (superior_realsequence seq1).n + (
superior_realsequence seq2).n
proof
assume seq1 is bounded_above & seq2 is bounded_above;
then seq1 ^\n is bounded_above & seq2 ^\n is bounded_above by SEQM_3:27;
then upper_bound(seq1 ^\n + seq2 ^\n) <=
upper_bound(seq1 ^\n) + upper_bound(seq2 ^\n) by Th16;
then
A1: upper_bound((seq1+seq2) ^\n) <=
upper_bound(seq1 ^\n) + upper_bound(seq2 ^\n) by SEQM_3:15;
(superior_realsequence seq1).n = upper_bound(seq1 ^\n) &
(superior_realsequence
seq2 ).n = upper_bound(seq2 ^\n) by Th37;
hence thesis by A1,Th37;
end;
theorem
seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative
implies (inferior_realsequence(seq1(#)seq2)).n >= (inferior_realsequence seq1).
n * (inferior_realsequence seq2).n
proof
assume seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative;
then seq1 ^\n is bounded_below nonnegative & seq2 ^\n is bounded_below
nonnegative by Th17,SEQM_3:28;
then lower_bound((seq1 ^\n)(#)(seq2 ^\n))>=
lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by Th20;
then
A1: lower_bound((seq1 (#) seq2) ^\n) >=
lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by SEQM_3:19;
(inferior_realsequence seq1).n = lower_bound(seq1 ^\n) &
(inferior_realsequence
seq2 ).n = lower_bound(seq2 ^\n) by Th36;
hence thesis by A1,Th36;
end;
theorem Th79:
seq1 is bounded_below nonnegative & seq2 is bounded_below
nonnegative implies (inferior_realsequence(seq1(#)seq2)).n >= (
inferior_realsequence seq1).n * (inferior_realsequence seq2).n
proof
assume seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative;
then seq1 ^\n is bounded_below nonnegative & seq2 ^\n is bounded_below
nonnegative by Th17,SEQM_3:28;
then lower_bound((seq1 ^\n)(#)(seq2 ^\n))>=
lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by Th20;
then
A1: lower_bound((seq1 (#) seq2) ^\n) >=
lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by SEQM_3:19;
(inferior_realsequence seq1).n = lower_bound(seq1 ^\n) &
(inferior_realsequence
seq2 ).n = lower_bound(seq2 ^\n) by Th36;
hence thesis by A1,Th36;
end;
theorem Th80:
seq1 is bounded_above nonnegative & seq2 is bounded_above
nonnegative implies (superior_realsequence(seq1(#)seq2)).n <= (
superior_realsequence seq1).n * (superior_realsequence seq2).n
proof
assume seq1 is bounded_above nonnegative & seq2 is bounded_above nonnegative;
then seq1 ^\n is bounded_above nonnegative & seq2 ^\n is bounded_above
nonnegative by Th17,SEQM_3:27;
then upper_bound((seq1 ^\n)(#)(seq2 ^\n))<=
upper_bound(seq1 ^\n) * upper_bound(seq2 ^\n) by Th21;
then
A1: upper_bound((seq1 (#) seq2) ^\n) <=
upper_bound(seq1 ^\n) * upper_bound(seq2 ^\n) by SEQM_3:19;
(superior_realsequence seq1).n = upper_bound(seq1 ^\n) &
(superior_realsequence
seq2 ).n = upper_bound(seq2 ^\n) by Th37;
hence thesis by A1,Th37;
end;
definition
let seq be Real_Sequence;
func lim_sup seq -> Real equals
lower_bound superior_realsequence seq;
coherence;
end;
definition
let seq be Real_Sequence;
func lim_inf seq -> Real equals
upper_bound inferior_realsequence seq;
coherence;
end;
theorem Th81:
seq is bounded implies (lim_inf seq <= r iff for s st 0<s holds
for n ex k st seq.(n+k)<r+s )
proof
set seq1 = inferior_realsequence seq;
assume
A1: seq is bounded;
then
A2: seq1 is bounded by Th56;
thus lim_inf seq <= r implies for s st 0<s holds for n ex k st seq.(n+k)<r+s
proof
assume
A3: lim_inf seq <= r;
let s such that
A4: 0<s;
for n ex k st seq.(n+k)<r+s
proof
let n;
consider k such that
A5: seq.(n+k) < seq1.n+s by A1,A4,Th40;
seq1.n <= r by A2,A3,Th9;
then seq.(n+k)+seq1.n < r+(seq1.n+s) by A5,XREAL_1:8;
then seq.(n+k) < r+(seq1.n+s)-seq1.n by XREAL_1:20;
hence thesis;
end;
hence thesis;
end;
assume
A6: for s st 0<s holds for n ex k st seq.(n+k)<r+s;
for s st 0<s holds lim_inf seq<=r+s
proof
let s such that
A7: 0<s;
for n holds seq1.n <= r+s
proof
let n;
consider k such that
A8: seq.(n+k)<r+s by A6,A7;
seq1.n <= seq.(n+k) by A1,Th40;
hence thesis by A8,XXREAL_0:2;
end;
hence thesis by Th9;
end;
hence thesis by XREAL_1:41;
end;
theorem Th82:
seq is bounded implies (r <= lim_inf seq iff for s st 0<s holds
ex n st for k holds r-s<seq.(n+k) )
proof
set seq1 = inferior_realsequence seq;
assume
A1: seq is bounded;
then
A2: seq1 is bounded by Th56;
thus r <= lim_inf seq implies for s st 0<s holds ex n st for k holds r-s<seq
.(n+k)
proof
assume
A3: r <= lim_inf seq;
let s such that
A4: 0<s;
ex n st for k holds r-s<seq.(n+k)
proof
consider n1 be Nat such that
A5: seq1.n1 > upper_bound seq1-s by A2,A4,Th7;
seq1.n1 + upper_bound seq1 > r + (upper_bound seq1-s)
by A3,A5,XREAL_1:8;
then seq1.n1 + upper_bound seq1 > r - s + upper_bound seq1;
then
A6: (seq1.n1 + upper_bound seq1) - upper_bound seq1 > r-s by XREAL_1:20;
now
let k;
seq1.n1 <= seq.(n1+k) by A1,Th40;
then (r-s) + seq1.n1 < seq.(n1+k) + seq1.n1 by A6,XREAL_1:8;
then (r-s) + seq1.n1 - seq1.n1 < seq.(n1+k) by XREAL_1:19;
hence r-s<seq.(n1+k);
end;
hence thesis;
end;
hence thesis;
end;
assume
A7: for s st 0<s holds ex n st for k holds r-s<seq.(n+k);
for s st 0<s holds r-s<=lim_inf seq
proof
let s;
assume 0<s;
then consider n1 be Nat such that
A8: for k holds r-s<seq.(n1+k) by A7;
for k holds r-s<=seq.(n1+k) by A8;
then
A9: r-s <= seq1.n1 by A1,Th42;
seq1.n1 <= upper_bound seq1 by A2,Th7;
hence thesis by A9,XXREAL_0:2;
end;
hence thesis by XREAL_1:57;
end;
theorem
seq is bounded implies (r = lim_inf seq iff for s st 0<s holds (for n
ex k st seq.(n+k)<r+s) & ex n st for k holds r-s<seq.(n+k) )
proof
assume
A1: seq is bounded;
hence
r = lim_inf seq implies for s st 0<s holds (for n ex k st seq.(n+k)<r+s
) & ex n st for k holds r-s<seq.(n+k) by Th81,Th82;
assume
A2: for s st 0<s holds (for n ex k st seq.(n+k)<r+s) & ex n st for k
holds r-s<seq.(n+k);
then for s st 0<s holds ex n st for k holds r-s<seq.(n+k);
then
A3: r <= lim_inf seq by A1,Th82;
for s st 0<s holds for n ex k st seq.(n+k)<r+s by A2;
then lim_inf seq <= r by A1,Th81;
hence thesis by A3,XXREAL_0:1;
end;
theorem Th84:
seq is bounded implies (r <= lim_sup seq iff for s st 0<s holds
for n ex k st seq.(n+k)>r-s )
proof
set seq1 = superior_realsequence seq;
assume
A1: seq is bounded;
then
A2: seq1 is bounded by Th56;
thus r <= lim_sup seq implies for s st 0<s holds for n ex k st seq.(n+k)>r-s
proof
assume
A3: r <= lim_sup seq;
let s such that
A4: 0<s;
for n ex k st seq.(n+k)>r-s
proof
let n;
consider k such that
A5: seq.(n+k) > seq1.n-s by A1,A4,Th41;
seq1.n >= r by A2,A3,Th10;
then seq1.n+seq.(n+k) > r+(seq1.n-s) by A5,XREAL_1:8;
then seq.(n+k) > r+seq1.n-s-seq1.n by XREAL_1:19;
hence thesis;
end;
hence thesis;
end;
assume
A6: for s st 0<s holds for n ex k st seq.(n+k)>r-s;
for s st 0<s holds lim_sup seq>=r-s
proof
let s such that
A7: 0<s;
for n holds r-s <= seq1.n
proof
let n;
consider k such that
A8: r-s<seq.(n+k) by A6,A7;
seq.(n+k) <= seq1.n by A1,Th41;
hence thesis by A8,XXREAL_0:2;
end;
hence thesis by Th10;
end;
hence thesis by XREAL_1:57;
end;
theorem Th85:
seq is bounded implies (lim_sup seq <= r iff for s st 0<s holds
ex n st for k holds seq.(n+k)<r+s )
proof
set seq1 = superior_realsequence seq;
assume
A1: seq is bounded;
then
A2: seq1 is bounded by Th56;
thus lim_sup seq <= r implies for s st 0<s holds ex n st for k holds seq.(n+
k)<r+s
proof
assume
A3: lim_sup seq <= r;
for s st 0<s holds ex n st for k holds seq.(n+k)<r+s
proof
let s such that
A4: 0<s;
ex n st for k holds seq.(n+k)<r+s
proof
consider n1 be Nat such that
A5: seq1.n1 < lower_bound seq1+s by A2,A4,Th8;
seq1.n1 + lower_bound seq1 < r + (lower_bound seq1+s)
by A3,A5,XREAL_1:8;
then seq1.n1 + lower_bound seq1 < r + s + lower_bound seq1;
then
A6: (seq1.n1 + lower_bound seq1) - lower_bound seq1 < r+s by XREAL_1:19;
now
let k;
seq.(n1+k) <= seq1.n1 by A1,Th41;
then seq.(n1+k) + seq1.n1 < (r+s) + seq1.n1 by A6,XREAL_1:8;
then seq.(n1+k) + seq1.n1 - seq1.n1 < (r+s) by XREAL_1:19;
hence seq.(n1+k) < r+s;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
assume
A7: for s st 0<s holds ex n st for k holds seq.(n+k)<r+s;
for s st 0<s holds lim_sup seq<=r+s
proof
let s;
assume 0<s;
then consider n1 be Nat such that
A8: for k holds seq.(n1+k)<r+s by A7;
for k holds seq.(n1+k)<=r+s by A8;
then
A9: seq1.n1<=r+s by A1,Th44;
lower_bound seq1 <= seq1.n1 by A2,Th8;
hence thesis by A9,XXREAL_0:2;
end;
hence thesis by XREAL_1:41;
end;
theorem
seq is bounded implies (r = lim_sup seq iff for s st 0<s holds (for n
holds ex k st seq.(n+k)>r-s) & ex n st for k holds seq.(n+k)<r+s )
proof
assume
A1: seq is bounded;
hence
r = lim_sup seq implies for s st 0<s holds (for n holds ex k st seq.(n+
k)>r-s) & ex n st for k holds seq.(n+k)<r+s by Th84,Th85;
assume
A2: for s st 0<s holds (for n holds ex k st seq.(n+k)>r-s) & ex n st for
k holds seq.(n+k)<r+s;
then for s st 0<s holds ex n st for k holds seq.(n+k)<r+s;
then
A3: lim_sup seq <= r by A1,Th85;
for s st 0<s holds for n holds ex k st seq.(n+k)>r-s by A2;
then r <= lim_sup seq by A1,Th84;
hence thesis by A3,XXREAL_0:1;
end;
theorem
seq is bounded implies lim_inf seq <= lim_sup seq by Th55;
theorem Th88:
seq is bounded & lim_sup seq = lim_inf seq iff seq is convergent
proof
thus seq is bounded & lim_sup seq = lim_inf seq implies seq is convergent
proof
reconsider r= lower_bound superior_realsequence seq as Real;
assume that
A1: seq is bounded and
A2: lim_sup seq = lim_inf seq;
A3: inferior_realsequence seq is bounded by A1,Th56;
A4: inferior_realsequence seq is non-decreasing by A1,Th50;
A5: superior_realsequence seq is non-increasing by A1,Th51;
A6: superior_realsequence seq is bounded by A1,Th56;
for s st 0<s ex n st for m st n<=m holds |.seq.m-r.| < s
proof
let s such that
A7: 0 < s;
consider k2 be Nat such that
A8: (superior_realsequence seq).k2 < r + s by A6,A7,Th8;
consider k1 be Nat such that
A9: r - s < (inferior_realsequence seq).k1 by A2,A3,A7,Th7;
reconsider k = max(k1,k2) as Nat by TARSKI:1;
k2 <= k by XXREAL_0:25;
then
A10: (superior_realsequence seq).k <= (superior_realsequence seq).k2
by A5,SEQM_3:8;
k1 <= k by XXREAL_0:25;
then
A11: (inferior_realsequence seq).k1 <= (inferior_realsequence seq). k
by A4,SEQM_3:6;
ex n st for m st n<=m holds |.seq.m-r.| < s
proof
take k;
let m;
assume k <= m;
then consider k3 being Nat such that
A12: m = k + k3 by NAT_1:10;
seq.m <= (superior_realsequence seq).k by A1,A12,Th41;
then seq.m <= (superior_realsequence seq).k2 by A10,XXREAL_0:2;
then
A13: seq.m < r + s by A8,XXREAL_0:2;
(inferior_realsequence seq).k <= seq.m by A1,A12,Th40;
then (inferior_realsequence seq).k1 <= seq.m by A11,XXREAL_0:2;
then r - s < seq.m by A9,XXREAL_0:2;
hence thesis by A13,Th1;
end;
hence thesis;
end;
hence thesis by SEQ_2:def 6;
end;
assume
A14: seq is convergent;
then consider r such that
A15: for p st 0 < p ex n st for m st n<=m holds |.seq.m-r.| < p by SEQ_2:def 6;
A16: seq is bounded by A14;
A17: for p st 0 < p ex n st r - p <= (inferior_realsequence seq).n & (
superior_realsequence seq).n <= r + p
proof
let p;
assume 0 < p;
then consider n such that
A18: for m st n<=m holds |.seq.m-r.| < p by A15;
A19: for m st n<=m holds r - p <= seq.m & seq.m <= r + p
proof
let m;
assume n<=m;
then |.seq.m-r.| < p by A18;
hence thesis by Th1;
end;
then for m st n<=m holds seq.m <= r + p;
then
A20: (superior_realsequence seq).n <= r + p by A16,Th45;
for m st n<=m holds r - p <= seq.m by A19;
then r - p <= (inferior_realsequence seq).n by A16,Th43;
hence thesis by A20;
end;
A21: superior_realsequence seq is bounded & inferior_realsequence seq is
bounded by A16,Th56;
A22: for p holds 0 < p implies r - p <= upper_bound inferior_realsequence seq &
lower_bound
superior_realsequence seq <= r + p
proof
let p;
assume 0 < p;
then consider n such that
A23: r - p <= (inferior_realsequence seq).n & (superior_realsequence
seq).n <= r + p by A17;
(inferior_realsequence seq).n <= upper_bound inferior_realsequence seq &
lower_bound
superior_realsequence seq <= (superior_realsequence seq).n by A21,Th7,Th8;
hence thesis by A23,XXREAL_0:2;
end;
reconsider r as Real;
A24: for p holds 0 < p implies lower_bound superior_realsequence seq <= r + p
by A22;
then
A25: lower_bound superior_realsequence seq <= r by XREAL_1:41;
for p holds 0 < p implies r <= upper_bound inferior_realsequence seq + p
proof
let p;
assume 0 < p;
then r - p <= upper_bound inferior_realsequence seq by A22;
hence thesis by XREAL_1:20;
end;
then
A26: r <= upper_bound inferior_realsequence seq by XREAL_1:41;
A27: upper_bound (inferior_realsequence seq) <=
lower_bound (superior_realsequence seq) by A14,Th55;
lower_bound superior_realsequence seq <= r by A24,XREAL_1:41;
then upper_bound inferior_realsequence seq <= r by A27,XXREAL_0:2;
then r = upper_bound inferior_realsequence seq by A26,XXREAL_0:1;
hence thesis by A14,A27,A25,XXREAL_0:1;
end;
theorem
seq is convergent implies lim seq = lim_sup seq & lim seq = lim_inf seq
proof
reconsider r= lim seq as Real;
assume
A1: seq is convergent;
then
A2: upper_bound(inferior_realsequence seq) <=
lower_bound(superior_realsequence seq) by Th55;
A3: seq is bounded by A1;
then
A4: superior_realsequence seq is bounded & inferior_realsequence seq is
bounded by Th56;
A5: for p holds 0 < p implies r - p <= upper_bound inferior_realsequence seq &
lower_bound
superior_realsequence seq <= r + p
proof
let p;
assume 0 < p;
then consider k such that
A6: for m st k <= m holds |.seq.m-r.|<p by A1,SEQ_2:def 7;
A7: for m st k <= m holds r - p <= seq.m & seq.m <= r + p
proof
let m;
assume k <= m;
then |.seq.m - r.| < p by A6;
hence thesis by Th1;
end;
then for m st k <= m holds r - p <= seq.m;
then
A8: r - p <= (inferior_realsequence seq).k by A3,Th43;
for m st k <= m holds seq.m <= r + p by A7;
then
A9: (superior_realsequence seq).k <= r + p by A3,Th45;
(inferior_realsequence seq).k <= upper_bound inferior_realsequence seq &
lower_bound
superior_realsequence seq <= (superior_realsequence seq).k by A4,Th7,Th8;
hence thesis by A8,A9,XXREAL_0:2;
end;
A10: for p holds 0 < p implies r <= upper_bound inferior_realsequence seq + p
proof
let p;
assume 0 < p;
then r - p <= upper_bound inferior_realsequence seq by A5;
hence thesis by XREAL_1:20;
end;
then
A11: r <= upper_bound inferior_realsequence seq by XREAL_1:41;
r <= upper_bound inferior_realsequence seq by A10,XREAL_1:41;
then
A12: r <= lower_bound superior_realsequence seq by A2,XXREAL_0:2;
for p holds 0 < p implies lower_bound superior_realsequence seq <=
r + p by A5;
then
A13: lower_bound superior_realsequence seq <= r by XREAL_1:41;
then upper_bound inferior_realsequence seq <= r by A2,XXREAL_0:2;
hence thesis by A13,A11,A12,XXREAL_0:1;
end;
theorem Th90:
seq is bounded implies lim_sup -seq = - lim_inf seq & lim_inf -
seq = - lim_sup seq
proof
assume
A1: seq is bounded;
then inferior_realsequence seq is bounded by Th56;
then
A2: - lim_inf seq = - - lower_bound - inferior_realsequence seq by Th13
.= lower_bound - -superior_realsequence(-seq) by A1,Th61
.= lim_sup -seq;
superior_realsequence seq is bounded by A1,Th56;
then - lim_sup seq = - - upper_bound - superior_realsequence seq by Th14
.= upper_bound - -inferior_realsequence(-seq) by A1,Th62
.= lim_inf -seq;
hence thesis by A2;
end;
theorem
seq1 is bounded & seq2 is bounded & (for n holds seq1.n <= seq2.n)
implies lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2
proof
assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n holds seq1.n <= seq2.n;
A4: superior_realsequence seq1 is convergent & inferior_realsequence seq1 is
convergent by A1,Th57,Th58;
superior_realsequence seq2 is bounded by A2,Th56;
then
A5: lim superior_realsequence seq2 = lower_bound superior_realsequence seq2
by A2,Th25,Th51;
inferior_realsequence seq1 is bounded by A1,Th56;
then
A6: lim inferior_realsequence seq1 = upper_bound inferior_realsequence seq1
by A1,Th24,Th50;
superior_realsequence seq1 is bounded by A1,Th56;
then
A7: lim superior_realsequence seq1 = lower_bound superior_realsequence seq1
by A1,Th25,Th51;
A8: superior_realsequence seq2 is convergent & inferior_realsequence seq2 is
convergent by A2,Th57,Th58;
inferior_realsequence seq2 is bounded by A2,Th56;
then
A9: lim inferior_realsequence seq2 = upper_bound inferior_realsequence seq2
by A2,Th24,Th50;
( for n holds (superior_realsequence seq1).n <= (superior_realsequence
seq2).n) & for n holds (inferior_realsequence seq1).n <= (inferior_realsequence
seq2).n by A1,A2,A3,Th75;
hence thesis by A4,A8,A7,A6,A5,A9,SEQ_2:18;
end;
theorem
seq1 is bounded & seq2 is bounded implies lim_inf seq1 + lim_inf seq2
<= lim_inf (seq1+seq2) & lim_inf (seq1+seq2) <= lim_inf seq1 + lim_sup seq2 &
lim_inf (seq1+seq2) <= lim_sup seq1 + lim_inf seq2 & lim_inf seq1 + lim_sup
seq2 <= lim_sup (seq1+seq2) & lim_sup seq1 + lim_inf seq2 <= lim_sup (seq1+seq2
) & lim_sup (seq1+seq2) <= lim_sup seq1 + lim_sup seq2 & (seq1 is convergent or
seq2 is convergent implies lim_inf (seq1+seq2) = lim_inf seq1 + lim_inf seq2 &
lim_sup (seq1+seq2) = lim_sup seq1 + lim_sup seq2 )
proof
assume
A1: seq1 is bounded & seq2 is bounded;
A2: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_sup (seq1+
seq2) <= lim_sup seq1 + lim_sup seq2
proof
let seq1,seq2;
set r1 = lim_sup seq1, r2 = lim_sup seq2;
assume that
A3: seq1 is bounded and
A4: seq2 is bounded;
for s st 0<s holds ex n st for k holds (seq1+seq2).(n+k) < r1+r2+s
proof
let s;
assume 0<s;
then
A5: 0<s/2 by XREAL_1:215;
then consider n1 being Nat such that
A6: for k holds seq1.(n1+k) < r1+s/2 by A3,Th85;
consider n2 being Nat such that
A7: for k holds seq2.(n2+k) < r2+s/2 by A4,A5,Th85;
for k holds (seq1+seq2).(n1+n2+k) < r1+r2+s
proof
let k;
seq1.(n1+(n2+k)) < r1+s/2 & seq2.(n2+(n1+k)) < r2+s/2 by A6,A7;
then seq1.(n1+n2+k) + seq2.(n1+n2+k) < (r1+s/2)+(r2+s/2) by XREAL_1:8;
hence thesis by SEQ_1:7;
end;
hence thesis;
end;
hence thesis by A3,A4,Th85;
end;
A8: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf seq1 +
lim_sup seq2 <= lim_sup (seq1+seq2)
proof
let seq1,seq2;
assume that
A9: seq1 is bounded and
A10: seq2 is bounded;
lim_sup ((seq1+seq2)+(-seq1)) <= lim_sup (-seq1) + lim_sup (seq1+
seq2) by A2,A9,A10;
then lim_sup (seq1+seq2+-seq1) <= -lim_inf seq1 + lim_sup (seq1+seq2) by A9
,Th90;
then lim_sup (seq2+seq1-seq1) <= lim_sup (seq1+seq2) - lim_inf seq1;
then lim_sup seq2 <= lim_sup (seq1+seq2) - lim_inf seq1 by Th2;
hence thesis by XREAL_1:19;
end;
then
A11: lim_inf seq1 + lim_sup seq2 <= lim_sup (seq1+seq2) by A1;
A12: lim_sup seq1 + lim_inf seq2 <= lim_sup (seq1+seq2) by A8,A1;
A13: lim_sup (seq1+seq2) <= lim_sup seq1 + lim_sup seq2 by A2,A1;
A14: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf seq1 +
lim_inf seq2 <= lim_inf (seq1+seq2)
proof
let seq1,seq2;
set r1 = lim_inf seq1, r2 = lim_inf seq2;
assume that
A15: seq1 is bounded and
A16: seq2 is bounded;
for s st 0<s holds ex n st for k holds r1+r2-s < (seq1+seq2).(n+k)
proof
let s;
assume 0<s;
then
A17: 0<s/2 by XREAL_1:215;
then consider n1 being Nat such that
A18: for k holds r1-s/2 < seq1.(n1+k) by A15,Th82;
consider n2 being Nat such that
A19: for k holds r2-s/2 < seq2.(n2+k) by A16,A17,Th82;
for k holds r1+r2-s < (seq1+seq2).(n1+n2+k)
proof
let k;
r1-s/2 < seq1.(n1+(n2+k)) & r2-s/2 < seq2.(n2+(n1+k)) by A18,A19;
then (r1-s/2)+(r2-s/2) < seq1.(n1+n2+k) + seq2.(n1+n2+k) by XREAL_1:8;
hence thesis by SEQ_1:7;
end;
hence thesis;
end;
hence thesis by A15,A16,Th82;
end;
then
A20: lim_inf seq1 + lim_inf seq2 <= lim_inf (seq1+seq2) by A1;
A21: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf (seq1+
seq2) <= lim_inf seq1 + lim_sup seq2
proof
let seq1,seq2;
assume that
A22: seq1 is bounded and
A23: seq2 is bounded;
lim_inf ((seq1+seq2)+(-seq2)) >= lim_inf (seq1+seq2) + lim_inf (-
seq2) by A14,A22,A23;
then lim_inf (seq1+seq2+-seq2) >= lim_inf (seq1+seq2) +- lim_sup seq2 by
A23,Th90;
then lim_inf (seq1+seq2-seq2) >= lim_inf (seq1+seq2) - lim_sup seq2;
then lim_inf seq1 >= lim_inf (seq1+seq2) - lim_sup seq2 by Th2;
hence thesis by XREAL_1:20;
end;
then
A24: lim_inf (seq1+seq2) <= lim_sup seq1 + lim_inf seq2 by A1;
A25: lim_inf (seq1+seq2) <= lim_inf seq1 + lim_sup seq2 by A21,A1;
seq1 is convergent or seq2 is convergent implies lim_inf (seq1+seq2) =
lim_inf seq1 + lim_inf seq2 & lim_sup (seq1+seq2) = lim_sup seq1 + lim_sup seq2
proof
assume
A26: seq1 is convergent or seq2 is convergent;
per cases by A26;
suppose
seq1 is convergent;
then lim_inf seq1 = lim_sup seq1 by Th88;
hence thesis by A20,A24,A11,A13,XXREAL_0:1;
end;
suppose
seq2 is convergent;
then lim_inf seq2 = lim_sup seq2 by Th88;
hence thesis by A20,A25,A12,A13,XXREAL_0:1;
end;
end;
hence thesis by A14,A21,A2,A8,A1;
end;
theorem
seq1 is bounded nonnegative & seq2 is bounded nonnegative implies (
lim_inf seq1) * (lim_inf seq2) <= lim_inf(seq1(#)seq2) & lim_sup(seq1(#)seq2)
<= (lim_sup seq1) * (lim_sup seq2)
proof
A1: for seq1,seq2 st seq1 is bounded & seq1 is nonnegative & seq2 is
bounded & seq2 is nonnegative holds lim_sup(seq1(#)seq2) <= (lim_sup seq1) * (
lim_sup seq2)
proof
let seq1,seq2;
assume that
A2: seq1 is bounded nonnegative and
A3: seq2 is bounded nonnegative;
set seq3 = superior_realsequence seq1, seq4 = superior_realsequence seq2,
seq5 = superior_realsequence(seq1(#)seq2);
A4: seq5 is convergent by A2,A3,Th58;
A5: lower_bound seq5 = lim seq5 & lower_bound seq3 = lim seq3 by A2,A3,Th58;
A6: lower_bound seq4 =lim seq4 by A3,Th58;
A7: for n holds seq5.n <= (seq3(#)seq4).n
proof
let n;
seq5.n <= seq3.n * seq4.n by A2,A3,Th80;
hence thesis by SEQ_1:8;
end;
A8: seq3 is convergent & seq4 is convergent by A2,A3,Th58;
then (seq3(#)seq4) is convergent;
then lim seq5 <= lim (seq3(#)seq4) by A4,A7,SEQ_2:18;
hence thesis by A8,A5,A6,SEQ_2:15;
end;
for seq1,seq2 st seq1 is bounded nonnegative & seq2 is bounded
nonnegative holds (lim_inf seq1) * (lim_inf seq2) <= lim_inf(seq1(#)seq2)
proof
let seq1,seq2;
assume that
A9: seq1 is bounded nonnegative and
A10: seq2 is bounded nonnegative;
set seq3 = inferior_realsequence seq1, seq4 = inferior_realsequence seq2,
seq5 = inferior_realsequence(seq1(#)seq2);
A11: seq5 is convergent by A9,A10,Th57;
A12: upper_bound seq5 = lim seq5 & upper_bound seq3 = lim seq3 by A9,A10,Th57;
A13: upper_bound seq4 =lim seq4 by A10,Th57;
A14: for n holds seq5.n >= (seq3(#)seq4).n
proof
let n;
seq5.n >= seq3.n * seq4.n by A9,A10,Th79;
hence thesis by SEQ_1:8;
end;
A15: seq3 is convergent & seq4 is convergent by A9,A10,Th57;
then (seq3(#)seq4) is convergent;
then lim seq5 >= lim (seq3(#)seq4) by A11,A14,SEQ_2:18;
hence thesis by A15,A12,A13,SEQ_2:15;
end;
hence thesis by A1;
end;