:: 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-2011 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 b₁ 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 } & b₁ . n = inf Y )

proof end;

uniqueness
for b₁, b₂ 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 } & b₁ . 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 } & b₂ . n = inf Y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines inferior_realsequence RINFSUP2:def 6 :
for seq, b₂ being ExtREAL_sequence holds
( b₂ = 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 } & b₂ . 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 b₁ 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 } & b₁ . n = sup Y )

proof end;

uniqueness
for b₁, b₂ 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 } & b₁ . 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 } & b₂ . n = sup Y ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines superior_realsequence RINFSUP2:def 7 :
for seq, b₂ being ExtREAL_sequence holds
( b₂ = 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 } & b₂ . 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

canceled;
canceled;
canceled;
canceled;
let seq be ExtREAL_sequence;
func lim_sup seq -> Element of ExtREAL equals :: RINFSUP2:def 12
inf (superior_realsequence seq);
coherence
inf (superior_realsequence seq) is Element of ExtREAL ;
func lim_inf seq -> Element of ExtREAL equals :: RINFSUP2:def 13
sup (inferior_realsequence seq);
coherence
sup (inferior_realsequence seq) is Element of ExtREAL ;

end;

:: deftheorem RINFSUP2:def 8 :
canceled;

:: deftheorem RINFSUP2:def 9 :
canceled;

:: deftheorem RINFSUP2:def 10 :
canceled;

:: deftheorem RINFSUP2:def 11 :
canceled;

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

:: deftheorem defines lim_inf RINFSUP2:def 13 :
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 bounded_above )

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 bounded_below )

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;