text:
:: Inferior Limit and Superior Limit of Sequences of Real Numbers
::  by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura

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;
 definitions TARSKI, XBOOLE_0, PARTFUN3, XXREAL_2;
 equalities VALUED_1;
 expansions TARSKI, XBOOLE_0, PARTFUN3, VALUED_1, XXREAL_2;
 theorems FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, NAT_1, TARSKI, XREAL_0, SEQ_4,
      SEQM_3, SETLIM_1, LIMFUNC1, PREPOWER, XREAL_1, XXREAL_0, ORDINAL1,
      RELAT_1, XXREAL_2, VALUED_0, MEASURE6, MEMBER_1;
 schemes FUNCT_2, NAT_1;

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;

Lm1: for s st 0 < s & r1 <= r2 holds r1 < r2 + s & r1 - s < r2
proof
  let s such that
A1: 0<s;
  assume r1 <= r2;
  then r1 + 0 < r2 + s by A1,XREAL_1:8;
  hence thesis by XREAL_1:19;
end;

theorem Th1:
  s - r < t & s + r > t iff |.t-s.| < r
proof
  thus s - r < t & s + r > t implies |.t-s.| < r
  proof
    assume that
A1: s - r < t and
A2: s + r > t;
    -r + s < t by A1;
    then
A3: -r < t - s by XREAL_1:20;
    t - s < r by A2,XREAL_1:19;
    hence thesis by A3,SEQ_2:1;
  end;
  assume
A4: |.t-s.| < r;
  then -r < t - s by SEQ_2:1;
  then
A5: s + -r < t by XREAL_1:20;
  t - s < r by A4,SEQ_2:1;
  hence thesis by A5,XREAL_1:19;
end;

definition
  let seq be Real_Sequence;
  func upper_bound seq -> Real equals
  upper_bound rng seq;
  coherence;
end;

definition
  let seq be Real_Sequence;
  func lower_bound seq -> Real equals
  lower_bound rng seq;
  coherence;
end;

theorem Th2:
  seq1+seq2-seq2=seq1
proof
  for n being Element of NAT holds (seq1+seq2-seq2).n = seq1.n
  proof
    let n be Element of NAT;
    (seq1+seq2-seq2).n = (seq1+(seq2-seq2)).n by SEQ_1:31
      .= seq1.n + (seq2+-seq2).n by SEQ_1:7
      .= seq1.n + (seq2.n +(-seq2).n) by SEQ_1:7
      .= seq1.n + (seq2.n +-seq2.n) by SEQ_1:10
      .= seq1.n;
    hence thesis;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th3:
  r in rng seq iff -r in rng(-seq)
proof
  thus r in rng seq implies -r in rng(-seq)
  proof
    assume r in rng seq;
    then consider n being Element of NAT such that
A1: r=seq.n by FUNCT_2:113;
    -r=(-seq).n by A1,SEQ_1:10;
    hence thesis by VALUED_0:28;
  end;
  assume -r in rng(-seq);
  then consider n being Element of NAT such that
A2: -r=(-seq).n by FUNCT_2:113;
  r=-(-seq).n by A2;
  then r= - -seq.n by SEQ_1:10;
  hence thesis by VALUED_0:28;
end;

theorem Th4:
  rng (-seq) = -- rng seq
proof
  thus rng (-seq) c= -- rng seq
  proof
    let x be object;
    assume
A1: x in rng(-seq);
    then reconsider r = x as Real;
    -r in rng -(-seq) by A1,Th3;
    then - -r in -- rng seq by MEASURE6:40;
    hence thesis;
  end;
  let x be object;
  assume
A2: x in -- rng seq;
  then reconsider r = x as Real;
  -r in -- -- rng seq by A2,MEMBER_1:12;
  then - -r in rng (-seq) by Th3;
  hence thesis;
end;

theorem Th5:
  seq is bounded_above iff rng seq is bounded_above
proof
A1: seq is bounded_above implies rng seq is bounded_above
  proof
    assume seq is bounded_above;
    then consider t such that
A2: for n holds seq.n<t by SEQ_2:def 3;
    t is UpperBound of rng seq
    proof
      let r be ExtReal;
      assume r in rng seq;
      then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3;
      hence r<=t by A2;
    end;
    hence thesis;
  end;
  rng seq is bounded_above implies seq is bounded_above
  proof
    assume rng seq is bounded_above;
    then consider t such that
A3:  t is UpperBound of rng seq;
A4: for r st r in rng seq holds r<=t by A3,XXREAL_2:def 1;
    now
      let n;
A5:   n in NAT by ORDINAL1:def 12;
      seq.n <= t by A4,FUNCT_2:4,A5;
      hence seq.n < t+1 by Lm1;
    end;
    hence thesis by SEQ_2:def 3;
  end;
  hence thesis by A1;
end;

theorem Th6:
  seq is bounded_below iff rng seq is bounded_below
proof
A1: seq is bounded_below implies rng seq is bounded_below
  proof
    assume seq is bounded_below;
    then consider t such that
A2: for n holds t<seq.n by SEQ_2:def 4;
    t is LowerBound of rng seq
    proof
      let r be ExtReal;
      assume r in rng seq;
      then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3;
      hence t<=r by A2;
    end;
    hence thesis;
  end;
  rng seq is bounded_below implies seq is bounded_below
  proof
    assume rng seq is bounded_below;
    then consider t such that
A3:  t is LowerBound of rng seq;
A4: for r st r in rng seq holds t<=r by A3,XXREAL_2:def 2;
    now
      let n;
A5:   n in NAT by ORDINAL1:def 12;
      t <= seq.n by A4,FUNCT_2:4,A5;
      hence t - 1 < seq.n by Lm1;
    end;
    hence thesis by SEQ_2:def 4;
  end;
  hence thesis by A1;
end;

theorem Th7:
  seq is bounded_above implies ( r = upper_bound seq iff (for n holds seq.n
  <= r) & for s st 0<s holds ex k st r-s < seq.k )
proof
  set R = rng seq;
  assume seq is bounded_above;
  then
A1: rng seq is bounded_above by Th5;
A2: rng seq <> {} by RELAT_1:41;
A3: (for n holds seq.n <= r) & (for s st 0<s holds ex k st r-s<seq.k)
  implies r = upper_bound seq
  proof
    assume that
A4: for n holds seq.n <= r and
A5: for s st 0<s holds ex k st r-s<seq.k;
A6: now
      let s;
      assume 0<s;
      then consider k such that
A7:   r-s< seq.k by A5;
A8:   k in NAT by ORDINAL1:def 12;
      consider r2 such that
A9:   r2 in R & r2 = seq.k by FUNCT_2:4,A8;
      take r2;
      thus r2 in R & r-s < r2 by A7,A9;
    end;
    now
      let r1;
      assume r1 in R;
      then ex n being object st n in dom seq & seq.n = r1 by FUNCT_1:def 3;
      hence r1 <= r by A4;
    end;
    hence thesis by A1,A2,A6,SEQ_4:def 1;
  end;
  r = upper_bound seq implies (for n holds seq.n <= r) &
  for s st 0<s holds ex k
  st r-s<seq.k
  proof
    assume
A10: r = upper_bound seq;
A11: now
      let s;
      assume 0<s;
      then consider r2 such that
A12:  r2 in R and
A13:  r-s<r2 by A1,A2,A10,SEQ_4:def 1;
      consider k being Nat such that
A14:  r2 = seq.k by A12,SETLIM_1:4;
       reconsider k as Nat;
      take k;
      thus r-s < seq.k by A13,A14;
    end;
    now
      let n;
A15:   n in NAT by ORDINAL1:def 12;
      seq.n in R by FUNCT_2:4,A15;
      hence seq.n <= r by A1,A10,SEQ_4:def 1;
    end;
    hence thesis by A11;
  end;
  hence thesis by A3;
end;

theorem Th8:
  seq is bounded_below implies (r = lower_bound seq iff (for n holds r <=
  seq.n) & for s st 0<s holds ex k st seq.k < r+s )
proof
  set R = rng seq;
  assume seq is bounded_below;
  then
A1: rng seq is bounded_below by Th6;
A2: rng seq <> {} by RELAT_1:41;
A3: (for n holds r <= seq.n) & (for s st 0<s holds ex k st seq.k<r+s)
  implies r = lower_bound seq
  proof
    assume that
A4: for n holds r <= seq.n and
A5: for s st 0<s holds ex k st seq.k<r+s;
A6: now
      let s;
      assume 0<s;
      then consider k such that
A7:   seq.k < r+s by A5;
A8:   k in NAT by ORDINAL1:def 12;
      consider r2 such that
A9:   r2 in R & r2 = seq.k by FUNCT_2:4,A8;
      take r2;
      thus r2 in R & r2 <r+s by A7,A9;
    end;
    now
      let r1;
      assume r1 in R;
      then ex n being object st n in dom seq & seq.n = r1 by FUNCT_1:def 3;
      hence r <= r1 by A4;
    end;
    hence thesis by A1,A2,A6,SEQ_4:def 2;
  end;
  r = lower_bound seq implies (for n holds r <= seq.n) &
  for s st 0<s holds ex k
  st seq.k<r+s
  proof
    assume
A10: r = lower_bound seq;
A11: now
      let s;
      assume 0<s;
      then consider r2 such that
A12:  r2 in R and
A13:  r2<r+s by A1,A2,A10,SEQ_4:def 2;
      consider k being Nat such that
A14:  r2 = seq.k by A12,SETLIM_1:4;
       reconsider k as Nat;
      take k;
      thus seq.k<r+s by A13,A14;
    end;
    now
      let n;
      n in NAT by ORDINAL1:def 12;
      then seq.n in R by FUNCT_2:4;
      hence r <= seq.n by A1,A10,SEQ_4:def 2;
    end;
    hence thesis by A11;
  end;
  hence thesis by A3;
end;

theorem Th9:
  (for n holds seq.n <= r) iff seq is bounded_above & upper_bound seq <= r
proof
  thus (for n holds seq.n <= r) implies seq is bounded_above &
  upper_bound seq <= r
  proof
    assume
A1: for n holds seq.n <= r;
    now
      let m;
      seq.m <= r by A1;
      hence seq.m < r + 1 by Lm1;
    end;
    hence
A2: seq is bounded_above by SEQ_2:def 3;
    now
      set r1= (upper_bound seq) - r;
      assume r < upper_bound seq;
      then r1 > 0 by XREAL_1:50;
      then ex k st (upper_bound seq) - r1 < seq.k by A2,Th7;
      hence contradiction by A1;
    end;
    hence thesis;
  end;
  assume that
A3: seq is bounded_above and
A4: upper_bound seq <= r;
  now
    let n;
    seq.n <= upper_bound seq by A3,Th7;
    hence seq.n <= r by A4,XXREAL_0:2;
  end;
  hence thesis;
end;

theorem Th10:
  (for n holds r <= seq.n) iff seq is bounded_below & r <= lower_bound seq
proof
  thus (for n holds r <= seq.n) implies seq is bounded_below &
  r <= lower_bound seq
  proof
    assume
A1: for n holds r <= seq.n;
    now
      let m;
      r <= seq.m by A1;
      hence r -1 < seq.m by Lm1;
    end;
    hence
A2: seq is bounded_below by SEQ_2:def 4;
    now
      set r1=r - (lower_bound seq);
      assume r > lower_bound seq;
      then r1 > 0 by XREAL_1:50;
      then ex k st seq.k < (lower_bound seq) + r1 by A2,Th8;
      hence contradiction by A1;
    end;
    hence thesis;
  end;
  assume that
A3: seq is bounded_below and
A4: r <= lower_bound seq;
  now
    let n;
    lower_bound seq <= seq.n by A3,Th8;
    hence r <= seq.n by A4,XXREAL_0:2;
  end;
  hence thesis;
end;

theorem
  seq is bounded_above iff -seq is bounded_below
proof
  set seq1=-seq;
  thus seq is bounded_above implies -seq is bounded_below;
  assume seq1 is bounded_below;
  then consider t such that
A1: for n holds seq1.n>t by SEQ_2:def 4;
  for n holds seq.n < -t
  proof
    let n;
    seq1.n=-seq.n by SEQ_1:10;
    then
A2: -seq1.n = seq.n;
    seq1.n > t by A1;
    hence thesis by A2,XREAL_1:24;
  end;
  hence thesis by SEQ_2:def 3;
end;

theorem
  seq is bounded_below iff -seq is bounded_above
proof
  - -seq = seq;
  hence thesis;
end;

theorem Th13:
  seq is bounded_above implies upper_bound seq = -lower_bound (-seq)
proof
  assume seq is bounded_above;
  then rng seq is non empty bounded_above by Th5,RELAT_1:41;
  then upper_bound rng seq = - lower_bound (--(rng seq)) by MEASURE6:44
    .= - lower_bound rng -seq by Th4;
  hence thesis;
end;

theorem Th14:
  seq is bounded_below implies lower_bound seq = -upper_bound (-seq)
