:: Inferior Limit, Superior Limit and Convergence of Sequences of Extended
:: Real Numbers
:: by Hiroshi Yamazaki , Noboru Endou , Yasunari Shidama and Hiroyuki Okazaki
::
:: Received August 28, 2007
:: Copyright (c) 2007-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, XBOOLE_0, XXREAL_2, ORDINAL2, XXREAL_0, SEQ_4,
MESFUNC5, RELAT_1, FUNCT_1, RINFSUP1, VALUED_0, SEQ_1, ARYTM_3, TARSKI,
CARD_1, ARYTM_1, SEQ_2, COMPLEX1, NAT_1, REAL_1, MESFUNC1, SUPINF_2,
XCMPLX_0, SUPINF_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, MEMBERED,
XXREAL_3, XCMPLX_0, COMPLEX1, RELAT_1, FUNCT_1, REAL_1, XXREAL_0,
RELSET_1, FUNCT_2, NAT_1, XXREAL_2, SUPINF_1, VALUED_0, SUPINF_2, SEQ_1,
COMSEQ_2, SEQ_2, SEQ_4, RINFSUP1, MEASURE6, EXTREAL1, MESFUNC1, MESFUNC5;
constructors REAL_1, NAT_1, DOMAIN_1, EXTREAL1, COMPLEX1, MEASURE6, MESFUNC1,
PARTFUN3, LIMFUNC1, RINFSUP1, MESFUNC5, SUPINF_1, SEQ_4, RELSET_1,
BINOP_2, RVSUM_1, COMSEQ_2;
registrations SUBSET_1, RELSET_1, XREAL_0, MEMBERED, ORDINAL1, INT_1, NUMBERS,
XBOOLE_0, VALUED_0, SEQ_2, SEQ_4, XXREAL_3, FUNCT_2, NAT_1, VALUED_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, VALUED_0;
equalities RINFSUP1, XXREAL_3, SUPINF_2;
expansions TARSKI, VALUED_0;
theorems NAT_1, TARSKI, FUNCT_1, FUNCT_2, SUPINF_2, INT_1, EXTREAL1, SEQ_2,
SEQ_4, RINFSUP1, XREAL_0, XBOOLE_0, XREAL_1, XXREAL_0, ORDINAL1,
MESFUNC5, XXREAL_2, XXREAL_3;
schemes FUNCT_2;
begin :: Inferior limit, superior limit and convergence of sequence
:: of extended real numbers
reserve n,m,k,k1,k2 for Nat;
reserve X for non empty Subset of ExtREAL;
reserve Y for non empty Subset of REAL;
theorem Th1:
X = Y & Y is bounded_above implies X is bounded_above & sup X = upper_bound Y
proof
assume that
A1: X=Y and
A2: Y is bounded_above;
A3: for s be Real st s in Y holds s <= sup X by A1,XXREAL_2:4;
not -infty in X by A1;
then
A4: X <> {-infty} by TARSKI:def 1;
for r be ExtReal st r in X
holds r <= upper_bound Y by A1,A2,SEQ_4:def 1;
then
A5: upper_bound Y is UpperBound of X by XXREAL_2:def 1;
hence X is bounded_above by XXREAL_2:def 10;
then sup X in REAL by A4,XXREAL_2:57;
then
A6: upper_bound Y <= sup X by A3,SEQ_4:45;
sup X <= upper_bound Y by A5,XXREAL_2:def 3;
hence thesis by A6,XXREAL_0:1;
end;
theorem
X = Y & X is bounded_above implies Y is bounded_above & sup X = upper_bound Y
by Th1;
theorem Th3:
X = Y & Y is bounded_below implies X is bounded_below & inf X = lower_bound Y
proof
assume that
A1: X=Y and
A2: Y is bounded_below;
A3: for s be Real st s in Y holds inf X <= s by A1,XXREAL_2:3;
not +infty in X by A1;
then
A4: X <> {+infty} by TARSKI:def 1;
for r be ExtReal st r in X
holds lower_bound Y <= r by A1,A2,SEQ_4:def 2;
then
A5: lower_bound Y is LowerBound of X by XXREAL_2:def 2;
hence X is bounded_below by XXREAL_2:def 9;
then inf X in REAL by A4,XXREAL_2:58;
then
A6: inf X <= lower_bound Y by A3,SEQ_4:43;
lower_bound Y <= inf X by A5,XXREAL_2:def 4;
hence thesis by A6,XXREAL_0:1;
end;
theorem
X = Y & X is bounded_below implies Y is bounded_below & inf X = lower_bound Y
by Th3;
definition
let seq be ExtREAL_sequence;
func sup seq -> Element of ExtREAL equals
sup rng seq;
coherence;
func inf seq -> Element of ExtREAL equals
inf rng seq;
coherence;
end;
definition
let seq be ExtREAL_sequence;
attr seq is bounded_below means
rng seq is bounded_below;
attr seq is bounded_above means
rng seq is bounded_above;
end;
definition
let seq be ExtREAL_sequence;
attr seq is bounded means
seq is bounded_above & seq is bounded_below;
end;
reserve seq for ExtREAL_sequence;
theorem Th5:
for seq,n holds {seq.k: n <= k} is non empty Subset of ExtREAL
proof
let seq,n;
deffunc F(Nat) = seq.$1;
defpred P[Nat] means n <= $1;
set Y = {F(k): P[k]};
A1: seq.n in Y;
Y c= ExtREAL
proof let x be object;
assume x in Y;
then consider k such that
A2: F(k) = x and
P[k];
thus thesis by A2;
end;
hence thesis by A1;
end;
definition
let seq be ExtREAL_sequence;
func inferior_realsequence seq -> ExtREAL_sequence means
:Def6:
for n ex Y being non empty Subset of ExtREAL
st Y = {seq.k: n <= k} & it.n = inf Y;
existence
proof
defpred P[Nat, Element of ExtREAL] means ex Y being non empty
Subset of ExtREAL st Y = {seq.k: $1 <= k} & $2 = inf Y;
A1: for n being Element of NAT ex y being Element of ExtREAL st P[n,y]
proof
let n be Element of NAT;
reconsider Y={seq.k: n <= k} as non empty Subset of ExtREAL by Th5;
reconsider y = inf Y as Element of ExtREAL;
take y;
thus thesis;
end;
consider f being sequence of ExtREAL 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 ExtREAL_sequence such that
A3: for n ex Y being non empty Subset of ExtREAL st
Y = {seq.k: n <= k} & seq1.n = inf Y and
A4: for n ex Y being non empty Subset of ExtREAL st
Y = {seq.k: n <= k} & seq2.n = inf Y;
A5: for y be object st y in NAT holds seq1.y = seq2.y
proof
let y be object;
assume y in NAT;
then reconsider n=y as Element of NAT;
A6: ex Z be non empty Subset of ExtREAL
st Z = {seq.k: n <= k} & seq2.n=inf Z by A4;
ex Y be non empty Subset of ExtREAL
st Y = {seq.k: n <= k} & seq1.n=inf Y by A3;
hence thesis by A6;
end;
A7: NAT = dom seq2 by FUNCT_2:def 1;
NAT = dom seq1 by FUNCT_2:def 1;
hence thesis by A5,A7,FUNCT_1:2;
end;
end;
definition
let seq be ExtREAL_sequence;
func superior_realsequence seq -> ExtREAL_sequence means
:Def7:
for n ex Y being non empty Subset of ExtREAL
st Y = {seq.k where k: n <= k} & it.n = sup Y;
existence
proof
defpred P[Nat, Element of ExtREAL] means ex Y being non empty
Subset of ExtREAL st Y = {seq.k: $1 <= k} & $2 = sup Y;
A1: for n being Element of NAT ex y being Element of ExtREAL st P[n,y]
proof
let n be Element of NAT;
reconsider Y={seq.k: n <= k} as non empty Subset of ExtREAL by Th5;
reconsider y = sup Y as Element of ExtREAL;
take y;
thus thesis;
end;
consider f being sequence of ExtREAL 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 P[n, f.n] by A2;
end;
uniqueness
proof
let seq1,seq2 be ExtREAL_sequence such that
A3: for n ex Y being non empty Subset of ExtREAL st
Y = {seq.k: n <= k} & seq1.n = sup Y and
A4: for m ex Y being non empty Subset of ExtREAL st
Y = {seq.k: m <= k} & seq2.m = sup Y;
A5: for y be object st y in NAT holds seq1.y = seq2.y
proof
let y be object;
assume y in NAT;
then reconsider n=y as Element of NAT;
A6: ex Z be non empty Subset of ExtREAL
st Z = {seq.k : n <= k} & seq2.n=sup Z by A4;
ex Y be non empty Subset of ExtREAL
st Y = {seq.k: n <= k} & seq1.n=sup Y by A3;
hence thesis by A6;
end;
A7: NAT = dom seq2 by FUNCT_2:def 1;
NAT = dom seq1 by FUNCT_2:def 1;
hence thesis by A5,A7,FUNCT_1:2;
end;
end;
theorem
seq is real-valued implies seq is Real_Sequence
by FUNCT_2:6;
reserve e1,e2 for ExtReal;
theorem Th7:
(seq is increasing iff for n,m be Nat st m<n holds seq
.m<seq.n) & (seq is decreasing iff for n,m be Nat st m<n holds seq.n
<seq.m) & (seq is non-decreasing iff for n,m be Nat st m<=n holds
seq.m<=seq.n) & (seq is non-increasing iff
for n,m be Nat st m<=n holds seq.n<=seq.m)
proof
A1: dom seq = NAT by FUNCT_2:def 1;
thus seq is increasing implies for n,m be Nat st m<n holds seq.m<seq.n
proof assume
A2: seq is increasing;
let n,m be Nat;
n in NAT & m in NAT by ORDINAL1:def 12;
hence thesis by A2,A1;
end;
thus (for n,m be Nat st m<n holds seq.m<seq.n) implies seq is increasing;
thus seq is decreasing implies for n,m be Nat st m<n holds seq.m>seq.n
proof assume
A3: seq is decreasing;
let n,m be Nat;
n in NAT & m in NAT by ORDINAL1:def 12;
hence thesis by A3,A1;
end;
thus (for n,m be Nat st m<n holds seq.n <seq.m) implies seq is decreasing;
thus seq is non-decreasing implies for n,m be Nat st m<=n holds seq.m<=seq.n
proof assume
A4: seq is non-decreasing;
let n,m be Nat;
n in NAT & m in NAT by ORDINAL1:def 12;
hence thesis by A4,A1;
end;
thus (for n,m be Nat st m<=n holds seq.m<=seq.n)
implies seq is non-decreasing;
thus seq is non-increasing implies for n,m be Nat st m<=n holds seq.m>=seq.n
proof assume
A5: seq is non-increasing;
let n,m be Nat;
n in NAT & m in NAT by ORDINAL1:def 12;
hence thesis by A5,A1;
end;
assume
A6: for n,m be Nat st m<=n holds seq.n<=seq.m;
let e1,e2;
thus thesis by A6;
end;
theorem Th8:
(inferior_realsequence seq).n <= seq.n & seq.n <= (
superior_realsequence seq).n
proof
consider Y being non empty Subset of ExtREAL such that
A1: Y = {seq.k: n <= k} and
A2: (inferior_realsequence seq).n = inf Y by Def6;
A3: seq.n in Y by A1;
hence (inferior_realsequence seq).n <= seq.n by A2,XXREAL_2:3;
ex Z being non empty Subset of ExtREAL
st Z = {seq.k: n <= k} & (superior_realsequence seq).n = sup Z by Def7;
hence thesis by A1,A3,XXREAL_2:4;
end;
Lm1: superior_realsequence seq is non-increasing
proof
now
let n,m be Nat;
consider Y being non empty Subset of ExtREAL such that
A1: Y = {seq.k: m <= k} and
A2: (superior_realsequence seq).m = sup Y by Def7;
consider Z being non empty Subset of ExtREAL such that
A3: Z = {seq.k: n <= k} and
A4: (superior_realsequence seq).n = sup Z by Def7;
assume
A5: m<=n;
Z c= Y
proof
let z be object;
assume z in Z;
then consider k such that
A6: z=seq.k and
A7: n <= k by A3;
m <= k by A5,A7,XXREAL_0:2;
hence thesis by A1,A6;
end;
hence
(superior_realsequence seq).n <= (superior_realsequence seq).m by A2,A4,
XXREAL_2:59;
end;
hence thesis;
end;
Lm2: inferior_realsequence seq is non-decreasing
proof
now
let n,m be Nat;
consider Y being non empty Subset of ExtREAL such that
A1: Y = {seq.k: m <= k} and
A2: (inferior_realsequence seq).m = inf Y by Def6;
consider Z being non empty Subset of ExtREAL such that
A3: Z = {seq.k: n <= k} and
A4: (inferior_realsequence seq).n = inf Z by Def6;
assume
A5: m<=n;
Z c= Y
proof
let z be object;
assume z in Z;
then consider k such that
A6: z=seq.k and
A7: n <= k by A3;
m <= k by A5,A7,XXREAL_0:2;
hence thesis by A1,A6;
end;
hence
(inferior_realsequence seq).m <= (inferior_realsequence seq).n by A2,A4,
XXREAL_2:60;
end;
hence thesis;
end;
registration
let seq;
cluster superior_realsequence seq -> non-increasing;
coherence by Lm1;
cluster inferior_realsequence seq -> non-decreasing;
coherence by Lm2;
end;
definition
let seq be ExtREAL_sequence;
func lim_sup seq -> Element of ExtREAL equals
inf superior_realsequence seq;
coherence;
func lim_inf seq -> Element of ExtREAL equals
sup inferior_realsequence seq;
coherence;
end;
reserve rseq for Real_Sequence;
theorem Th9:
seq = rseq & rseq is bounded implies superior_realsequence seq =
superior_realsequence rseq & lim_sup seq = lim_sup rseq
proof
assume that
A1: seq=rseq and
A2: rseq is bounded;
A3: NAT = dom superior_realsequence rseq by FUNCT_2:def 1;
A4: now
let x be object;
assume x in NAT;
then reconsider n = x as Element of NAT;
now
let x be object;
assume x in {rseq.k: n <= k};
then ex k st x=rseq.k & n<= k;
hence x in REAL by XREAL_0:def 1;
end;
then reconsider
Y2={rseq.k: n <= k} as Subset of REAL by TARSKI:def 3;
A5: Y2 is bounded_above by A2,RINFSUP1:31;
ex Y1 being non empty Subset of ExtREAL st Y1
= {seq.k: n <= k} & (superior_realsequence seq).n = sup Y1 by Def7;
then (superior_realsequence seq).x =upper_bound Y2 by A1,A5,Th1;
hence (superior_realsequence seq).x =(superior_realsequence rseq).x by
RINFSUP1:def 5;
end;
superior_realsequence rseq is bounded by A2,RINFSUP1:56;
then
A6: rng superior_realsequence rseq is bounded_below by RINFSUP1:6;
NAT = dom superior_realsequence seq by FUNCT_2:def 1;
then superior_realsequence seq = superior_realsequence rseq by A4,A3,
FUNCT_1:2;
hence thesis by A6,Th3;
end;
theorem Th10:
seq = rseq & rseq is bounded implies inferior_realsequence seq =
inferior_realsequence rseq & lim_inf seq=lim_inf rseq
proof
assume that
A1: seq=rseq and
A2: rseq is bounded;
A3: NAT = dom (inferior_realsequence rseq) by FUNCT_2:def 1;
A4: now
let x be object;
assume x in NAT;
then reconsider n = x as Element of NAT;
consider Y1 being non empty Subset of ExtREAL such that
A5: Y1 = {seq.k: n <= k} and
A6: (inferior_realsequence seq).n = inf Y1 by Def6;
now
let x be object;
assume x in {rseq.k: n <= k};
then ex k st x=rseq.k & n<= k;
hence x in REAL by XREAL_0:def 1;
end;
then reconsider
Y2={rseq.k: n <= k} as Subset of REAL by TARSKI:def 3;
Y2 is bounded_below by A2,RINFSUP1:32;
then inf Y1= lower_bound Y2 by A1,A5,Th3;
hence
(inferior_realsequence seq).x = (inferior_realsequence rseq).x by A6,
RINFSUP1:def 4;
end;
inferior_realsequence rseq is bounded by A2,RINFSUP1:56;
then
A7: rng inferior_realsequence rseq is bounded_above by RINFSUP1:5;
NAT = dom (inferior_realsequence seq) by FUNCT_2:def 1;
then inferior_realsequence seq = inferior_realsequence rseq by A4,A3,
FUNCT_1:2;
hence thesis by A7,Th1;
end;
theorem Th11:
seq is bounded implies seq is Real_Sequence
proof
assume
A1: seq is bounded;
then seq is bounded_below;
then rng seq is bounded_below;
then consider UL being Real such that
A2: UL is LowerBound of rng seq by XXREAL_2:def 9;
A3: UL in REAL by XREAL_0:def 1;
seq is bounded_above by A1;
then rng seq is bounded_above;
then consider UB being Real such that
A4: UB is UpperBound of rng seq by XXREAL_2:def 10;
A5: UB in REAL by XREAL_0:def 1;
A6: now
let x be object;
assume x in NAT;
then
A7: seq.x in rng seq by FUNCT_2:4;
then
A8: seq.x <> -infty by A2,A3,XXREAL_0:12,XXREAL_2:def 2;
seq.x <> +infty by A5,A4,A7,XXREAL_0:9,XXREAL_2:def 1;
hence seq.x in REAL by A8,XXREAL_0:14;
end;
dom seq =NAT by FUNCT_2:def 1;
hence thesis by A6,FUNCT_2:3;
end;
theorem Th12:
seq = rseq implies (seq is bounded_above iff rseq is bounded_above)
proof
assume
A1: seq=rseq;
hereby
assume seq is bounded_above;
then rng rseq is bounded_above by A1;
then consider p be Real such that
A2: p is UpperBound of rng rseq by XXREAL_2:def 10;
A3: for y be Real st y in rng rseq holds y <= p by A2,XXREAL_2:def 1;
now
let n be Nat;
n in NAT by ORDINAL1:def 12;
then rseq.n in rng rseq by FUNCT_2:4;
then 0 + rseq.n < 1+ p by A3,XREAL_1:8;
hence rseq.n < p+1;
end;
hence rseq is bounded_above by SEQ_2:def 3;
end;
assume rseq is bounded_above;
then consider q be Real such that
A4: for n be Nat holds rseq.n < q by SEQ_2:def 3;
now
let r be ExtReal;
assume r in rng seq;
then ex x be object st x in dom rseq & r=rseq.x by A1,FUNCT_1:def 3;
hence r <= q by A4;
end;
then q is UpperBound of rng seq by XXREAL_2:def 1;
hence rng seq is bounded_above by XXREAL_2:def 10;
end;
theorem Th13:
seq = rseq implies (seq is bounded_below iff rseq is bounded_below)
proof
assume
A1: seq=rseq;
hereby
assume seq is bounded_below;
then rng rseq is bounded_below by A1;
then consider p be Real such that
A2: p is LowerBound of rng rseq by XXREAL_2:def 9;
A3: for y be Real st y in rng rseq holds p <= y by A2,XXREAL_2:def 2;
now
let n be Nat;
n in NAT by ORDINAL1:def 12;
then rseq.n in rng rseq by FUNCT_2:4;
then p-1 < rseq.n - 0 by A3,XREAL_1:15;
hence p-1 <rseq.n;
end;
hence rseq is bounded_below by SEQ_2:def 4;
end;
assume rseq is bounded_below;
then consider q be Real such that
A4: for n be Nat holds q < rseq.n by SEQ_2:def 4;
now
let r be ExtReal;
assume r in rng seq;
then ex x be object st x in dom rseq & r = rseq.x by A1,FUNCT_1:def 3;
hence q<=r by A4;
end;
then q is LowerBound of rng seq by XXREAL_2:def 2;
hence rng seq is bounded_below by XXREAL_2:def 9;
end;
theorem Th14:
seq=rseq & rseq is convergent implies seq is
convergent_to_finite_number & seq is convergent & lim seq = lim rseq
proof
assume that
A1: seq = rseq and
A2: rseq is convergent;
reconsider lrs = lim rseq as R_eal by XXREAL_0:def 1;
A3: now
let e be Real;
assume 0 < e;
then consider n be Nat such that
A4: for m be Nat st n <= m holds |.rseq.m-lim rseq qua Complex.| < e
by A2,SEQ_2:def 7;
set N=n;
now
let m be Nat;
A5: rseq.m - lim rseq = seq.m - lim rseq by A1,SUPINF_2:3;
assume N <= m;
then |.rseq.m-lim rseq qua Complex.| < e by A4;
hence |. seq.m - lim rseq .| < e by A5,EXTREAL1:12;
end;
hence
ex N be Nat st for m be Nat st N <= m
holds |. seq.m - lrs .| < e;
end;
then
A6: seq is convergent_to_finite_number by MESFUNC5:def 8;
then seq is convergent by MESFUNC5:def 11;
hence thesis by A3,A6,MESFUNC5:def 12;
end;
theorem Th15:
seq=rseq & seq is convergent_to_finite_number implies rseq is
convergent & lim seq = lim rseq
proof
assume that
A1: seq=rseq and
A2: seq is convergent_to_finite_number;
A3: not (lim seq = +infty & seq is convergent_to_+infty) by A2,MESFUNC5:50;
A4: not (lim seq = -infty & seq is convergent_to_-infty) by A2,MESFUNC5:51;
seq is convergent by A2,MESFUNC5:def 11;
then consider g be Real such that
A5: lim seq = g and
A6: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |.seq.m-lim seq.| < p and
seq is convergent_to_finite_number by A3,A4,MESFUNC5:def 12;
A7: for p be Real st 0<p
ex n st for m st n<=m holds |.rseq.m-g qua Complex.| < p
proof
let p be Real;
assume 0 < p;
then consider n be Nat such that
A8: for m be Nat st n <= m holds |.seq.m-lim seq .| < p by A6;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
take N;
hereby
let m be Nat;
assume N <= m;
then
A9: |.seq.m-lim seq .| < p by A8;
rseq.m - g = seq.m - lim seq by A1,A5,SUPINF_2:3;
hence |.rseq.m - g qua Complex.| < p by A9,EXTREAL1:12;
end;
end;
then rseq is convergent by SEQ_2:def 6;
hence thesis by A5,A7,SEQ_2:def 7;
end;
theorem Th16:
seq^\k is convergent_to_finite_number implies seq is
convergent_to_finite_number & seq is convergent & lim seq = lim(seq^\k)
proof
set seq0=seq^\k;
assume
A1: seq^\k is convergent_to_finite_number;
then
A2: not(lim seq0 = +infty & seq0 is convergent_to_+infty) by MESFUNC5:50;
A3: not(lim seq0 = -infty & seq0 is convergent_to_-infty) by A1,MESFUNC5:51;
seq0 is convergent by A1,MESFUNC5:def 11;
then
A4: ex g be Real st lim seq0 = g & (for p be Real st 0<p ex n
be Nat st for m be Nat st n<=m holds |.seq0.m-lim seq0 .| < p) & seq0 is
convergent_to_finite_number by A2,A3,MESFUNC5:def 12;
then consider g be Real such that
A5: lim seq0 = g;
A6: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m holds |.
seq.m-lim seq0 .| < p
proof
let p be Real;
assume 0 < p;
then consider n be Nat such that
A7: for m be Nat st n<=m holds |.seq0.m-lim seq0 .| < p by A4;
take n1 = n+k;
hereby
let m be Nat;
assume
A8: n1 <= m;
k <= n+k by NAT_1:11;
then reconsider mk = m-k as Element of NAT by A8,INT_1:5,XXREAL_0:2;
A9: seq0.(m-k) = seq.(mk+k) by NAT_1:def 3;
n+k-k <= m-k by A8,XREAL_1:9;
hence |.seq.m -lim seq0 .| < p by A7,A9;
end;
end;
lim seq0 = g by A5;
hence
A10: seq is convergent_to_finite_number by A6,MESFUNC5:def 8;
hence seq is convergent by MESFUNC5:def 11;
hence thesis by A5,A6,A10,MESFUNC5:def 12;
end;
theorem Th17:
seq^\k is convergent implies seq is convergent & lim seq = lim( seq^\k)
proof
set seq0=seq^\k;
assume
A1: seq^\k is convergent;
per cases by A1,MESFUNC5:def 11;
suppose
seq0 is convergent_to_finite_number;
hence thesis by Th16;
end;
suppose
A2: seq0 is convergent_to_+infty;
for g be Real st 0 < g ex n be Nat st for m be Nat st n<=m
holds g <= seq.m
proof
let g be Real;
assume 0<g;
then consider n be Nat such that
A3: for m be Nat st n<=m holds g <= seq0.m by A2,MESFUNC5:def 9;
take n1=n+k;
hereby
let m be Nat;
assume
A4: n1 <= m;
k <= n+k by NAT_1:11;
then reconsider mk = m-k as Element of NAT by A4,INT_1:5,XXREAL_0:2;
A5: seq0.(m-k) = seq.(mk+k) by NAT_1:def 3;
n+k-k <= m-k by A4,XREAL_1:9;
hence g <= seq.m by A3,A5;
end;
end;
then
A6: seq is convergent_to_+infty by MESFUNC5:def 9;
hence
A7: seq is convergent by MESFUNC5:def 11;
lim seq0 = +infty by A1,A2,MESFUNC5:def 12;
hence thesis by A6,A7,MESFUNC5:def 12;
end;
suppose
A8: seq0 is convergent_to_-infty;
for g be Real st g<0 ex n be Nat st for m be Nat st n<=m holds
seq.m <= g
proof
let g be Real;
assume g < 0;
then consider n be Nat such that
A9: for m be Nat st n<=m holds seq0.m <= g by A8,MESFUNC5:def 10;
take n1=n+k;
hereby
let m be Nat;
assume
A10: n1 <= m;
k <= n+k by NAT_1:11;
then reconsider mk = m-k as Element of NAT by A10,INT_1:5,XXREAL_0:2;
A11: seq0.(m-k) = seq.(mk+k) by NAT_1:def 3;
n+k-k <= m-k by A10,XREAL_1:9;
hence seq.m <= g by A9,A11;
end;
end;
then
A12: seq is convergent_to_-infty by MESFUNC5:def 10;
hence
A13: seq is convergent by MESFUNC5:def 11;
lim seq0=-infty by A1,A8,MESFUNC5:def 12;
hence thesis by A12,A13,MESFUNC5:def 12;
end;
end;
theorem Th18:
lim_sup seq = lim_inf seq & lim_inf seq in REAL implies ex k st
seq^\k is bounded
proof
assume that
A1: lim_sup seq = lim_inf seq and
A2: lim_inf seq in REAL;
reconsider a=lim_inf seq as Real by A2;
set K1=a+1;
ex k1 be Element of NAT st (superior_realsequence seq).k1 <= K1
proof
assume
A3: not ex k1 be Element of NAT st (superior_realsequence seq).k1 <= K1;
now
let x be ExtReal;
assume x in rng (superior_realsequence seq);
then ex n be object st n in dom (superior_realsequence seq) & x = (
superior_realsequence seq).n by FUNCT_1:def 3;
hence K1 <= x by A3;
end;
then K1 is LowerBound of rng superior_realsequence seq by XXREAL_2:def 2;
then a+1 <= a by A1,XXREAL_2:def 4;
hence contradiction by XREAL_1:29;
end;
then consider k1 be Element of NAT such that
A4: (superior_realsequence seq).k1 <= K1;
set K2=a-1;
ex k2 be Element of NAT st K2 <= (inferior_realsequence seq).k2
proof
assume
A5: not (ex k2 be Element of NAT st K2 <= (inferior_realsequence seq) .k2);
now
let x be ExtReal;
assume x in rng (inferior_realsequence seq);
then ex n be object st n in dom inferior_realsequence seq & x = (
inferior_realsequence seq).n by FUNCT_1:def 3;
hence x <= K2 by A5;
end;
then K2 is UpperBound of rng inferior_realsequence seq by XXREAL_2:def 1;
then a <= a-1 by XXREAL_2:def 3;
then a+0 < a-1+1 by XREAL_1:8;
hence contradiction;
end;
then consider k2 be Element of NAT such that
A6: K2 <= (inferior_realsequence seq).k2;
take k=max(k1,k2);
k2<=k by XXREAL_0:25;
then (inferior_realsequence seq).k2 <= (inferior_realsequence seq).k by Th7;
then
A7: K2<=(inferior_realsequence seq).k by A6,XXREAL_0:2;
k1<=k by XXREAL_0:25;
then (superior_realsequence seq).k <= (superior_realsequence seq).k1 by Th7;
then
A8: (superior_realsequence seq).k <= K1 by A4,XXREAL_0:2;
A9: for n be Element of NAT st k <=n holds seq.n <= K1 & K2 <= seq.n
proof
let n be Element of NAT;
A10: (inferior_realsequence seq).n <= seq.n by Th8;
assume
A11: k <= n;
then
(superior_realsequence seq).n <= (superior_realsequence seq).k by Th7;
then
A12: (superior_realsequence seq).n <= K1 by A8,XXREAL_0:2;
(inferior_realsequence seq).k <= (inferior_realsequence seq).n by A11,Th7;
then
A13: K2<= (inferior_realsequence seq).n by A7,XXREAL_0:2;
seq.n <= (superior_realsequence seq).n by Th8;
hence thesis by A12,A13,A10,XXREAL_0:2;
end;
now
let x be ExtReal;
assume x in rng (seq^\k);
then consider n be object such that
A14: n in dom (seq^\k) and
A15: x=(seq^\k).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A14;
A16: k <= n+k by NAT_1:11;
x=seq.(n+k) by A15,NAT_1:def 3;
hence x <= K1 by A9,A16;
end;
then K1 is UpperBound of rng (seq^\k) by XXREAL_2:def 1;
hence rng (seq^\k) is bounded_above by XXREAL_2:def 10;
now
let x be ExtReal;
assume x in rng(seq^\k);
then consider n be object such that
A17: n in dom(seq^\k) and
A18: x = (seq^\k).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A17;
A19: k <= n+k by NAT_1:11;
x=seq.(n+k) by A18,NAT_1:def 3;
hence K2 <= x by A9,A19;
end;
then K2 is LowerBound of rng (seq^\k) by XXREAL_2:def 2;
hence rng (seq^\k) is bounded_below by XXREAL_2:def 9;
end;
theorem Th19:
seq is convergent_to_finite_number implies ex k st seq^\k is bounded
proof
assume
A1: seq is convergent_to_finite_number;
then
A2: not (lim seq = +infty & seq is convergent_to_+infty) by MESFUNC5:50;
A3: not (lim seq = -infty & seq is convergent_to_-infty) by A1,MESFUNC5:51;
seq is convergent by A1,MESFUNC5:def 11;
then
A4: ex g be Real st lim seq =g & (for p be Real st 0<p ex n be
Nat st for m be Nat st n<=m holds |.seq.m-lim seq .| < p) & seq is
convergent_to_finite_number by A2,A3,MESFUNC5:def 12;
then consider g be Real such that
A5: lim seq = g;
reconsider jj=1 as Real;
set UB = g+jj;
consider k be Nat such that
A6: for m be Nat st k<=m holds |.seq.m-lim seq .| < 1 by A4;
reconsider K = k as Element of NAT by ORDINAL1:def 12;
take K;
now
let r be ExtReal;
assume r in rng (seq^\K);
then consider n be object such that
A7: n in dom(seq^\K) and
A8: r=(seq^\K).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A7;
|.seq.(n+k)-lim seq .| <= 1. by A6,NAT_1:11;
then seq.(n+k)-lim seq <= 1. by EXTREAL1:23;
then seq.(n+k)+-lim seq +lim seq <= 1. +lim seq by XXREAL_3:36;
then seq.(n+k)+(-lim seq +lim seq) <= 1. +lim seq by A5,XXREAL_3:29;
then seq.(n+k)+0. <= 1. +lim seq by XXREAL_3:7;
then seq.(n+k) <= 1. +lim seq by XXREAL_3:4;
then seq.(n+k) <= UB by A5,SUPINF_2:1;
hence r <= UB by A8,NAT_1:def 3;
end;
then UB is UpperBound of rng(seq^\K) by XXREAL_2:def 1;
hence rng (seq^\K) is bounded_above by XXREAL_2:def 10;
set UL = g-1;
now
let r be ExtReal;
assume r in rng (seq^\K);
then consider n be object such that
A9: n in dom (seq^\K) and
A10: r=(seq^\K).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A9;
|.seq.(n+k)-lim seq .| < 1 by A6,NAT_1:11;
then -1. <=seq.(n+k)-lim seq by EXTREAL1:23;
then -1. +lim seq <= seq.(n+k)+-lim seq +lim seq by XXREAL_3:36;
then -1. +lim seq <= seq.(n+k)+(-lim seq +lim seq) by A5,XXREAL_3:29;
then
A11: -1. +lim seq <= seq.(n+k)+0. by XXREAL_3:7;
-1.= -jj by SUPINF_2:2;
then -jj+ g = -1.+ lim seq by A5,SUPINF_2:1;
then UL <= seq.(n+k) by A11,XXREAL_3:4;
hence UL <= r by A10,NAT_1:def 3;
end;
then UL is LowerBound of rng (seq^\K) by XXREAL_2:def 2;
hence rng (seq^\K) is bounded_below by XXREAL_2:def 9;
end;
theorem Th20:
seq is convergent_to_finite_number implies seq^\k is
convergent_to_finite_number & seq^\k is convergent & lim seq = lim(seq^\k)
proof
set seq0=seq^\k;
assume
A1: seq is convergent_to_finite_number;
then
A2: not (lim seq = +infty & seq is convergent_to_+infty) by MESFUNC5:50;
A3: not (lim seq = -infty & seq is convergent_to_-infty) by A1,MESFUNC5:51;
seq is convergent by A1,MESFUNC5:def 11;
then
A4: ex g be Real st lim seq = g & (for p be Real st 0<p ex n
be Nat st for m be Nat st n<=m holds |.seq.m-lim seq .| < p ) & seq is
convergent_to_finite_number by A2,A3,MESFUNC5:def 12;
then consider g be Real such that
A5: lim seq = g;
A6: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m holds |.
seq0.m-lim seq .| < p
proof
let p be Real;
assume 0<p;
then consider n be Nat such that
A7: for m be Nat st n<=m holds |.seq.m-lim seq .| < p by A4;
take n;
hereby
let m be Nat such that
A8: n <= m;
m <= m+k by NAT_1:11;
then n <= m+k by A8,XXREAL_0:2;
then |.seq.(m+k) -lim seq .| < p by A7;
hence |.seq0.m -lim seq .| < p by NAT_1:def 3;
end;
end;
lim seq = g by A5;
hence
A9: seq0 is convergent_to_finite_number by A6,MESFUNC5:def 8;
hence seq0 is convergent by MESFUNC5:def 11;
hence thesis by A5,A6,A9,MESFUNC5:def 12;
end;
theorem
seq is convergent implies seq^\k is convergent & lim seq = lim(seq^\k)
proof
set seq0 = seq^\k;
assume
A1: seq is convergent;
per cases by A1,MESFUNC5:def 11;
suppose
seq is convergent_to_finite_number;
hence thesis by Th20;
end;
suppose
A2: seq is convergent_to_+infty;
for g be Real st 0 < g ex n be Nat st for m be Nat st n<=m
holds g <= seq0.m
proof
let g be Real;
assume 0<g;
then consider n be Nat such that
A3: for m be Nat st n <= m holds g <= seq.m by A2,MESFUNC5:def 9;
take n;
hereby
let m be Nat such that
A4: n <= m;
m <= m+k by NAT_1:11;
then n <= m+k by A4,XXREAL_0:2;
then g <=seq.(m+k) by A3;
hence g <= seq0.m by NAT_1:def 3;
end;
end;
then
A5: seq0 is convergent_to_+infty by MESFUNC5:def 9;
hence
A6: seq0 is convergent by MESFUNC5:def 11;
lim seq = +infty by A1,A2,MESFUNC5:def 12;
hence thesis by A5,A6,MESFUNC5:def 12;
end;
suppose
A7: seq is convergent_to_-infty;
for g be Real st g < 0 ex n be Nat st for m be Nat st n <= m
holds seq0.m <= g
proof
let g be Real;
assume g < 0;
then consider n be Nat such that
A8: for m be Nat st n <= m holds seq.m <= g by A7,MESFUNC5:def 10;
take n;
hereby
let m be Nat such that
A9: n <= m;
m <= m+k by NAT_1:11;
then n <= m+k by A9,XXREAL_0:2;
then seq.(m+k) <= g by A8;
hence seq0.m <= g by NAT_1:def 3;
end;
end;
then
A10: seq0 is convergent_to_-infty by MESFUNC5:def 10;
hence
A11: seq0 is convergent by MESFUNC5:def 11;
lim seq = -infty by A1,A7,MESFUNC5:def 12;
hence thesis by A10,A11,MESFUNC5:def 12;
end;
end;
theorem
(seq is bounded_above implies seq^\k is bounded_above) & (seq is
bounded_below implies seq^\k is bounded_below)
proof
hereby
assume seq is bounded_above;
then rng seq is bounded_above;
then consider UB being Real such that
A1: UB is UpperBound of rng seq by XXREAL_2:def 10;
now
let r be ExtReal;
assume r in rng (seq^\k);
then consider n be object such that
A2: n in dom (seq^\k) and
A3: r = (seq^\k).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A2;
n+k in NAT by ORDINAL1:def 12;
then seq.(n+k) <= UB by A1,FUNCT_2:4,XXREAL_2:def 1;
hence r <= UB by A3,NAT_1:def 3;
end;
then UB is UpperBound of rng (seq^\k) by XXREAL_2:def 1;
then rng (seq^\k) is bounded_above by XXREAL_2:def 10;
hence seq^\k is bounded_above;
end;
hereby
assume seq is bounded_below;
then rng seq is bounded_below;
then consider UB being Real such that
A4: UB is LowerBound of rng seq by XXREAL_2:def 9;
now
let r be ExtReal;
assume r in rng (seq^\k);
then consider n be object such that
A5: n in dom (seq^\k) and
A6: r=(seq^\k).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A5;
n+k in NAT by ORDINAL1:def 12;
then seq.(n+k) in rng seq by FUNCT_2:4;
then UB <= seq.(n+k) by A4,XXREAL_2:def 2;
hence UB <= r by A6,NAT_1:def 3;
end;
then UB is LowerBound of rng (seq^\k) by XXREAL_2:def 2;
then rng (seq^\k) is bounded_below by XXREAL_2:def 9;
hence seq^\k is bounded_below;
end;
end;
theorem Th23:
inf seq <= seq.n & seq.n <= sup seq
proof
A1: inf rng seq is LowerBound of rng seq by XXREAL_2:def 4;
A2: sup rng seq is UpperBound of rng seq by XXREAL_2:def 3;
n in NAT by ORDINAL1:def 12;
then seq.n in rng seq by FUNCT_2:4;
hence thesis by A1,A2,XXREAL_2:def 1,def 2;
end;
theorem Th24:
inf seq <= sup seq
proof
A1: seq.0 <= sup seq by Th23;
inf seq <= seq.0 by Th23;
hence thesis by A1,XXREAL_0:2;
end;
theorem Th25:
seq is non-increasing implies seq^\k is non-increasing & inf seq
= inf(seq^\k)
proof
set seq0 = seq^\k;
assume
A1: seq is non-increasing;
now
let n,m be Nat;
assume m<=n;
then k+m <= k+n by XREAL_1:6;
then seq.(k+n) <=seq.(k+m) by A1,Th7;
then seq0.n <= seq.(k+m) by NAT_1:def 3;
hence seq0.n <= seq0.m by NAT_1:def 3;
end;
hence seq^\k is non-increasing;
now
let y be ExtReal;
assume y in rng seq;
then consider n be object such that
A2: n in dom seq and
A3: y=seq.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A2;
seq0.n = seq.(n+k) by NAT_1:def 3;
then
A4: inf seq0 <= seq.(n+k) by Th23;
n <= n+k by NAT_1:11;
then seq.(n+k) <= seq.n by A1,Th7;
hence inf rng seq0 <= y by A3,A4,XXREAL_0:2;
end;
then inf rng seq0 is LowerBound of rng seq by XXREAL_2:def 2;
then
A5: inf rng seq0 <= inf rng seq by XXREAL_2:def 4;
now
let y be ExtReal;
assume y in rng seq0;
then consider n be object such that
A6: n in dom seq0 and
A7: y=seq0.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A6;
seq0.n= seq.(n+k) by NAT_1:def 3;
then inf seq <= seq0.n by Th23;
hence inf rng seq <= y by A7;
end;
then inf rng seq is LowerBound of rng seq0 by XXREAL_2:def 2;
then inf rng seq <= inf rng seq0 by XXREAL_2:def 4;
hence thesis by A5,XXREAL_0:1;
end;
theorem Th26:
seq is non-decreasing implies seq^\k is non-decreasing & sup seq
= sup(seq^\k)
proof
set seq0 = seq^\k;
assume
A1: seq is non-decreasing;
now
let n,m be Nat;
assume m <= n;
then k+m <= k+n by XREAL_1:6;
then seq.(k+m) <=seq.(k+n) by A1,Th7;
then seq0.m <= seq.(k+n) by NAT_1:def 3;
hence seq0.m <= seq0.n by NAT_1:def 3;
end;
hence seq^\k is non-decreasing;
now
let y be ExtReal;
assume y in rng seq;
then consider n be object such that
A2: n in dom seq and
A3: y=seq.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A2;
seq0.n= seq.(n+k) by NAT_1:def 3;
then
A4: seq.(n+k) <= sup seq0 by Th23;
n <=n+k by NAT_1:11;
then seq.n <= seq.(n+k) by A1,Th7;
hence y <= sup rng seq0 by A3,A4,XXREAL_0:2;
end;
then sup rng seq0 is UpperBound of rng seq by XXREAL_2:def 1;
then
A5: sup rng seq <= sup rng seq0 by XXREAL_2:def 3;
now
let y be ExtReal;
assume y in rng seq0;
then consider n be object such that
A6: n in dom seq0 and
A7: y=seq0.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A6;
seq0.n= seq.(n+k) by NAT_1:def 3;
then seq0.n <=sup seq by Th23;
hence y <= sup rng seq by A7;
end;
then sup rng seq is UpperBound of rng seq0 by XXREAL_2:def 1;
then sup rng seq0 <= sup rng seq by XXREAL_2:def 3;
hence thesis by A5,XXREAL_0:1;
end;
theorem
(superior_realsequence seq).n = sup(seq^\n) & (inferior_realsequence
seq).n = inf(seq^\n)
proof
set rseq=seq^\n;
A1: ex Z being non empty Subset of ExtREAL
st Z = {seq.k : n <= k} & (inferior_realsequence seq).n = inf Z by Def6;
now
let x be object;
assume x in {seq.k: n <= k};
then consider k be Nat such that
A2: x=seq.k and
A3: n <= k;
reconsider k1=k-n as Element of NAT by A3,INT_1:5;
x = seq.(n+k1) by A2;
then x = rseq.k1 by NAT_1:def 3;
hence x in rng rseq by FUNCT_2:4;
end;
then
A4: {seq.k: n <= k} c= rng rseq;
now
let x be object;
assume x in rng rseq;
then consider z be object such that
A5: z in dom rseq and
A6: x=rseq.z by FUNCT_1:def 3;
reconsider k0=z as Element of NAT by A5;
A7: n <=n+k0 by NAT_1:11;
x = seq.(n+k0) by A6,NAT_1:def 3;
hence x in {seq.k: n <= k} by A7;
end;
then
A8: rng rseq c= { seq.k: n <= k};
ex Y being non empty Subset of ExtREAL
st Y = {seq.k : n <= k} & (superior_realsequence seq).n = sup Y by Def7;
hence thesis by A1,A4,A8,XBOOLE_0:def 10;
end;
theorem Th28:
for seq be ExtREAL_sequence,j be Element of NAT holds
superior_realsequence (seq^\j) = (superior_realsequence seq)^\j & lim_sup (seq
^\j) = lim_sup seq
proof
let seq be ExtREAL_sequence,j be Element of NAT;
set rseq=seq^\j;
now
let n be Element of NAT;
A1: ex Y2 being non empty Subset of ExtREAL
st Y2 = {rseq.k : n <= k} & (superior_realsequence rseq).n = sup Y2
by Def7;
A2: ex Y3 being non empty Subset of ExtREAL
st Y3 = { seq.k: (j+n) <= k} & (superior_realsequence seq).(j+n) = sup Y3
by Def7;
now
let x be object;
assume x in {seq.k where k: j+n <= k};
then consider k be Nat such that
A3: x=seq.k and
A4: j+n <= k;
j <= j+n by NAT_1:11;
then reconsider k1=k-j as Element of NAT by A4,INT_1:5,XXREAL_0:2;
A5: x = seq.(j+k1) by A3;
j+n - j <= k - j by A4,XREAL_1:9;
hence x in {seq.(j+k2) where k2: n<= k2} by A5;
end;
then
A6: {seq.k where k: j+n <= k} c= {seq.(j+k) where k: n <= k};
now
let x be object;
assume x in {seq.(j+k) where k: n <= k};
then consider k be Nat such that
A7: x=seq.(j+k) and
A8: n <= k;
j+n <= j+k by A8,XREAL_1:6;
hence x in { seq.k1 where k1: j+n <= k1} by A7;
end;
then {seq.(j+k) where k: n <= k} c= {seq.k where k: j+n <= k};
then
A9: {seq.(j+k) where k: n <= k} = { seq.k where k: (j+n) <= k}
by A6,XBOOLE_0:def 10;
now
let x be object;
assume x in {seq.(j+k) where k: n <= k};
then consider k be Nat such that
A10: x=seq.(j+k) and
A11: n <= k;
x = rseq.k by A10,NAT_1:def 3;
hence x in { rseq.k1 where k1: n<= k1} by A11;
end;
then
A12: {seq.(j+k) where k: n <= k} c= {rseq.k where k: n <= k};
now
let x be object;
assume x in {rseq.k where k: n <= k};
then consider k be Nat such that
A13: x=rseq.k and
A14: n <= k;
x = seq.(j+k) by A13,NAT_1:def 3;
hence x in { seq.(j+k1) where k1: n <= k1} by A14;
end;
then {rseq.k where k: n <= k} c= { seq.(j+k) where k: n <= k};
then {rseq.k where k: n <= k} = {seq.(j+k) where k: n <= k}
by A12,XBOOLE_0:def 10;
hence (superior_realsequence rseq).n = ((superior_realsequence seq)^\j).n
by A1,A2,A9,NAT_1:def 3;
end;
then (superior_realsequence seq)^\j = superior_realsequence rseq by
FUNCT_2:63;
hence thesis by Th25;
end;
theorem Th29:
for seq be ExtREAL_sequence,j be Element of NAT holds
inferior_realsequence (seq^\j) = (inferior_realsequence seq)^\j & lim_inf (seq
^\j) = lim_inf seq
proof
let seq be ExtREAL_sequence,j be Element of NAT;
set rseq=seq^\j;
now
let n be Element of NAT;
A1: ex Y2 being non empty Subset of ExtREAL
st Y2 = {rseq.k : n <= k} & (inferior_realsequence rseq).n = inf Y2
by Def6;
A2: ex Y3 being non empty Subset of ExtREAL
st Y3 = { seq.k: (j+n) <= k} & (inferior_realsequence seq).(j+n) = inf Y3
by Def6;
now
let x be object;
assume x in {seq.k where k: j+n <= k};
then consider k be Nat such that
A3: x=seq.k and
A4: j+n <= k;
j <= j+n by NAT_1:11;
then reconsider k1=k-j as Element of NAT by A4,INT_1:5,XXREAL_0:2;
A5: x=seq.(j+k1) by A3;
j+n - j <=k - j by A4,XREAL_1:9;
hence x in { seq.(j+k2) where k2: n<= k2} by A5;
end;
then
A6: {seq.k where k: j+n <= k} c= {seq.(j+k) where k: n <= k};
now
let x be object;
assume x in {seq.(j+k) where k: n <= k};
then consider k be Nat such that
A7: x=seq.(j+k) and
A8: n <= k;
j+n <= j+k by A8,XREAL_1:6;
hence x in { seq.k1 where k1: j+n <= k1} by A7;
end;
then {seq.(j+k) where k: n <= k} c= {seq.k where k: j+n <= k};
then
A9: {seq.(j+k) where k: n <= k} = {seq.k where k: (j+n) <= k}
by A6,XBOOLE_0:def 10;
now
let x be object;
assume x in {seq.(j+k) where k: n <= k};
then consider k be Nat such that
A10: x=seq.(j+k) and
A11: n <= k;
x = rseq.k by A10,NAT_1:def 3;
hence x in { rseq.k1 where k1: n<= k1} by A11;
end;
then
A12: {seq.(j+k) where k: n <= k} c= {rseq.k where k: n <= k};
now
let x be object;
assume x in {rseq.k where k: n <= k};
then consider k be Nat such that
A13: x=rseq.k and
A14: n <= k;
x = seq.(j+k) by A13,NAT_1:def 3;
hence x in {seq.(j+k1) where k1: n <= k1} by A14;
end;
then {rseq.k where k: n <= k} c= {seq.(j+k) where k: n <= k};
then {rseq.k where k: n <= k} = {seq.(j+k) where k: n <= k}
by A12,XBOOLE_0:def 10;
hence (inferior_realsequence rseq).n = ((inferior_realsequence seq)^\j).n
by A1,A2,A9,NAT_1:def 3;
end;
then (inferior_realsequence seq)^\j = inferior_realsequence rseq by
FUNCT_2:63;
hence thesis by Th26;
end;
theorem Th30:
for seq be ExtREAL_sequence, k be Element of NAT st seq is
non-increasing & -infty < seq.k & seq.k < +infty holds seq^\k is bounded_above
& sup(seq^\k) = seq.k
proof
let seq be ExtREAL_sequence, k be Element of NAT;
assume that
A1: seq is non-increasing and
A2: -infty < seq.k and
A3: seq.k < +infty;
set seq0=seq^\k;
now
let y be ExtReal;
assume y in rng seq0;
then consider n be object such that
A4: n in dom seq0 and
A5: y=seq0.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A4;
k <= n+k by NAT_1:11;
then seq.(n+k) <= seq.k by A1,Th7;
hence y <= seq.k by A5,NAT_1:def 3;
end;
then
A6: seq.k is UpperBound of rng seq0 by XXREAL_2:def 1;
seq0.0= seq.(0+k) by NAT_1:def 3;
then
A7: seq.k in rng seq0 by FUNCT_2:4;
seq.k in REAL by A2,A3,XXREAL_0:14;
then rng seq0 is bounded_above by A6,XXREAL_2:def 10;
hence thesis by A6,A7,XXREAL_2:55;
end;
theorem Th31:
for seq be ExtREAL_sequence, k be Element of NAT st seq is
non-decreasing & -infty < seq.k & seq.k < +infty holds seq^\k is bounded_below
& inf (seq^\k) = seq.k
proof
let seq be ExtREAL_sequence, k be Element of NAT;
assume that
A1: seq is non-decreasing and
A2: -infty < seq.k and
A3: seq.k < +infty;
set seq0=seq^\k;
now
let y be ExtReal;
assume y in rng seq0;
then consider n be object such that
A4: n in dom seq0 and
A5: y=seq0.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A4;
k <= n+k by NAT_1:11;
then seq.k <= seq.(n+k) by A1,Th7;
hence seq.k <= y by A5,NAT_1:def 3;
end;
then
A6: seq.k is LowerBound of rng seq0 by XXREAL_2:def 2;
seq0.0 = seq.(0+k) by NAT_1:def 3;
then
A7: seq.k in rng seq0 by FUNCT_2:4;
seq.k in REAL by A2,A3,XXREAL_0:14;
then rng seq0 is bounded_below by A6,XXREAL_2:def 9;
hence thesis by A6,A7,XXREAL_2:56;
end;
Lm3: for seq be ExtREAL_sequence st seq is bounded & seq is non-increasing
holds seq is convergent_to_finite_number & seq is convergent & lim seq = inf
seq
proof
let seq be ExtREAL_sequence;
assume that
A1: seq is bounded and
A2: seq is non-increasing;
reconsider rseq=seq as Real_Sequence by A1,Th11;
A3: seq is bounded_below by A1;
then
A4: rseq is bounded_below by Th13;
then lim rseq = lim_sup rseq by A2,RINFSUP1:89;
then lim rseq = lower_bound rseq by A2,RINFSUP1:70;
then
A5: lim seq = lower_bound rseq by A2,A4,Th14;
rng seq is bounded_below by A3;
hence thesis by A2,A4,A5,Th3,Th14;
end;
Lm4: for seq be ExtREAL_sequence st seq is bounded & seq is non-decreasing
holds seq is convergent_to_finite_number & seq is convergent & lim seq = sup
seq
proof
let seq be ExtREAL_sequence;
assume that
A1: seq is bounded and
A2: seq is non-decreasing;
reconsider rseq = seq as Real_Sequence by A1,Th11;
A3: seq is bounded_above by A1;
then
A4: rseq is bounded_above by Th12;
then lim rseq = lim_inf rseq by A2,RINFSUP1:89;
then lim rseq = upper_bound rseq by A2,RINFSUP1:64;
then
A5: lim seq = upper_bound rseq by A2,A4,Th14;
rng seq is bounded_above by A3;
hence thesis by A2,A4,A5,Th1,Th14;
end;
theorem Th32:
for seq be ExtREAL_sequence st (for n be Element of NAT holds
+infty <= seq.n) holds seq is convergent_to_+infty
proof
let seq be ExtREAL_sequence;
assume
A1: for n be Element of NAT holds +infty <= seq.n;
now
let g be Real;
assume 0 < g;
now
let m be Nat;
assume 0 <= m;
m is Element of NAT by ORDINAL1:def 12;
then
A2: +infty <= seq.m by A1;
g <= +infty by XXREAL_0:3;
hence g <= seq.m by A2,XXREAL_0:2;
end;
hence ex n be Nat st for m be Nat st n <= m holds g <= seq.m;
end;
hence thesis by MESFUNC5:def 9;
end;
theorem Th33:
for seq be ExtREAL_sequence st (for n be Element of NAT holds
seq.n <= -infty) holds seq is convergent_to_-infty
proof
let seq be ExtREAL_sequence;
assume
A1: for n be Element of NAT holds seq.n <= -infty;
now
let g be Real;
assume g < 0;
now
let m be Nat;
assume 0 <= m;
m is Element of NAT by ORDINAL1:def 12;
then
A2: seq.m <= -infty by A1;
-infty <= g by XXREAL_0:5;
hence seq.m <= g by A2,XXREAL_0:2;
end;
hence ex n be Nat st for m be Nat st n <=m holds seq.m <= g;
end;
hence thesis by MESFUNC5:def 10;
end;
theorem Th34:
for seq be ExtREAL_sequence st seq is non-increasing & -infty =
inf seq holds seq is convergent_to_-infty & lim seq = -infty
proof
let seq be ExtREAL_sequence;
assume that
A1: seq is non-increasing and
A2: -infty = inf seq;
A3: seq is convergent_to_-infty
proof
assume not seq is convergent_to_-infty;
then consider g be Real such that
g < 0 and
A4: for n be Nat ex m be Nat st n<=m & g < seq.m by MESFUNC5:def 10;
for y be ExtReal st y in rng seq holds g <= y
proof
let y be ExtReal;
assume y in rng seq;
then consider n be object such that
A5: n in NAT and
A6: y=seq.n by FUNCT_2:11;
reconsider n as Element of NAT by A5;
consider m be Nat such that
A7: n<=m and
A8: g < seq.m by A4;
seq.m <= seq.n by A1,A7,Th7;
hence thesis by A6,A8,XXREAL_0:2;
end;
then g is LowerBound of rng seq by XXREAL_2:def 2;
then
A9: g <= inf rng seq by XXREAL_2:def 4;
g in REAL by XREAL_0:def 1;
hence contradiction by A2,A9,XXREAL_0:12;
end;
then seq is convergent by MESFUNC5:def 11;
hence thesis by A3,MESFUNC5:def 12;
end;
theorem Th35:
for seq be ExtREAL_sequence st seq is non-decreasing & +infty =
sup seq holds seq is convergent_to_+infty & lim seq = +infty
proof
let seq be ExtREAL_sequence;
assume that
A1: seq is non-decreasing and
A2: +infty = sup seq;
A3: seq is convergent_to_+infty
proof
assume not seq is convergent_to_+infty;
then consider g be Real such that
0 < g and
A4: for n be Nat ex m be Nat st n<=m & seq.m < g by MESFUNC5:def 9;
for y be ExtReal st y in rng seq holds y <= g
proof
let y be ExtReal;
assume y in rng seq;
then consider n be object such that
A5: n in NAT and
A6: y=seq.n by FUNCT_2:11;
reconsider n as Element of NAT by A5;
consider m be Nat such that
A7: n<=m and
A8: seq.m < g by A4;
seq.n <= seq.m by A1,A7,Th7;
hence thesis by A6,A8,XXREAL_0:2;
end;
then g is UpperBound of rng seq by XXREAL_2:def 1;
then
A9: sup rng seq <= g by XXREAL_2:def 3;
g in REAL by XREAL_0:def 1;
hence contradiction by A2,A9,XXREAL_0:9;
end;
then seq is convergent by MESFUNC5:def 11;
hence thesis by A3,MESFUNC5:def 12;
end;
theorem Th36:
for seq be ExtREAL_sequence st seq is non-increasing holds seq
is convergent & lim seq = inf seq
proof
let seq be ExtREAL_sequence;
assume
A1: seq is non-increasing;
per cases;
suppose
A2: for n be Element of NAT holds +infty <= seq.n;
now
let y be object;
assume y in {+infty};
then
A3: y=+infty by TARSKI:def 1;
now
assume
A4: not y in rng seq;
now
let n be Element of NAT;
n in NAT;
then n in dom seq by FUNCT_2:def 1;
then seq.n<>+infty by A3,A4,FUNCT_1:def 3;
hence contradiction by A2,XXREAL_0:4;
end;
hence contradiction;
end;
hence y in rng seq;
end;
then
A5: {+infty} c= rng seq;
A6: seq is convergent_to_+infty by A2,Th32;
hence
A7: seq is convergent by MESFUNC5:def 11;
now
let y be object;
assume y in rng seq;
then ex x be object st x in dom seq & seq.x=y by FUNCT_1:def 3;
then y = +infty by A2,XXREAL_0:4;
hence y in {+infty} by TARSKI:def 1;
end;
then rng seq c={+infty};
then rng seq = {+infty} by A5,XBOOLE_0:def 10;
then inf seq = +infty by XXREAL_2:13;
hence thesis by A6,A7,MESFUNC5:def 12;
end;
suppose
not (for n be Element of NAT holds +infty <= seq.n);
then consider k be Element of NAT such that
A8: seq.k < +infty;
per cases;
suppose
A9: -infty <> inf seq;
set seq0=seq^\k;
A10: inf seq = inf seq0 by A1,Th25;
A11: now
assume rng seq0 ={-infty};
then
A12: -infty in rng seq0 by TARSKI:def 1;
-infty is LowerBound of rng seq0 by XXREAL_2:42;
hence contradiction by A9,A10,A12,XXREAL_2:56;
end;
A13: inf seq0 <= sup seq0 by Th24;
A14: inf rng seq0 is LowerBound of rng seq0 by XXREAL_2:def 4;
inf seq <= seq.k by Th23;
then -infty < seq.k by A9,XXREAL_0:2,6;
then
A15: seq0 is bounded_above by A1,A8,Th30;
then rng seq0 is bounded_above;
then sup rng seq0 < +infty by A11,XXREAL_0:9,XXREAL_2:57;
then inf rng seq0 in REAL by A9,A10,A13,XXREAL_0:14;
then rng seq0 is bounded_below by A14,XXREAL_2:def 9;
then seq0 is bounded_below;
then
A16: seq0 is bounded by A15;
A17: seq0 is non-increasing by A1,Th25;
then
A18: lim seq0 = inf seq0 by A16,Lm3;
seq0 is convergent by A17,A16,Lm3;
hence thesis by A10,A18,Th17;
end;
suppose
A19: -infty = inf seq;
then seq is convergent_to_-infty by A1,Th34;
hence seq is convergent by MESFUNC5:def 11;
thus thesis by A1,A19,Th34;
end;
end;
end;
theorem Th37:
for seq be ExtREAL_sequence st seq is non-decreasing holds seq
is convergent & lim seq = sup seq
proof
let seq be ExtREAL_sequence;
assume
A1: seq is non-decreasing;
per cases;
suppose
A2: for n be Element of NAT holds seq.n <= -infty;
now
let y be object;
assume y in {-infty};
then
A3: y = -infty by TARSKI:def 1;
now
assume
A4: not y in rng seq;
now
let n be Element of NAT;
n in NAT;
then n in dom seq by FUNCT_2:def 1;
then seq.n <> -infty by A3,A4,FUNCT_1:def 3;
hence contradiction by A2,XXREAL_0:6;
end;
hence contradiction;
end;
hence y in rng seq;
end;
then
A5: {-infty} c= rng seq;
A6: seq is convergent_to_-infty by A2,Th33;
hence
A7: seq is convergent by MESFUNC5:def 11;
now
let y be object;
assume y in rng seq;
then ex x be object st x in dom seq & seq.x=y by FUNCT_1:def 3;
then y = -infty by A2,XXREAL_0:6;
hence y in {-infty} by TARSKI:def 1;
end;
then rng seq c={-infty};
then rng seq = {-infty} by A5,XBOOLE_0:def 10;
then sup seq = -infty by XXREAL_2:11;
hence thesis by A6,A7,MESFUNC5:def 12;
end;
suppose
not (for n be Element of NAT holds seq.n <= -infty);
then consider k be Element of NAT such that
A8: -infty < seq.k;
per cases;
suppose
A9: +infty <> sup seq;
set seq0=seq^\k;
A10: sup seq = sup seq0 by A1,Th26;
A11: now
assume rng seq0 ={+infty};
then
A12: +infty in rng seq0 by TARSKI:def 1;
+infty is UpperBound of rng seq0 by XXREAL_2:41;
hence contradiction by A9,A10,A12,XXREAL_2:55;
end;
A13: inf seq0 <= sup seq0 by Th24;
A14: sup rng seq0 is UpperBound of rng seq0 by XXREAL_2:def 3;
seq.k <= sup seq by Th23;
then seq.k < +infty by A9,XXREAL_0:2,4;
then
A15: seq0 is bounded_below by A1,A8,Th31;
then rng seq0 is bounded_below;
then -infty < inf rng seq0 by A11,XXREAL_0:12,XXREAL_2:58;
then sup rng seq0 in REAL by A9,A10,A13,XXREAL_0:14;
then rng seq0 is bounded_above by A14,XXREAL_2:def 10;
then seq0 is bounded_above;
then
A16: seq0 is bounded by A15;
A17: seq0 is non-decreasing by A1,Th26;
then
A18: lim seq0 = sup seq0 by A16,Lm4;
seq0 is convergent by A17,A16,Lm4;
hence thesis by A10,A18,Th17;
end;
suppose
A19: +infty = sup seq;
then seq is convergent_to_+infty by A1,Th35;
hence seq is convergent by MESFUNC5:def 11;
thus thesis by A1,A19,Th35;
end;
end;
end;
theorem Th38:
for seq1,seq2 be ExtREAL_sequence st seq1 is convergent & seq2
is convergent & (for n holds seq1.n <=seq2.n) holds lim seq1
<= lim seq2
proof
let seq1,seq2 be ExtREAL_sequence;
assume that
A1: seq1 is convergent and
A2: seq2 is convergent and
A3: for n holds seq1.n <=seq2.n;
per cases by A1,MESFUNC5:def 11;
suppose
A4: seq1 is convergent_to_finite_number;
A5: not seq2 is convergent_to_-infty
proof
assume
A6: seq2 is convergent_to_-infty;
now
let g be Real;
assume g < 0;
then consider n be Nat such that
A7: for m be Nat st n<=m holds seq2.m <= g by A6,MESFUNC5:def 10;
now
let m be Nat;
A8: seq1.m <= seq2.m by A3;
assume n <= m;
then seq2.m <= g by A7;
hence seq1.m <= g by A8,XXREAL_0:2;
end;
hence ex n be Nat st for m be Nat st n<=m holds seq1.m <= g;
end;
then seq1 is convergent_to_-infty by MESFUNC5:def 10;
hence contradiction by A4,MESFUNC5:51;
end;
per cases by A2,A5,MESFUNC5:def 11;
suppose
A9: seq2 is convergent_to_finite_number;
consider k1 be Nat such that
A10: seq1^\k1 is bounded by A4,Th19;
seq1^\k1 is bounded_above by A10;
then rng(seq1^\k1) is bounded_above;
then consider UB being Real such that
A11: UB is UpperBound of rng (seq1^\k1) by XXREAL_2:def 10;
consider k2 be Nat such that
A12: seq2^\k2 is bounded by A9,Th19;
reconsider k = max(k1,k2) as Element of NAT by ORDINAL1:def 12;
A13: lim seq2 = lim(seq2^\k) by A9,Th20;
A14: dom(seq1^\k1) = NAT by FUNCT_2:def 1;
now
reconsider k2=k-k1 as Element of NAT by INT_1:5,XXREAL_0:25;
let y be object;
assume y in rng (seq1^\k);
then consider n be object such that
A15: n in dom (seq1^\k) and
A16: (seq1^\k).n=y by FUNCT_1:def 3;
reconsider n as Element of NAT by A15;
y=seq1.(k+n) by A16,NAT_1:def 3;
then y = seq1.(k1 +(k2+n));
then y = (seq1^\k1).(k2+n) by NAT_1:def 3;
hence y in rng(seq1^\k1) by A14,FUNCT_1:def 3;
end;
then
A17: rng (seq1^\k) c=rng (seq1^\k1);
then UB is UpperBound of rng (seq1^\k) by A11,XXREAL_2:6;
then rng (seq1^\k)is bounded_above by XXREAL_2:def 10;
then
A18: seq1^\k is bounded_above;
seq1^\k1 is bounded_below by A10;
then rng(seq1^\k1) is bounded_below;
then consider LB being Real such that
A19: LB is LowerBound of rng (seq1^\k1) by XXREAL_2:def 9;
LB is LowerBound of rng (seq1^\k) by A17,A19,XXREAL_2:5;
then rng (seq1^\k)is bounded_below by XXREAL_2:def 9;
then seq1^\k is bounded_below;
then seq1^\k is bounded by A18;
then reconsider rseq1=seq1^\k as Real_Sequence by Th11;
seq2^\k2 is bounded_below by A12;
then rng(seq2^\k2)is bounded_below;
then consider LB being Real such that
A20: LB is LowerBound of rng(seq2^\k2) by XXREAL_2:def 9;
A21: lim seq1 = lim(seq1^\k) by A4,Th20;
seq2^\k2 is bounded_above by A12;
then rng(seq2^\k2) is bounded_above;
then consider UB being Real such that
A22: UB is UpperBound of rng (seq2^\k2) by XXREAL_2:def 10;
A23: dom(seq2^\k2) = NAT by FUNCT_2:def 1;
now
reconsider k3=k-k2 as Element of NAT by INT_1:5,XXREAL_0:25;
let y be object;
assume y in rng (seq2^\k);
then consider n be object such that
A24: n in dom (seq2^\k) and
A25: (seq2^\k).n=y by FUNCT_1:def 3;
reconsider n as Element of NAT by A24;
y=seq2.(k+n) by A25,NAT_1:def 3;
then y=seq2.(k2 +(k3+n));
then y=(seq2^\k2).(k3+n) by NAT_1:def 3;
hence y in rng(seq2^\k2) by A23,FUNCT_1:def 3;
end;
then
A26: rng (seq2^\k) c= rng (seq2^\k2);
then UB is UpperBound of rng (seq2^\k) by A22,XXREAL_2:6;
then rng (seq2^\k ) is bounded_above by XXREAL_2:def 10;
then
A27: seq2^\k is bounded_above;
LB is LowerBound of rng (seq2^\k) by A20,A26,XXREAL_2:5;
then rng (seq2^\k)is bounded_below by XXREAL_2:def 9;
then seq2^\k is bounded_below;
then seq2^\k is bounded by A27;
then reconsider rseq2=seq2^\k as Real_Sequence by Th11;
A28: seq2^\k is convergent_to_finite_number by A9,Th20;
then
A29: rseq2 is convergent by Th15;
A30: for n holds rseq1.n <= rseq2.n
proof
let n;
A31: (seq2^\k).n =seq2.(k+n) by NAT_1:def 3;
(seq1^\k).n =seq1.(k+n) by NAT_1:def 3;
hence thesis by A3,A31;
end;
A32: seq1^\k is convergent_to_finite_number by A4,Th20;
then
A33: lim(seq1^\k) = lim rseq1 by Th15;
A34: lim(seq2^\k) = lim rseq2 by A28,Th15;
rseq1 is convergent by A32,Th15;
hence thesis by A29,A33,A34,A30,A21,A13,SEQ_2:18;
end;
suppose
A35: seq2 is convergent_to_+infty;
then seq2 is convergent by MESFUNC5:def 11;
then lim seq2=+infty by A35,MESFUNC5:def 12;
hence thesis by XXREAL_0:3;
end;
end;
suppose
A36: seq1 is convergent_to_+infty;
now
let g be Real;
assume 0 < g;
then consider n be Nat such that
A37: for m be Nat st n<=m holds g <= seq1.m by A36,MESFUNC5:def 9;
now
let m be Nat;
A38: seq1.m <= seq2.m by A3;
assume n<=m;
then g <= seq1.m by A37;
hence g <= seq2.m by A38,XXREAL_0:2;
end;
hence ex n be Nat st for m be Nat st n<=m holds g <= seq2.m;
end;
then
A39: seq2 is convergent_to_+infty by MESFUNC5:def 9;
then seq2 is convergent by MESFUNC5:def 11;
then lim seq2=+infty by A39,MESFUNC5:def 12;
hence thesis by XXREAL_0:3;
end;
suppose
A40: seq1 is convergent_to_-infty;
then seq1 is convergent by MESFUNC5:def 11;
then lim seq1 = -infty by A40,MESFUNC5:def 12;
hence thesis by XXREAL_0:5;
end;
end;
theorem
for seq be ExtREAL_sequence holds lim_inf seq <= lim_sup seq
proof
let seq be ExtREAL_sequence;
A1: lim superior_realsequence seq = lim_sup seq by Th36;
A2: inferior_realsequence seq is convergent by Th37;
A3: now
let n be Nat;
A4: seq.n <= (superior_realsequence seq).n by Th8;
(inferior_realsequence seq).n <=seq.n by Th8;
hence (inferior_realsequence seq).n <= (superior_realsequence seq).n by A4,
XXREAL_0:2;
end;
A5: lim inferior_realsequence seq = lim_inf seq by Th37;
superior_realsequence seq is convergent by Th36;
hence thesis by A1,A2,A5,A3,Th38;
end;
Lm5: for seq be ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq =
+infty holds seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq
proof
let seq be ExtREAL_sequence;
assume that
A1: lim_inf seq = lim_sup seq and
A2: lim_inf seq = +infty;
A3: inferior_realsequence seq is convergent_to_+infty by A2,Th35;
now
let g be Real;
assume 0 < g;
then consider n be Nat such that
A4: for m be Nat st n<=m holds g <= (inferior_realsequence seq).m by A3,
MESFUNC5:def 9;
now
let m be Nat;
A5: (inferior_realsequence seq).m <= seq.m by Th8;
assume n<=m;
then g <= (inferior_realsequence seq).m by A4;
hence g <= seq.m by A5,XXREAL_0:2;
end;
hence ex n be Nat st for m be Nat st n<=m holds g <= seq.m;
end;
then
A6: seq is convergent_to_+infty by MESFUNC5:def 9;
then seq is convergent by MESFUNC5:def 11;
hence thesis by A1,A2,A6,MESFUNC5:def 12;
end;
Lm6: for seq be ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq =
-infty holds seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq
proof
let seq be ExtREAL_sequence;
assume that
A1: lim_inf seq = lim_sup seq and
A2: lim_inf seq = -infty;
A3: superior_realsequence seq is convergent_to_-infty by A1,A2,Th34;
now
let g be Real;
assume g < 0;
then consider n be Nat such that
A4: for m be Nat st n<=m holds (superior_realsequence seq).m <= g by A3,
MESFUNC5:def 10;
now
let m be Nat;
A5: seq.m <=(superior_realsequence seq).m by Th8;
assume n<=m;
then (superior_realsequence seq).m <= g by A4;
hence seq.m <= g by A5,XXREAL_0:2;
end;
hence ex n be Nat st for m be Nat st n<=m holds seq.m <= g;
end;
then
A6: seq is convergent_to_-infty by MESFUNC5:def 10;
then seq is convergent by MESFUNC5:def 11;
hence thesis by A1,A2,A6,MESFUNC5:def 12;
end;
Lm7: for seq be ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq in
REAL holds seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq
proof
let seq be ExtREAL_sequence;
assume that
A1: lim_inf seq = lim_sup seq and
A2: lim_inf seq in REAL;
consider k be Nat such that
A3: seq^\k is bounded by A1,A2,Th18;
reconsider rseq0=seq^\k as Real_Sequence by A3,Th11;
seq^\k is bounded_below by A3;
then
A4: rseq0 is bounded_below by Th13;
A5: k in NAT by ORDINAL1:def 12;
seq^\k is bounded_above by A3;
then
A6: rseq0 is bounded_above by Th12;
then lim_sup rseq0 = lim_sup (seq^\k) by A4,Th9;
then
A7: lim_sup rseq0 = lim_sup seq by Th28,A5;
lim_inf rseq0 = lim_inf (seq^\k) by A6,A4,Th10;
then
A8: lim_inf rseq0 = lim_inf seq by Th29,A5;
then
A9: rseq0 is convergent by A1,A6,A4,A7,RINFSUP1:88;
then
A10: lim rseq0 = lim_inf seq by A8,RINFSUP1:89;
A11: seq^\k is convergent by A9,Th14;
A12: lim rseq0 = lim (seq^\k) by A9,Th14;
lim rseq0 = lim_sup seq by A7,A9,RINFSUP1:89;
hence thesis by A10,A12,A11,Th17;
end;
theorem Th40:
for seq be ExtREAL_sequence holds seq is convergent iff lim_inf
seq = lim_sup seq
proof
let seq be ExtREAL_sequence;
set a=lim_inf seq;
thus seq is convergent implies lim_inf seq = lim_sup seq
proof
assume
A1: seq is convergent;
per cases by A1,MESFUNC5:def 11;
suppose
A2: seq is convergent_to_finite_number;
then consider k be Nat such that
A3: seq^\k is bounded by Th19;
reconsider rseq0=seq^\k as Real_Sequence by A3,Th11;
A4: k in NAT by ORDINAL1:def 12;
seq^\k is convergent_to_finite_number by A2,Th20;
then
A5: rseq0 is convergent by Th15;
then
A6: rseq0 is bounded;
then lim_sup rseq0 = lim_sup (seq^\k) by Th9;
then
A7: lim_sup rseq0 = lim_sup seq by Th28,A4;
lim_inf rseq0 = lim_inf (seq^\k) by A6,Th10;
then lim_inf rseq0 = lim_inf seq by Th29,A4;
hence thesis by A5,A7,RINFSUP1:88;
end;
suppose
A8: seq is convergent_to_-infty;
now
let g be Real;
assume g < 0;
then consider n be Nat such that
A9: for m be Nat st n<=m holds seq.m <= g by A8,MESFUNC5:def 10;
now
let m be Nat;
A10: (inferior_realsequence seq).m <= seq.m by Th8;
assume n<=m;
then seq.m <= g by A9;
hence (inferior_realsequence seq).m <= g by A10,XXREAL_0:2;
end;
hence ex n be Nat st for m be Nat st n<=m holds (inferior_realsequence
seq).m <= g;
end;
then
A11: inferior_realsequence seq is convergent_to_-infty by MESFUNC5:def 10;
then inferior_realsequence seq is convergent by MESFUNC5:def 11;
then lim inferior_realsequence seq = -infty by A11,MESFUNC5:def 12;
then
A12: lim_inf seq =-infty by Th37;
A13: superior_realsequence seq is convergent_to_-infty
proof
set iseq=superior_realsequence seq;
assume not iseq is convergent_to_-infty;
then consider g be Real such that
A14: g < 0 and
A15: for n be Nat ex m be Nat st n<=m & g < iseq.m by MESFUNC5:def 10;
consider N be Nat such that
A16: for m be Nat st N<=m holds seq.m <= g by A8,A14,MESFUNC5:def 10;
now
let m be Nat;
consider Y being non empty Subset of ExtREAL such that
A17: Y = {seq.k: m <= k} and
A18: (superior_realsequence seq).m = sup Y by Def7;
assume
A19: N <= m;
now
let x be ExtReal;
assume x in Y;
then consider k be Nat such that
A20: x=seq.k and
A21: m <= k by A17;
N <= k by A19,A21,XXREAL_0:2;
hence x <= g by A16,A20;
end;
then g is UpperBound of Y by XXREAL_2:def 1;
hence iseq.m <= g by A18,XXREAL_2:def 3;
end;
hence contradiction by A15;
end;
then superior_realsequence seq is convergent by MESFUNC5:def 11;
then lim superior_realsequence seq = -infty by A13,MESFUNC5:def 12;
hence thesis by A12,Th36;
end;
suppose
A22: seq is convergent_to_+infty;
now
let g be Real;
assume 0 < g;
then consider n be Nat such that
A23: for m be Nat st n<=m holds g <= seq.m by A22,MESFUNC5:def 9;
now
let m be Nat;
A24: seq.m <= (superior_realsequence seq).m by Th8;
assume n <= m;
then g <= seq.m by A23;
hence g <= (superior_realsequence seq).m by A24,XXREAL_0:2;
end;
hence ex n be Nat st for m be Nat st n<=m holds g <= (
superior_realsequence seq).m;
end;
then
A25: superior_realsequence seq is convergent_to_+infty by MESFUNC5:def 9;
then superior_realsequence seq is convergent by MESFUNC5:def 11;
then lim superior_realsequence seq = +infty by A25,MESFUNC5:def 12;
then
A26: lim_sup seq =+infty by Th36;
A27: inferior_realsequence seq is convergent_to_+infty
proof
set iseq=inferior_realsequence seq;
assume not iseq is convergent_to_+infty;
then consider g be Real such that
A28: 0 < g and
A29: for n be Nat ex m be Nat st n<=m & iseq.m < g by MESFUNC5:def 9;
consider N be Nat such that
A30: for m be Nat st N<=m holds g <= seq.m by A22,A28,MESFUNC5:def 9;
now
let m be Nat;
consider Y being non empty Subset of ExtREAL such that
A31: Y = {seq.k: m <= k} and
A32: (inferior_realsequence seq).m = inf Y by Def6;
assume
A33: N <= m;
now
let x be ExtReal;
assume x in Y;
then consider k be Nat such that
A34: x = seq.k and
A35: m <= k by A31;
N <= k by A33,A35,XXREAL_0:2;
hence g <= x by A30,A34;
end;
then g is LowerBound of Y by XXREAL_2:def 2;
hence g<=iseq.m by A32,XXREAL_2:def 4;
end;
hence contradiction by A29;
end;
then inferior_realsequence seq is convergent by MESFUNC5:def 11;
then lim inferior_realsequence seq = +infty by A27,MESFUNC5:def 12;
hence thesis by A26,Th37;
end;
end;
assume
A36: lim_inf seq = lim_sup seq;
per cases by XXREAL_0:14;
suppose
a in REAL;
hence thesis by A36,Lm7;
end;
suppose
a = +infty;
hence thesis by A36,Lm5;
end;
suppose
a = -infty;
hence thesis by A36,Lm6;
end;
end;
theorem
for seq be ExtREAL_sequence st seq is convergent holds lim seq =
lim_inf seq & lim seq = lim_sup seq
proof
let seq be ExtREAL_sequence;
set a = lim_inf seq;
assume seq is convergent;
then
A1: lim_inf seq = lim_sup seq by Th40;
per cases by XXREAL_0:14;
suppose
a in REAL;
hence thesis by A1,Lm7;
end;
suppose
a = +infty;
hence thesis by A1,Lm5;
end;
suppose
a = -infty;
hence thesis by A1,Lm6;
end;
end;