:: Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
:: by Hiroshi Yamazaki , Noboru Endou , Yasunari Shidama and Hiroyuki Okazaki
::
:: Received August 28, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: RINFSUP2:1
for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & Y is bounded_above holds
( X is bounded_above & sup X = upper_bound Y )
proof end;

theorem :: RINFSUP2:2
for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & X is bounded_above holds
( Y is bounded_above & sup X = upper_bound Y ) by Th1;

theorem Th3: :: RINFSUP2:3
for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & Y is bounded_below holds
( X is bounded_below & inf X = lower_bound Y )
proof end;

theorem :: RINFSUP2:4
for X being non empty Subset of ExtREAL
for Y being non empty Subset of REAL st X = Y & X is bounded_below holds
( Y is bounded_below & inf X = lower_bound Y ) by Th3;

definition
let seq be ExtREAL_sequence;
func sup seq -> Element of ExtREAL equals :: RINFSUP2:def 1
sup (rng seq);
coherence
sup (rng seq) is Element of ExtREAL
;
func inf seq -> Element of ExtREAL equals :: RINFSUP2:def 2
inf (rng seq);
coherence
inf (rng seq) is Element of ExtREAL
;
end;

:: deftheorem defines sup RINFSUP2:def 1 :
for seq being ExtREAL_sequence holds sup seq = sup (rng seq);

:: deftheorem defines inf RINFSUP2:def 2 :
for seq being ExtREAL_sequence holds inf seq = inf (rng seq);

definition
let seq be ExtREAL_sequence;
attr seq is bounded_below means :Def3: :: RINFSUP2:def 3
rng seq is bounded_below ;
attr seq is bounded_above means :Def4: :: RINFSUP2:def 4
rng seq is bounded_above ;
end;

:: deftheorem Def3 defines bounded_below RINFSUP2:def 3 :
for seq being ExtREAL_sequence holds
( seq is bounded_below iff rng seq is bounded_below );

:: deftheorem Def4 defines bounded_above RINFSUP2:def 4 :
for seq being ExtREAL_sequence holds
( seq is bounded_above iff rng seq is bounded_above );

definition
let seq be ExtREAL_sequence;
attr seq is bounded means :Def5: :: RINFSUP2:def 5
( seq is bounded_above & seq is bounded_below );
end;

:: deftheorem Def5 defines bounded RINFSUP2:def 5 :
for seq being ExtREAL_sequence holds
( seq is bounded iff ( seq is bounded_above & seq is bounded_below ) );

theorem Th5: :: RINFSUP2:5
for seq being ExtREAL_sequence
for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL
proof end;

definition
let seq be ExtREAL_sequence;
func inferior_realsequence seq -> ExtREAL_sequence means :Def6: :: RINFSUP2:def 6
for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & it . n = inf Y );
existence
ex b1 being ExtREAL_sequence st
for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & b1 . n = inf Y )
proof end;
uniqueness
for b1, b2 being ExtREAL_sequence st ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & b1 . n = inf Y ) ) & ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & b2 . n = inf Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines inferior_realsequence RINFSUP2:def 6 :
for seq, b2 being ExtREAL_sequence holds
( b2 = inferior_realsequence seq iff for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & b2 . n = inf Y ) );

definition
let seq be ExtREAL_sequence;
func superior_realsequence seq -> ExtREAL_sequence means :Def7: :: RINFSUP2:def 7
for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & it . n = sup Y );
existence
ex b1 being ExtREAL_sequence st
for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & b1 . n = sup Y )
proof end;
uniqueness
for b1, b2 being ExtREAL_sequence st ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & b1 . n = sup Y ) ) & ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & b2 . n = sup Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines superior_realsequence RINFSUP2:def 7 :
for seq, b2 being ExtREAL_sequence holds
( b2 = superior_realsequence seq iff for n being Element of NAT ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Element of NAT : n <= k } & b2 . n = sup Y ) );

theorem :: RINFSUP2:6
for seq being ExtREAL_sequence st seq is real-valued holds
seq is Real_Sequence
proof end;

theorem Th7: :: RINFSUP2:7
for seq being ExtREAL_sequence holds
( ( seq is increasing implies for n, m being Element of NAT st m < n holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st m < n holds
seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds
seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds
seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds
seq . n <= seq . m ) implies seq is non-increasing ) )
proof end;

theorem Th8: :: RINFSUP2:8
for n being Element of NAT
for seq being ExtREAL_sequence holds
( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )
proof end;

Lm1: for seq being ExtREAL_sequence holds superior_realsequence seq is non-increasing
proof end;

Lm2: for seq being ExtREAL_sequence holds inferior_realsequence seq is non-decreasing
proof end;

registration
let seq be ExtREAL_sequence;
cluster superior_realsequence seq -> non-increasing ;
coherence
superior_realsequence seq is non-increasing
by Lm1;
cluster inferior_realsequence seq -> non-decreasing ;
coherence
inferior_realsequence seq is non-decreasing
by Lm2;
end;

definition
let seq be ExtREAL_sequence;
func lim_sup seq -> Element of ExtREAL equals :: RINFSUP2:def 8
inf (superior_realsequence seq);
coherence
inf (superior_realsequence seq) is Element of ExtREAL
;
func lim_inf seq -> Element of ExtREAL equals :: RINFSUP2:def 9
sup (inferior_realsequence seq);
coherence
sup (inferior_realsequence seq) is Element of ExtREAL
;
end;

:: deftheorem defines lim_sup RINFSUP2:def 8 :
for seq being ExtREAL_sequence holds lim_sup seq = inf (superior_realsequence seq);

:: deftheorem defines lim_inf RINFSUP2:def 9 :
for seq being ExtREAL_sequence holds lim_inf seq = sup (inferior_realsequence seq);

