:: 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<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);

theorem :: RINFSUP2:8
  (inferior_realsequence seq).n <= seq.n & seq.n <= (
  superior_realsequence seq).n;

registration
  let seq;
  cluster superior_realsequence seq -> 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;