:: 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 0r-s ); theorem :: RINFSUP1:85 seq is bounded implies (lim_sup seq <= r iff for s st 0r-s) & ex n st for k holds seq.(n+k)