:: Inferior Limit and Superior Limit of Sequences of Real Numbers
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 29, 2005
:: Copyright (c) 2005-2018 Association of Mizar Users

Lm1: for r1, r2, s being Real st 0 < s & r1 <= r2 holds
( r1 < r2 + s & r1 - s < r2 )

proof end;

theorem Th1: :: RINFSUP1:1
for r, s, t being Real holds
( ( s - r < t & s + r > t ) iff |.(t - s).| < r )
proof end;

definition
let seq be Real_Sequence;
func upper_bound seq -> Real equals :: RINFSUP1:def 1
upper_bound (rng seq);
coherence
upper_bound (rng seq) is Real
;
end;

:: deftheorem defines upper_bound RINFSUP1:def 1 :
for seq being Real_Sequence holds upper_bound seq = upper_bound (rng seq);

definition
let seq be Real_Sequence;
func lower_bound seq -> Real equals :: RINFSUP1:def 2
lower_bound (rng seq);
coherence
lower_bound (rng seq) is Real
;
end;

:: deftheorem defines lower_bound RINFSUP1:def 2 :
for seq being Real_Sequence holds lower_bound seq = lower_bound (rng seq);

theorem Th2: :: RINFSUP1:2
for seq1, seq2 being Real_Sequence holds (seq1 + seq2) - seq2 = seq1
proof end;

theorem Th3: :: RINFSUP1:3
for r being Real
for seq being Real_Sequence holds
( r in rng seq iff - r in rng (- seq) )
proof end;

theorem Th4: :: RINFSUP1:4
for seq being Real_Sequence holds rng (- seq) = -- (rng seq)
proof end;

theorem Th5: :: RINFSUP1:5
for seq being Real_Sequence holds
( seq is V95() iff rng seq is bounded_above )
proof end;

theorem Th6: :: RINFSUP1:6
for seq being Real_Sequence holds
( seq is V96() iff rng seq is bounded_below )
proof end;

theorem Th7: :: RINFSUP1:7
for r being Real
for seq being Real_Sequence st seq is V95() holds
( r = upper_bound seq iff ( ( for n being Nat holds seq . n <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . k ) ) )
proof end;

theorem Th8: :: RINFSUP1:8
for r being Real
for seq being Real_Sequence st seq is V96() holds
( r = lower_bound seq iff ( ( for n being Nat holds r <= seq . n ) & ( for s being Real st 0 < s holds
ex k being Nat st seq . k < r + s ) ) )
proof end;

theorem Th9: :: RINFSUP1:9
for r being Real
for seq being Real_Sequence holds
( ( for n being Nat holds seq . n <= r ) iff ( seq is V95() & upper_bound seq <= r ) )
proof end;

theorem Th10: :: RINFSUP1:10
for r being Real
for seq being Real_Sequence holds
( ( for n being Nat holds r <= seq . n ) iff ( seq is V96() & r <= lower_bound seq ) )
proof end;

theorem :: RINFSUP1:11
for seq being Real_Sequence holds
( seq is V95() iff - seq is V96() )
proof end;

theorem :: RINFSUP1:12
for seq being Real_Sequence holds
( seq is V96() iff - seq is V95() )
proof end;

theorem Th13: :: RINFSUP1:13
for seq being Real_Sequence st seq is V95() holds
upper_bound seq = - (lower_bound (- seq))
proof end;

theorem Th14: :: RINFSUP1:14
for seq being Real_Sequence st seq is V96() holds
lower_bound seq = - (upper_bound (- seq))
proof end;

theorem Th15: :: RINFSUP1:15
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq2 is V96() holds
lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2)
proof end;

theorem Th16: :: RINFSUP1:16
for seq1, seq2 being Real_Sequence st seq1 is V95() & seq2 is V95() holds
upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)
proof end;

notation end;

definition
let f be Real_Sequence;
redefine attr f is nonnegative-yielding means :: RINFSUP1:def 3
for n being Nat holds f . n >= 0 ;
compatibility
( f is nonnegative iff for n being Nat holds f . n >= 0 )
proof end;
end;

