:: Monotone Real Sequences. Subsequences
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

Lm1: for n, m being Element of NAT st n < m holds
ex k being Element of NAT st m = (n + 1) + k

proof end;

Lm2: for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . n < seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) & ( ( for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies for n being Element of NAT holds seq . n < seq . (n + 1) ) )

proof end;

Lm3: for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . (n + 1) < seq . n ) implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) & ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n ) )

proof end;

Lm4: for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . n <= seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n <= seq . (n + k) ) & ( ( for n, k being Element of NAT holds seq . n <= seq . (n + k) ) implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies for n being Element of NAT holds seq . n <= seq . (n + 1) ) )

proof end;

Lm5: for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . (n + 1) <= seq . n ) implies for n, k being Element of NAT holds seq . (n + k) <= seq . n ) & ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) implies for n being Element of NAT holds seq . (n + 1) <= seq . n ) )

proof end;

definition
let f be NAT -defined REAL -valued Function;
redefine attr f is increasing means :Def1: :: SEQM_3:def 1
for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n;
compatibility
( f is increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n )
proof end;
redefine attr f is decreasing means :Def2: :: SEQM_3:def 2
for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n;
compatibility
( f is decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n )
proof end;
redefine attr f is non-decreasing means :Def3: :: SEQM_3:def 3
for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n;
compatibility
( f is non-decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n )
proof end;
redefine attr f is non-increasing means :Def4: :: SEQM_3:def 4
for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n;
compatibility
( f is non-increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n )
proof end;
end;

:: deftheorem Def1 defines increasing SEQM_3:def 1 :
for f being NAT -defined REAL -valued Function holds
( f is increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n );

:: deftheorem Def2 defines decreasing SEQM_3:def 2 :
for f being NAT -defined REAL -valued Function holds
( f is decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n );

:: deftheorem Def3 defines non-decreasing SEQM_3:def 3 :
for f being NAT -defined REAL -valued Function holds
( f is non-decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n );

:: deftheorem Def4 defines non-increasing SEQM_3:def 4 :
for f being NAT -defined REAL -valued Function holds
( f is non-increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n );

Lm6: for f being Real_Sequence holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )

proof end;

Lm7: for f being Real_Sequence holds
( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) )

proof end;

Lm8: for f being Real_Sequence holds
( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) )

proof end;

Lm9: for f being Real_Sequence holds
( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) )

proof end;

definition
let seq be Real_Sequence;
attr seq is monotone means :Def5: :: SEQM_3:def 5
( seq is non-decreasing or seq is non-increasing );
end;

:: deftheorem Def5 defines monotone SEQM_3:def 5 :
for seq being Real_Sequence holds
( seq is monotone iff ( seq is non-decreasing or seq is non-increasing ) );

theorem Th1: :: SEQM_3:1
for seq being Real_Sequence holds
( seq is increasing iff for n, m being Element of NAT st n < m holds
seq . n < seq . m )
proof end;

theorem :: SEQM_3:2
for seq being Real_Sequence holds
( seq is increasing iff for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) )
proof end;

theorem Th3: :: SEQM_3:3
for seq being Real_Sequence holds
( seq is decreasing iff for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n )
proof end;

theorem Th4: :: SEQM_3:4
for seq being Real_Sequence holds
( seq is decreasing iff for n, m being Element of NAT st n < m holds
seq . m < seq . n )
proof end;

theorem Th5: :: SEQM_3:5
for seq being Real_Sequence holds
( seq is non-decreasing iff for n, k being Element of NAT holds seq . n <= seq . (n + k) )
proof end;

theorem Th6: :: SEQM_3:6
for seq being Real_Sequence holds
( seq is non-decreasing iff for n, m being Element of NAT st n <= m holds
seq . n <= seq . m )
proof end;

theorem Th7: :: SEQM_3:7
for seq being Real_Sequence holds
( seq is non-increasing iff for n, k being Element of NAT holds seq . (n + k) <= seq . n )
proof end;

theorem Th8: :: SEQM_3:8
for seq being Real_Sequence holds
( seq is non-increasing iff for n, m being Element of NAT st n <= m holds
seq . m <= seq . n )
proof end;

::
:: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES
::
theorem :: SEQM_3:9
for seq being Real_Sequence st seq is increasing holds
for n being Element of NAT st 0 < n holds
seq . 0 < seq . n by Th1;

theorem :: SEQM_3:10
for seq being Real_Sequence st seq is decreasing holds
for n being Element of NAT st 0 < n holds
seq . n < seq . 0 by Th4;

theorem Th11: :: SEQM_3:11
for seq being Real_Sequence st seq is non-decreasing holds
for n being Element of NAT holds seq . 0 <= seq . n by Th6;

theorem Th12: :: SEQM_3:12
for seq being Real_Sequence st seq is non-increasing holds
for n being Element of NAT holds seq . n <= seq . 0 by Th8;