theorem Th9: :: RINFSUP2:9
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & rseq is bounded holds
( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq )
proof end;

theorem Th10: :: RINFSUP2:10
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & rseq is bounded holds
( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq )
proof end;

theorem Th11: :: RINFSUP2:11
for seq being ExtREAL_sequence st seq is bounded holds
seq is Real_Sequence
proof end;

theorem Th12: :: RINFSUP2:12
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_above iff rseq is V64() )
proof end;

theorem Th13: :: RINFSUP2:13
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq holds
( seq is bounded_below iff rseq is V65() )
proof end;

theorem Th14: :: RINFSUP2:14
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & rseq is convergent holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq )
proof end;

theorem Th15: :: RINFSUP2:15
for seq being ExtREAL_sequence
for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds
( rseq is convergent & lim seq = lim rseq )
proof end;

theorem Th16: :: RINFSUP2:16
for k being Element of NAT
for seq being ExtREAL_sequence st seq ^\ k is convergent_to_finite_number holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) )
proof end;

theorem Th17: :: RINFSUP2:17
for k being Element of NAT
for seq being ExtREAL_sequence st seq ^\ k is convergent holds
( seq is convergent & lim seq = lim (seq ^\ k) )
proof end;

theorem Th18: :: RINFSUP2:18
for seq being ExtREAL_sequence st lim_sup seq = lim_inf seq & lim_inf seq in REAL holds
ex k being Element of NAT st seq ^\ k is bounded
proof end;

theorem Th19: :: RINFSUP2:19
for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds
ex k being Element of NAT st seq ^\ k is bounded
proof end;

theorem Th20: :: RINFSUP2:20
for k being Element of NAT
for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds
( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
proof end;

theorem :: RINFSUP2:21
for k being Element of NAT
for seq being ExtREAL_sequence st seq is convergent holds
( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )
proof end;

theorem :: RINFSUP2:22
for k being Element of NAT
for seq being ExtREAL_sequence holds
( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) )
proof end;

theorem Th23: :: RINFSUP2:23
for n being Element of NAT
for seq being ExtREAL_sequence holds
( inf seq <= seq . n & seq . n <= sup seq )
proof end;

theorem Th24: :: RINFSUP2:24
for seq being ExtREAL_sequence holds inf seq <= sup seq
proof end;

theorem Th25: :: RINFSUP2:25
for k being Element of NAT
for seq being ExtREAL_sequence st seq is non-increasing holds
( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )
proof end;

theorem Th26: :: RINFSUP2:26
for k being Element of NAT
for seq being ExtREAL_sequence st seq is non-decreasing holds
( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) )
proof end;

theorem :: RINFSUP2:27
for n being Element of NAT
for seq being ExtREAL_sequence holds
( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) )
proof end;

theorem Th28: :: RINFSUP2:28
for seq being ExtREAL_sequence
for j being Element of NAT holds
( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq )
proof end;

theorem Th29: :: RINFSUP2:29
for seq being ExtREAL_sequence
for j being Element of NAT holds
( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq )
proof end;

theorem Th30: :: RINFSUP2:30
for seq being ExtREAL_sequence
for k being Element of NAT st seq is non-increasing & -infty < seq . k & seq . k < +infty holds
( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k )
proof end;

theorem Th31: :: RINFSUP2:31
for seq being ExtREAL_sequence
for k being Element of NAT st seq is non-decreasing & -infty < seq . k & seq . k < +infty holds
( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k )
proof end;

Lm3: for seq being ExtREAL_sequence st seq is bounded & seq is non-increasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq )

proof end;

Lm4: for seq being ExtREAL_sequence st seq is bounded & seq is non-decreasing holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq )

proof end;

theorem Th32: :: RINFSUP2:32
for seq being ExtREAL_sequence st ( for n being Element of NAT holds +infty <= seq . n ) holds
seq is convergent_to_+infty
proof end;

theorem Th33: :: RINFSUP2:33
for seq being ExtREAL_sequence st ( for n being Element of NAT holds seq . n <= -infty ) holds
seq is convergent_to_-infty
proof end;

theorem Th34: :: RINFSUP2:34
for seq being ExtREAL_sequence st seq is non-increasing & -infty = inf seq holds
( seq is convergent_to_-infty & lim seq = -infty )
proof end;

theorem Th35: :: RINFSUP2:35
for seq being ExtREAL_sequence st seq is non-decreasing & +infty = sup seq holds
( seq is convergent_to_+infty & lim seq = +infty )
proof end;

theorem Th36: :: RINFSUP2:36
for seq being ExtREAL_sequence st seq is non-increasing holds
( seq is convergent & lim seq = inf seq )
proof end;

theorem Th37: :: RINFSUP2:37
for seq being ExtREAL_sequence st seq is non-decreasing holds
( seq is convergent & lim seq = sup seq )
proof end;

theorem Th38: :: RINFSUP2:38
for seq1, seq2 being ExtREAL_sequence st seq1 is convergent & seq2 is convergent & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds
lim seq1 <= lim seq2
proof end;

theorem :: RINFSUP2:39
for seq being ExtREAL_sequence holds lim_inf seq <= lim_sup seq
proof end;

Lm5: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = +infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )

proof end;

Lm6: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = -infty holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )

proof end;

Lm7: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq in REAL holds
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )

proof end;

theorem Th40: :: RINFSUP2:40
for seq being ExtREAL_sequence holds
( seq is convergent iff lim_inf seq = lim_sup seq )
proof end;

theorem :: RINFSUP2:41
for seq being ExtREAL_sequence st seq is convergent holds
( lim seq = lim_inf seq & lim seq = lim_sup seq )
proof end;