:: deftheorem defines nonnegative RINFSUP1:def 3 :
for f being Real_Sequence holds
( f is nonnegative iff for n being Nat holds f . n >= 0 );

theorem Th17: :: RINFSUP1:17
for k being Nat
for seq being Real_Sequence st seq is nonnegative holds
seq ^\ k is nonnegative
proof end;

theorem Th18: :: RINFSUP1:18
for seq being Real_Sequence st seq is V96() & seq is nonnegative holds
lower_bound seq >= 0 by Th10;

theorem :: RINFSUP1:19
for seq being Real_Sequence st seq is V95() & seq is nonnegative holds
upper_bound seq >= 0
proof end;

theorem Th20: :: RINFSUP1:20
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq1 is nonnegative & seq2 is V96() & seq2 is nonnegative holds
( seq1 (#) seq2 is V96() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) )
proof end;

theorem Th21: :: RINFSUP1:21
for seq1, seq2 being Real_Sequence st seq1 is V95() & seq1 is nonnegative & seq2 is V95() & seq2 is nonnegative holds
( seq1 (#) seq2 is V95() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) )
proof end;

theorem :: RINFSUP1:22
for seq being Real_Sequence st seq is V54() & seq is V95() holds
seq is bounded ;

theorem :: RINFSUP1:23
for seq being Real_Sequence st seq is V55() & seq is V96() holds
seq is bounded ;

theorem Th24: :: RINFSUP1:24
for seq being Real_Sequence st seq is V54() & seq is V95() holds
lim seq = upper_bound seq
proof end;

theorem Th25: :: RINFSUP1:25
for seq being Real_Sequence st seq is V55() & seq is V96() holds
lim seq = lower_bound seq
proof end;

theorem :: RINFSUP1:26
for k being Nat
for seq being Real_Sequence st seq is V95() holds
seq ^\ k is V95() by SEQM_3:27;

theorem :: RINFSUP1:27
for k being Nat
for seq being Real_Sequence st seq is V96() holds
seq ^\ k is V96() by SEQM_3:28;

theorem :: RINFSUP1:28
for k being Nat
for seq being Real_Sequence st seq is bounded holds
seq ^\ k is bounded by SEQM_3:29;

theorem Th29: :: RINFSUP1:29
for seq being Real_Sequence
for n being Nat holds { (seq . k) where k is Nat : n <= k } is Subset of REAL
proof end;

theorem Th30: :: RINFSUP1:30
for k being Nat
for seq being Real_Sequence holds rng (seq ^\ k) = { (seq . n) where n is Nat : k <= n }
proof end;

theorem Th31: :: RINFSUP1:31
for seq being Real_Sequence st seq is V95() holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_above
proof end;

theorem Th32: :: RINFSUP1:32
for seq being Real_Sequence st seq is V96() holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is bounded_below
proof end;

theorem Th33: :: RINFSUP1:33
for seq being Real_Sequence st seq is bounded holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
R is real-bounded by ;

theorem Th34: :: RINFSUP1:34
for seq being Real_Sequence st seq is V54() holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n
proof end;

theorem Th35: :: RINFSUP1:35
for seq being Real_Sequence st seq is V55() holds
for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
upper_bound R = seq . n
proof end;

definition
let seq be Real_Sequence;
func inferior_realsequence seq -> Real_Sequence means :Def4: :: RINFSUP1:def 4
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
it . n = lower_bound Y;
existence
ex b1 being Real_Sequence st
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b1 . n = lower_bound Y
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b1 . n = lower_bound Y ) & ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b2 . n = lower_bound Y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def 4 :
for seq, b2 being Real_Sequence holds
( b2 = inferior_realsequence seq iff for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b2 . n = lower_bound Y );

definition
let seq be Real_Sequence;
func superior_realsequence seq -> Real_Sequence means :Def5: :: RINFSUP1:def 5
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
it . n = upper_bound Y;
existence
ex b1 being Real_Sequence st
for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b1 . n = upper_bound Y
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b1 . n = upper_bound Y ) & ( for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b2 . n = upper_bound Y ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines superior_realsequence RINFSUP1:def 5 :
for seq, b2 being Real_Sequence holds
( b2 = superior_realsequence seq iff for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b2 . n = upper_bound Y );

theorem Th36: :: RINFSUP1:36
for n being Nat
for seq being Real_Sequence holds () . n = lower_bound (seq ^\ n)
proof end;

theorem Th37: :: RINFSUP1:37
for n being Nat
for seq being Real_Sequence holds () . n = upper_bound (seq ^\ n)
proof end;

theorem Th38: :: RINFSUP1:38
for seq being Real_Sequence st seq is V96() holds
() . 0 = lower_bound seq
proof end;

theorem Th39: :: RINFSUP1:39
for seq being Real_Sequence st seq is V95() holds
() . 0 = upper_bound seq
proof end;

theorem Th40: :: RINFSUP1:40
for n being Nat
for r being Real
for seq being Real_Sequence st seq is V96() holds
( r = () . n iff ( ( for k being Nat holds r <= seq . (n + k) ) & ( for s being Real st 0 < s holds
ex k being Nat st seq . (n + k) < r + s ) ) )
proof end;

theorem Th41: :: RINFSUP1:41
for n being Nat
for r being Real
for seq being Real_Sequence st seq is V95() holds
( r = () . n iff ( ( for k being Nat holds seq . (n + k) <= r ) & ( for s being Real st 0 < s holds
ex k being Nat st r - s < seq . (n + k) ) ) )
proof end;

theorem Th42: :: RINFSUP1:42
for n being Nat
for r being Real
for seq being Real_Sequence st seq is V96() holds
( ( for k being Nat holds r <= seq . (n + k) ) iff r <= () . n )
proof end;

theorem Th43: :: RINFSUP1:43
for n being Nat
for r being Real
for seq being Real_Sequence st seq is V96() holds
( ( for m being Nat st n <= m holds
r <= seq . m ) iff r <= () . n )
proof end;

theorem Th44: :: RINFSUP1:44
for n being Nat
for r being Real
for seq being Real_Sequence st seq is V95() holds
( ( for k being Nat holds seq . (n + k) <= r ) iff () . n <= r )
proof end;

theorem Th45: :: RINFSUP1:45
for n being Nat
for r being Real
for seq being Real_Sequence st seq is V95() holds
( ( for m being Nat st n <= m holds
seq . m <= r ) iff () . n <= r )
proof end;

theorem Th46: :: RINFSUP1:46
for n being Nat
for seq being Real_Sequence st seq is V96() holds
() . n = min ((() . (n + 1)),(seq . n))
proof end;

theorem Th47: :: RINFSUP1:47
for n being Nat
for seq being Real_Sequence st seq is V95() holds
() . n = max ((() . (n + 1)),(seq . n))
proof end;

theorem Th48: :: RINFSUP1:48
for n being Nat
for seq being Real_Sequence st seq is V96() holds
() . n <= () . (n + 1)
proof end;

theorem Th49: :: RINFSUP1:49
for n being Nat
for seq being Real_Sequence st seq is V95() holds
() . (n + 1) <= () . n
proof end;

theorem Th50: :: RINFSUP1:50
for seq being Real_Sequence st seq is V96() holds
inferior_realsequence seq is V54() by Th48;

theorem Th51: :: RINFSUP1:51
for seq being Real_Sequence st seq is V95() holds
superior_realsequence seq is V55() by Th49;

theorem :: RINFSUP1:52
for n being Nat
for seq being Real_Sequence st seq is bounded holds
() . n <= () . n
proof end;

theorem Th53: :: RINFSUP1:53
for n being Nat
for seq being Real_Sequence st seq is bounded holds
() . n <= lower_bound ()
proof end;

theorem Th54: :: RINFSUP1:54
for n being Nat
for seq being Real_Sequence st seq is bounded holds
upper_bound () <= () . n
proof end;

theorem Th55: :: RINFSUP1:55
for seq being Real_Sequence st seq is bounded holds
upper_bound () <= lower_bound ()
proof end;

theorem Th56: :: RINFSUP1:56
for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )
proof end;

theorem Th57: :: RINFSUP1:57
for seq being Real_Sequence st seq is bounded holds
( inferior_realsequence seq is convergent & lim () = upper_bound () )
proof end;

theorem Th58: :: RINFSUP1:58
for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is convergent & lim () = lower_bound () )
proof end;

theorem Th59: :: RINFSUP1:59
for n being Nat
for seq being Real_Sequence st seq is V96() holds
() . n = - ((superior_realsequence (- seq)) . n)
proof end;

theorem Th60: :: RINFSUP1:60
for n being Nat
for seq being Real_Sequence st seq is V95() holds
() . n = - ((inferior_realsequence (- seq)) . n)
proof end;

theorem Th61: :: RINFSUP1:61
for seq being Real_Sequence st seq is V96() holds
inferior_realsequence seq = - (superior_realsequence (- seq))
proof end;

theorem Th62: :: RINFSUP1:62
for seq being Real_Sequence st seq is V95() holds
superior_realsequence seq = - (inferior_realsequence (- seq))
proof end;

theorem :: RINFSUP1:63
for n being Nat
for seq being Real_Sequence st seq is V54() holds
seq . n <= () . (n + 1)
proof end;

Lm2: for n being Nat
for seq being Real_Sequence st seq is V54() holds
() . n = seq . n

proof end;

theorem :: RINFSUP1:64
for seq being Real_Sequence st seq is V54() holds
inferior_realsequence seq = seq
proof end;

theorem Th65: :: RINFSUP1:65
for n being Nat
for seq being Real_Sequence st seq is V54() & seq is V95() holds
seq . n <= () . (n + 1)
proof end;

theorem Th66: :: RINFSUP1:66
for n being Nat
for seq being Real_Sequence st seq is V54() & seq is V95() holds
() . n = () . (n + 1)
proof end;

theorem Th67: :: RINFSUP1:67
for n being Nat
for seq being Real_Sequence st seq is V54() & seq is V95() holds
( () . n = upper_bound seq & superior_realsequence seq is constant )
proof end;

theorem :: RINFSUP1:68
for seq being Real_Sequence st seq is V54() & seq is V95() holds
lower_bound () = upper_bound seq
proof end;

theorem :: RINFSUP1:69
for n being Nat
for seq being Real_Sequence st seq is V55() holds
() . (n + 1) <= seq . n
proof end;

Lm3: for n being Nat
for seq being Real_Sequence st seq is V55() holds
() . n = seq . n

proof end;

theorem :: RINFSUP1:70
for seq being Real_Sequence st seq is V55() holds
superior_realsequence seq = seq
proof end;

theorem Th71: :: RINFSUP1:71
for n being Nat
for seq being Real_Sequence st seq is V55() & seq is V96() holds
() . (n + 1) <= seq . n
proof end;

theorem Th72: :: RINFSUP1:72
for n being Nat
for seq being Real_Sequence st seq is V55() & seq is V96() holds
() . n = () . (n + 1)
proof end;

theorem Th73: :: RINFSUP1:73
for n being Nat
for seq being Real_Sequence st seq is V55() & seq is V96() holds
( () . n = lower_bound seq & inferior_realsequence seq is constant )
proof end;

theorem :: RINFSUP1:74
for seq being Real_Sequence st seq is V55() & seq is V96() holds
upper_bound () = lower_bound seq
proof end;

theorem Th75: :: RINFSUP1:75
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( ( for n being Nat holds () . n <= () . n ) & ( for n being Nat holds () . n <= () . n ) )
proof end;

theorem :: RINFSUP1:76
for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq2 is V96() holds
(inferior_realsequence (seq1 + seq2)) . n >= (() . n) + (() . n)
proof end;

theorem :: RINFSUP1:77
for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V95() & seq2 is V95() holds
(superior_realsequence (seq1 + seq2)) . n <= (() . n) + (() . n)
proof end;

theorem :: RINFSUP1:78
for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq1 is nonnegative & seq2 is V96() & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= (() . n) * (() . n)
proof end;

theorem Th79: :: RINFSUP1:79
for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V96() & seq1 is nonnegative & seq2 is V96() & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= (() . n) * (() . n)
proof end;

theorem Th80: :: RINFSUP1:80
for n being Nat
for seq1, seq2 being Real_Sequence st seq1 is V95() & seq1 is nonnegative & seq2 is V95() & seq2 is nonnegative holds
(superior_realsequence (seq1 (#) seq2)) . n <= (() . n) * (() . n)
proof end;

definition
let seq be Real_Sequence;
func lim_sup seq -> Real equals :: RINFSUP1:def 6
lower_bound ();
coherence ;
end;

:: deftheorem defines lim_sup RINFSUP1:def 6 :
for seq being Real_Sequence holds lim_sup seq = lower_bound ();

definition
let seq be Real_Sequence;
func lim_inf seq -> Real equals :: RINFSUP1:def 7
upper_bound ();
coherence ;
end;

:: deftheorem defines lim_inf RINFSUP1:def 7 :
for seq being Real_Sequence holds lim_inf seq = upper_bound ();

theorem Th81: :: RINFSUP1:81
for r being Real
for seq being Real_Sequence st seq is bounded holds
( lim_inf seq <= r iff for s being Real st 0 < s holds
for n being Nat ex k being Nat st seq . (n + k) < r + s )
proof end;

theorem Th82: :: RINFSUP1:82
for r being Real
for seq being Real_Sequence st seq is bounded holds
( r <= lim_inf seq iff for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds r - s < seq . (n + k) )
proof end;

theorem :: RINFSUP1:83
for r being Real
for seq being Real_Sequence st seq is bounded holds
( r = lim_inf seq iff for s being Real st 0 < s holds
( ( for n being Nat ex k being Nat st seq . (n + k) < r + s ) & ex n being Nat st
for k being Nat holds r - s < seq . (n + k) ) )
proof end;

theorem Th84: :: RINFSUP1:84
for r being Real
for seq being Real_Sequence st seq is bounded holds
( r <= lim_sup seq iff for s being Real st 0 < s holds
for n being Nat ex k being Nat st seq . (n + k) > r - s )
proof end;

theorem Th85: :: RINFSUP1:85
for r being Real
for seq being Real_Sequence st seq is bounded holds
( lim_sup seq <= r iff for s being Real st 0 < s holds
ex n being Nat st
for k being Nat holds seq . (n + k) < r + s )
proof end;

theorem :: RINFSUP1:86
for r being Real
for seq being Real_Sequence st seq is bounded holds
( r = lim_sup seq iff for s being Real st 0 < s holds
( ( for n being Nat ex k being Nat st seq . (n + k) > r - s ) & ex n being Nat st
for k being Nat holds seq . (n + k) < r + s ) )
proof end;

theorem :: RINFSUP1:87
for seq being Real_Sequence st seq is bounded holds
lim_inf seq <= lim_sup seq by Th55;

theorem Th88: :: RINFSUP1:88
for seq being Real_Sequence holds
( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent )
proof end;

theorem :: RINFSUP1:89
for seq being Real_Sequence st seq is convergent holds
( lim seq = lim_sup seq & lim seq = lim_inf seq )
proof end;

theorem Th90: :: RINFSUP1:90
for seq being Real_Sequence st seq is bounded holds
( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) )
proof end;

theorem :: RINFSUP1:91
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )
proof end;

theorem :: RINFSUP1:92
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
( (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 end;

theorem :: RINFSUP1:93
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds
( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )
proof end;