registration
cluster Function-like constant -> non-decreasing non-increasing for Element of K19(K20(NAT,REAL));
coherence
for b1 being PartFunc of NAT,REAL st b1 is constant holds
( b1 is non-decreasing & b1 is non-increasing )
proof end;
cluster Function-like non-decreasing non-increasing -> constant for Element of K19(K20(NAT,REAL));
coherence
for b1 being PartFunc of NAT,REAL st b1 is non-decreasing & b1 is non-increasing holds
b1 is constant
proof end;
end;

Lm10: ( incl NAT is increasing & incl NAT is natural-valued )
proof end;

Lm11: ( id NAT is increasing & id NAT is natural-valued )
;

registration
cluster Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued natural-valued increasing for Element of K19(K20(NAT,REAL));
existence
ex b1 being Real_Sequence st
( b1 is increasing & b1 is natural-valued )
by Lm10;
end;

registration
cluster Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing for Element of K19(K20(NAT,NAT));
existence
ex b1 being sequence of NAT st b1 is increasing
by Lm11;
end;

Lm12: for f being sequence of NAT holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )

proof end;

theorem :: SEQM_3:13
for seq being Real_Sequence holds
( seq is sequence of NAT iff for n being Element of NAT holds seq . n is Element of NAT )
proof end;

registration
let Nseq be increasing sequence of NAT;
let k be Element of NAT ;
cluster Nseq ^\ k -> ext-real-valued natural-valued increasing for ext-real-valued Function;
coherence
for b1 being ext-real-valued Function st b1 = Nseq ^\ k holds
( b1 is increasing & b1 is natural-valued )
proof end;
end;

definition
let f be Real_Sequence;
redefine attr f is increasing means :: SEQM_3:def 6
for n being Element of NAT holds f . n < f . (n + 1);
compatibility
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
by Lm6;
redefine attr f is decreasing means :: SEQM_3:def 7
for n being Element of NAT holds f . n > f . (n + 1);
compatibility
( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) )
by Lm7;
redefine attr f is non-decreasing means :: SEQM_3:def 8
for n being Element of NAT holds f . n <= f . (n + 1);
compatibility
( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) )
by Lm8;
redefine attr f is non-increasing means :: SEQM_3:def 9
for n being Element of NAT holds f . n >= f . (n + 1);
compatibility
( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) )
by Lm9;
end;

:: deftheorem defines increasing SEQM_3:def 6 :
for f being Real_Sequence holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) );

:: deftheorem defines decreasing SEQM_3:def 7 :
for f being Real_Sequence holds
( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) );

:: deftheorem defines non-decreasing SEQM_3:def 8 :
for f being Real_Sequence holds
( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) );

:: deftheorem defines non-increasing SEQM_3:def 9 :
for f being Real_Sequence holds
( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) );

theorem :: SEQM_3:14
for Nseq being increasing sequence of NAT
for n being Element of NAT holds n <= Nseq . n
proof end;

registration
let s be Real_Sequence;
let k be Nat;
cluster s ^\ k -> real-valued ;
coherence
s ^\ k is real-valued
;
end;

theorem Th15: :: SEQM_3:15
for k being Element of NAT
for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
proof end;

theorem Th16: :: SEQM_3:16
for k being Element of NAT
for seq being Real_Sequence holds (- seq) ^\ k = - (seq ^\ k)
proof end;

theorem :: SEQM_3:17
for k being Element of NAT
for seq, seq1 being Real_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
proof end;

theorem Th18: :: SEQM_3:18
for k being Element of NAT
for seq being Real_Sequence holds (seq ") ^\ k = (seq ^\ k) "
proof end;

theorem Th19: :: SEQM_3:19
for k being Element of NAT
for seq, seq1 being Real_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)
proof end;

theorem :: SEQM_3:20
for k being Element of NAT
for seq, seq1 being Real_Sequence holds (seq /" seq1) ^\ k = (seq ^\ k) /" (seq1 ^\ k)
proof end;

theorem :: SEQM_3:21
for k being Element of NAT
for r being real number
for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)
proof end;

::
:: SUBSEQUENCES OF MONOTONE SEQUENCE
:: SUBSEQUENCE OF BOUNDED SEQUENCE
::
theorem :: SEQM_3:22
for seq, seq1 being Real_Sequence st seq is increasing & seq1 is subsequence of seq holds
seq1 is increasing
proof end;

theorem :: SEQM_3:23
for seq, seq1 being Real_Sequence st seq is decreasing & seq1 is subsequence of seq holds
seq1 is decreasing
proof end;

theorem Th24: :: SEQM_3:24
for seq, seq1 being Real_Sequence st seq is non-decreasing & seq1 is subsequence of seq holds
seq1 is non-decreasing
proof end;

theorem Th25: :: SEQM_3:25
for seq, seq1 being Real_Sequence st seq is non-increasing & seq1 is subsequence of seq holds
seq1 is non-increasing
proof end;