proof
  assume seq is bounded_below;
  then rng seq is non empty bounded_below by Th6,RELAT_1:41;
  then lower_bound rng seq = - upper_bound --(rng seq) by MEASURE6:43
    .= - upper_bound rng -seq by Th4;
  hence thesis;
end;

theorem Th15:
  seq1 is bounded_below & seq2 is bounded_below implies lower_bound (seq1
  + seq2) >= lower_bound seq1 + lower_bound seq2
proof
  assume that
A1: seq1 is bounded_below and
A2: seq2 is bounded_below;
  for n holds (seq1 + seq2).n >= lower_bound seq1 + lower_bound seq2
  proof
    let n;
A3: seq2.n >= lower_bound seq2 by A2,Th8;
    (seq1 + seq2).n = seq1.n + seq2.n & seq1.n >= lower_bound seq1
    by A1,Th8,SEQ_1:7;
    hence thesis by A3,XREAL_1:7;
  end;
  hence thesis by Th10;
end;

theorem Th16:
  seq1 is bounded_above & seq2 is bounded_above implies upper_bound (seq1
  + seq2) <= upper_bound seq1 + upper_bound seq2
proof
  assume that
A1: seq1 is bounded_above and
A2: seq2 is bounded_above;
  for n holds (seq1 + seq2).n <= upper_bound seq1 + upper_bound seq2
  proof
    let n;
A3: seq2.n <= upper_bound seq2 by A2,Th7;
    (seq1 + seq2).n = seq1.n + seq2.n & seq1.n <= upper_bound seq1
    by A1,Th7,SEQ_1:7;
    hence thesis by A3,XREAL_1:7;
  end;
  hence thesis by Th9;
end;

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
  for n holds f.n >= 0;
  compatibility
  proof
    thus f is nonnegative implies for n holds f.n >= 0 by VALUED_0:28;
    assume
A1: for n holds f.n >= 0;
    let r be Real;
    assume r in rng f;
    then ex x being Element of NAT st r = f.x by FUNCT_2:113;
    hence thesis by A1;
  end;
end;

theorem Th17:
  seq is nonnegative implies seq ^\k is nonnegative
proof
  assume
A1: seq is nonnegative;
  for n holds (seq ^\k).n >= 0
  proof
    let n;
    (seq ^\k).n = seq.(n+k) by NAT_1:def 3;
    hence thesis by A1;
  end;
  hence thesis;
end;

theorem Th18:
  seq is bounded_below nonnegative implies lower_bound seq >= 0
by Th10;

theorem
  seq is bounded_above nonnegative implies upper_bound seq >= 0
proof
  assume
A1: seq is bounded_above nonnegative;
  then
A2: seq.0 <= upper_bound seq by Th7;
  0 <= seq.0 by A1;
  hence thesis by A2;
end;

theorem Th20:
  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)
proof
  assume that
