:: Inferior Limit and Superior Limit of Sequences of Real Numbers
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 29, 2005
:: Copyright (c) 2005-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, SEQ_1, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1,
COMPLEX1, ORDINAL2, REAL_1, SEQ_4, RELAT_1, FUNCT_1, TARSKI, XXREAL_2,
XBOOLE_0, SUPINF_2, PARTFUN3, NAT_1, VALUED_1, VALUED_0, SEQ_2, RINFSUP1,
MEMBER_1;
notations ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1,
COMPLEX1, TARSKI, XXREAL_2, VALUED_0, FUNCT_1, SEQ_4, XBOOLE_0, SUBSET_1,
COMSEQ_2, SEQ_2, RELSET_1, FUNCT_2, MEASURE6, VALUED_1, SEQ_1, PARTFUN3,
MEMBER_1;
constructors REAL_1, NAT_1, COMPLEX1, SEQM_3, LIMFUNC1, PARTFUN3, PARTFUN1,
XXREAL_2, SEQ_4, RELSET_1, BINOP_2, SEQ_2, MEASURE6, MEMBER_1, SQUARE_1,
COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, RFUNCT_1, MEMBER_1, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve n,m,k,k1,k2 for Nat;
reserve r,r1,r2,s,t,p for Real;
reserve seq,seq1,seq2 for Real_Sequence;
reserve x,y for set;
theorem :: RINFSUP1:1
s - r < t & s + r > t iff |.t-s.| < r;
definition
let seq be Real_Sequence;
func upper_bound seq -> Real equals
:: RINFSUP1:def 1
upper_bound rng seq;
end;
definition
let seq be Real_Sequence;
func lower_bound seq -> Real equals
:: RINFSUP1:def 2
lower_bound rng seq;
end;
theorem :: RINFSUP1:2
seq1+seq2-seq2=seq1;
theorem :: RINFSUP1:3
r in rng seq iff -r in rng(-seq);
theorem :: RINFSUP1:4
rng (-seq) = -- rng seq;
theorem :: RINFSUP1:5
seq is bounded_above iff rng seq is bounded_above;
theorem :: RINFSUP1:6
seq is bounded_below iff rng seq is bounded_below;
theorem :: RINFSUP1:7
seq is bounded_above implies ( r = upper_bound seq iff (for n holds seq.n
<= r) & for s st 0~~= lower_bound seq1 + lower_bound seq2;
theorem :: RINFSUP1:16
seq1 is bounded_above & seq2 is bounded_above implies upper_bound (seq1
+ seq2) <= upper_bound seq1 + upper_bound seq2;
notation
let f be Real_Sequence;
synonym f is nonnegative for f is nonnegative-yielding;
end;
definition
let f be Real_Sequence;
redefine attr f is nonnegative means
:: RINFSUP1:def 3
for n holds f.n >= 0;
end;
theorem :: RINFSUP1:17
seq is nonnegative implies seq ^\k is nonnegative;
theorem :: RINFSUP1:18
seq is bounded_below nonnegative implies lower_bound seq >= 0;
theorem :: RINFSUP1:19
seq is bounded_above nonnegative implies upper_bound seq >= 0;
theorem :: RINFSUP1:20
seq1 is bounded_below nonnegative & seq2 is bounded_below
nonnegative implies (seq1(#)seq2) is bounded_below &
lower_bound (seq1 (#) seq2) >= (
lower_bound seq1) * (lower_bound seq2);
theorem :: RINFSUP1:21
seq1 is bounded_above nonnegative & seq2 is bounded_above
nonnegative implies (seq1(#)seq2) is bounded_above &
upper_bound (seq1 (#) seq2) <= (
upper_bound seq1) * (upper_bound seq2);
theorem :: RINFSUP1:22
seq is non-decreasing bounded_above implies seq is bounded;
theorem :: RINFSUP1:23
seq is non-increasing bounded_below implies seq is bounded;
theorem :: RINFSUP1:24
seq is non-decreasing bounded_above implies lim seq = upper_bound seq;
theorem :: RINFSUP1:25
seq is non-increasing bounded_below implies lim seq = lower_bound seq;
theorem :: RINFSUP1:26
seq is bounded_above implies seq ^\k is bounded_above;
theorem :: RINFSUP1:27
seq is bounded_below implies seq ^\k is bounded_below;
theorem :: RINFSUP1:28
seq is bounded implies seq ^\k is bounded;
theorem :: RINFSUP1:29
for seq, n holds
{seq.k: n <= k} is Subset of REAL;
theorem :: RINFSUP1:30
rng (seq ^\ k) = {seq.n where n: k <= n};
theorem :: RINFSUP1:31
seq is bounded_above implies for n for R being Subset of REAL st
R = {seq.k : n <= k} holds R is bounded_above;
theorem :: RINFSUP1:32
seq is bounded_below implies for n for R being Subset of REAL st
R = {seq.k : n <= k} holds R is bounded_below;
theorem :: RINFSUP1:33
seq is bounded implies for n for R being Subset of REAL st R = {
seq.k : n <= k} holds R is real-bounded;
theorem :: RINFSUP1:34
seq is non-decreasing implies for n for R being Subset of REAL
st R = {seq.k : n <= k} holds lower_bound R = seq.n;
theorem :: RINFSUP1:35
seq is non-increasing implies for n for R being Subset of REAL
st R = {seq.k : n <= k} holds upper_bound R = seq.n;
definition
let seq be Real_Sequence;
func inferior_realsequence seq -> Real_Sequence means
:: RINFSUP1:def 4
for n for Y being Subset of REAL st Y = {seq.k : n <= k}
holds it.n = lower_bound Y;
end;
definition
let seq be Real_Sequence;
func superior_realsequence seq -> Real_Sequence means
:: RINFSUP1:def 5
for n for Y
being Subset of REAL st Y = {seq.k : n <= k} holds it.n = upper_bound Y;
end;
theorem :: RINFSUP1:36
(inferior_realsequence seq).n = lower_bound (seq ^\n);
theorem :: RINFSUP1:37
(superior_realsequence seq).n = upper_bound (seq ^\n);
theorem :: RINFSUP1:38
seq is bounded_below implies (inferior_realsequence seq).0 = lower_bound seq;
theorem :: RINFSUP1:39
seq is bounded_above implies (superior_realsequence seq).0 = upper_bound seq;
theorem :: RINFSUP1:40
seq is bounded_below implies (r = (inferior_realsequence seq).n
iff (for k holds r <= seq.(n+k)) & for s st 0~~~~= (inferior_realsequence seq1).n + (
inferior_realsequence seq2).n;
theorem :: RINFSUP1:77
seq1 is bounded_above & seq2 is bounded_above implies (
superior_realsequence(seq1+seq2)).n <= (superior_realsequence seq1).n + (
superior_realsequence seq2).n;
theorem :: RINFSUP1:78
seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative
implies (inferior_realsequence(seq1(#)seq2)).n >= (inferior_realsequence seq1).
n * (inferior_realsequence seq2).n;
theorem :: RINFSUP1:79
seq1 is bounded_below nonnegative & seq2 is bounded_below
nonnegative implies (inferior_realsequence(seq1(#)seq2)).n >= (
inferior_realsequence seq1).n * (inferior_realsequence seq2).n;
theorem :: RINFSUP1:80
seq1 is bounded_above nonnegative & seq2 is bounded_above
nonnegative implies (superior_realsequence(seq1(#)seq2)).n <= (
superior_realsequence seq1).n * (superior_realsequence seq2).n;
definition
let seq be Real_Sequence;
func lim_sup seq -> Real equals
:: RINFSUP1:def 6
lower_bound superior_realsequence seq;
end;
definition
let seq be Real_Sequence;
func lim_inf seq -> Real equals
:: RINFSUP1:def 7
upper_bound inferior_realsequence seq;
end;
theorem :: RINFSUP1:81
seq is bounded implies (lim_inf seq <= r iff for s st 0~~~~r-s );
theorem :: RINFSUP1:85
seq is bounded implies (lim_sup seq <= r iff for s st 0~~~~r-s) & ex n st for k holds seq.(n+k)~~