theorem :: SEQM_3:26
for seq, seq1 being Real_Sequence st seq is monotone & seq1 is subsequence of seq holds
seq1 is monotone
proof end;

theorem Th27: :: SEQM_3:27
for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is subsequence of seq holds
seq1 is bounded_above
proof end;

theorem Th28: :: SEQM_3:28
for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is subsequence of seq holds
seq1 is bounded_below
proof end;

theorem :: SEQM_3:29
for seq, seq1 being Real_Sequence st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded
proof end;

::
:: OPERATIONS ON MONOTONE SEQUENCES
::
theorem :: SEQM_3:30
for r being real number
for seq being Real_Sequence holds
( ( seq is increasing & 0 < r implies r (#) seq is increasing ) & ( 0 = r implies r (#) seq is constant ) & ( seq is increasing & r < 0 implies r (#) seq is decreasing ) )
proof end;

theorem :: SEQM_3:31
for r being real number
for seq being Real_Sequence holds
( ( seq is decreasing & 0 < r implies r (#) seq is decreasing ) & ( seq is decreasing & r < 0 implies r (#) seq is increasing ) )
proof end;

theorem :: SEQM_3:32
for r being real number
for seq being Real_Sequence holds
( ( seq is non-decreasing & 0 <= r implies r (#) seq is non-decreasing ) & ( seq is non-decreasing & r <= 0 implies r (#) seq is non-increasing ) )
proof end;

theorem :: SEQM_3:33
for r being real number
for seq being Real_Sequence holds
( ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) & ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing ) )
proof end;

theorem Th34: :: SEQM_3:34
for seq, seq1 being Real_Sequence holds
( ( seq is increasing & seq1 is increasing implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is decreasing implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing ) )
proof end;

theorem :: SEQM_3:35
for seq, seq1 being Real_Sequence holds
( ( seq is increasing & seq1 is constant implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is constant implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is constant implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is constant implies seq + seq1 is non-increasing ) )
proof end;

::
:: OPERATIONS ON BOUNDED SEQUENCES
::
theorem Th36: :: SEQM_3:36
for r being real number
for seq being Real_Sequence holds
( ( seq is bounded_above & 0 < r implies r (#) seq is bounded_above ) & ( 0 = r implies r (#) seq is bounded ) & ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below ) )
proof end;

theorem :: SEQM_3:37
for seq being Real_Sequence holds
( ( seq is bounded implies for r being real number holds r (#) seq is bounded ) & ( seq is bounded implies - seq is bounded ) & ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) )
proof end;

::
:: OPERATIONS ON BOUNDED & MONOTONE SEQUENCES
::
theorem :: SEQM_3:38
for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is non-increasing holds
seq + seq1 is bounded_above
proof end;

theorem :: SEQM_3:39
for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is non-decreasing holds
seq + seq1 is bounded_below
proof end;

theorem :: SEQM_3:40
( incl NAT is increasing & incl NAT is natural-valued ) by Lm10;

registration
cluster -> natural-valued for FinSequence of NAT ;
coherence
for b1 being FinSequence of NAT holds b1 is natural-valued
;
end;

begin

theorem Th41: :: SEQM_3:41
for r, s being Real holds
( abs (r - s) = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )
proof end;

theorem :: SEQM_3:42
for i, j, n, m being Element of NAT holds
( (abs (i - j)) + (abs (n - m)) = 1 iff ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) )
proof end;

theorem :: SEQM_3:43
for n being Element of NAT holds
( n > 1 iff ex m being Element of NAT st
( n = m + 1 & m > 0 ) )
proof end;

theorem :: SEQM_3:44
for f being FinSequence
for n, m, k being Element of NAT st len f = m + 1 & n in dom f & k in Seg m & not (Del (f,n)) . k = f . k holds
(Del (f,n)) . k = f . (k + 1)
proof end;

definition
let f be FinSequence;
redefine attr f is constant means :: SEQM_3:def 10
for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m;
compatibility
( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m )
proof end;
end;

:: deftheorem defines constant SEQM_3:def 10 :
for f being FinSequence holds
( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m );

registration
cluster -> real-valued for FinSequence of REAL ;
coherence
for b1 being FinSequence of REAL holds b1 is real-valued
;
end;

registration
cluster Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued increasing V54() FinSequence-like FinSubsequence-like for FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st
( not b1 is empty & b1 is increasing )
proof end;
end;

registration
cluster Relation-like NAT -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued V54() FinSequence-like FinSubsequence-like for FinSequence of REAL ;
existence
ex b1 being FinSequence of REAL st b1 is constant
proof end;
end;

theorem Th45: :: SEQM_3:45
for v being FinSequence of REAL
for n, i, m being Element of NAT st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being Element of NAT st k in dom v & v . k = i holds
k <= m ) holds
( m + 1 in dom v & v . (m + 1) = i + 1 )
proof end;

theorem :: SEQM_3:46
for v being FinSequence of REAL
for n being Element of NAT st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) holds
( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) )
proof end;