A1: seq1 is bounded_below nonnegative and
A2: seq2 is bounded_below nonnegative;
  for n holds (seq1 (#) seq2).n >= (lower_bound seq1) * (lower_bound seq2)
  proof
    let n;
A3: (seq1 (#) seq2).n = seq1.n * seq2.n & seq1.n >=
lower_bound seq1 by A1,Th8,SEQ_1:8;
A4: lower_bound seq2 >= 0 by A2,Th18;
    seq2.n >= lower_bound seq2 & lower_bound seq1 >= 0 by A1,A2,Th8,Th18;
    hence thesis by A3,A4,XREAL_1:66;
  end;
  hence thesis by Th10;
end;

theorem Th21:
  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)
proof
  assume that
A1: seq1 is bounded_above nonnegative and
A2: seq2 is bounded_above nonnegative;
  for n holds (seq1 (#) seq2).n <= (upper_bound seq1) * (upper_bound seq2)
  proof
    let n;
A3: (seq1 (#) seq2).n = seq1.n * seq2.n & seq1.n <= upper_bound seq1
by A1,Th7,SEQ_1:8;
A4: seq2.n >= 0 by A2;
    seq2.n <= upper_bound seq2 & seq1.n >= 0 by A1,A2,Th7;
    hence thesis by A3,A4,XREAL_1:66;
  end;
  hence thesis by Th9;
end;

theorem
  seq is non-decreasing bounded_above implies seq is bounded;

theorem
  seq is non-increasing bounded_below implies seq is bounded;

theorem Th24:
  seq is non-decreasing bounded_above implies lim seq = upper_bound seq
proof
  assume
A1: seq is non-decreasing bounded_above;
  then for n holds seq.n <= lim seq by SEQ_4:37;
  then
A2: upper_bound seq <= lim seq by Th9;
  for n holds seq.n <= upper_bound seq by A1,Th7;
  then lim seq <= upper_bound seq by A1,PREPOWER:2;
  hence thesis by A2,XXREAL_0:1;
end;

theorem Th25:
  seq is non-increasing bounded_below implies lim seq = lower_bound seq
proof
  assume
A1: seq is non-increasing bounded_below;
  then for n holds lim seq <= seq.n by SEQ_4:38;
  then
A2: lim seq <= lower_bound seq by Th10;
  for n holds lower_bound seq <= seq.n by A1,Th8;
  then lower_bound seq <= lim seq by A1,PREPOWER:1;
  hence thesis by A2,XXREAL_0:1;
end;

theorem
  seq is bounded_above implies seq ^\k is bounded_above by SEQM_3:27;

theorem
  seq is bounded_below implies seq ^\k is bounded_below by SEQM_3:28;

theorem
  seq is bounded implies seq ^\k is bounded by SEQM_3:29;

theorem Th29:
  for seq, n holds
    {seq.k: n <= k} is Subset of REAL
proof
  let seq, n;
  set Y = {seq.k: n <= k};
  now
    let x be object;
    assume x in Y;
    then consider z1 be set such that
A1: z1 = x and
A2: z1 in Y;
    consider k1 being Nat such that
A3: z1 = seq.k1 & n <= k1 by A2;
    reconsider k1 as Element of NAT by ORDINAL1:def 12;
    z1 = seq.k1 by A3;
    hence x in REAL by A1;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th30:
  rng (seq ^\ k) = {seq.n where n: k <= n}
proof
  set seq1 = seq ^\ k;
  set Z = {seq.m where m: k <= m};
  now
    let x be object;
    assume x in Z;
    then consider k1 being Nat such that
A1: x=seq.k1 and
A2: k <= k1;
    consider k2 being Nat such that
A3: k1 = k + k2 by A2,NAT_1:10;
    reconsider k2 as Element of NAT by ORDINAL1:def 12;
    x = seq1.k2 by A1,A3,NAT_1:def 3;
    hence x in rng seq1 by FUNCT_2:4;
  end;
  then
A4: Z c= rng seq1;
A5: dom seq1 = NAT by FUNCT_2:def 1;
  now
    let y be object;
    assume y in rng seq1;
    then consider m1 be object such that
A6: m1 in NAT and
A7: y = seq1.m1 by A5,FUNCT_1:def 3;
    reconsider m1 as Nat by A6;
    reconsider km1 = k+m1 as Nat;
    y = seq.(km1) by A7,NAT_1:def 3;
    hence y in Z by SETLIM_1:1;
  end;
  then rng seq1 c= Z;
  hence thesis by A4;
end;

theorem Th31:
  seq is bounded_above implies for n for R being Subset of REAL st
  R = {seq.k : n <= k} holds R is bounded_above
proof
  assume
A1: seq is bounded_above;
  let n;
  set seq1 = seq ^\n;
  seq1 is bounded_above by A1,SEQM_3:27;
  then
A2: rng seq1 is bounded_above by Th5;
  let R be Subset of REAL;
  assume R = {seq.k : n <= k};
  hence thesis by A2,Th30;
end;

theorem Th32:
  seq is bounded_below implies for n for R being Subset of REAL st
  R = {seq.k : n <= k} holds R is bounded_below
proof
  assume
A1: seq is bounded_below;
  let n;
  set seq1 = seq ^\n;
  seq1 is bounded_below by A1,SEQM_3:28;
  then
A2: rng seq1 is bounded_below by Th6;
  let R be Subset of REAL;
  assume R = {seq.k : n <= k};
  hence thesis by A2,Th30;
end;

theorem Th33:
  seq is bounded implies for n for R being Subset of REAL st R = {
  seq.k : n <= k} holds R is real-bounded
by Th31,Th32;

theorem Th34:
  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
proof
  assume
A1: seq is non-decreasing;
  let n;
A2: now
    let r;
    assume r in {seq.k : n <= k};
    then consider r1 being Real such that
A3: r = r1 & r1 in {seq.k : n <= k};
    consider k1 such that
A4: r1 = seq.k1 and
A5: n <= k1 by A3;
    consider k being Nat such that
A6: n + k =k1 by A5,NAT_1:10;
    thus seq.n <= r by A1,A3,A4,A6,SEQM_3:5;
  end;
  let R be Subset of REAL;
A7: now
    let s;
A8: seq.n in {seq.k : n <= k};
    assume 0 < s;
    hence ex r st r in {seq.k : n <= k} & r< seq.n + s by A8,XREAL_1:29;
  end;
  assume
A9: R = {seq.k : n <= k};
  then
A10: R <> {} by SETLIM_1:1;
  R is bounded_below by A1,A9,Th32,LIMFUNC1:1;
  hence thesis by A9,A10,A2,A7,SEQ_4:def 2;
end;

theorem Th35:
  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
proof
  assume
A1: seq is non-increasing;
  let n;
A2: now
    let r;
    assume r in {seq.k : n <= k};
    then consider r1 being Real such that
A3: r = r1 & r1 in {seq.k : n <= k};
    consider k1 such that
A4: r1 = seq.k1 and
A5: n <= k1 by A3;
    consider k being Nat such that
A6: n + k =k1 by A5,NAT_1:10;
    thus r <= seq.n by A1,A3,A4,A6,SEQM_3:7;
  end;
  let R be Subset of REAL;
A7: now
    let s;
A8: seq.n in {seq.k : n <= k};
    assume 0 < s;
    hence ex r st r in {seq.k : n <= k} & seq.n - s < r by A8,XREAL_1:44;
  end;
  assume
A9: R = {seq.k : n <= k};
  then
A10: R <> {} by SETLIM_1:1;
  R is bounded_above by A1,A9,Th31,LIMFUNC1:1;
  hence thesis by A9,A10,A2,A7,SEQ_4:def 1;
end;

definition
  let seq be Real_Sequence;
  func inferior_realsequence seq -> Real_Sequence means
  :Def4:
  for n for Y being Subset of REAL st Y = {seq.k : n <= k}
    holds it.n = lower_bound Y;
  existence
proof
  defpred P[Element of NAT, Element of REAL] means for Y being Subset of REAL
  st Y = {seq.k: $1 <= k} holds $2 = lower_bound Y;
A1: for n being Element of NAT ex y being Element of REAL st P[n,y]
  proof
    let n be Element of NAT;
    reconsider Y={seq.k: n <= k} as Subset of REAL by Th29;
    reconsider y = lower_bound Y as Element of REAL by XREAL_0:def 1;
    for Y being Subset of REAL st Y = {seq.k: n <= k} holds y = lower_bound Y;
    hence thesis;
  end;
  consider f being sequence of REAL 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 Real_Sequence such that
A3: for n for Y being Subset of REAL st Y = {seq.k : n <= k} holds
    seq1.n = lower_bound Y and
A4: for m for Y being Subset of REAL st Y = {seq.k : m <= k} holds
    seq2.m = lower_bound Y;
A5: for y being object st y in NAT holds seq1.y = seq2.y
    proof
      let y be object;
      assume y in NAT;
      then reconsider y as Element of NAT;
      reconsider Y = {seq.k: y <= k} as Subset of REAL by Th29;
      seq1.y = lower_bound Y by A3;
      hence thesis by A4;
    end;
    NAT = dom seq1 & NAT = dom seq2 by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

definition
  let seq be Real_Sequence;
  func superior_realsequence seq -> Real_Sequence means
  :Def5:
  for n for Y
  being Subset of REAL st Y = {seq.k : n <= k} holds it.n = upper_bound Y;
  existence
proof
  defpred P[Element of NAT, Element of REAL] means for Y being Subset of REAL
  st Y = {seq.k: $1 <= k} holds $2 = upper_bound Y;
A1: for n being Element of NAT ex y being Element of REAL st P[n,y]
  proof
    let n be Element of NAT;
    reconsider Y={seq.k: n <= k} as Subset of REAL by Th29;
    reconsider y = upper_bound Y as Element of REAL by XREAL_0:def 1;
    for Y being Subset of REAL st Y = {seq.k: n <= k} holds y = upper_bound Y;
    hence thesis;
  end;
  consider f being sequence of REAL 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 Real_Sequence such that
A3: for n for Y being Subset of REAL st Y = {seq.k : n <= k} holds
    seq1.n = upper_bound Y and
A4: for m for Y being Subset of REAL st Y = {seq.k : m <= k} holds
    seq2.m = upper_bound Y;
A5: for y being object st y in NAT holds seq1.y = seq2.y
    proof
      let y be object;
      assume y in NAT;
      then reconsider y as Element of NAT;
      reconsider Y = {seq.k: y <= k} as Subset of REAL by Th29;
      seq1.y = upper_bound Y by A3;
      hence thesis by A4;
    end;
    NAT = dom seq1 & NAT = dom seq2 by FUNCT_2:def 1;
    hence thesis by A5,FUNCT_1:2;
  end;
end;

theorem Th36:
  (inferior_realsequence seq).n = lower_bound (seq ^\n)
proof
  reconsider Y = {seq.k: n <= k} as Subset of REAL by Th29;
  (inferior_realsequence seq).n = lower_bound Y by Def4
    .= lower_bound rng (seq ^\ n) by Th30;
  hence thesis;
end;

theorem Th37:
  (superior_realsequence seq).n = upper_bound (seq ^\n)
proof
  reconsider Y = {seq.k: n <= k} as Subset of REAL by Th29;
  (superior_realsequence seq).n = upper_bound Y by Def5
    .= upper_bound rng (seq ^\ n) by Th30;
  hence thesis;
end;

theorem Th38:
  seq is bounded_below implies (inferior_realsequence seq).0 = lower_bound seq
proof
  reconsider Y1 = {seq.k : 0 <= k} as Subset of REAL by Th29;
  (inferior_realsequence seq).0 = lower_bound Y1 by Def4
    .= lower_bound seq by SETLIM_1:5;
  hence thesis;
end;

theorem Th39:
  seq is bounded_above implies (superior_realsequence seq).0 = upper_bound seq
proof
  reconsider Y1 = {seq.k : 0 <= k} as Subset of REAL by Th29;
  (superior_realsequence seq).0 = upper_bound Y1 by Def5
    .= upper_bound seq by SETLIM_1:5;
  hence thesis;
end;

theorem Th40:
  seq is bounded_below implies (r = (inferior_realsequence seq).n
  iff (for k holds r <= seq.(n+k)) & for s st 0<s ex k st seq.(n+k)<r+s)
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume seq is bounded_below;
  then
A1: Y1 is non empty bounded_below by Th32,SETLIM_1:1;
  thus r = (inferior_realsequence seq).n implies (for k holds r<=seq.(n+k)) &
  for s st 0<s ex k st seq.(n+k)<r+s
  proof
    assume r = (inferior_realsequence seq).n;
    then
A2: r = lower_bound Y1 by Def4;
A3: for s st 0<s ex k st seq.(n+k)<r+s
    proof
      let s;
      assume 0<s;
      then consider r1 such that
A4:   r1 in Y1 and
A5:   r1<r+s by A1,A2,SEQ_4:def 2;
      consider k1 such that
A6:   r1=seq.k1 and
A7:   n <= k1 by A4;
      consider k2 being Nat such that
A8:   k1 = n + k2 by A7,NAT_1:10;
      thus thesis by A5,A6,A8;
    end;
    for k holds r<=seq.(n+k)
    proof
      let k;
      seq.(n+k) in Y1 by SETLIM_1:1;
      hence thesis by A1,A2,SEQ_4:def 2;
    end;
    hence thesis by A3;
  end;
  assume that
A9: for k holds r <= seq.(n+k) and
A10: for s st 0<s ex k st seq.(n+k)<r+s;
A11: for s st 0<s ex r1 st r1 in Y1 & r1<r+s
  proof
    let s;
    assume 0<s;
    then consider k such that
A12: seq.(n+k)<r+s by A10;
    n + k >= n by NAT_1:11;
    then seq.(n+k) in Y1;
    hence thesis by A12;
  end;
  for r1 st r1 in Y1 holds r <= r1
  proof
    let r1;
    assume r1 in Y1;
    then consider k1 such that
A13: r1=seq.k1 and
A14: n <= k1;
    consider k2 being Nat such that
A15: k1 = n + k2 by A14,NAT_1:10;
    thus thesis by A9,A13,A15;
  end;
  then r=lower_bound Y1 by A1,A11,SEQ_4:def 2;
  hence thesis by Def4;
end;

theorem Th41:
  seq is bounded_above implies (r = (superior_realsequence seq).n
  iff (for k holds seq.(n+k) <= r) & for s st 0<s ex k st r-s<seq.(n+k))
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume seq is bounded_above;
  then
A1: Y1 is non empty bounded_above by Th31,SETLIM_1:1;
  thus r = (superior_realsequence seq).n implies (for k holds seq.(n+k) <= r)
  & for s st 0<s ex k st r-s<seq.(n+k)
  proof
    assume r = (superior_realsequence seq).n;
    then
A2: r = upper_bound Y1 by Def5;
A3: for s st 0<s ex k st r-s<seq.(n+k)
    proof
      let s;
      assume 0<s;
      then consider r1 such that
A4:   r1 in Y1 and
A5:   r-s<r1 by A1,A2,SEQ_4:def 1;
      consider k1 such that
A6:   r1=seq.k1 and
A7:   n <= k1 by A4;
      consider k2 being Nat such that
A8:   k1 = n + k2 by A7,NAT_1:10;
      thus thesis by A5,A6,A8;
    end;
    for k holds seq.(n+k) <= r
    proof
      let k;
      seq.(n+k) in Y1 by SETLIM_1:1;
      hence thesis by A1,A2,SEQ_4:def 1;
    end;
    hence thesis by A3;
  end;
  assume that
A9: for k holds seq.(n+k) <= r and
A10: for s st 0<s ex k st r-s<seq.(n+k);
A11: for s st 0<s ex r1 st r1 in Y1 & r-s<r1
  proof
    let s;
    assume 0<s;
    then consider k such that
A12: r-s<seq.(n+k) by A10;
    n + k >= n by NAT_1:11;
    then seq.(n+k) in Y1;
    hence thesis by A12;
  end;
  for r1 st r1 in Y1 holds r1 <= r
  proof
    let r1;
    assume r1 in Y1;
    then consider k1 such that
A13: r1=seq.k1 and
A14: n <= k1;
    consider k2 being Nat such that
A15: k1 = n + k2 by A14,NAT_1:10;
    thus thesis by A9,A13,A15;
  end;
  then r=upper_bound Y1 by A1,A11,SEQ_4:def 1;
  hence thesis by Def5;
end;

theorem Th42:
  seq is bounded_below implies ((for k holds r <= seq.(n+k)) iff r
  <= (inferior_realsequence seq).n)
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  set seq1 = seq ^\n;
  assume seq is bounded_below;
  then
A1: seq1 is bounded_below by SEQM_3:28;
A2: rng seq1 = Y1 by Th30;
  thus (for k holds r <= seq.(n+k)) implies r <= (inferior_realsequence seq).n
  proof
    assume
A3: for k holds r <= seq.(n+k);
    now
      let n1 being Nat;
      n1 in NAT by ORDINAL1:def 12;
      then seq1.n1 in rng seq1 by FUNCT_2:4;
      then consider r1 such that
A4:   seq1.n1= r1 and
A5:   r1 in Y1 by A2;
      consider k1 being Nat such that
A6:   r1 = seq.k1 and
A7:   n <= k1 by A5;
      consider k2 being Nat such that
A8:   k1 = n + k2 by A7,NAT_1:10;
      thus r <= seq1.n1 by A3,A4,A6,A8;
    end;
    then r <= lower_bound seq1 by Th10;
    then r <= lower_bound Y1 by Th30;
    hence thesis by Def4;
  end;
  assume r <= (inferior_realsequence seq).n;
  then r <= lower_bound Y1 by Def4;
  then
A9: r <= lower_bound seq1 by Th30;
  now
    let m1 be Nat;
    n <= n+m1 by NAT_1:11;
    then seq.(n+m1) in Y1;
    then seq.(n+m1) in rng seq1 by Th30;
    then ex k being object st k in dom seq1 & seq1.k = seq.(n+m1)
by FUNCT_1:def 3;
    hence r <= seq.(n+m1) by A1,A9,Th10;
  end;
  hence thesis;
end;

theorem Th43:
  seq is bounded_below implies ((for m st n <= m holds r <= seq.m)
  iff r <= (inferior_realsequence seq).n)
proof
  assume
A1: seq is bounded_below;
  thus (for m st n<=m holds r <= seq.m) implies r <= (inferior_realsequence
  seq).n
  proof
    assume for m st n<=m holds r <= seq.m;
    then for k holds r <= seq.(n+k) by NAT_1:11;
    hence thesis by A1,Th42;
  end;
  assume
A2: r <= (inferior_realsequence seq).n;
  now
    let m;
    assume n<=m;
    then consider k being Nat such that
A3: m = n + k by NAT_1:10;
    thus r <= seq.m by A1,A2,A3,Th42;
  end;
  hence thesis;
end;

theorem Th44:
  seq is bounded_above implies ((for k holds seq.(n+k) <= r) iff (
  superior_realsequence seq).n <= r)
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  set seq1 = seq ^\n;
  assume seq is bounded_above;
  then
A1: seq1 is bounded_above by SEQM_3:27;
A2: rng seq1 = Y1 by Th30;
  thus (for k holds seq.(n+k) <= r) implies (superior_realsequence seq).n <= r
  proof
    assume
A3: for k holds seq.(n+k) <= r;
    now
      let n1 being Nat;
      n1 in NAT by ORDINAL1:def 12;
      then seq1.n1 in rng seq1 by FUNCT_2:4;
      then consider r1 such that
A4:   seq1.n1= r1 and
A5:   r1 in Y1 by A2;
      consider k1 being Nat such that
A6:   r1 = seq.k1 and
A7:   n <= k1 by A5;
      consider k2 being Nat such that
A8:   k1 = n + k2 by A7,NAT_1:10;
      thus seq1.n1 <= r by A3,A4,A6,A8;
    end;
    then upper_bound seq1 <= r by Th9;
    then upper_bound Y1 <= r by Th30;
    hence thesis by Def5;
  end;
  assume (superior_realsequence seq).n <= r;
  then upper_bound Y1 <= r by Def5;
  then
A9: upper_bound seq1 <= r by Th30;
  now
    let m1 being Nat;
    n <= n+m1 by NAT_1:11;
    then seq.(n+m1) in Y1;
    then seq.(n+m1) in rng seq1 by Th30;
    then ex k being object st k in dom seq1 & seq1.k = seq.(n+m1)
by FUNCT_1:def 3;
    hence seq.(n+m1) <= r by A1,A9,Th9;
  end;
  hence thesis;
end;

theorem Th45:
  seq is bounded_above implies ((for m st n<=m holds seq.m <= r)
  iff (superior_realsequence seq).n <= r)
proof
  assume
A1: seq is bounded_above;
  thus (for m st n<=m holds seq.m <= r) implies (superior_realsequence seq).n
  <= r
  proof
    assume for m st n<=m holds seq.m <= r;
    then for k holds seq.(n+k) <= r by NAT_1:11;
    hence thesis by A1,Th44;
  end;
  assume
A2: (superior_realsequence seq).n <= r;
  now
    let m;
    assume n<=m;
    then consider k being Nat such that
A3: m = n + k by NAT_1:10;
    thus seq.m <= r by A1,A2,A3,Th44;
  end;
  hence thesis;
end;

theorem Th46:
  seq is bounded_below implies (inferior_realsequence seq).n = min
  ((inferior_realsequence seq).(n+1),seq.n)
proof
  reconsider Y2 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  reconsider Y3 = {seq.n} as Subset of REAL;
A1: (inferior_realsequence seq).(n+1) = lower_bound Y2 by Def4;
  assume
A2: seq is bounded_below;
  then
A3: Y2 <> {} & Y2 is bounded_below by Th32,SETLIM_1:1;
A4: Y3 is bounded_below
  proof
    consider t such that
A5: for m holds t<seq.m by A2,SEQ_2:def 4;
    t is LowerBound of Y3
    proof
      let r be ExtReal;
      assume r in Y3;
      then r = seq.n by TARSKI:def 1;
      hence t <= r by A5;
    end;
    hence thesis;
  end;
  (inferior_realsequence seq).n = lower_bound Y1 by Def4;
  then (inferior_realsequence seq).n = lower_bound (Y2 \/ Y3) by SETLIM_1:2
    .= min(lower_bound Y2,lower_bound Y3) by A3,A4,SEQ_4:142
    .= min((inferior_realsequence seq).(n+1),seq.n) by A1,SEQ_4:9;
  hence thesis;
end;

theorem Th47:
  seq is bounded_above implies (superior_realsequence seq).n = max
  ((superior_realsequence seq).(n+1),seq.n)
proof
  reconsider Y2 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  reconsider Y3 = {seq.n} as Subset of REAL;
A1: (superior_realsequence seq).(n+1) = upper_bound Y2 by Def5;
  assume
A2: seq is bounded_above;
  then
A3: Y2 <> {} & Y2 is bounded_above by Th31,SETLIM_1:1;
A4: Y3 is bounded_above
  proof
    consider t such that
A5: for m holds seq.m<t by A2,SEQ_2:def 3;
    t is UpperBound of Y3
    proof
      let r be ExtReal;
      assume r in Y3;
      then r = seq.n by TARSKI:def 1;
      hence r <=t by A5;
    end;
    hence thesis;
  end;
  (superior_realsequence seq).n = upper_bound Y1 by Def5;
  then (superior_realsequence seq).n = upper_bound (Y2 \/ Y3) by SETLIM_1:2
    .= max(upper_bound Y2,upper_bound Y3) by A3,A4,SEQ_4:143
    .= max((superior_realsequence seq).(n+1),seq.n) by A1,SEQ_4:9;
  hence thesis;
end;

theorem Th48:
  seq is bounded_below implies (inferior_realsequence seq).n <= (
  inferior_realsequence seq).(n+1)
proof
A1: min((inferior_realsequence seq).(n+1),seq.n) <= (inferior_realsequence
  seq).(n+1) by XXREAL_0:17;
  assume seq is bounded_below;
  hence thesis by A1,Th46;
end;

theorem Th49:
  seq is bounded_above implies (superior_realsequence seq).(n+1)
  <= (superior_realsequence seq).n
proof
A1: (superior_realsequence seq).(n+1) <= max((superior_realsequence seq).(n+
  1),seq.n) by XXREAL_0:25;
  assume seq is bounded_above;
  hence thesis by A1,Th47;
end;

theorem Th50:
  seq is bounded_below implies inferior_realsequence seq is non-decreasing
by Th48;

theorem Th51:
  seq is bounded_above implies superior_realsequence seq is non-increasing
by Th49;

theorem
  seq is bounded implies (inferior_realsequence seq).n <= (
  superior_realsequence seq).n
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume
A1: seq is bounded;
A2: Y1 <> {} by SETLIM_1:1;
  (superior_realsequence seq).n = upper_bound Y1 &
  (inferior_realsequence seq).n =
  lower_bound Y1 by Def4,Def5;
  hence thesis by A1,A2,Th33,SEQ_4:11;
end;

theorem Th53:
  seq is bounded implies (inferior_realsequence seq).n <= lower_bound (
  superior_realsequence seq)
proof
  reconsider Y2 = {seq.k2 : n <= k2} as Subset of REAL by Th29;
  assume
A1: seq is bounded;
A2: now
    let m;
    reconsider Y1 = {seq.k1 : m <= k1} as Subset of REAL by Th29;
    n <= n + m by NAT_1:11;
    then
A3: seq.(n+m) in Y2;
    Y2 is real-bounded by A1,Th33;
    then Y2 is bounded_below;
    then
A4: lower_bound Y2 <= seq.(n+m) by A3,SEQ_4:def 2;
    m <= n + m by NAT_1:11;
    then
A5: seq.(n+m) in Y1;
    Y1 is real-bounded by A1,Th33;
    then Y1 is bounded_above;
    then
A6: seq.(n+m) <= upper_bound Y1 by A5,SEQ_4:def 1;
    (superior_realsequence seq).m = upper_bound Y1 by Def5;
    hence lower_bound Y2 <= (superior_realsequence seq).m by A6,A4,XXREAL_0:2;
  end;
  (inferior_realsequence seq).n = lower_bound Y2 by Def4;
  hence thesis by A2,Th10;
end;

theorem Th54:
  seq is bounded implies upper_bound(inferior_realsequence seq) <= (
  superior_realsequence seq).n
proof
  reconsider Y2 = {seq.k2 : n <= k2} as Subset of REAL by Th29;
  assume
A1: seq is bounded;
A2: now
    let m;
    reconsider Y1 = {seq.k1 : m <= k1} as Subset of REAL by Th29;
    n <= n + m by NAT_1:11;
    then
A3: seq.(n+m) in Y2;
    Y2 is real-bounded by A1,Th33;
    then Y2 is bounded_above;
    then
A4: upper_bound Y2 >= seq.(n+m) by A3,SEQ_4:def 1;
    m <= n + m by NAT_1:11;
    then
A5: seq.(n+m) in Y1;
    Y1 is real-bounded by A1,Th33;
    then Y1 is bounded_below;
    then
A6: seq.(n+m) >= lower_bound Y1 by A5,SEQ_4:def 2;
    (inferior_realsequence seq).m = lower_bound Y1 by Def4;
    hence upper_bound Y2 >= (inferior_realsequence seq).m by A6,A4,XXREAL_0:2;
  end;
  (superior_realsequence seq).n = upper_bound Y2 by Def5;
  hence thesis by A2,Th9;
end;

theorem Th55:
  seq is bounded implies upper_bound(inferior_realsequence seq) <= lower_bound(
  superior_realsequence seq)
proof
  set seq1 = (inferior_realsequence seq);
  set r = lower_bound(superior_realsequence seq);
  assume seq is bounded;
  then seq1.n <= r by Th53;
  hence thesis by Th9;
end;

theorem Th56:
  seq is bounded implies superior_realsequence seq is bounded &
  inferior_realsequence seq is bounded
proof
  assume
A1: seq is bounded;
  then inferior_realsequence seq is non-decreasing by Th50;
  then
A2: inferior_realsequence seq is bounded_below by LIMFUNC1:1;
  now
    let m;
    upper_bound(inferior_realsequence seq) <= (superior_realsequence seq).m
    by A1,Th54;
    hence (upper_bound(inferior_realsequence seq)) - 1 <
    (superior_realsequence seq).m
    by Lm1;
  end;
  then
A3: (superior_realsequence seq) is bounded_below by SEQ_2:def 4;
  now
    let m;
    (inferior_realsequence seq).m <= lower_bound (superior_realsequence seq)
    by A1,Th53;
    hence (inferior_realsequence seq).m <
    (lower_bound (superior_realsequence seq)) +1
    by Lm1;
  end;
  then
A4: (inferior_realsequence seq) is bounded_above by SEQ_2:def 3;
  superior_realsequence seq is non-increasing by A1,Th51;
  then superior_realsequence seq is bounded_above by LIMFUNC1:1;
  hence thesis by A2,A4,A3;
end;

theorem Th57:
  seq is bounded implies inferior_realsequence seq is convergent &
  lim inferior_realsequence seq = upper_bound inferior_realsequence seq
proof
  assume seq is bounded;
  then
  inferior_realsequence seq is non-decreasing & inferior_realsequence seq
  is bounded by Th50,Th56;
  hence thesis by Th24;
end;

theorem Th58:
  seq is bounded implies superior_realsequence seq is convergent &
  lim superior_realsequence seq = lower_bound superior_realsequence seq
proof
  assume seq is bounded;
  then
  superior_realsequence seq is non-increasing & superior_realsequence seq
  is bounded by Th51,Th56;
  hence thesis by Th25;
end;

theorem Th59:
  seq is bounded_below implies (inferior_realsequence seq).n = - (
  superior_realsequence(-seq)).n
proof
  assume
A1: seq is bounded_below;
  (inferior_realsequence seq).n = lower_bound (seq ^\n) by Th36
    .= - upper_bound -(seq ^\n) by A1,Th14,SEQM_3:28
    .= - upper_bound ((-seq) ^\n) by SEQM_3:16;
  hence thesis by Th37;
end;

theorem Th60:
  seq is bounded_above implies (superior_realsequence seq).n = - (
  inferior_realsequence(-seq)).n
proof
  assume
A1: seq is bounded_above;
  (superior_realsequence seq).n = upper_bound (seq ^\n) by Th37
    .= - lower_bound -(seq ^\n) by A1,Th13,SEQM_3:27
    .= - lower_bound ((-seq) ^\n) by SEQM_3:16;
  hence thesis by Th36;
end;

theorem Th61:
  seq is bounded_below implies (inferior_realsequence seq) = - (
  superior_realsequence(-seq))
proof
  assume seq is bounded_below;
  then (inferior_realsequence seq).n = - (superior_realsequence(-seq)).n by
Th59;
  hence thesis by SEQ_1:10;
end;

theorem Th62:
  seq is bounded_above implies (superior_realsequence seq) = - (
  inferior_realsequence(-seq))
proof
  assume seq is bounded_above;
  then (superior_realsequence seq).n = - (inferior_realsequence(-seq)).n by
Th60;
  hence thesis by SEQ_1:10;
end;

theorem
  seq is non-decreasing implies seq.n <= (inferior_realsequence seq).(n+ 1)
proof
  reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: (inferior_realsequence seq).(n+1) = lower_bound Y1 by Def4;
  assume
A2: seq is non-decreasing;
  then lower_bound Y1 = seq.(n+1) by Th34;
  hence thesis by A2,A1;
end;

Lm2: seq is non-decreasing implies (inferior_realsequence seq).n = seq.n
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume
A1: seq is non-decreasing;
  (inferior_realsequence seq).n = lower_bound Y1 by Def4;
  hence thesis by A1,Th34;
end;

theorem
  seq is non-decreasing implies inferior_realsequence seq = seq
proof
  assume seq is non-decreasing;
  then for n being Element of NAT holds
   (inferior_realsequence seq).n = seq.n by Lm2;
  hence thesis by FUNCT_2:63;
end;

theorem Th65:
  seq is non-decreasing bounded_above implies seq.n <= (
  superior_realsequence seq).(n+1)
proof
  reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: seq.(n+1) in Y1;
  assume
A2: seq is non-decreasing bounded_above;
  then Y1 is bounded_above by Th31;
  then
A3: seq.(n+1) <= upper_bound Y1 by A1,SEQ_4:def 1;
A4: (superior_realsequence seq).(n+1) = upper_bound Y1 by Def5;
  seq.n <= seq.(n+1) by A2;
  hence thesis by A4,A3,XXREAL_0:2;
end;

theorem Th66:
  seq is non-decreasing bounded_above implies (
  superior_realsequence seq).n = (superior_realsequence seq).(n+1)
proof
  assume
A1: seq is non-decreasing bounded_above;
  then seq.n <= (superior_realsequence seq).(n+1) by Th65;
  then max((superior_realsequence seq).(n+1),seq.n) = (superior_realsequence
  seq).(n+1) by XXREAL_0:def 10;
  hence thesis by A1,Th47;
end;

theorem Th67:
  seq is non-decreasing bounded_above implies (
  superior_realsequence seq).n = upper_bound seq & (superior_realsequence seq)
   is
  constant
proof
  reconsider ubs = upper_bound seq as Element of REAL by XREAL_0:def 1;
  defpred P[Nat] means (superior_realsequence seq).$1 = ubs;
  assume
A1: seq is non-decreasing bounded_above;
A2: for k being Nat st P[k] holds P[k+1]
  by A1,Th66;
A3: P[0] by A1,Th39;
  for k being Nat holds P[k] from NAT_1:sch 2(A3,A2);
  hence thesis by VALUED_0:def 18;
end;

theorem
  seq is non-decreasing bounded_above implies
  lower_bound (superior_realsequence
  seq) = upper_bound seq
proof
  assume
A1: seq is non-decreasing bounded_above;
  then (superior_realsequence seq) is constant by Th67;
  then consider r1 being Element of REAL such that
A2: rng (superior_realsequence seq)={r1} by FUNCT_2:111;
  r1 in rng (superior_realsequence seq) by A2,TARSKI:def 1;
  then ex n being Element of NAT
st r1 = (superior_realsequence seq).n by FUNCT_2:113;
  then rng (superior_realsequence seq)= {upper_bound seq} by A1,A2,Th67;
  hence thesis by SEQ_4:9;
end;

theorem
  seq is non-increasing implies (superior_realsequence seq).(n+1) <= seq .n
proof
  reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: (superior_realsequence seq).(n+1) = upper_bound Y1 by Def5;
  assume
A2: seq is non-increasing;
  then upper_bound Y1 = seq.(n+1) by Th35;
  hence thesis by A2,A1;
end;

Lm3: seq is non-increasing implies (superior_realsequence seq).n = seq.n
proof
  reconsider Y1 = {seq.k : n <= k} as Subset of REAL by Th29;
  assume
A1: seq is non-increasing;
  (superior_realsequence seq).n = upper_bound Y1 by Def5;
  hence thesis by A1,Th35;
end;

theorem
  seq is non-increasing implies superior_realsequence seq = seq
proof
  assume seq is non-increasing;
  then for n being Element of NAT holds
   (superior_realsequence seq).n = seq.n by Lm3;
  hence thesis by FUNCT_2:63;
end;

theorem Th71:
  seq is non-increasing bounded_below implies (
  inferior_realsequence seq).(n+1) <= seq.n
proof
  reconsider Y1 = {seq.k : n+1 <= k} as Subset of REAL by Th29;
A1: seq.(n+1) in Y1;
  assume
A2: seq is non-increasing bounded_below;
  then Y1 is bounded_below by Th32;
  then
A3: lower_bound Y1 <= seq.(n+1) by A1,SEQ_4:def 2;
A4: (inferior_realsequence seq).(n+1) = lower_bound Y1 by Def4;
  seq.(n+1) <= seq.n by A2;
  hence thesis by A4,A3,XXREAL_0:2;
end;

theorem Th72:
  seq is non-increasing bounded_below implies (
  inferior_realsequence seq).n = (inferior_realsequence seq).(n+1)
proof
  assume
A1: seq is non-increasing bounded_below;
  then (inferior_realsequence seq).(n+1) <= seq.n by Th71;
  then min((inferior_realsequence seq).(n+1),seq.n) = (inferior_realsequence
  seq).(n+1) by XXREAL_0:def 9;
  hence thesis by A1,Th46;
end;

theorem Th73:
  seq is non-increasing & seq is bounded_below implies (
  inferior_realsequence seq).n = lower_bound seq &
  (inferior_realsequence seq) is
  constant
proof
  assume that
A1: seq is non-increasing and
A2: seq is bounded_below;
   reconsider lbs = lower_bound seq as Element of REAL by XREAL_0:def 1;
  defpred P[Nat] means (inferior_realsequence seq).$1 = lbs;
A3: for k being Nat st P[k] holds P[k+1]
  by A1,A2,Th72;
A4: P[0] by A2,Th38;
  for k being Nat holds P[k] from NAT_1:sch 2(A4,A3);
  hence thesis by VALUED_0:def 18;
end;

theorem
  seq is non-increasing bounded_below implies upper_bound inferior_realsequence
  seq = lower_bound seq
proof
  assume
A1: seq is non-increasing bounded_below;
  then inferior_realsequence seq is constant by Th73;
  then consider r1 being Element of REAL such that
A2: rng inferior_realsequence seq={r1} by FUNCT_2:111;
  r1 in rng inferior_realsequence seq by A2,TARSKI:def 1;
  then ex n being Element of NAT
st r1 = (inferior_realsequence seq).n by FUNCT_2:113;
  then upper_bound inferior_realsequence seq =
  upper_bound {lower_bound seq} by A1,A2,Th73
    .= lower_bound seq by SEQ_4:9;
  hence thesis;
end;

theorem Th75:
  seq1 is bounded & seq2 is bounded & (for n holds seq1.n <= seq2.
  n) implies (for n holds (superior_realsequence seq1).n <= (
superior_realsequence seq2).n) & for n holds (inferior_realsequence seq1).n <=
  (inferior_realsequence seq2).n
proof
  assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n holds seq1.n <= seq2.n;
  now
    let n;
    reconsider Y2 = {seq2.k2 : n <= k2} as Subset of REAL by Th29;
    reconsider Y1 = {seq1.k1 : n <= k1} as Subset of REAL by Th29;
A4: Y1 <> {} & Y2 <> {} by SETLIM_1:1;
A5: (inferior_realsequence seq1).n = lower_bound Y1 &
(inferior_realsequence seq2)
    .n = lower_bound Y2 by Def4;
    Y1 is real-bounded by A1,Th33;
    then
A6: Y1 is bounded_below;
    now
      let r;
      assume r in Y2;
      then consider k such that
A7:   r = seq2.k and
A8:   n <= k;
      seq1.k in Y1 by A8;
      then
A9:   lower_bound Y1 <= seq1.k by A6,SEQ_4:def 2;
      seq1.k <= r by A3,A7;
      hence lower_bound Y1 <= r by A9,XXREAL_0:2;
    end;
    then
A10: for r be Real st r in Y2 holds lower_bound Y1 <= r;
    Y2 is real-bounded by A2,Th33;
    then
A11: Y2 is bounded_above;
A12: now
      let r be Real;
      assume r in Y1;
      then consider k such that
A13:  r = seq1.k and
A14:  n <= k;
      seq2.k in Y2 by A14;
      then
A15:  seq2.k <= upper_bound Y2 by A11,SEQ_4:def 1;
      r <= seq2.k by A3,A13;
      hence r <= upper_bound Y2 by A15,XXREAL_0:2;
    end;
    (superior_realsequence seq1).n = upper_bound Y1 &
    (superior_realsequence seq2)
    .n = upper_bound Y2 by Def5;
    hence (superior_realsequence seq1).n <= (superior_realsequence seq2).n & (
inferior_realsequence seq1).n <= (inferior_realsequence seq2).n
     by A5,A4,A12,A10,SEQ_4:113,144;
  end;
  hence thesis;
end;

theorem
  seq1 is bounded_below & seq2 is bounded_below implies (
  inferior_realsequence(seq1+seq2)).n >= (inferior_realsequence seq1).n + (
  inferior_realsequence seq2).n
proof
  assume seq1 is bounded_below & seq2 is bounded_below;
  then seq1 ^\n is bounded_below & seq2 ^\n is bounded_below by SEQM_3:28;
  then lower_bound(seq1 ^\n + seq2 ^\n) >=
  lower_bound(seq1 ^\n) + lower_bound(seq2 ^\n) by Th15;
  then
A1: lower_bound((seq1+seq2) ^\n) >=
lower_bound(seq1 ^\n) + lower_bound(seq2 ^\n) by SEQM_3:15;
  (inferior_realsequence seq1).n =
  lower_bound(seq1 ^\n) & (inferior_realsequence
  seq2 ).n = lower_bound(seq2 ^\n) by Th36;
  hence thesis by A1,Th36;
end;

theorem
  seq1 is bounded_above & seq2 is bounded_above implies (
  superior_realsequence(seq1+seq2)).n <= (superior_realsequence seq1).n + (
  superior_realsequence seq2).n
proof
  assume seq1 is bounded_above & seq2 is bounded_above;
  then seq1 ^\n is bounded_above & seq2 ^\n is bounded_above by SEQM_3:27;
  then upper_bound(seq1 ^\n + seq2 ^\n) <=
  upper_bound(seq1 ^\n) + upper_bound(seq2 ^\n) by Th16;
  then
A1: upper_bound((seq1+seq2) ^\n) <=
upper_bound(seq1 ^\n) + upper_bound(seq2 ^\n) by SEQM_3:15;
  (superior_realsequence seq1).n = upper_bound(seq1 ^\n) &
  (superior_realsequence
  seq2 ).n = upper_bound(seq2 ^\n) by Th37;
  hence thesis by A1,Th37;
end;

theorem
  seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative
implies (inferior_realsequence(seq1(#)seq2)).n >= (inferior_realsequence seq1).
  n * (inferior_realsequence seq2).n
proof
  assume seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative;
  then seq1 ^\n is bounded_below nonnegative & seq2 ^\n is bounded_below
  nonnegative by Th17,SEQM_3:28;
  then lower_bound((seq1 ^\n)(#)(seq2 ^\n))>=
  lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by Th20;
  then
A1: lower_bound((seq1 (#) seq2) ^\n) >=
lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by SEQM_3:19;
  (inferior_realsequence seq1).n = lower_bound(seq1 ^\n) &
  (inferior_realsequence
  seq2 ).n = lower_bound(seq2 ^\n) by Th36;
  hence thesis by A1,Th36;
end;

theorem Th79:
  seq1 is bounded_below nonnegative & seq2 is bounded_below
  nonnegative implies (inferior_realsequence(seq1(#)seq2)).n >= (
  inferior_realsequence seq1).n * (inferior_realsequence seq2).n
proof
  assume seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative;
  then seq1 ^\n is bounded_below nonnegative & seq2 ^\n is bounded_below
  nonnegative by Th17,SEQM_3:28;
  then lower_bound((seq1 ^\n)(#)(seq2 ^\n))>=
  lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by Th20;
  then
A1: lower_bound((seq1 (#) seq2) ^\n) >=
lower_bound(seq1 ^\n) * lower_bound(seq2 ^\n) by SEQM_3:19;
  (inferior_realsequence seq1).n = lower_bound(seq1 ^\n) &
  (inferior_realsequence
  seq2 ).n = lower_bound(seq2 ^\n) by Th36;
  hence thesis by A1,Th36;
end;

theorem Th80:
  seq1 is bounded_above nonnegative & seq2 is bounded_above
  nonnegative implies (superior_realsequence(seq1(#)seq2)).n <= (
  superior_realsequence seq1).n * (superior_realsequence seq2).n
proof
  assume seq1 is bounded_above nonnegative & seq2 is bounded_above nonnegative;
  then seq1 ^\n is bounded_above nonnegative & seq2 ^\n is bounded_above
  nonnegative by Th17,SEQM_3:27;
  then upper_bound((seq1 ^\n)(#)(seq2 ^\n))<=
  upper_bound(seq1 ^\n) * upper_bound(seq2 ^\n) by Th21;
  then
A1: upper_bound((seq1 (#) seq2) ^\n) <=
upper_bound(seq1 ^\n) * upper_bound(seq2 ^\n) by SEQM_3:19;
  (superior_realsequence seq1).n = upper_bound(seq1 ^\n) &
  (superior_realsequence
  seq2 ).n = upper_bound(seq2 ^\n) by Th37;
  hence thesis by A1,Th37;
end;

definition
  let seq be Real_Sequence;
  func lim_sup seq -> Real equals
  lower_bound superior_realsequence seq;
  coherence;
end;

definition
  let seq be Real_Sequence;
  func lim_inf seq -> Real equals
  upper_bound inferior_realsequence seq;
  coherence;
end;

theorem Th81:
  seq is bounded implies (lim_inf seq <= r iff for s st 0<s holds
  for n ex k st seq.(n+k)<r+s )
proof
  set seq1 = inferior_realsequence seq;
  assume
A1: seq is bounded;
  then
A2: seq1 is bounded by Th56;
  thus lim_inf seq <= r implies for s st 0<s holds for n ex k st seq.(n+k)<r+s
  proof
    assume
A3: lim_inf seq <= r;
    let s such that
A4: 0<s;
    for n ex k st seq.(n+k)<r+s
    proof
      let n;
      consider k such that
A5:   seq.(n+k) < seq1.n+s by A1,A4,Th40;
      seq1.n <= r by A2,A3,Th9;
      then seq.(n+k)+seq1.n < r+(seq1.n+s) by A5,XREAL_1:8;
      then seq.(n+k) < r+(seq1.n+s)-seq1.n by XREAL_1:20;
      hence thesis;
    end;
    hence thesis;
  end;
  assume
A6: for s st 0<s holds for n ex k st seq.(n+k)<r+s;
  for s st 0<s holds lim_inf seq<=r+s
  proof
    let s such that
A7: 0<s;
    for n holds seq1.n <= r+s
    proof
      let n;
      consider k such that
A8:   seq.(n+k)<r+s by A6,A7;
      seq1.n <= seq.(n+k) by A1,Th40;
      hence thesis by A8,XXREAL_0:2;
    end;
    hence thesis by Th9;
  end;
  hence thesis by XREAL_1:41;
end;

theorem Th82:
  seq is bounded implies (r <= lim_inf seq iff for s st 0<s holds
  ex n st for k holds r-s<seq.(n+k) )
proof
  set seq1 = inferior_realsequence seq;
  assume
A1: seq is bounded;
  then
A2: seq1 is bounded by Th56;
  thus r <= lim_inf seq implies for s st 0<s holds ex n st for k holds r-s<seq
  .(n+k)
  proof
    assume
A3: r <= lim_inf seq;
    let s such that
A4: 0<s;
    ex n st for k holds r-s<seq.(n+k)
    proof
      consider n1 be Nat such that
A5:   seq1.n1 > upper_bound seq1-s by A2,A4,Th7;
      seq1.n1 + upper_bound seq1 > r + (upper_bound seq1-s)
      by A3,A5,XREAL_1:8;
      then seq1.n1 + upper_bound seq1 > r - s + upper_bound seq1;
      then
A6:   (seq1.n1 + upper_bound seq1) - upper_bound seq1 > r-s by XREAL_1:20;
      now
        let k;
        seq1.n1 <= seq.(n1+k) by A1,Th40;
        then (r-s) + seq1.n1 < seq.(n1+k) + seq1.n1 by A6,XREAL_1:8;
        then (r-s) + seq1.n1 - seq1.n1 < seq.(n1+k) by XREAL_1:19;
        hence r-s<seq.(n1+k);
      end;
      hence thesis;
    end;
    hence thesis;
  end;
  assume
A7: for s st 0<s holds ex n st for k holds r-s<seq.(n+k);
  for s st 0<s holds r-s<=lim_inf seq
  proof
    let s;
    assume 0<s;
    then consider n1 be Nat such that
A8: for k holds r-s<seq.(n1+k) by A7;
    for k holds r-s<=seq.(n1+k) by A8;
    then
A9: r-s <= seq1.n1 by A1,Th42;
    seq1.n1 <= upper_bound seq1 by A2,Th7;
    hence thesis by A9,XXREAL_0:2;
  end;
  hence thesis by XREAL_1:57;
end;

theorem
  seq is bounded implies (r = lim_inf seq iff for s st 0<s holds (for n
  ex k st seq.(n+k)<r+s) & ex n st for k holds r-s<seq.(n+k) )
proof
  assume
A1: seq is bounded;
  hence
  r = lim_inf seq implies for s st 0<s holds (for n ex k st seq.(n+k)<r+s
  ) & ex n st for k holds r-s<seq.(n+k) by Th81,Th82;
  assume
A2: for s st 0<s holds (for n ex k st seq.(n+k)<r+s) & ex n st for k
  holds r-s<seq.(n+k);
  then for s st 0<s holds ex n st for k holds r-s<seq.(n+k);
  then
A3: r <= lim_inf seq by A1,Th82;
  for s st 0<s holds for n ex k st seq.(n+k)<r+s by A2;
  then lim_inf seq <= r by A1,Th81;
  hence thesis by A3,XXREAL_0:1;
end;

theorem Th84:
  seq is bounded implies (r <= lim_sup seq iff for s st 0<s holds
  for n ex k st seq.(n+k)>r-s )
proof
  set seq1 = superior_realsequence seq;
  assume
A1: seq is bounded;
  then
A2: seq1 is bounded by Th56;
  thus r <= lim_sup seq implies for s st 0<s holds for n ex k st seq.(n+k)>r-s
  proof
    assume
A3: r <= lim_sup seq;
    let s such that
A4: 0<s;
    for n ex k st seq.(n+k)>r-s
    proof
      let n;
      consider k such that
A5:   seq.(n+k) > seq1.n-s by A1,A4,Th41;
      seq1.n >= r by A2,A3,Th10;
      then seq1.n+seq.(n+k) > r+(seq1.n-s) by A5,XREAL_1:8;
      then seq.(n+k) > r+seq1.n-s-seq1.n by XREAL_1:19;
      hence thesis;
    end;
    hence thesis;
  end;
  assume
A6: for s st 0<s holds for n ex k st seq.(n+k)>r-s;
  for s st 0<s holds lim_sup seq>=r-s
  proof
    let s such that
A7: 0<s;
    for n holds r-s <= seq1.n
    proof
      let n;
      consider k such that
A8:   r-s<seq.(n+k) by A6,A7;
      seq.(n+k) <= seq1.n by A1,Th41;
      hence thesis by A8,XXREAL_0:2;
    end;
    hence thesis by Th10;
  end;
  hence thesis by XREAL_1:57;
end;

theorem Th85:
  seq is bounded implies (lim_sup seq <= r iff for s st 0<s holds
  ex n st for k holds seq.(n+k)<r+s )
proof
  set seq1 = superior_realsequence seq;
  assume
A1: seq is bounded;
  then
A2: seq1 is bounded by Th56;
  thus lim_sup seq <= r implies for s st 0<s holds ex n st for k holds seq.(n+
  k)<r+s
  proof
    assume
A3: lim_sup seq <= r;
    for s st 0<s holds ex n st for k holds seq.(n+k)<r+s
    proof
      let s such that
A4:   0<s;
      ex n st for k holds seq.(n+k)<r+s
      proof
        consider n1 be Nat such that
A5:     seq1.n1 < lower_bound seq1+s by A2,A4,Th8;
        seq1.n1 + lower_bound seq1 < r + (lower_bound seq1+s)
        by A3,A5,XREAL_1:8;
        then seq1.n1 + lower_bound seq1 < r + s + lower_bound seq1;
        then
A6:     (seq1.n1 + lower_bound seq1) - lower_bound seq1 < r+s by XREAL_1:19;
        now
          let k;
          seq.(n1+k) <= seq1.n1 by A1,Th41;
          then seq.(n1+k) + seq1.n1 < (r+s) + seq1.n1 by A6,XREAL_1:8;
          then seq.(n1+k) + seq1.n1 - seq1.n1 < (r+s) by XREAL_1:19;
          hence seq.(n1+k) < r+s;
        end;
        hence thesis;
      end;
      hence thesis;
    end;
    hence thesis;
  end;
  assume
A7: for s st 0<s holds ex n st for k holds seq.(n+k)<r+s;
  for s st 0<s holds lim_sup seq<=r+s
  proof
    let s;
    assume 0<s;
    then consider n1 be Nat such that
A8: for k holds seq.(n1+k)<r+s by A7;
    for k holds seq.(n1+k)<=r+s by A8;
    then
A9: seq1.n1<=r+s by A1,Th44;
    lower_bound seq1 <= seq1.n1 by A2,Th8;
    hence thesis by A9,XXREAL_0:2;
  end;
  hence thesis by XREAL_1:41;
end;

theorem
  seq is bounded implies (r = lim_sup seq iff for s st 0<s holds (for n
  holds ex k st seq.(n+k)>r-s) & ex n st for k holds seq.(n+k)<r+s )
proof
  assume
A1: seq is bounded;
  hence
  r = lim_sup seq implies for s st 0<s holds (for n holds ex k st seq.(n+
  k)>r-s) & ex n st for k holds seq.(n+k)<r+s by Th84,Th85;
  assume
A2: for s st 0<s holds (for n holds ex k st seq.(n+k)>r-s) & ex n st for
  k holds seq.(n+k)<r+s;
  then for s st 0<s holds ex n st for k holds seq.(n+k)<r+s;
  then
A3: lim_sup seq <= r by A1,Th85;
  for s st 0<s holds for n holds ex k st seq.(n+k)>r-s by A2;
  then r <= lim_sup seq by A1,Th84;
  hence thesis by A3,XXREAL_0:1;
end;

theorem
  seq is bounded implies lim_inf seq <= lim_sup seq by Th55;

theorem Th88:
  seq is bounded & lim_sup seq = lim_inf seq iff seq is convergent
proof
  thus seq is bounded & lim_sup seq = lim_inf seq implies seq is convergent
  proof
    reconsider r= lower_bound superior_realsequence seq as Real;
    assume that
A1: seq is bounded and
A2: lim_sup seq = lim_inf seq;
A3: inferior_realsequence seq is bounded by A1,Th56;
A4: inferior_realsequence seq is non-decreasing by A1,Th50;
A5: superior_realsequence seq is non-increasing by A1,Th51;
A6: superior_realsequence seq is bounded by A1,Th56;
    for s st 0<s ex n st for m st n<=m holds |.seq.m-r.| < s
    proof
      let s such that
A7:   0 < s;
      consider k2 be Nat such that
A8:   (superior_realsequence seq).k2 < r + s by A6,A7,Th8;
      consider k1 be Nat such that
A9:   r - s < (inferior_realsequence seq).k1 by A2,A3,A7,Th7;
      reconsider k = max(k1,k2) as Nat by TARSKI:1;
      k2 <= k by XXREAL_0:25;
      then
A10:  (superior_realsequence seq).k <= (superior_realsequence seq).k2
      by A5,SEQM_3:8;
      k1 <= k by XXREAL_0:25;
      then
A11:  (inferior_realsequence seq).k1 <= (inferior_realsequence seq). k
      by A4,SEQM_3:6;
      ex n st for m st n<=m holds |.seq.m-r.| < s
      proof
        take k;
        let m;
        assume k <= m;
        then consider k3 being Nat such that
A12:    m = k + k3 by NAT_1:10;
        seq.m <= (superior_realsequence seq).k by A1,A12,Th41;
        then seq.m <= (superior_realsequence seq).k2 by A10,XXREAL_0:2;
        then
A13:    seq.m < r + s by A8,XXREAL_0:2;
        (inferior_realsequence seq).k <= seq.m by A1,A12,Th40;
        then (inferior_realsequence seq).k1 <= seq.m by A11,XXREAL_0:2;
        then r - s < seq.m by A9,XXREAL_0:2;
        hence thesis by A13,Th1;
      end;
      hence thesis;
    end;
    hence thesis by SEQ_2:def 6;
  end;
  assume
A14: seq is convergent;
  then consider r such that
A15: for p st 0 < p ex n st for m st n<=m holds |.seq.m-r.| < p by SEQ_2:def 6;
A16: seq is bounded by A14;
A17: for p st 0 < p ex n st r - p <= (inferior_realsequence seq).n & (
  superior_realsequence seq).n <= r + p
  proof
    let p;
    assume 0 < p;
    then consider n such that
A18: for m st n<=m holds |.seq.m-r.| < p by A15;
A19: for m st n<=m holds r - p <= seq.m & seq.m <= r + p
    proof
      let m;
      assume n<=m;
      then |.seq.m-r.| < p by A18;
      hence thesis by Th1;
    end;
    then for m st n<=m holds seq.m <= r + p;
    then
A20: (superior_realsequence seq).n <= r + p by A16,Th45;
    for m st n<=m holds r - p <= seq.m by A19;
    then r - p <= (inferior_realsequence seq).n by A16,Th43;
    hence thesis by A20;
  end;
A21: superior_realsequence seq is bounded & inferior_realsequence seq is
  bounded by A16,Th56;
A22: for p holds 0 < p implies r - p <= upper_bound inferior_realsequence seq &
 lower_bound
  superior_realsequence seq <= r + p
  proof
    let p;
    assume 0 < p;
    then consider n such that
A23: r - p <= (inferior_realsequence seq).n & (superior_realsequence
    seq).n <= r + p by A17;
    (inferior_realsequence seq).n <= upper_bound inferior_realsequence seq &
    lower_bound
    superior_realsequence seq <= (superior_realsequence seq).n by A21,Th7,Th8;
    hence thesis by A23,XXREAL_0:2;
  end;
  reconsider r as Real;
A24: for p holds 0 < p implies lower_bound superior_realsequence seq <= r + p
by A22;
  then
A25: lower_bound superior_realsequence seq <= r by XREAL_1:41;
  for p holds 0 < p implies r <= upper_bound inferior_realsequence seq + p
  proof
    let p;
    assume 0 < p;
    then r - p <= upper_bound inferior_realsequence seq by A22;
    hence thesis by XREAL_1:20;
  end;
  then
A26: r <= upper_bound inferior_realsequence seq by XREAL_1:41;
A27: upper_bound (inferior_realsequence seq) <=
lower_bound (superior_realsequence seq) by A14,Th55;
  lower_bound superior_realsequence seq <= r by A24,XREAL_1:41;
  then upper_bound inferior_realsequence seq <= r by A27,XXREAL_0:2;
  then r = upper_bound inferior_realsequence seq by A26,XXREAL_0:1;
  hence thesis by A14,A27,A25,XXREAL_0:1;
end;

theorem
  seq is convergent implies lim seq = lim_sup seq & lim seq = lim_inf seq
proof
  reconsider r= lim seq as Real;
  assume
A1: seq is convergent;
  then
A2: upper_bound(inferior_realsequence seq) <=
lower_bound(superior_realsequence seq) by Th55;
A3: seq is bounded by A1;
  then
A4: superior_realsequence seq is bounded & inferior_realsequence seq is
  bounded by Th56;
A5: for p holds 0 < p implies r - p <= upper_bound inferior_realsequence seq &
 lower_bound
  superior_realsequence seq <= r + p
  proof
    let p;
    assume 0 < p;
    then consider k such that
A6: for m st k <= m holds |.seq.m-r.|<p by A1,SEQ_2:def 7;
A7: for m st k <= m holds r - p <= seq.m & seq.m <= r + p
    proof
      let m;
      assume k <= m;
      then |.seq.m - r.| < p by A6;
      hence thesis by Th1;
    end;
    then for m st k <= m holds r - p <= seq.m;
    then
A8: r - p <= (inferior_realsequence seq).k by A3,Th43;
    for m st k <= m holds seq.m <= r + p by A7;
    then
A9: (superior_realsequence seq).k <= r + p by A3,Th45;
    (inferior_realsequence seq).k <= upper_bound inferior_realsequence seq &
     lower_bound
    superior_realsequence seq <= (superior_realsequence seq).k by A4,Th7,Th8;
    hence thesis by A8,A9,XXREAL_0:2;
  end;
A10: for p holds 0 < p implies r <= upper_bound inferior_realsequence seq + p
  proof
    let p;
    assume 0 < p;
    then r - p <= upper_bound inferior_realsequence seq by A5;
    hence thesis by XREAL_1:20;
  end;
  then
A11: r <= upper_bound inferior_realsequence seq by XREAL_1:41;
  r <= upper_bound inferior_realsequence seq by A10,XREAL_1:41;
  then
A12: r <= lower_bound superior_realsequence seq by A2,XXREAL_0:2;
  for p holds 0 < p implies lower_bound superior_realsequence seq <=
   r + p by A5;
  then
A13: lower_bound superior_realsequence seq <= r by XREAL_1:41;
  then upper_bound inferior_realsequence seq <= r by A2,XXREAL_0:2;
  hence thesis by A13,A11,A12,XXREAL_0:1;
end;

theorem Th90:
  seq is bounded implies lim_sup -seq = - lim_inf seq & lim_inf -
  seq = - lim_sup seq
proof
  assume
A1: seq is bounded;
  then inferior_realsequence seq is bounded by Th56;
  then
A2: - lim_inf seq = - - lower_bound - inferior_realsequence seq by Th13
    .= lower_bound - -superior_realsequence(-seq) by A1,Th61
    .= lim_sup -seq;
  superior_realsequence seq is bounded by A1,Th56;
  then - lim_sup seq = - - upper_bound - superior_realsequence seq by Th14
    .= upper_bound - -inferior_realsequence(-seq) by A1,Th62
    .= lim_inf -seq;
  hence thesis by A2;
end;

theorem
  seq1 is bounded & seq2 is bounded & (for n holds seq1.n <= seq2.n)
  implies lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2
proof
  assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n holds seq1.n <= seq2.n;
A4: superior_realsequence seq1 is convergent & inferior_realsequence seq1 is
  convergent by A1,Th57,Th58;
  superior_realsequence seq2 is bounded by A2,Th56;
  then
A5: lim superior_realsequence seq2 = lower_bound superior_realsequence seq2
by A2,Th25,Th51;
  inferior_realsequence seq1 is bounded by A1,Th56;
  then
A6: lim inferior_realsequence seq1 = upper_bound inferior_realsequence seq1
by A1,Th24,Th50;
  superior_realsequence seq1 is bounded by A1,Th56;
  then
A7: lim superior_realsequence seq1 = lower_bound superior_realsequence seq1
by A1,Th25,Th51;
A8: superior_realsequence seq2 is convergent & inferior_realsequence seq2 is
  convergent by A2,Th57,Th58;
  inferior_realsequence seq2 is bounded by A2,Th56;
  then
A9: lim inferior_realsequence seq2 = upper_bound inferior_realsequence seq2
by A2,Th24,Th50;
  ( for n holds (superior_realsequence seq1).n <= (superior_realsequence
seq2).n) & for n holds (inferior_realsequence seq1).n <= (inferior_realsequence
  seq2).n by A1,A2,A3,Th75;
  hence thesis by A4,A8,A7,A6,A5,A9,SEQ_2:18;
end;

theorem
  seq1 is bounded & seq2 is bounded implies lim_inf seq1 + lim_inf seq2
  <= lim_inf (seq1+seq2) & lim_inf (seq1+seq2) <= lim_inf seq1 + lim_sup seq2 &
  lim_inf (seq1+seq2) <= lim_sup seq1 + lim_inf seq2 & lim_inf seq1 + lim_sup
seq2 <= lim_sup (seq1+seq2) & lim_sup seq1 + lim_inf seq2 <= lim_sup (seq1+seq2
) & lim_sup (seq1+seq2) <= lim_sup seq1 + lim_sup seq2 & (seq1 is convergent or
seq2 is convergent implies lim_inf (seq1+seq2) = lim_inf seq1 + lim_inf seq2 &
  lim_sup (seq1+seq2) = lim_sup seq1 + lim_sup seq2 )
proof
  assume
A1: seq1 is bounded & seq2 is bounded;
A2: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_sup (seq1+
  seq2) <= lim_sup seq1 + lim_sup seq2
  proof
    let seq1,seq2;
    set r1 = lim_sup seq1, r2 = lim_sup seq2;
    assume that
A3: seq1 is bounded and
A4: seq2 is bounded;
    for s st 0<s holds ex n st for k holds (seq1+seq2).(n+k) < r1+r2+s
    proof
      let s;
      assume 0<s;
      then
A5:   0<s/2 by XREAL_1:215;
      then consider n1 being Nat such that
A6:   for k holds seq1.(n1+k) < r1+s/2 by A3,Th85;
      consider n2 being Nat such that
A7:   for k holds seq2.(n2+k) < r2+s/2 by A4,A5,Th85;
      for k holds (seq1+seq2).(n1+n2+k) < r1+r2+s
      proof
        let k;
        seq1.(n1+(n2+k)) < r1+s/2 & seq2.(n2+(n1+k)) < r2+s/2 by A6,A7;
        then seq1.(n1+n2+k) + seq2.(n1+n2+k) < (r1+s/2)+(r2+s/2) by XREAL_1:8;
        hence thesis by SEQ_1:7;
      end;
      hence thesis;
    end;
    hence thesis by A3,A4,Th85;
  end;
A8: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf seq1 +
  lim_sup seq2 <= lim_sup (seq1+seq2)
  proof
    let seq1,seq2;
    assume that
A9: seq1 is bounded and
A10: seq2 is bounded;
    lim_sup ((seq1+seq2)+(-seq1)) <= lim_sup (-seq1) + lim_sup (seq1+
    seq2) by A2,A9,A10;
    then lim_sup (seq1+seq2+-seq1) <= -lim_inf seq1 + lim_sup (seq1+seq2) by A9
,Th90;
    then lim_sup (seq2+seq1-seq1) <= lim_sup (seq1+seq2) - lim_inf seq1;
    then lim_sup seq2 <= lim_sup (seq1+seq2) - lim_inf seq1 by Th2;
    hence thesis by XREAL_1:19;
  end;
  then
A11: lim_inf seq1 + lim_sup seq2 <= lim_sup (seq1+seq2) by A1;
A12: lim_sup seq1 + lim_inf seq2 <= lim_sup (seq1+seq2) by A8,A1;
A13: lim_sup (seq1+seq2) <= lim_sup seq1 + lim_sup seq2 by A2,A1;
A14: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf seq1 +
  lim_inf seq2 <= lim_inf (seq1+seq2)
  proof
    let seq1,seq2;
    set r1 = lim_inf seq1, r2 = lim_inf seq2;
    assume that
A15: seq1 is bounded and
A16: seq2 is bounded;
    for s st 0<s holds ex n st for k holds r1+r2-s < (seq1+seq2).(n+k)
    proof
      let s;
      assume 0<s;
      then
A17:  0<s/2 by XREAL_1:215;
      then consider n1 being Nat such that
A18:  for k holds r1-s/2 < seq1.(n1+k) by A15,Th82;
      consider n2 being Nat such that
A19:  for k holds r2-s/2 < seq2.(n2+k) by A16,A17,Th82;
      for k holds r1+r2-s < (seq1+seq2).(n1+n2+k)
      proof
        let k;
        r1-s/2 < seq1.(n1+(n2+k)) & r2-s/2 < seq2.(n2+(n1+k)) by A18,A19;
        then (r1-s/2)+(r2-s/2) < seq1.(n1+n2+k) + seq2.(n1+n2+k) by XREAL_1:8;
        hence thesis by SEQ_1:7;
      end;
      hence thesis;
    end;
    hence thesis by A15,A16,Th82;
  end;
  then
A20: lim_inf seq1 + lim_inf seq2 <= lim_inf (seq1+seq2) by A1;
A21: for seq1,seq2 st seq1 is bounded & seq2 is bounded holds lim_inf (seq1+
  seq2) <= lim_inf seq1 + lim_sup seq2
  proof
    let seq1,seq2;
    assume that
A22: seq1 is bounded and
A23: seq2 is bounded;
    lim_inf ((seq1+seq2)+(-seq2)) >= lim_inf (seq1+seq2) + lim_inf (-
    seq2) by A14,A22,A23;
    then lim_inf (seq1+seq2+-seq2) >= lim_inf (seq1+seq2) +- lim_sup seq2 by
A23,Th90;
    then lim_inf (seq1+seq2-seq2) >= lim_inf (seq1+seq2) - lim_sup seq2;
    then lim_inf seq1 >= lim_inf (seq1+seq2) - lim_sup seq2 by Th2;
    hence thesis by XREAL_1:20;
  end;
  then
A24: lim_inf (seq1+seq2) <= lim_sup seq1 + lim_inf seq2 by A1;
A25: lim_inf (seq1+seq2) <= lim_inf seq1 + lim_sup seq2 by A21,A1;
  seq1 is convergent or seq2 is convergent implies lim_inf (seq1+seq2) =
lim_inf seq1 + lim_inf seq2 & lim_sup (seq1+seq2) = lim_sup seq1 + lim_sup seq2
  proof
    assume
A26: seq1 is convergent or seq2 is convergent;
    per cases by A26;
    suppose
      seq1 is convergent;
      then lim_inf seq1 = lim_sup seq1 by Th88;
      hence thesis by A20,A24,A11,A13,XXREAL_0:1;
    end;
    suppose
      seq2 is convergent;
      then lim_inf seq2 = lim_sup seq2 by Th88;
      hence thesis by A20,A25,A12,A13,XXREAL_0:1;
    end;
  end;
  hence thesis by A14,A21,A2,A8,A1;
end;

theorem
  seq1 is bounded nonnegative & seq2 is bounded nonnegative implies (
  lim_inf seq1) * (lim_inf seq2) <= lim_inf(seq1(#)seq2) & lim_sup(seq1(#)seq2)
  <= (lim_sup seq1) * (lim_sup seq2)
proof
A1: for seq1,seq2 st seq1 is bounded & seq1 is nonnegative & seq2 is
bounded & seq2 is nonnegative holds lim_sup(seq1(#)seq2) <= (lim_sup seq1) * (
  lim_sup seq2)
  proof
    let seq1,seq2;
    assume that
A2: seq1 is bounded nonnegative and
A3: seq2 is bounded nonnegative;
    set seq3 = superior_realsequence seq1, seq4 = superior_realsequence seq2,
    seq5 = superior_realsequence(seq1(#)seq2);
A4: seq5 is convergent by A2,A3,Th58;
A5: lower_bound seq5 = lim seq5 & lower_bound seq3 = lim seq3 by A2,A3,Th58;
A6: lower_bound seq4 =lim seq4 by A3,Th58;
A7: for n holds seq5.n <= (seq3(#)seq4).n
    proof
      let n;
      seq5.n <= seq3.n * seq4.n by A2,A3,Th80;
      hence thesis by SEQ_1:8;
    end;
A8: seq3 is convergent & seq4 is convergent by A2,A3,Th58;
    then (seq3(#)seq4) is convergent;
    then lim seq5 <= lim (seq3(#)seq4) by A4,A7,SEQ_2:18;
    hence thesis by A8,A5,A6,SEQ_2:15;
  end;
  for seq1,seq2 st seq1 is bounded nonnegative & seq2 is bounded
  nonnegative holds (lim_inf seq1) * (lim_inf seq2) <= lim_inf(seq1(#)seq2)
  proof
    let seq1,seq2;
    assume that
A9: seq1 is bounded nonnegative and
A10: seq2 is bounded nonnegative;
    set seq3 = inferior_realsequence seq1, seq4 = inferior_realsequence seq2,
    seq5 = inferior_realsequence(seq1(#)seq2);
A11: seq5 is convergent by A9,A10,Th57;
A12: upper_bound seq5 = lim seq5 & upper_bound seq3 = lim seq3 by A9,A10,Th57;
A13: upper_bound seq4 =lim seq4 by A10,Th57;
A14: for n holds seq5.n >= (seq3(#)seq4).n
    proof
      let n;
      seq5.n >= seq3.n * seq4.n by A9,A10,Th79;
      hence thesis by SEQ_1:8;
    end;
A15: seq3 is convergent & seq4 is convergent by A9,A10,Th57;
    then (seq3(#)seq4) is convergent;
    then lim seq5 >= lim (seq3(#)seq4) by A11,A14,SEQ_2:18;
    hence thesis by A15,A12,A13,SEQ_2:15;
  end;
  hence thesis by A1;
end;

subset_name: curated


TITLE: Constant $C$ in differential equation
QUESTION [2 upvotes]: I have differential equations:
$$  dy + x(y+1)dx = 0.$$
I'm dividing boths sides by $(y+1)$:
$$ \frac{dy}{y+1} + xdx = 0.$$
The solution is:
$$ \ln|y+1| + \frac{x^{2}}{2}  = \ln |C|.$$
As we can see, I've assumed that arbitrary constant is $ \ln|C|.$
Next:
$$ \ln \left|\frac{y+1}{c}\right| = -\frac{x^{2}}{2} $$
$$ e^{\frac{-x^{2}}{2}} = \left|\frac{y+1}{c}\right| $$
$$ \pm e^{\frac{-x^{2}}{2}}  = \frac{y+1}{c}.$$
Letting $d = \pm c,$
$$ d e^ \frac{-x^{2}}{2} = y+1 $$
$$ y = de^{-\frac{-x^2}{2}} -1 $$
Could I write additional note that  $C \neq  0$? Because $ \ln 0 $ doesn't exist right?

REPLY [0 votes]: I have a similiar example here:
differential equation
Could I exclude in similiar way solution $ y \neq 1 $, because $ln(0)$ dosen't exist in solution $ y = e^{c sin(x)} $ ?


TITLE: Is there a Fermat-era proof of Theorem 69 from Dickson's Intro to NT?
QUESTION [3 upvotes]: In Dickson’s Introduction to the Theory of Numbers (Ch. VI, pp. 91-93), he gives the following [wonderful and wonderfully general] theorem.

Theorem 69: All integral solutions of
  $$x^2-my^2=zw$$
  are given by
  \begin{align}
x &= \pm \rho(e\xi u+f\eta u-f\xi v-g\eta v),
& y &= \rho(\xi v+\eta u),  \\
z &= \rho(e\xi^2+2f\xi\eta+g\eta^2),
& w &= \rho(eu^2-2fuv+gv^2),
\end{align}
  where $\rho,\xi,\eta,u,v$ are arbitrary integers, while $e,f,g$ take only the finite set of integral values such that the forms
  $$F(\xi,\eta)=e\xi^2+2f\xi\eta+g\eta^2$$
  are representative forms, just one being chosen from each class of forms of determinant
  $$f^2-eg=m.$$

Dickson gives several examples (including $m=-1$), and his proof is remarkably elementary (n.b. Dickson developed several proofs over the years, in increasingly elementary terms.)…
But I would offer that the proof is not quite “Fermat-era”: I highly doubt Fermat thought about “representative forms” or “class[es] of forms of [a] determinant”.
So here's my

QUESTION: Does Theorem 69 have a proof using only Fermat-era math, either in the general case, or in the specific cases that Fermat is known to have played around with regularly (i.e., $m=-1$, $m=-2$, and $m=-3$)? For instance, how could Fermat have proven that, given
  $$a^2+b^2=(c^2+d^2)e, \qquad a,b,c,d,e \in \mathbb{Z}$$
  you can always find integers $e_1$ and $e_2$ such that $e=e_1^2+e_2^2$ and [up to sign]
  $$(a,b)=(ce_1 \pm de_2, ce_2 \mp de_1)  \tag{$\star$}$$
  holds?

I know Fermat claimed to have a proof (by infinite descent) of the existence of the form $e=e_1^2+e_2^2$, and have seen proofs of that fact using only Fermat-era math.
But what about the implication/form given by ($\star$)? Is there a proof that you can always find integers $e_1$ and $e_2$ that satisfy, using only Fermat-era math?

REPLY [1 votes]: In his Diophantine Analysis [pp. 31–33], Carmichael gives a series of lemmas and a final corollary which essentially duplicates Dickson’s theorem in the case $m=-1$. He even goes so far as to say that the result is “due to Fermat”. So it seems that case, at least, already has a Fermat-era proof.


TITLE: Finding exceptional regular representations of $\tilde{D}_4$ efficiently
QUESTION [2 upvotes]: Let $A$ be the path algebra of the quiver $\tilde{D}_4$. I would like to find its exceptional regular representations with as little computation as possible.
Of course, we can compute the whole Auslander-Reiten quiver and compute all the $\text{Hom}_A(X,X)$ and $\text{Ext}_A^1(X,X)$ for all the regular representations, but surely there must be a better way to do it?
A conjecture I have is that an exceptional indecomposable representation must be on the border of the regular component of the AR-quiver. By the border I mean the set of vertices of the quiver such that there is only one incoming and one outgoing edge. If anyone knows a standard term for this set, please tell me in the comments! I think there are only 6 exceptional regular representations of $\tilde{D}_4$, all of which are of this form. This conjecture seems plausible to me, but I haven't managed to prove this in general.
EDIT: it seems that it's very much untrue that an exceptional module must be on the border of a regular component, but I think I managed to prove this for the components on which the Auslander-Reiten translate $\tau$ satisfies $\tau^2=\text{id}$, and with that it is indeed possible to find the exceptional modules without computing the whole quiver. I will write down an answer here as soon as I find the time.

REPLY [4 votes]: The AR quiver of the regular representations of an affine quiver consists of infinitely many "tubes". A tube of rank $r$ has $r$ modules on what you call the border. Let me number them $B_1, B_2, \dots, B_r$. Then, if I numbered them in the convenient way, there are another $r$ modules $C_1, \dots C_r$, and irreducible morphisms from $B_i$ to $C_i$ and from $C_i$ to $B_{i+1}$. Then there are another $r$ modules $D_i$ with morphisms from $C_i$ to $D_i$ and from $D_i$ to $C_{i+1}$. This pattern continues infinitely. The Auslander--Reiten translation sends the module on each level numbered $i$ to the object numbered $i-1$ (cyclically).
The AR quiver of an affine quiver consists of infinitely many rank 1 tubes and up to three tubes of higher rank. The tubes are standard, meaning that you can calculate Homs by looking at compositions of arrows in the component modulo mesh relations. $\operatorname{Ext}^1(V,V)$ is dual to $\operatorname{Hom}(V,\tau V)$, so its dimension can be calculated the same way. One discovers that the exceptional representations in a tube of rank $r$ lie in the bottom $r-1$ layers of the tube.
In $\widetilde D_n$, there are three exceptional tubes, of rank 2, 2, and $n-2$. This provides $2 + 2 + (n-2)(n-3) = n^2 -5n + 10$ exceptional representations.
A possible reference is Chapter 7 of the book "An introduction to quiver representations" by Derksen and Weyman. Though they say they don't give full details and encourage the reader to consult "Indecomposable graphs and algebras" by Dlab and Ringel, published in the Memoirs of the AMS.
Another excellent reference would be the notes by Crawley-Boevey. The answer for $\widetilde D_4$ is given on page 35.


TITLE: Mexican Hat Function that Converges to 1
QUESTION [2 upvotes]: The Ricker wavelet, also known as the Mexican Hat function, converges to 0 for negative and positive infinity.

I'm looking for a function with the same shape in the center, but that converges back to 1 (or a value really close to 1) when approaching negative or positive infinity.
P.S: Obviously $f(x) + 1$ does not work, as the new maximum will be close to 2.

REPLY [0 votes]: Something like this seems to work:
$$f(x)=1-0.1e^{-0.36x^2}-1.3x^2e^{-x^2}$$


TITLE: How is time dilation invariant of observer?
QUESTION [1 upvotes]: From one observer's perspective, on all moving objects time will run slower. But from the perspective of one of those objects, it's the observer who's slow. And the answer seems to be that both are correct!
Then there are (correct) statements like the ISS runs slower than the Earth. Based on above how can this be true? Why not the other way around?

REPLY [1 votes]: That's a good question, and it highlights the fact that special relativity describes far more than just motion at a constant speed in a straight line, and therefore the Lorentz transformations. Confusion about time dilation is almost invariably due to taking an overly simplistic view of special relativity.
The only way two observers can directly compare their clocks is if they are at the sample place in space. Two observers in linear motion can directly compare their clocks only once because by definition they can never meet again. That's why both can conclude the other's clock is running slow without fear of contradiction.
However accelerated observers can compare their clocks more than once - the obvious example is the infamous twin paradox (which isn't a paradox, but that's a rant for another day). When two observers can directly compare their clocks twice, or more, there can be no ambiguity about which clock has been running slow.
The ISS moves in a circle around the Earth. In principle I can put an observer hovering in space in the path of the ISS, so the ISS passes the observer once every orbit. That observer and the astronauts on the ISS can compare their clocks whenever they meet, and when they do all parties will agree that the clocks on the ISS have run slower than the clock held by the hovering observer. That's why we say the clocks on the ISS are running slow.


TITLE: Lagrangian of Klein Gordon equation
QUESTION [4 upvotes]: Consider the following Lagrangian density
$$
\mathcal{L}(\Phi,\partial_\mu\Phi)=-\frac{1}{2}\partial_\mu\Phi\partial^\mu\Phi-\frac{m\Phi^2}{2}.
$$
I want to calculate the equation of motion using the Euler-Lagrange equation to derive the Klein-Gordon equation. The E-L equation states $$\frac{\partial \mathcal{L}}{\partial\Phi}-\partial_\mu\frac{\partial\mathcal{L}}{\partial\,(\partial_\mu\Phi)}=0$$ So, I calculated
 $\frac{\partial\mathcal{L}}{\partial\Phi}=-m^2\Phi$, and for the other term
$$
\partial_\mu\frac{\partial\mathcal{L}}{\partial(\partial_\mu\Phi)}=-\frac{1}{2}\partial_\mu\bigg(\frac{\partial}{\partial(\partial_\mu\Phi)}\bigg)\underbrace{(\partial_\nu\Phi g^{\nu\alpha}\partial_\alpha\Phi)}_{\text{New free index, $\nu$}}=-\frac{1}{2}\partial_\mu g^{\nu \alpha}(\delta^{\mu}_\nu\partial_\alpha\Phi+\delta^\mu_\alpha \partial_\nu\Phi=-\frac{1}{2}\partial_\mu(\partial^\mu\Phi+\partial^\mu\Phi)=-\partial_\mu\partial^\mu\Phi.
$$
My question is, is it correct that I have to introduce the free index $\nu$, or are there easier ways to do this?

REPLY [3 votes]: My question is, is it correct that I have to introduce the free index $\nu$
  , or are there easier ways to do this?

You didn't introduce a free index $\nu$ as it is contracted with another one. A free index means that the index is not summed over. What you did was introduce a $dummy$ index to sum over.

The answer to your question, however, is no there is not an easier was to do this. In quantum field theory, this is as easy as it gets. The way to prove the derivative of $(\partial \Phi)^2$ is to do precisely what you did by using the definition $\partial_\mu \Phi \partial_\nu \Phi g^{\mu\nu}$ and then use the product rule.
The resulting Klein Gordon equation should not depend on what convention you use for the metric, as you can just multiply by a minus sign to get the relative minus signs correct.

The above, however, may give you the impression that equations of motion will not "look" different in different metrics. But that would be wrong. Maxwells equations are a fine example of this.
$$
\partial_\mu F^{\mu\nu} = j^\nu \qquad (+---)
$$
and
$$
\partial_\mu F^{\mu\nu} = -j^\nu \qquad (-+++).
$$
The equations look different but they are not. Indeed the "extra" minus sign in the latter equation comes from the fact that $A_\mu = (-\Phi, \mathbf{A})$ in the $(-+++)$ convention. So the equations are identical. I think that this answer may be of some use.


TITLE: Proof for if $(x-a_1)(x-a_2)...(x-a_n)=(x-b_1)(x-b_2)...(x-b_n)$, then $a_k=b_k$ for all $k$.
QUESTION [1 upvotes]: So I tried proving the equality above. This is my proof:
We prove the equation by induction. If $n=1$, the equality holds. Suppose that it holds for $n=k$. Then $x-a_{k+1}=x-b_{k+1}$ whenever $x$ is not equal to $a_1,...,a_k$. Then $a_{k+1}=b_{k+1} $.

REPLY [0 votes]: If $$(x-a_1)(x-a_2)...(x-a_n)=(x-b_1)(x-b_2)...(x-b_n)$$ is true $\forall x$, and $$(x-a_1)(x-a_2)...(x-a_n)(x-a)=(x-b_1)(x-b_2)...(x-b_n)(x-b)$$ is true $\forall x$, then $\forall x\notin\{a_1,\dots,a_n,a,b\}$:
$(x-a)=\frac{(x-b_1)(x-b_2)...(x-b_n)}{(x-a_1)(x-a_2)...(x-a_n)}(x-b)$
$\therefore x-a=x-b \qquad\forall x\notin\{a_1,\dots,a_n,a,b\}$
$\therefore a=b$.


TITLE: multiple knapsack problem?
QUESTION [2 upvotes]: I have a weight X. This should be distributed into multiple knapsacks w1...wY.
It should be distributed to the largest knapsacks first and smallest last.
Yet the optimal distribution should be found leaving ideally the smallest unused space.
Example:
X = 17 -> w7, w5 -> w7 = 3, w5 = 0 -> unused 4 (wrong)
X = 17 -> w7, w5 -> w7 = 2, w5 = 1 -> unused 2 (wrong)
X = 17 -> w7, w5 -> w7 = 1, w5 = 2 -> unused 0 (correct)

X = 15 -> w7, w5 -> w7 = 0, w5 = 3 -> unused 0 (correct)

X = 14 -> w7, w5 -> w7 = 2, w5 = 0 -> unused 0 (correct)

X = 13 -> w7, w5 -> w7 = 1, w5 = 2 -> unused 4 (wrong)
X = 13 -> w7, w5 -> w7 = 2, w5 = 0 -> unused 1 (correct)

What algorithm could be used?
I think this is a variant of the knapsack problem and possibly can be solved by a variation of it?
The wikipedia article also mentions this but doesn't feature a solution.

After considering the comment, I think this should solve the problem:
Given w1...wY and weight X.
w1 + w2 + ... wY = Z

X - Z = 0 -> equal distribution
X - Z = A
    A / wY = integer
        (X - wY)/wY = count wY -> start over with w1 + w2 + ...w(Y-1), X - (A * wY) = X
    A / wY = float -> start over with w1 + w2 + ...w(Y-1), X - A = X

REPLY [1 votes]: It seems that you want to solve an integer programming problem
\begin{array}   \\  x,y \in \mathbb{Z} \\     x \ge 0 \\     y \ge 0 \\     7x + 5y -17 \ge  0 \\     7x + 5y  \to\min  \end{array}


TITLE: What is the fallacy in assuming the convergence of the series $ \sum\limits_{n=1}^{\infty} \frac{1}{n^{1 + |\sin(n)|}} $
QUESTION [1 upvotes]: So if we assume that $q = \min \{ |\sin k| : k \in \mathbb N\}$
So $q > 0$.
Then the series  $ \sum\limits_{n=1}^{\infty} \frac{1}{n^{1 + |\sin(n)|}}\leq\sum\limits_{n=1}^{\infty} \frac{1}{n^{1 + q}} $
This converges because it is a p series with power of n being greater than 1.

REPLY [4 votes]: The fallacy is that $\{|\sin k|:k\in\mathbb N\}$ doesn't have a minimum. It contains values arbitrarily close to (but not equal to) $0$. So the best lower bound you can put on the power is exactly $1$, which doesn't help determine convergence.