:: 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-2021 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;
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 :: RINFSUP2:1
X = Y & Y is bounded_above implies X is bounded_above & sup X = upper_bound Y
;
theorem :: RINFSUP2:2
X = Y & X is bounded_above implies Y is bounded_above & sup X = upper_bound Y
;
theorem :: RINFSUP2:3
X = Y & Y is bounded_below implies X is bounded_below & inf X = lower_bound Y
;
theorem :: RINFSUP2:4
X = Y & X is bounded_below implies Y is bounded_below & inf X = lower_bound Y
;
definition
let seq be ExtREAL_sequence;
func sup seq -> Element of ExtREAL equals
:: RINFSUP2:def 1
sup rng seq;
func inf seq -> Element of ExtREAL equals
:: RINFSUP2:def 2
inf rng seq;
end;
definition
let seq be ExtREAL_sequence;
attr seq is bounded_below means
:: RINFSUP2:def 3
rng seq is bounded_below;
attr seq is bounded_above means
:: RINFSUP2:def 4
rng seq is bounded_above;
end;
definition
let seq be ExtREAL_sequence;
attr seq is bounded means
:: RINFSUP2:def 5
seq is bounded_above & seq is bounded_below;
end;
reserve seq for ExtREAL_sequence;
theorem :: RINFSUP2:5
for seq,n holds {seq.k: n <= k} is non empty Subset of ExtREAL;
definition
let seq be ExtREAL_sequence;
func inferior_realsequence seq -> ExtREAL_sequence means
:: RINFSUP2:def 6
for n ex Y being non empty Subset of ExtREAL
st Y = {seq.k: n <= k} & it.n = inf Y;
end;
definition
let seq be ExtREAL_sequence;
func superior_realsequence seq -> ExtREAL_sequence means
:: RINFSUP2:def 7
for n ex Y being non empty Subset of ExtREAL
st Y = {seq.k where k: n <= k} & it.n = sup Y;
end;
theorem :: RINFSUP2:6
seq is real-valued implies seq is Real_Sequence;
reserve e1,e2 for ExtReal;
theorem :: RINFSUP2:7
(seq is increasing iff for n,m be Nat st m non-increasing;
cluster inferior_realsequence seq -> non-decreasing;
end;
definition
let seq be ExtREAL_sequence;
func lim_sup seq -> Element of ExtREAL equals
:: RINFSUP2:def 8
inf superior_realsequence seq;
func lim_inf seq -> Element of ExtREAL equals
:: RINFSUP2:def 9
sup inferior_realsequence seq;
end;
reserve rseq for Real_Sequence;
theorem :: RINFSUP2:9
seq = rseq & rseq is bounded implies superior_realsequence seq =
superior_realsequence rseq & lim_sup seq = lim_sup rseq;
theorem :: RINFSUP2:10
seq = rseq & rseq is bounded implies inferior_realsequence seq =
inferior_realsequence rseq & lim_inf seq=lim_inf rseq;
theorem :: RINFSUP2:11
seq is bounded implies seq is Real_Sequence;
theorem :: RINFSUP2:12
seq = rseq implies (seq is bounded_above iff rseq is bounded_above);
theorem :: RINFSUP2:13
seq = rseq implies (seq is bounded_below iff rseq is bounded_below);
theorem :: RINFSUP2:14
seq=rseq & rseq is convergent implies seq is
convergent_to_finite_number & seq is convergent & lim seq = lim rseq;
theorem :: RINFSUP2:15
seq=rseq & seq is convergent_to_finite_number implies rseq is
convergent & lim seq = lim rseq;
theorem :: RINFSUP2:16
seq^\k is convergent_to_finite_number implies seq is
convergent_to_finite_number & seq is convergent & lim seq = lim(seq^\k);
theorem :: RINFSUP2:17
seq^\k is convergent implies seq is convergent & lim seq = lim( seq^\k);
theorem :: RINFSUP2:18
lim_sup seq = lim_inf seq & lim_inf seq in REAL implies ex k st
seq^\k is bounded;
theorem :: RINFSUP2:19
seq is convergent_to_finite_number implies ex k st seq^\k is bounded;
theorem :: RINFSUP2:20
seq is convergent_to_finite_number implies seq^\k is
convergent_to_finite_number & seq^\k is convergent & lim seq = lim(seq^\k);
theorem :: RINFSUP2:21
seq is convergent implies seq^\k is convergent & lim seq = lim(seq^\k);
theorem :: RINFSUP2:22
(seq is bounded_above implies seq^\k is bounded_above) & (seq is
bounded_below implies seq^\k is bounded_below);
theorem :: RINFSUP2:23
inf seq <= seq.n & seq.n <= sup seq;
theorem :: RINFSUP2:24
inf seq <= sup seq;
theorem :: RINFSUP2:25
seq is non-increasing implies seq^\k is non-increasing & inf seq
= inf(seq^\k);
theorem :: RINFSUP2:26
seq is non-decreasing implies seq^\k is non-decreasing & sup seq
= sup(seq^\k);
theorem :: RINFSUP2:27
(superior_realsequence seq).n = sup(seq^\n) & (inferior_realsequence
seq).n = inf(seq^\n);
theorem :: RINFSUP2:28
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;
theorem :: RINFSUP2:29
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;
theorem :: RINFSUP2:30
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;
theorem :: RINFSUP2:31
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;
theorem :: RINFSUP2:32
for seq be ExtREAL_sequence st (for n be Element of NAT holds
+infty <= seq.n) holds seq is convergent_to_+infty;
theorem :: RINFSUP2:33
for seq be ExtREAL_sequence st (for n be Element of NAT holds
seq.n <= -infty) holds seq is convergent_to_-infty;
theorem :: RINFSUP2:34
for seq be ExtREAL_sequence st seq is non-increasing & -infty =
inf seq holds seq is convergent_to_-infty & lim seq = -infty;
theorem :: RINFSUP2:35
for seq be ExtREAL_sequence st seq is non-decreasing & +infty =
sup seq holds seq is convergent_to_+infty & lim seq = +infty;
theorem :: RINFSUP2:36
for seq be ExtREAL_sequence st seq is non-increasing holds seq
is convergent & lim seq = inf seq;
theorem :: RINFSUP2:37
for seq be ExtREAL_sequence st seq is non-decreasing holds seq
is convergent & lim seq = sup seq;
theorem :: RINFSUP2:38
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;
theorem :: RINFSUP2:39
for seq be ExtREAL_sequence holds lim_inf seq <= lim_sup seq;
theorem :: RINFSUP2:40
for seq be ExtREAL_sequence holds seq is convergent iff lim_inf
seq = lim_sup seq;
theorem :: RINFSUP2:41
for seq be ExtREAL_sequence st seq is convergent holds lim seq =
lim_inf seq & lim seq = lim_sup seq;