:: 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-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, 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 MESFUNC1, 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 mseq.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=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 +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;