:: Monotone Real Sequences. Subsequences
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, SEQ_1, ARYTM_3, NAT_1, CARD_1, FUNCT_1,
XXREAL_0, PARTFUN1, ORDINAL2, RELAT_1, TARSKI, VALUED_0, ARYTM_1,
VALUED_1, XXREAL_2, REAL_1, COMPLEX1, FINSEQ_1, SEQM_3, XBOOLE_0,
FINSEQ_3, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_3, FINSEQ_1, FINSEQ_3,
VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, REAL_1, COMPLEX1, NAT_1, VALUED_0;
constructors PARTFUN1, FUNCT_3, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1,
VALUED_1, SEQ_2, FINSEQ_1, RECDEF_1, RELSET_1, FINSEQ_3, COMSEQ_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
XREAL_0, MEMBERED, VALUED_0, FUNCT_2, VALUED_1, SEQ_2, RFUNCT_1, RELAT_1,
NAT_1, FINSEQ_1, CARD_1, INT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, SEQ_2, FUNCT_1, VALUED_0;
equalities VALUED_1;
expansions SEQ_2, FUNCT_1, VALUED_0, VALUED_1;
theorems FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, NAT_1, FUNCT_2, XREAL_1, XXREAL_0,
ORDINAL1, VALUED_0, VALUED_1, RELAT_1, COMPLEX1, INT_1, FINSEQ_1,
FINSEQ_3, XBOOLE_1, TARSKI, NUMBERS;
schemes NAT_1;
begin
reserve n,m,k for Nat;
reserve r,r1 for Real;
reserve f,seq,seq1 for Real_Sequence;
reserve x,y for set;
Lm1: n 0 by A1,A2;
then consider n1 be Nat such that
A3: k1=n1+1 by NAT_1:6;
reconsider n1 as Element of NAT by ORDINAL1:def 12;
take n1;
thus thesis by A2,A3;
end;
Lm2: ((for n holds seq.n f.n;
compatibility;
redefine attr f is non-decreasing means
for m,n st m in dom f & n in dom f & m <= n holds f.m <= f.n;
compatibility;
redefine attr f is non-increasing means
for m,n st m in dom f & n in dom f & m <= n holds f.m >= f.n;
compatibility;
end;
definition
let seq;
attr seq is monotone means
seq is non-decreasing or seq is non-increasing;
end;
theorem Th1:
seq is increasing iff for n,m st n non-decreasing non-increasing for PartFunc of NAT, REAL;
coherence;
cluster non-decreasing non-increasing -> constant for PartFunc of NAT, REAL;
coherence
proof
let f be PartFunc of NAT, REAL such that
A1: f is non-decreasing non-increasing;
let x,y be object;
assume
A2: x in dom f & y in dom f;
dom f c= NAT by RELAT_1:def 18;
then reconsider m = x, n = y as Element of NAT by A2;
m <= n or n <= m;
then f.m <= f.n & f.n <= f.m by A1,A2;
hence thesis by XXREAL_0:1;
end;
end;
:: DEFINITIONS OF INCREASING SEQUENCE OF NATURAL NUMBERS,
:: RESTRICTION OF SEQUENCE.
Lm6: id NAT is increasing natural-valued;
registration
cluster increasing natural-valued for Real_Sequence;
existence
proof
reconsider i = id NAT as Real_Sequence by FUNCT_2:7, NUMBERS:19;
take i;
thus thesis;
end;
end;
registration
cluster increasing for sequence of NAT;
existence by Lm6;
end;
Lm7: for f being sequence of NAT holds f is increasing iff
for n being Nat holds f.n < f.(n+1);
reserve Nseq for increasing sequence of NAT;
theorem
seq is sequence of NAT iff for n holds seq.n is Element of NAT
proof
thus seq is sequence of NAT implies for n holds seq.n is Element of NAT
by ORDINAL1:def 12;
assume
A1: for n holds seq.n is Element of NAT;
rng seq c= NAT
proof
let x be object;
assume x in rng seq;
then consider y being object such that
A2: y in dom seq and
A3: x = seq.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A2,FUNCT_2:def 1;
x = seq.y by A3;
then x is Element of NAT by A1;
hence thesis;
end;
hence thesis by FUNCT_2:6;
end;
registration
let Nseq,k;
cluster Nseq ^\ k -> increasing natural-valued for ext-real-valued Function;
coherence
proof
now
let n;
Nseq.(n+k) f.(n+1);
compatibility;
redefine attr f is non-decreasing means
for n being Nat holds f.n <= f.(n+1);
compatibility;
redefine attr f is non-increasing means
for n being Nat holds f.n >= f.(n+1);
compatibility;
end;
theorem
for n holds n<=Nseq.n
proof
defpred X[Nat] means $1<=Nseq.$1;
A1: now
let k such that
A2: X[k];
Nseq.kreal-valued;
coherence;
end;
theorem Th15:
(seq+seq1) ^\k=(seq ^\k) + (seq1 ^\k)
proof
now
let n be Element of NAT;
thus ((seq+seq1) ^\k).n=(seq+seq1).(n+k) by NAT_1:def 3
.=seq.(n+k) + seq1.(n+k) by SEQ_1:7
.=(seq ^\k).n +seq1.(n+k) by NAT_1:def 3
.=(seq ^\k).n +(seq1 ^\k).n by NAT_1:def 3
.=((seq ^\k) +(seq1 ^\k)).n by SEQ_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th16:
(-seq) ^\k=-(seq ^\k)
proof
now
let n be Element of NAT;
thus ((-seq) ^\k).n=(-seq).(n+k) by NAT_1:def 3
.=-(seq.(n+k)) by SEQ_1:10
.=-((seq ^\ k).n) by NAT_1:def 3
.=(-(seq ^\k)).n by SEQ_1:10;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq-seq1) ^\k=(seq ^\k)-(seq1 ^\k)
proof
thus (seq-seq1) ^\k=(seq ^\k)+((-seq1) ^\k) by Th15
.=(seq ^\k)-(seq1 ^\k) by Th16;
end;
theorem Th18:
(seq") ^\k=(seq ^\k)"
proof
now
let n be Element of NAT;
thus ((seq") ^\k).n=(seq").(n+k) by NAT_1:def 3
.=(seq.(n+k))" by VALUED_1:10
.=((seq ^\k).n)" by NAT_1:def 3
.=((seq ^\k)").n by VALUED_1:10;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th19:
(seq(#)seq1) ^\k=(seq ^\k)(#)(seq1 ^\k)
proof
now
let n be Element of NAT;
thus ((seq(#)seq1) ^\k).n=(seq(#)seq1).(n+k) by NAT_1:def 3
.=seq.(n+k)*seq1.(n+k) by SEQ_1:8
.=(seq ^\k).n*seq1.(n+k) by NAT_1:def 3
.=(seq ^\k).n*(seq1 ^\k).n by NAT_1:def 3
.=((seq ^\k)(#)(seq1 ^\k)).n by SEQ_1:8;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq/"seq1) ^\k=(seq ^\k)/"(seq1 ^\k)
proof
thus (seq/"seq1) ^\k=(seq ^\k)(#)((seq1") ^\k) by Th19
.=(seq ^\k)/"(seq1 ^\k) by Th18;
end;
theorem
(r(#)seq) ^\k=r(#)(seq ^\k)
proof
now
let n be Element of NAT;
thus ((r(#)seq) ^\k).n=(r(#)seq).(n+k) by NAT_1:def 3
.=r*(seq.(n+k)) by SEQ_1:9
.=r*((seq ^\k).n) by NAT_1:def 3
.=(r(#)(seq ^\k)).n by SEQ_1:9;
end;
hence thesis by FUNCT_2:63;
end;
::
:: SUBSEQUENCES OF MONOTONE SEQUENCE
:: SUBSEQUENCE OF BOUNDED SEQUENCE
::
theorem
seq is increasing & seq1 is subsequence of seq implies seq1 is increasing
proof
assume that
A1: seq is increasing and
A2: seq1 is subsequence of seq;
let n;
consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
A4: n in NAT by ORDINAL1:def 12;
Nseq.n natural-valued for FinSequence of NAT;
coherence;
end;
begin :: moved from GOBOARD1, 2010.03.01, A.T.
reserve v for FinSequence of REAL,
r,s for Real,
n,m,i,j,k for Nat;
::$CT
theorem Th40:
|.r-s.|=1 iff r>s & r=s+1 or r~~s & r=s+1 or r~~~~s;
then 0s & r=s+1 or r~~~~s & r=s+1;
hence thesis by ABSVALUE:def 1;
end;
suppose
A6: s>r & s=r+1;
thus |.r-s.|=|.-(r-s).| by COMPLEX1:52
.= 1 by A6,ABSVALUE:def 1;
end;
end;
theorem
|.i-j.|+|.n-m.|=1 iff |.i-j.|=1 & n=m or |.n-m.|=1 & i=j
proof
thus |.i-j.|+|.n-m.|=1 implies |.i-j.|=1 & n=m or |.n-m.|=1 & i=j
proof
assume
A1: |.i-j.|+|.n-m.|=1;
now
per cases;
suppose
A2: n=m;
then 1=|.i-j.|+|.0.| by A1
.=|.i-j.|+ (0 qua Real) by ABSVALUE:2
.= |.i-j.|;
hence thesis by A2;
end;
suppose
A3: n<>m;
now
per cases by A3,XXREAL_0:1;
suppose
A4: nm;
then reconsider l=n-m as Element of NAT by INT_1:5;
01 iff ex m st n=m+1 & m>0
proof
thus n>1 implies ex m st n=m+1 & m>0
proof
assume
A1: 1 0 by A1,A2;
hence thesis by A2;
end;
given m such that
A3: n=m+1 & m>0;
0+1 real-valued for FinSequence of REAL;
coherence;
end;
registration
cluster non empty increasing for FinSequence of REAL;
existence
proof
take v = <* In(0,REAL) *>;
thus v is non empty;
let n,m;
assume that
A1: n in dom v and
A2: m in dom v;
A3: dom<* 0 *> = { 1 } by FINSEQ_1:2,38;
then n = 1 by A1,TARSKI:def 1;
hence thesis by A3,A2,TARSKI:def 1;
end;
end;
registration
cluster constant for FinSequence of REAL;
existence
proof
take v = <*>REAL;
let n,m;
assume that
n in dom v and
m in dom v;
thus thesis;
end;
end;
theorem Th44:
v<>{} & rng v c= Seg n & v.(len v) = n & (for k st 1<=k & k<=len
v - 1 holds for r,s st r = v.k & s = v.(k+1) holds |.r-s.| = 1 or r=s) & i in
Seg n & i+1 in Seg n & m in dom v & v.m = i & (for k st k in dom v & v.k = i
holds k<=m) implies m+1 in dom v & v.(m+1)=i+1
proof
assume that
A1: v<>{} and
A2: rng v c= Seg n and
A3: v.(len v) = n and
A4: for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1)
holds |.r-s.| = 1 or r=s and
A5: i in Seg n and
A6: i+1 in Seg n and
A7: m in dom v and
A8: v.m = i and
A9: for k st k in dom v & v.k = i holds k<=m;
A10: m<=len v by A7,FINSEQ_3:25;
0+1<=len v by A1,NAT_1:13;
then
A11: len v in dom v by FINSEQ_3:25;
reconsider r=v.(m+1) as Real;
A12: i<=n by A5,FINSEQ_1:1;
A13: 1<=m by A7,FINSEQ_3:25;
A14: i+1<=n by A6,FINSEQ_1:1;
A15: now
assume not m+1 in dom v;
then 1>m+1 or m+1>len v by FINSEQ_3:25;
then
A16: len v <=m by NAT_1:11,13;
ir & i=r+1;
defpred P[set] means for k,r st k=$1 & k>0 & m+k in dom v & r=v.(m+k
) holds r~~*0 and
A26: m+j in dom v and
A27: s=v.(m+j);
now
per cases;
suppose
k=0;
hence thesis by A21,A24,A27;
end;
suppose
A28: k<>0;
A29: m+k<=m+k+1 by NAT_1:11;
m<=m+k by NAT_1:11;
then
A30: 1<=m+k by A13,XXREAL_0:2;
A31: m+(k+1)<=len v by A24,A26,FINSEQ_3:25;
then m+k<=len v by A29,XXREAL_0:2;
then
A32: m+k in dom v by A30,FINSEQ_3:25;
then v.(m+k) in rng v by FUNCT_1:def 3;
then v.(m+k) in Seg n by A2;
then reconsider r1=v.(m+k) as Element of NAT;
A33: r1**s & r1=s+1;
hence thesis by A33,XXREAL_0:2;
end;
suppose
r1*~~{} & rng v c= Seg n & v.1 = 1 & v.(len v) = n & (for k st 1<=k & k
<=len v - 1 holds for r,s st r = v.k & s = v.(k+1) holds |.r-s.| = 1 or r=s)
implies (for i st i in Seg n ex k st k in dom v & v.k = i) & for m,k,i,r st m
in dom v & v.m = i & (for j st j in dom v & v.j = i holds j<=m) & m{} and
A2: rng v c= Seg n and
A3: v.1 = 1 and
A4: v.(len v) = n and
A5: for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1)
holds |.r-s.| = 1 or r=s;
defpred P[Nat] means
$1 in Seg n implies ex k st k in dom v & v.k = $1;
A6: 0+1<=len v by A1,NAT_1:13;
then
A7: len v in dom v by FINSEQ_3:25;
A8: for i st P[i] holds P[i+1]
proof
let i such that
A9: i in Seg n implies ex k st k in dom v & v.k = i;
assume
A10: i+1 in Seg n;
now
per cases;
suppose
A11: i = 0;
take k=1;
thus k in dom v & v.k = i+1 by A3,A6,A11,FINSEQ_3:25;
end;
suppose
A12: i<>0;
defpred R[set] means $1 in dom v & v.$1 = i;
A13: for k be Nat holds R[k] implies k<=len v by FINSEQ_3:25;
i+1<=n by A10,FINSEQ_1:1;
then
A14: i<=n by NAT_1:13;
A15: 0+1<=i by A12,NAT_1:13;
then
A16: ex k be Nat st R[k] by A9,A14,FINSEQ_1:1;
consider m be Nat such that
A17: R[m] & for k be Nat st R[k] holds k<=m from NAT_1:sch 6(A13,
A16);
reconsider m as Element of NAT by ORDINAL1:def 12;
take k = m+1;
i in Seg n by A15,A14,FINSEQ_1:1;
hence k in dom v & v.k = i+1 by A1,A2,A4,A5,A10,A17,Th44;
end;
end;
hence thesis;
end;
A18: P[0] by FINSEQ_1:1;
thus for i holds P[i] from NAT_1:sch 2(A18,A8);
let m,k,i,r;
assume that
A19: m in dom v and
A20: v.m = i and
A21: for j st j in dom v & v.j = i holds j<=m and
A22: mn;
defpred P[set] means for j,s st j=$1 & j>0 & m+j in dom v & s=v.(m+j)
holds i~~~~0 and
A35: m+j in dom v and
A36: s=v.(m+j);
per cases;
suppose
k=0;
hence thesis by A30,A33,A36,NAT_1:13;
end;
suppose
A37: k<>0;
m<=m+k by NAT_1:11;
then
A38: 1<=m+k by A26,XXREAL_0:2;
s in rng v by A35,A36,FUNCT_1:def 3;
then s in Seg n by A2;
then reconsider s1=s as Element of NAT;
A39: m+(k+1)<=len v by A33,A35,FINSEQ_3:25;
m+k<=m+k+1 by NAT_1:11;
then m+k<=len v by A39,XXREAL_0:2;
then
A40: m+k in dom v by A38,FINSEQ_3:25;
then v.(m+k) in rng v by FUNCT_1:def 3;
then v.(m+k) in Seg n by A2;
then reconsider r1=v.(m+k) as Element of NAT;
A41: is & r1=s+1;
then
A45: i<=s1 by A41,NAT_1:13;
now
per cases by A45,XXREAL_0:1;
case
i~~