Copyright (c) 1999 Association of Mizar Users
environ
vocabulary ASYMPT_0, BOOLE, NEWTON, NAT_1, INT_1, POWER, SERIES_1, SQUARE_1,
ABSVALUE, SEQ_2, SEQ_1, FUNCT_1, ARYTM_1, FUNCT_2, ARYTM_3, RELAT_1,
ORDINAL2, RLVECT_1, FUNCOP_1, FRAENKEL, QC_LANG1, PROB_1, GROUP_1,
FINSEQ_1, FINSEQ_2, ZF_LANG, ASYMPT_1, FINSEQ_4, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, FUNCT_1, FUNCT_2, FRAENKEL, INT_1, NAT_1, SEQ_1, SEQ_2, RELAT_1,
NEWTON, POWER, SERIES_1, BHSP_4, PRE_CIRC, SQUARE_1, LIMFUNC1, ABSVALUE,
SEQM_3, DOMAIN_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, RVSUM_1, ASYMPT_0;
constructors SERIES_1, BHSP_4, DOMAIN_1, FINSEQ_4, ASYMPT_0, SETWISEO, SEQ_2,
PRE_CIRC, REAL_1, SFMASTR3, PARTFUN1, LIMFUNC1, PREPOWER, NAT_1,
RVSUM_1;
clusters XREAL_0, INT_1, RELSET_1, FINSEQ_2, ASYMPT_0, SEQ_1, SUBSET_1,
MEMBERED, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions ASYMPT_0;
theorems TARSKI, FUNCT_2, INT_1, NAT_1, AXIOMS, REAL_1, SEQ_1, SQUARE_1,
SEQ_2, ABSVALUE, REAL_2, FUNCOP_1, POWER, NEWTON, GROUP_4, EULER_2,
GR_CY_1, BHSP_4, SERIES_1, SEQM_3, FINSEQ_1, UNIFORM1, FINSEQ_3,
FINSEQ_4, WSIERP_1, PRE_FF, GROUP_5, SCMFSA9A, RVSUM_1, FINSEQ_2,
ASYMPT_0, FRAENKEL, RELSET_1, XREAL_0, XBOOLE_0, XCMPLX_0, XCMPLX_1;
schemes FUNCT_2, SEQ_1, INT_2, NAT_1, RECDEF_1;
begin :: Examples from the text
definition
cluster -> non negative Element of NAT;
coherence by NAT_1:18;
end;
reserve c, c1, c2, d, d1, d2, e for Real,
i, k, n, m, N, n1, n2, N0, N1, N2, N3, M for Nat,
x for set;
Lm1:
for n st n >= 2 holds 2 to_power n > n+1
proof defpred _P[Nat] means 2 to_power $1 > $1+1;
2 to_power 2 = 2^2 by POWER:53
.= 2*2 by SQUARE_1:def 3
.= 4;
then A1: _P[2];
A2: for k st k >= 2 & _P[k] holds _P[k+1] proof
let k such that
k >= 2 and
A3: 2 to_power k > k+1;
2 to_power (k+1) = (2 to_power k)*(2 to_power 1) by POWER:32
.= (2 to_power k)*2 by POWER:30
.= (2 to_power k) + (2 to_power k) by XCMPLX_1:11;
then A4: 2 to_power (k+1) > (k+1) + (2 to_power k) by A3,REAL_1:53;
2 to_power k > 0 by POWER:39;
then 2 to_power k >= 0 + 1 by INT_1:20;
then (k+1) + (2 to_power k) >= (k+1) + 1 by AXIOMS:24;
hence 2 to_power (k+1) > (k+1) + 1 by A4,AXIOMS:22;
end;
for n st n >= 2 holds _P[n] from Ind1(A1, A2);
hence thesis;
end;
theorem
for t,t1 being Real_Sequence st
(t.0 = 0 & (for n st n > 0 holds
t.n = 12*(n to_power 3)*log(2,n) - 5*n^2 + (log(2,n))^2
+36)) &
(t1.0 = 0 & (for n st n > 0 holds t1.n = (n to_power 3)*log(2,n)))
ex s,s1 being eventually-positive Real_Sequence
st s = t & s1 = t1 & s in Big_Oh(s1)
proof
let f,g be Real_Sequence such that
A1: f.0 = 0 & (for n st n > 0 holds
f.n = 12*(n to_power 3)*log(2,n) - 5*n^2 + (log(2,n))^2
+ 36)
and
A2: g.0 = 0 & (for n st n > 0 holds g.n = (n to_power 3)*log(2,n));
f is eventually-positive proof
take 3;
let n; assume
A3: n >= 3;
then n > 1 by AXIOMS:22;
then A4: n to_power 3 > n to_power 2 by POWER:44;
A5: n to_power 2 > 0 by A3,POWER:39;
A6: log(2,n) >= log(2,3) by A3,PRE_FF:12;
log(2,3) > log(2,2) by POWER:65;
then log(2,3) > 1 by POWER:60;
then log(2,n) > 1 by A6,AXIOMS:22;
then (n to_power 3)*log(2,n) > (n to_power 2)*1 by A4,A5,REAL_2:199;
then 12*((n to_power 3)*log(2,n)) > 5*(n to_power 2) by A5,REAL_2:199;
then 12*(n to_power 3)*log(2,n) > 5*(n to_power 2) by XCMPLX_1:4;
then 12*(n to_power 3)*log(2,n) > 5*n^2 + 0 by POWER:53;
then A7: 12*(n to_power 3)*log(2,n) - 5*n^2 > 0 by REAL_1:86;
(log(2,n))^2 >= 0 by SQUARE_1:72;
then (12*(n to_power 3)*log(2,n)-5*n^2)+(log(2,n))^2>0+0 by A7,REAL_1:
67;
then (12*(n to_power 3)*log(2,n)-5*n^2)+(log(2,n))^2+36 > 0+0 by REAL_1
:67;
hence f.n > 0 by A1,A3;
end;
then reconsider f as eventually-positive Real_Sequence;
g is eventually-positive proof
take 2;
let n; assume
A8: n >= 2;
then log(2,n) >= log(2,2) by PRE_FF:12;
then A9: log(2,n) >= 1 by POWER:60;
n to_power 3 > 0 by A8,POWER:39;
then (n to_power 3)*log(2,n) > (n to_power 3)*0 by A9,REAL_1:70;
hence g.n > 0 by A2,A8;
end;
then reconsider g as eventually-positive Real_Sequence;
take f, g;
ex s being Real_Sequence st
(s.0 = 0 & (for n st n > 0 holds s.n = 12*(n to_power 3)*log(2,n) - 5*n^2
))
proof
defpred P[Nat,Real] means
($1 = 0 implies $2 = 0) &
($1 > 0 implies $2 = 12*($1 to_power 3)*log(2,$1) - 5*($1)^2);
A10: for x being Element of NAT ex y being Element of REAL st P[x,y] proof
let n;
n = 0 or n > 0;
hence thesis;
end;
consider h being Function of NAT,REAL such that
A11: for x being Element of NAT holds P[x,h.x] from FuncExD(A10);
take h;
thus h.0 = 0 by A11;
let n; thus thesis by A11;
end;
then consider p being Real_Sequence such that
A12: p.0 = 0 &
(for n st n > 0 holds p.n = 12*(n to_power 3)*log(2,n) - 5*n^2);
p is eventually-positive proof
take 3;
let n; assume
A13: n >= 3;
then n > 1 by AXIOMS:22;
then A14: n to_power 3 > n to_power 2 by POWER:44;
A15: n to_power 2 > 0 by A13,POWER:39;
A16: log(2,n) >= log(2,3) by A13,PRE_FF:12;
log(2,3) > log(2,2) by POWER:65;
then log(2,3) > 1 by POWER:60;
then log(2,n) > 1 by A16,AXIOMS:22;
then (n to_power 3)*log(2,n) > (n to_power 2)*1 by A14,A15,REAL_2:199;
then 12*((n to_power 3)*log(2,n)) > 5*(n to_power 2) by A15,REAL_2:199
;
then 12*(n to_power 3)*log(2,n) > 5*(n to_power 2) by XCMPLX_1:4;
then 12*(n to_power 3)*log(2,n) > 5*n^2 + 0 by POWER:53;
then 12*(n to_power 3)*log(2,n) - 5*n^2 > 0 by REAL_1:86;
hence p.n > 0 by A12,A13;
end;
then reconsider p as eventually-positive Real_Sequence;
ex s being Real_Sequence st
s.0 = 0 & (for n st n > 0 holds s.n = (log(2,n))^2 + 36) proof
defpred P[Nat,Real] means
($1 = 0 implies $2 = 0) & ($1 > 0 implies $2 = (log(2,$1))^2 + 36);
A17: for x being Element of NAT ex y being Element of REAL st P[x,y] proof
let n;
per cases;
suppose n = 0; hence thesis;
suppose n > 0; hence thesis;
end;
consider h being Function of NAT,REAL such that
A18: for x being Element of NAT holds P[x,h.x] from FuncExD(A17);
take h; thus thesis by A18;
end;
then consider q being Real_Sequence such that
A19: q.0 = 0 & (for n st n > 0 holds q.n = (log(2,n))^2 + 36);
q is eventually-positive proof
take 1;
let n; assume A20: n >= 1;
(log(2,n))^2 >= 0 by SQUARE_1:72;
then (log(2,n))^2 + 36 > 0+0 by REAL_1:67;
hence q.n > 0 by A19,A20;
end;
then reconsider q as eventually-positive Real_Sequence;
set t = max(p,q);
for n holds f.n = p.n + q.n proof
let n;
thus f.n = p.n + q.n proof
per cases;
suppose n = 0;
hence thesis by A1,A12,A19;
suppose
A21: n > 0;
then p.n = 12*(n to_power 3)*log(2,n) - 5*n^2 by A12;
then p.n + q.n = (12*(n to_power 3)*log(2,n)-5*n^2)+((log(2,n))^2
+36) by A19,A21
.= 12*(n to_power 3)*log(2,n)-5*n^2+(log(2,n))^2
+36 by XCMPLX_1:1;
hence thesis by A1,A21;
end;
end;
then A22: Big_Oh(f) = Big_Oh(p+q) by SEQ_1:11
.= Big_Oh(t) by ASYMPT_0:9;
4 = 2*2
.= 2^2 by SQUARE_1:def 3
.= 2 to_power 2 by POWER:53;
then A23: log(2,4) = 2*log(2,2) by POWER:63
.= 2*1 by POWER:60
.= 2;
A24:7 = 12 - 5;
A25: for n st n >= 4 holds 7*n^2 > q.n proof
defpred _P[Nat] means 7*$1^2 > q.$1;
A26: _P[4] proof
A27: 7*4^2 = 7*(4*4) by SQUARE_1:def 3
.= 112;
q.4 = 2^2 + 36 by A19,A23
.= 2*2 + 36 by SQUARE_1:def 3
.= 40;
hence thesis by A27;
end;
A28: for k st k >= 4 & _P[k] holds _P[k+1] proof
let k such that
A29: k >= 4 and
A30: 7*k^2 > q.k;
A31: q.k = (log(2,k))^2 + 36 by A19,A29;
7*(k+1)^2 = 7*(k^2 + 2*k + 1) by SQUARE_1:65
.= 7*(k^2 + (2*k + 1)) by XCMPLX_1:1
.= 7*k^2 + (7*(2*k + 1)) by XCMPLX_1:8
.= 7*k^2 + (7*(2*k) + 7*1) by XCMPLX_1:8;
then A32: 7*(k+1)^2 > q.k + (7*(2*k) + 7*1) by A30,REAL_1:53;
A33: q.(k+1) = (log(2,k+1))^2 + 36 by A19;
k >= 1 by A29,AXIOMS:22;
then k+k >= k+1 by AXIOMS:24;
then A34: log(2,k+k) >= log(2,k+1) by PRE_FF:12;
k+1 >= 4+0 by A29,REAL_1:67;
then log(2,k+1) >= 2 by A23,PRE_FF:12;
then (log(2,k+k))^2 >= (log(2,k+1))^2 by A34,SQUARE_1:77;
then A35: q.(k+1) <= (log(2,k+k))^2 + 36 by A33,AXIOMS:24;
log(2,k+k) = log(2,2*k) by XCMPLX_1:11;
then log(2,k+k) = log(2,k) + log(2,2) by A29,POWER:61;
then A36: (log(2,k+k))^2 = (log(2,k) + 1)^2 by POWER:60
.= (log(2,k))^2 + 2*log(2,k) + 1 by SQUARE_1:65;
k >= 2 by A29,AXIOMS:22;
then A37: 2 to_power k > k + 1 by Lm1;
A38: log(2,k) >= 2 by A23,A29,PRE_FF:12;
k+1 > k+0 by REAL_1:67;
then 2 to_power k > k by A37,AXIOMS:22;
then log(2,2 to_power k) > log(2,k) by A29,POWER:65;
then k*log(2,2) > log(2,k) by POWER:63;
then k*1 > log(2,k) by POWER:60;
then 14*k > 2*log(2,k) by A38,REAL_2:199;
then (7*2)*k + 7 > 2*log(2,k) + 1 by REAL_1:67;
then 7*(2*k) + 7 > 2*log(2,k) + 1 by XCMPLX_1:4;
then (log(2,k))^2 + (2*log(2,k) + 1) <
(log(2,k))^2 + (7*(2*k) + 7) by REAL_1:53;
then (log(2,k+k))^2 < (log(2,k))^2 + (7*(2*k) + 7) by A36,XCMPLX_1:1;
then (log(2,k+k))^2 + 36 <
((log(2,k))^2 + (7*(2*k) + 7)) + 36 by REAL_1:53;
then (log(2,k+k))^2 + 36 <
((log(2,k))^2 + 36) + (7*(2*k) + 7*1) by XCMPLX_1:1;
then q.k + (7*(2*k) + 7*1) > q.(k+1) by A31,A35,AXIOMS:22;
hence thesis by A32,AXIOMS:22;
end;
for n st n >= 4 holds _P[n] from Ind1(A26, A28);
hence thesis;
end;
A39: for n st n >= 4 holds p.n > 7*n^2 proof
let n; assume
A40: n >= 4;
then A41: p.n = 12*(n to_power 3)*log(2,n) - 5*n^2 by A12;
n > 1 by A40,AXIOMS:22;
then A42: n to_power 3 > n to_power 2 by POWER:44;
A43: n to_power 2 > 0 by A40,POWER:39;
log(2,n) >= log(2,4) by A40,PRE_FF:12;
then log(2,n) > 1 by A23,AXIOMS:22;
then (n to_power 3)*log(2,n) > (n to_power 2)*1 by A42,A43,REAL_2:199;
then 12*((n to_power 3)*log(2,n)) > 12*(n to_power 2) by REAL_1:70;
then 12*(n to_power 3)*log(2,n) > 12*(n to_power 2) by XCMPLX_1:4;
then 12*(n to_power 3)*log(2,n) > 12*n^2 by POWER:53;
then p.n > 12*n^2 - 5*n^2 by A41,REAL_1:54;
hence p.n > 7*n^2 by A24,XCMPLX_1:40;
end;
A44: for n st n >= 4 holds p.n > q.n proof
let n; assume
A45: n >= 4;
then A46: p.n > 7*n^2 by A39;
7*n^2 > q.n by A25,A45;
hence thesis by A46,AXIOMS:22;
end;
A47: for n st n >= 4 holds t.n = p.n proof
let n; assume
n >= 4;
then A48: p.n > q.n by A44;
thus t.n = max( p.n, q.n ) by ASYMPT_0:def 10
.= p.n by A48,SQUARE_1:def 2;
end;
A49: Big_Oh(g) = { s where s is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds s.n <= c*g.n & s.n >= 0 }
by ASYMPT_0:def 12;
A50: t is Element of Funcs(NAT, REAL) by FUNCT_2:11;
consider N such that
A51: for n st n >= N holds t.n > 0 by ASYMPT_0:def 6;
now let n; assume
A52: n >= max(4,N);
A53: max(4,N) >= 4 & max(4,N) >= N by SQUARE_1:46;
then A54: n >= 4 & n >= N by A52,AXIOMS:22;
then A55: t.n = p.n by A47
.= 12*(n to_power 3)*log(2,n) - 5*n^2 by A12,A52,A53;
n to_power 2 > 0 by A52,A53,POWER:39;
then n^2 > 0 by POWER:53;
then 5*n^2 > 5*0 by REAL_1:70;
then t.n <= 12*(n to_power 3)*log(2,n) - 0 by A55,REAL_1:92;
then t.n <= 12*((n to_power 3)*log(2,n)) by XCMPLX_1:4;
hence t.n <= 12*g.n by A2,A52,A53;
thus t.n >= 0 by A51,A54;
end;
then A56: t in Big_Oh(g) by A49,A50;
f in Big_Oh(f) by ASYMPT_0:10;
hence thesis by A22,A56,ASYMPT_0:12;
end;
Lm2:
for a being logbase Real, f being Real_Sequence st a > 1 &
(f.0 = 0 & (for n st n > 0 holds f.n = log(a,n)))
holds f is eventually-positive
proof
let a be logbase Real, f be Real_Sequence such that
A1: a > 1 and
A2: (f.0 = 0 & (for n st n > 0 holds f.n = log(a,n)));
A3: a > 0 & a <> 1 by ASYMPT_0:def 3;
set N = [/a\];
A4: [/a\] >= a by INT_1:def 5;
A5: N > 0 by A3,INT_1:def 5;
then reconsider N as Nat by INT_1:16;
now let n; assume
A6: n >= N+1;
N+1 > N+0 by REAL_1:67;
then n > N by A6,AXIOMS:22;
then A7: log(a,n) > log(a,N) by A1,A5,POWER:65;
log(a,N) >= log(a,a) by A1,A4,PRE_FF:12;
then log(a,n) > log(a,a) by A7,AXIOMS:22;
then log(a,n) > 0 by A3,POWER:60;
hence f.n > 0 by A2,A6;
end;
hence f is eventually-positive by ASYMPT_0:def 6;
end;
theorem
for a,b being logbase Real, f,g being Real_Sequence st a > 1 & b > 1 &
(f.0 = 0 & (for n st n > 0 holds f.n = log(a,n))) &
(g.0 = 0 & (for n st n > 0 holds g.n = log(b,n)))
holds ex s,s1 being eventually-positive Real_Sequence st
s = f & s1 = g & Big_Oh(s) = Big_Oh(s1)
proof
let a,b be logbase Real, f,g be Real_Sequence such that
A1: a > 1 and
A2: b > 1 and
A3: (f.0 = 0 & (for n st n > 0 holds f.n = log(a,n))) and
A4: (g.0 = 0 & (for n st n > 0 holds g.n = log(b,n)));
reconsider f as eventually-positive Real_Sequence by A1,A3,Lm2;
reconsider g as eventually-positive Real_Sequence by A2,A4,Lm2;
take f,g;
A5: a > 0 & a <> 1 by ASYMPT_0:def 3;
A6: b > 0 & b <> 1 by ASYMPT_0:def 3;
A7: Big_Oh(f) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 }
by ASYMPT_0:def 12;
A8: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 }
by ASYMPT_0:def 12;
now let x be set;
hereby assume x in Big_Oh(f);
then consider t being Element of Funcs(NAT, REAL) such that
A9: x = t and
A10: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A7;
consider c,N such that
A11: c > 0 and
A12: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A10;
log(a,b) > log(a,1) by A1,A2,POWER:65;
then log(a,b) > 0 by A5,POWER:59;
then A13: c*log(a,b) > c*0 by A11,REAL_1:70;
now take N1 = N+1; let n; assume
A14: n >= N1;
N+1 > N+0 by REAL_1:67;
then A15: n > N by A14,AXIOMS:22;
then A16: t.n <= c*f.n by A12;
f.n = log(a,n) by A3,A14
.= log(a,b)*log(b,n) by A5,A6,A14,POWER:64;
then t.n <= (c*log(a,b))*log(b,n) by A16,XCMPLX_1:4;
hence t.n <= (c*log(a,b))*g.n by A4,A14;
thus t.n >= 0 by A12,A15;
end;
hence x in Big_Oh(g) by A8,A9,A13;
end;
assume x in Big_Oh(g);
then consider t being Element of Funcs(NAT, REAL) such that
A17: x = t and
A18: ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A8;
consider c,N such that
A19: c > 0 and
A20: for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A18;
log(b,a) > log(b,1) by A1,A2,POWER:65;
then log(b,a) > 0 by A6,POWER:59;
then A21: c*log(b,a) > c*0 by A19,REAL_1:70;
now take N1 = N+1; let n; assume
A22: n >= N1;
N+1 > N+0 by REAL_1:67;
then A23: n > N by A22,AXIOMS:22;
then A24: t.n <= c*g.n by A20;
g.n = log(b,n) by A4,A22
.= log(b,a)*log(a,n) by A5,A6,A22,POWER:64;
then t.n <= (c*log(b,a))*log(a,n) by A24,XCMPLX_1:4;
hence t.n <= (c*log(b,a))*f.n by A3,A22;
thus t.n >= 0 by A20,A23;
end;
hence x in Big_Oh(f) by A7,A17,A21;
end;
hence thesis by TARSKI:2;
end;
definition let a,b,c be Real;
func seq_a^(a,b,c) -> Real_Sequence means :Def1:
it.n = a to_power (b*n+c);
existence proof
deffunc _F(Nat) = a to_power (b*$1+c);
consider h being Function of NAT, REAL such that
A1: for n being Nat holds h.n = _F(n) from LambdaD;
take h; let n; thus h.n = a to_power (b*n+c) by A1;
end;
uniqueness proof let j,k be Real_Sequence such that
A2: for n holds j.n = a to_power (b*n+c) and
A3: for n holds k.n = a to_power (b*n+c);
now let n; thus j.n = a to_power (b*n+c) by A2 .= k.n by A3; end;
hence j = k by FUNCT_2:113;
end;
end;
definition let a be positive Real, b,c be Real;
cluster seq_a^(a,b,c) -> eventually-positive;
coherence proof
set f = seq_a^(a,b,c);
take 0;
let n; assume n >= 0;
f.n = a to_power (b*n+c) by Def1;
hence f.n > 0 by POWER:39;
end;
end;
Lm3:
for a,b,c being Real st a > 0 & c > 0 & c <> 1
holds a to_power b = c to_power (b*log(c,a))
proof
let a,b,c be Real; assume that
A1: a > 0 and
A2: c > 0 and
A3: c <> 1;
A4: a to_power b > 0 by A1,POWER:39;
log(c, a to_power b) = b*log(c,a) by A1,A2,A3,POWER:63;
hence thesis by A2,A3,A4,POWER:def 3;
end;
theorem
for a,b being positive Real st a < b
holds not seq_a^(b,1,0) in Big_Oh(seq_a^(a,1,0))
proof
let a,b be positive Real such that
A1: a < b;
set f = seq_a^(b,1,0);
set g = seq_a^(a,1,0);
A2: Big_Oh(g) = { s where s is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds s.n <= c*g.n & s.n >= 0 }
by ASYMPT_0:def 12;
hereby assume f in Big_Oh(g);
then consider s being Element of Funcs(NAT, REAL) such that
A3: s = f and
A4: ex c,N st c > 0 & for n st n >= N holds s.n <= c*g.n & s.n >= 0 by A2;
consider c,N such that
A5: c > 0 and
A6: for n st n >= N holds s.n <= c*g.n & s.n >= 0 by A4;
set d = (log(2,b) - log(2,a));
log(2,b) > log(2,a) + 0 by A1,POWER:65;
then A7: d > 0 by REAL_1:86;
set N0 = [/log(2,c) / d\];
set N1 = max( N, N0 );
A8: N1 >= N & N1 >= N0 by SQUARE_1:46;
N1 = N or N1 = N0 by SQUARE_1:49;
then reconsider N1 as Nat by A8,INT_1:16;
set n = N1 + 1;
set e = (2 to_power (n*log(2,a)));
A9: e > 0 by POWER:39;
N1 + 1 > N1 + 0 by REAL_1:67;
then A10: n > N & n > N0 by A8,AXIOMS:22;
N0 >= log(2,c) / d by INT_1:def 5;
then n > log(2,c) / d by A10,AXIOMS:22;
then n*d > (log(2,c) / d)*d by A7,REAL_1:70;
then n*d > log(2,c) by A7,XCMPLX_1:88;
then 2 to_power (n*d) > 2 to_power log(2,c) by POWER:44;
then 2 to_power (n*d) > c by A5,POWER:def 3;
then 2 to_power (n*log(2,b) - n*log(2,a)) > c by XCMPLX_1:40;
then (2 to_power (n*log(2,b))) / e > c by POWER:34;
then ((2 to_power (n*log(2,b)))/e)*e > c*e by A9,REAL_1:70;
then 2 to_power (n*log(2,b)) > c*e by A9,XCMPLX_1:88;
then b to_power n > c*(2 to_power (n*log(2,a))) by Lm3;
then A11: b to_power n > c*(a to_power n) by Lm3;
f.n <= c*g.n by A3,A6,A10;
then b to_power (1*n + 0) <= c*g.n by Def1;
hence contradiction by A11,Def1;
end;
end;
:: Example p. 84
definition
func seq_logn -> Real_Sequence means :Def2:
it.0 = 0 & (for n st n > 0 holds it.n = log(2,n));
existence proof
defpred P[Nat,Real] means
($1 = 0 implies $2 = 0) & ($1 > 0 implies $2 = log(2,$1));
A1: for x being Element of NAT ex y being Element of REAL st P[x,y] proof
let n;
per cases;
suppose n = 0; hence thesis;
suppose n > 0; hence thesis;
end;
consider h being Function of NAT,REAL such that
A2: for x being Element of NAT holds P[x,h.x] from FuncExD(A1);
take h;
thus h.0 = 0 by A2;
let n; thus thesis by A2;
end;
uniqueness proof let j,k be Real_Sequence such that
A3: j.0 = 0 & (for n st n > 0 holds j.n = log(2,n)) and
A4: k.0 = 0 & (for n st n > 0 holds k.n = log(2,n));
now let n;
per cases;
suppose n = 0;
hence j.n = k.n by A3,A4;
suppose
A5: n > 0;
then j.n = log(2,n) by A3;
hence j.n = k.n by A4,A5;
end;
hence j = k by FUNCT_2:113;
end;
end;
definition let a be Real;
func seq_n^(a) -> Real_Sequence means :Def3:
it.0 = 0 & (for n st n > 0 holds it.n = n to_power a);
existence proof
defpred P[Nat,Real] means
($1 = 0 implies $2 = 0) & ($1 > 0 implies $2 = $1 to_power a);
A1: for x being Element of NAT ex y being Element of REAL st P[x,y] proof
let n;
per cases;
suppose n = 0; hence thesis;
suppose n > 0; hence thesis;
end;
consider h being Function of NAT,REAL such that
A2: for x being Element of NAT holds P[x,h.x] from FuncExD(A1);
take h;
thus h.0 = 0 by A2;
let n; thus thesis by A2;
end;
uniqueness proof let j,k be Real_Sequence such that
A3: j.0 = 0 & (for n st n > 0 holds j.n = n to_power a) and
A4: k.0 = 0 & (for n st n > 0 holds k.n = n to_power a);
now let n;
per cases;
suppose n = 0;
hence j.n = k.n by A3,A4;
suppose
A5: n > 0;
then j.n = n to_power a by A3;
hence j.n = k.n by A4,A5;
end;
hence j = k by FUNCT_2:113;
end;
end;
definition
cluster seq_logn -> eventually-positive;
coherence proof
set f = seq_logn;
take 2;
let n; assume
A1: n >= 2;
then A2: f.n = log(2,n) by Def2;
log(2,n) >= log(2,2) by A1,PRE_FF:12;
hence f.n > 0 by A2,POWER:60;
end;
end;
definition let a be Real;
cluster seq_n^(a) -> eventually-positive;
coherence proof
set f = seq_n^(a);
take 1;
let n; assume A1: n >= 1;
then f.n = n to_power a by Def3;
hence f.n > 0 by A1,POWER:39;
end;
end;
Lm4:
for f,g being Real_Sequence, n being Nat holds (f/"g).n = f.n/g.n
proof
let f,g be Real_Sequence, n be Nat;
thus (f/"g).n = (f(#)g").n by SEQ_1:def 9 .= f.n*g".n by SEQ_1:12
.= f.n*(g.n)" by SEQ_1:def 8 .= f.n/g.n by XCMPLX_0:def 9;
end;
Lm5:
for f,g being eventually-nonnegative Real_Sequence holds
f in Big_Oh(g) & g in Big_Oh(f) iff Big_Oh(f) = Big_Oh(g)
proof
let f,g be eventually-nonnegative Real_Sequence;
hereby assume f in Big_Oh(g) & g in Big_Oh(f);
then Big_Oh(f) c= Big_Oh(g) & Big_Oh(g) c= Big_Oh(f) by ASYMPT_0:11;
hence Big_Oh(f) = Big_Oh(g) by XBOOLE_0:def 10;
end;
thus thesis by ASYMPT_0:10;
end;
theorem Th4:
for f,g being eventually-nonnegative Real_Sequence holds
Big_Oh(f) c= Big_Oh(g) & not Big_Oh(f) = Big_Oh(g) iff
f in Big_Oh(g) & not f in Big_Omega(g)
proof
let f,g be eventually-nonnegative Real_Sequence;
A1: Big_Oh(f) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 }
by ASYMPT_0:def 12;
hereby assume
A2: Big_Oh(f) c= Big_Oh(g) & not Big_Oh(f) = Big_Oh(g);
A3: f in Big_Oh(f) by ASYMPT_0:10;
now assume f in Big_Omega(g);
then g in Big_Oh(f) by ASYMPT_0:19;
hence contradiction by A2,A3,Lm5;
end;
hence f in Big_Oh(g) & not f in Big_Omega(g) by A2,A3;
end;
assume
A4: f in Big_Oh(g) & not f in Big_Omega(g);
now let x be set; assume x in Big_Oh(f);
then consider t being Element of Funcs(NAT, REAL) such that
A5: x = t and
A6: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A1;
consider c,N such that
c > 0 and
A7: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A6;
now take N; let n; assume n >= N;
hence t.n >= 0 by A7;
end;
then A8: t is eventually-nonnegative by ASYMPT_0:def 4;
t in Big_Oh(f) by A1,A6;
hence x in Big_Oh(g) by A4,A5,A8,ASYMPT_0:12;
end;
hence Big_Oh(f) c= Big_Oh(g) by TARSKI:def 3;
assume Big_Oh(f) = Big_Oh(g);
then f in Big_Oh(g) & g in Big_Oh(f) by Lm5;
hence contradiction by A4,ASYMPT_0:19;
end;
Lm6:
for a, b, c being Real st 0 < a & a <= b & c >= 0 holds
a to_power c <= b to_power c
proof
let a, b, c be Real;
assume that
A1: 0 < a and
A2: a <= b and
A3: c >= 0;
per cases by A3;
suppose c = 0;
then a to_power c = 1 & b to_power c = 1 by POWER:29;
hence thesis;
suppose
A4: c > 0;
thus thesis proof
per cases by A2,REAL_1:def 5;
suppose a = b; hence thesis;
suppose a < b; hence thesis by A1,A4,POWER:42;
end;
end;
Lm7:
2 to_power 2 = 4
proof thus 2 to_power 2 = 2^2 by POWER:53 .= 2*2 by SQUARE_1:def 3 .= 4; end;
Lm8:
2 to_power 3 = 8
proof
thus 2 to_power 3 = 2 to_power (2+1)
.= (2 to_power 2)*(2 to_power 1) by POWER:32
.= 4*2 by Lm7,POWER:30
.= 8;
end;
Lm9:
2 to_power 4 = 16
proof
thus 2 to_power 4 = 2 to_power (2+2)
.= (2 to_power 2)*(2 to_power 2) by POWER:32
.= 16 by Lm7;
thus thesis;
end;
Lm10:
2 to_power 5 = 32
proof
thus 2 to_power 5 = 2 to_power (3+2)
.= (2 to_power 3)*(2 to_power 2) by POWER:32
.= 32 by Lm7,Lm8;
end;
Lm11:
2 to_power 6 = 64
proof
thus 2 to_power 6 = 2 to_power (3+3)
.= 2 to_power 3 * 2 to_power 3 by POWER:32
.= 64 by Lm8;
end;
Lm12:
for n st n >= 4 holds 2*n + 3 < 2 to_power n
proof defpred _P[Nat] means 2*$1 + 3 < 2 to_power $1;
A1: _P[4] by Lm9;
A2: for k st k >= 4 & _P[k] holds _P[k+1] proof
let k such that
A3: k >= 4 and
A4: 2*k + 3 < 2 to_power k;
2*(k+1) + 3 = (2*k + 2*1) + 3 by XCMPLX_1:8
.= 2 + (2*k + 3) by XCMPLX_1:1;
then A5: 2*(k+1) + 3 < 2 + (2 to_power k) by A4,REAL_1:53;
k > 1 by A3,AXIOMS:22;
then 2 to_power k > 2 to_power 1 by POWER:44;
then 2 to_power k > 2 by POWER:30;
then (2 to_power k) + (2 to_power k) > 2 + (2 to_power k) by REAL_1:53;
then 2*(k+1) + 3 < (2 to_power k) + (2 to_power k) by A5,AXIOMS:22;
then 2*(k+1) + 3 < 2*(2 to_power k) by XCMPLX_1:11;
then 2*(k+1) + 3 < (2 to_power 1)*(2 to_power k) by POWER:30;
hence thesis by POWER:32;
end;
for n st n >= 4 holds _P[n] from Ind1(A1, A2);
hence thesis;
end;
Lm13:
for n st n >= 6 holds (n+1)^2 < 2 to_power n
proof defpred _P[Nat] means ($1+1)^2 < 2 to_power $1;
(6+1)^2 = 7*7 by SQUARE_1:def 3;
then A1: _P[6] by Lm11;
A2: for k st k >= 6 & _P[k] holds _P[k+1] proof
let k such that
A3: k >= 6 and
A4: (k+1)^2 < 2 to_power k;
A5: ((k+1)+1)^2 = (k+(1+1))^2 by XCMPLX_1:1
.= k^2 + 2*k*2 + 2^2 by SQUARE_1:63
.= k^2 + (2*2)*k + 2^2 by XCMPLX_1:4
.= k^2 + (2+2)*k + 4 by SQUARE_1:def 3
.= k^2 + (2*k + 2*k) + 4 by XCMPLX_1:8
.= ((k^2 + 2*k) + 2*k) + 4 by XCMPLX_1:1
.= (k^2 + 2*k) + (2*k + (3+1)) by XCMPLX_1:1
.= (k^2 + 2*k) + ((2*k + 3) + 1) by XCMPLX_1:1
.= ((k^2 + 2*k) + 1) + (2*k + 3) by XCMPLX_1:1
.= (k+1)^2 + (2*k + 3) by SQUARE_1:65;
k >= 4 by A3,AXIOMS:22;
then 2*k + 3 < 2 to_power k by Lm12;
then A6: (k+1)^2 + (2*k + 3) < (k+1)^2 + (2 to_power k) by REAL_1:53;
(k+1)^2 + (2 to_power k) <
(2 to_power k) + (2 to_power k) by A4,REAL_1:53;
then (k+1)^2 + (2*k + 3) <
(2 to_power k) + (2 to_power k) by A6,AXIOMS:22;
then ((k+1)+1)^2 < 2*(2 to_power k) by A5,XCMPLX_1:11;
then ((k+1)+1)^2 < (2 to_power 1)*(2 to_power k) by POWER:30;
hence thesis by POWER:32;
end;
for n st n >= 6 holds _P[n] from Ind1(A1, A2);
hence thesis;
end;
Lm14:
for c being Real st c > 6 holds c^2 < 2 to_power c
proof
let c be Real such that
A1: c > 6;
A2: 5 = 6-1;
A3: c >= 0 by A1,AXIOMS:22;
set i0 = [\c/], i1 = [/c\];
per cases;
suppose i0 = i1;
then c is Integer by INT_1:59;
then reconsider c as Nat by A3,INT_1:16;
A4: (c+1)^2 < 2 to_power c by A1,Lm13;
c+0 < c+1 by REAL_1:67;
then c^2 < (c+1)^2 by SQUARE_1:78;
hence thesis by A4,AXIOMS:22;
suppose not i0 = i1;
then A5: i0 + 1 = i1 by INT_1:66;
then i0 + (1 + -1) = i1 + -1 by XCMPLX_1:1;
then A6: i0 = i1 - 1 by XCMPLX_0:def 8;
A7: i1 >= c by INT_1:def 5;
then reconsider i1 as Nat by A3,INT_1:16;
i1 > 6 by A1,A7,AXIOMS:22;
then A8: i0 > 5 by A2,A6,REAL_1:54;
then i0 >= 0 by AXIOMS:22;
then reconsider i0 as Nat by INT_1:16;
i0 >= 5 + 1 by A8,INT_1:20;
then A9: i1^2 < 2 to_power i0 by A5,Lm13;
i1 >= c by INT_1:def 5;
then i1^2 >= c^2 by A3,SQUARE_1:77;
then A10: c^2 < 2 to_power i0 by A9,AXIOMS:22;
i0 <= c by INT_1:def 4;
then 2 to_power i0 <= 2 to_power c by PRE_FF:10;
hence thesis by A10,AXIOMS:22;
end;
Lm15:
for e being positive Real, f being Real_Sequence st
(f.0 = 0 & (for n st n > 0 holds f.n = log(2,n to_power e)))
holds (f /" seq_n^(e)) is convergent & lim (f /" seq_n^(e)) = 0
proof
let e be positive Real, f be Real_Sequence such that
A1: (f.0 = 0 & (for n st n > 0 holds f.n = log(2,n to_power e)));
set g = seq_n^(e);
set h = f/"g;
A2: now let p be real number; assume
A3: p > 0;
reconsider p1 = p as Real by XREAL_0:def 1;
set i0 = [/(7/p1) to_power (1/e)\];
set i1 = [/(p1 to_power -(2/e)) + 1\];
set N = max( max(i0, i1), 2 );
A4: N >= max(i0, i1) & N >= 2 by SQUARE_1:46;
max(i0, i1) >= i0 & max(i0, i1) >= i1 by SQUARE_1:46;
then A5: N >= i0 & N >= i1 by A4,AXIOMS:22;
N is Integer proof
per cases by SQUARE_1:49;
suppose N = max(i0, i1);
hence thesis by SQUARE_1:49;
suppose N = 2; hence thesis;
end;
then reconsider N as Nat by A4,INT_1:16;
p" > 0 by A3,REAL_1:72;
then 7*p" > 7*0 by REAL_1:70;
then A6: 7/p > 0 by XCMPLX_0:def 9;
take N; let n; assume A7: n >= N;
then A8: n >= 2 & n >= i0 & n >= i1 by A4,A5,AXIOMS:22;
i0 >= (7/p) to_power (1/e) by INT_1:def 5;
then A9: n >= (7/p) to_power (1/e) by A8,AXIOMS:22;
(7/p1) to_power (1/e) > 0 by A6,POWER:39;
then n to_power e >= (7/p) to_power (1/e) to_power e by A9,Lm6;
then n to_power e >= (7/p1) to_power (e*(1/e)) by A6,POWER:38;
then n to_power e >= (7/p) to_power 1 by XCMPLX_1:107;
then n to_power e >= 7/p1 by POWER:30;
then p*(n to_power e) >= (7/p)*p by A3,AXIOMS:25;
then p*(n to_power e) >= 7 by A3,XCMPLX_1:88;
then p*(n to_power e) > 6 by AXIOMS:22;
then A10: (p1*(n to_power e))^2 < 2 to_power (p1*(n to_power e)) by Lm14;
set c = p1*(n to_power e);
A11: n to_power e > 0 by A4,A7,POWER:39;
then A12: (n to_power e)" > 0 by REAL_1:72;
A13:p*(n to_power e) > p*0 by A3,A11,REAL_1:70;
c*c < 2 to_power c by A10,SQUARE_1:def 3;
then c < (2 to_power c)/c by A13,REAL_2:178;
then n to_power e < ((2 to_power c)/c)/p by A3,REAL_2:178;
then A14: n to_power e < (2 to_power c)/(c*p) by XCMPLX_1:79;
A15:p1 to_power 2 > 0 by A3,POWER:39;
A16:i1 >= (p to_power -(2/e)) + 1 by INT_1:def 5;
(p to_power -(2/e)) + 1 > (p to_power -(2/e)) + 0 by REAL_1:67;
then i1 > (p to_power -(2/e)) by A16,AXIOMS:22;
then A17:n > p to_power -(2/e) by A8,AXIOMS:22;
p1 to_power -(2/e) > 0 by A3,POWER:39;
then n to_power e > p to_power (-(2/e)) to_power e by A17,POWER:42;
then n to_power e > p1 to_power ((-(2/e))*e) by A3,POWER:38;
then n to_power e > p to_power -((2/e)*e) by XCMPLX_1:175;
then n to_power e > p to_power -2 by XCMPLX_1:88;
then (p to_power 2)*(n to_power e) >
(p to_power 2)*(p to_power -2) by A15,REAL_1:70;
then (p1 to_power 2)*(n to_power e) > p1 to_power (2+-2) by A3,POWER:32;
then (p1 to_power 2)*(n to_power e) > 1 by POWER:29;
then p1^2*(n to_power e) > 1 by POWER:53;
then (p*p)*(n to_power e) > 1 by SQUARE_1:def 3;
then p*c > 1 by XCMPLX_1:4;
then A18: 1/(p*c) < 1/1 by REAL_2:151;
2 to_power c > 0 by POWER:39;
then (2 to_power c)*(1/(c*p)) < (2 to_power c)*(1/1) by A18,REAL_1:70;
then (2 to_power c)/(c*p) < (2 to_power c)*1 by XCMPLX_1:100;
then n to_power e < 2 to_power c by A14,AXIOMS:22;
then log(2,n to_power e) < log(2,2 to_power c) by A11,POWER:65;
then log(2,n to_power e) < c*log(2,2) by POWER:63;
then log(2,n to_power e) < c*1 by POWER:60;
then A19: log(2,n to_power e)/(n to_power e) < p by A11,REAL_2:178;
n > 1 by A8,AXIOMS:22;
then n to_power e > n to_power 0 by POWER:44;
then n to_power e > 1 by POWER:29;
then log(2,n to_power e) > log(2,1) by POWER:65;
then log(2,n to_power e) > 0 by POWER:59;
then log(2,n to_power e)*(n to_power e)" >
0*(n to_power e)" by A12,REAL_1:70;
then A20: log(2,n to_power e)/(n to_power e) > 0 by XCMPLX_0:def 9;
h.n = f.n/g.n by Lm4
.= log(2,n to_power e)/g.n by A1,A4,A7
.= log(2,n to_power e)/(n to_power e) by A4,A7,Def3;
hence abs(h.n-0) < p by A19,A20,ABSVALUE:def 1;
end;
hence h is convergent by SEQ_2:def 6;
hence lim h = 0 by A2,SEQ_2:def 7;
end;
Lm16:
for e being Real st e > 0 holds
(seq_logn /" seq_n^(e)) is convergent & lim(seq_logn /" seq_n^(e)) = 0
proof
let e be Real; assume
e > 0;
then reconsider e as positive Real;
A1: 1 = e/e by XCMPLX_1:60
.= e*(1/e) by XCMPLX_1:100;
set f = seq_logn;
set g = seq_n^(e);
set h = f/"g;
ex s being Real_Sequence st (s.0 = 0 &
(for n st n > 0 holds s.n = log(2,n to_power e))) proof
defpred P[Nat,Real] means
($1 = 0 implies $2 = 0) &
($1 > 0 implies $2 = log(2,$1 to_power e));
A2: for x being Element of NAT ex y being Element of REAL st P[x,y] proof
let n;
per cases;
suppose n = 0; hence thesis;
suppose n > 0; hence thesis;
end;
consider h being Function of NAT,REAL such that
A3: for x being Element of NAT holds P[x,h.x] from FuncExD(A2);
take h;
thus h.0 = 0 by A3;
let n; thus thesis by A3;
end;
then consider p being Real_Sequence such that
A4: p.0 = 0 & (for n st n > 0 holds p.n = log(2,n to_power e));
set q = p/"g;
A5: q is convergent & lim q = 0 by A4,Lm15;
A6:for n holds h.n = (1/e)*q.n proof
let n;
A7: h.n = f.n / g.n by Lm4;
A8: q.n = p.n / g.n by Lm4;
thus thesis proof
per cases;
suppose
A9: n = 0;
then h.n = 0 / g.n by A7,Def2
.= 0*(1/e);
hence thesis by A4,A8,A9;
suppose
A10: n > 0;
then A11: n to_power e > 0 by POWER:39;
h.n = log(2,n) / g.n by A7,A10,Def2
.= log(2,n to_power (e*(1/e))) / g.n by A1,POWER:30
.= log(2,n to_power e to_power (1/e)) / g.n by A10,POWER:38
.= ((1/e)*log(2,n to_power e)) / g.n by A11,POWER:63
.= ((1/e)*log(2,n to_power e)) * (g.n)" by XCMPLX_0:def 9
.= (1/e)*(log(2,n to_power e) * (g.n)") by XCMPLX_1:4
.= (1/e)*(log(2,n to_power e) / g.n) by XCMPLX_0:def 9;
hence thesis by A4,A8,A10;
end;
end;
then A12: h = (1/e)(#)q by SEQ_1:13;
lim h = lim((1/e)(#)q) by A6,SEQ_1:13
.= (1/e)*0 by A5,SEQ_2:22;
hence thesis by A5,A12,SEQ_2:21;
end;
theorem Th5:
Big_Oh(seq_logn) c= Big_Oh(seq_n^(1/2)) &
not Big_Oh(seq_logn) = Big_Oh(seq_n^(1/2))
proof
set f = seq_logn;
set g = seq_n^(1/2);
f/"g is convergent & lim (f/"g) = 0 by Lm16;
then f in Big_Oh(g) & not g in Big_Oh(f) by ASYMPT_0:16;
then f in Big_Oh(g) & not f in Big_Omega(g) by ASYMPT_0:19;
hence thesis by Th4;
end;
:: Example p. 86
theorem
seq_n^(1/2) in Big_Omega(seq_logn) & not seq_logn in Big_Omega(seq_n^(1/2))
proof
seq_logn in Big_Oh(seq_n^(1/2)) &
not seq_logn in Big_Omega(seq_n^(1/2)) by Th4,Th5;
hence thesis by ASYMPT_0:19;
end;
:: Example p. 88
Lm17:
for f being Real_Sequence holds
for N holds (for n st n <= N holds f.n >= 0) implies Sum(f,N) >= 0
proof let f be Real_Sequence;
defpred _P[Nat] means
(for n st n <= $1 holds f.n >= 0) implies Sum(f,$1) >= 0;
A1: _P[0] proof assume for n st n <= 0 holds f.n >= 0; then f.0 >= 0;
then (Partial_Sums(f)).0 >= 0 by SERIES_1:def 1;
hence thesis by BHSP_4:def 6;
end;
A2: for N st _P[N] holds _P[N+1] proof
let N; assume
A3: (for n st n <= N holds f.n >= 0) implies Sum(f,N) >= 0;
assume
A4: (for n st n <= (N+1) holds f.n >= 0);
A5: now let n; assume n <= N;
then n+0 <= N+1 by REAL_1:55;
hence f.n >= 0 by A4;
end;
f.(N+1) >= 0 by A4;
then Sum(f,N) + f.(N+1) >= 0 + 0 by A3,A5,REAL_1:55;
then (Partial_Sums(f)).N + f.(N+1) >= 0 by BHSP_4:def 6;
then (Partial_Sums(f)).(N+1) >= 0 by SERIES_1:def 1;
hence Sum(f,N+1) >= 0 by BHSP_4:def 6;
end;
for N holds _P[N] from Ind(A1, A2);
hence thesis;
end;
Lm18:
for f,g being Real_Sequence
holds for N holds (for n st n <= N holds f.n <= g.n) implies Sum(f,N) <= Sum
(g,N)
proof let f,g be Real_Sequence;
defpred _P[Nat] means
(for n st n <= $1 holds f.n <= g.n) implies Sum(f,$1) <= Sum(g,$1);
A1: _P[0] proof
assume (for n st n <= 0 holds f.n <= g.n);
then f.0 <= g.0;
then Partial_Sums(f).0 <= g.0 by SERIES_1:def 1;
then Partial_Sums(f).0 <= Partial_Sums(g).0 by SERIES_1:def 1;
then Sum(f,0) <= Partial_Sums(g).0 by BHSP_4:def 6;
hence Sum(f,0) <= Sum(g,0) by BHSP_4:def 6;
end;
A2: for N st _P[N] holds _P[N+1] proof
let N; assume
A3: (for n st n <= N holds f.n <= g.n) implies Sum(f,N) <= Sum(g,N);
assume
A4: (for n st n <= (N+1) holds f.n <= g.n);
A5: now let n; assume n <= N;
then n+0 <= N+1 by REAL_1:55;
hence f.n <= g.n by A4;
end;
f.(N+1) <= g.(N+1) by A4;
then Sum(f,N) + f.(N+1) <= Sum(g,N) + g.(N+1) by A3,A5,REAL_1:55;
then (Partial_Sums(f)).N + f.(N+1) <=
Sum(g,N) + g.(N+1) by BHSP_4:def 6;
then (Partial_Sums(f)).(N+1) <= Sum(g,N) + g.(N+1) by SERIES_1:def 1
;
then Sum(f,N+1) <= Sum(g,N) + g.(N+1) by BHSP_4:def 6;
then Sum(f,N+1) <= (Partial_Sums(g)).N + g.(N+1) by BHSP_4:def 6;
then Sum(f,N+1) <= (Partial_Sums(g)).(N+1) by SERIES_1:def 1;
hence Sum(f,N+1) <= Sum(g,N+1) by BHSP_4:def 6;
end;
for N holds _P[N] from Ind(A1, A2);
hence thesis;
end;
Lm19:
for f being Real_Sequence, b being Real st
(f.0 = 0 & (for n st n > 0 holds f.n = b))
holds for N being Nat holds Sum(f,N) = b*N
proof
let f be Real_Sequence, b be Real;
defpred _P[Nat] means Sum(f,$1) = b*$1;
assume
A1: f.0 = 0 & (for n st n > 0 holds f.n = b);
then (Partial_Sums(f)).0 = 0 by SERIES_1:def 1;
then A2: _P[0] by BHSP_4:def 6;
A3: for N st _P[N] holds _P[N+1] proof let N; assume
A4: Sum(f, N) = b*N;
Sum(f, N+1) = (Partial_Sums(f)).(N+1) by BHSP_4:def 6
.= (Partial_Sums(f)).N + f.(N+1) by SERIES_1:def 1
.= b*N + f.(N+1) by A4,BHSP_4:def 6
.= b*N + b*1 by A1
.= b*(N+1) by XCMPLX_1:8;
hence thesis;
end;
for N holds _P[N] from Ind( A2, A3 );
hence thesis;
end;
Lm20:
for f,g being Real_Sequence,
N,M being Nat holds Sum(f,N,M) + f.(N+1) = Sum(f,N+1,M)
proof
let f,g be Real_Sequence, N,M be Nat;
Sum(f,N,M) + f.(N+1) = Sum(f,N) - Sum(f,M) + f.(N+1) by BHSP_4:def 7
.= Sum(f,N) + -Sum(f,M) + f.(N+1) by XCMPLX_0:def 8
.= Sum(f,N) + f.(N+1) + -Sum(f,M) by XCMPLX_1:1
.= (Partial_Sums(f)).N + f.(N+1) + -Sum
(f,M) by BHSP_4:def 6
.= (Partial_Sums(f)).(N+1) + -Sum(f,M) by SERIES_1:def 1
.= Sum(f,N+1) + -Sum(f,M) by BHSP_4:def 6
.= Sum(f,N+1) - Sum(f,M) by XCMPLX_0:def 8
.= Sum(f,N+1,M) by BHSP_4:def 7;
hence Sum(f,N,M) + f.(N+1) = Sum(f,N+1,M);
end;
Lm21:
for f,g being Real_Sequence, M being Nat
holds for N st N >= M+1 holds
(for n st M+1 <= n & n <= N holds f.n <= g.n) implies Sum(f,N,M) <= Sum
(g,N,M)
proof
let f,g be Real_Sequence, M be Nat;
defpred _P[Nat] means
(for n st M+1 <= n & n <= $1 holds f.n <= g.n)
implies Sum(f,$1,M) <= Sum(g,$1,M);
A1: _P[M+1] proof assume
A2: (for n st M+1 <= n & n <= M+1 holds f.n <= g.n);
A3: Sum(f,M+1,M) = Sum(f,M+1) - Sum(f,M) by BHSP_4:def 7
.= (Partial_Sums(f)).(M+1) - Sum(f,M) by BHSP_4:def 6
.= f.(M+1) + (Partial_Sums(f)).M - Sum(f,M) by SERIES_1:def 1
.= f.(M+1) + Sum(f,M) - Sum(f,M) by BHSP_4:def 6
.= f.(M+1) + Sum(f,M) + -Sum(f,M) by XCMPLX_0:def 8
.= f.(M+1) + (Sum(f,M) + -Sum(f,M)) by XCMPLX_1:1
.= f.(M+1) + (Sum(f,M) - Sum(f,M)) by XCMPLX_0:def 8
.= f.(M+1) + 0 by XCMPLX_1:14;
Sum(g,M+1,M) = Sum(g,M+1) - Sum(g,M) by BHSP_4:def 7
.= (Partial_Sums(g)).(M+1) - Sum(g,M) by BHSP_4:def 6
.= g.(M+1) + (Partial_Sums(g)).M - Sum(g,M) by SERIES_1:def 1
.= g.(M+1) + Sum(g,M) - Sum(g,M) by BHSP_4:def 6
.= g.(M+1) + Sum(g,M) + -Sum(g,M) by XCMPLX_0:def 8
.= g.(M+1) + (Sum(g,M) + -Sum(g,M)) by XCMPLX_1:1
.= g.(M+1) + (Sum(g,M) - Sum(g,M)) by XCMPLX_0:def 8
.= g.(M+1) + 0 by XCMPLX_1:14;
hence Sum(f,M+1,M) <= Sum(g,M+1,M) by A2,A3;
end;
A4: for N1 st N1 >= M+1 & _P[N1] holds _P[N1+1] proof
let N1; assume that
A5: N1 >= M+1 and
A6: (for n st M+1 <= n & n <= N1 holds f.n <= g.n) implies
Sum(f,N1,M) <= Sum(g,N1,M);
assume
A7: (for n st M+1 <= n & n <= N1+1 holds f.n <= g.n);
A8: now let n; assume
A9: M+1 <= n & n <= N1;
then n + 0 <= N1 + 1 by REAL_1:55;
hence f.n <= g.n by A7,A9;
end;
N1+1 >= M+1+0 by A5,REAL_1:55;
then f.(N1+1) <= g.(N1+1) by A7;
then Sum(f,N1,M) + f.(N1+1) <= g.(N1+1) + Sum(g,N1,M) by A6,A8,REAL_1:
55;
then Sum(f,N1+1,M) <= g.(N1+1) + Sum(g,N1,M) by Lm20;
hence Sum(f,N1+1,M) <= Sum(g,N1+1,M) by Lm20;
end;
for N st N >= M+1 holds _P[N] from Ind1(A1, A4);
hence thesis;
end;
Lm22:
for n holds [/n/2\] <= n
proof
let n;
per cases;
suppose
n = 0;
hence thesis by INT_1:54;
suppose n > 0;
then A1: n >= 0+1 by NAT_1:38;
thus thesis proof
per cases by A1,REAL_1:def 5;
suppose
A2: n = 1;
now assume [/1/2\] > 1;
then A3: [/1/2\] >= 1+1 by INT_1:20;
[/1/2\] < 1/2 + 1 by INT_1:def 5;
hence contradiction by A3,AXIOMS:22;
end;
hence thesis by A2;
suppose n > 1;
then A4: n >= 1+1 by NAT_1:38;
A5: [/n/2\] < n/2 + 1 by INT_1:def 5;
now assume n/2 + 1 > n;
then 2*(n/2 + 1) > 2*n by REAL_1:70;
then 2*(n/2) + 2*1 > 2*n by XCMPLX_1:8;
then 2*(n*2") + 2 > 2*n by XCMPLX_0:def 9;
then (2*2")*n + 2 > 2*n by XCMPLX_1:4;
then 2 > 2*n - n by REAL_1:84;
then 2 > 2*n + -n by XCMPLX_0:def 8;
then 2 > 2*n + (-1)*n by XCMPLX_1:180;
then 2 > (2+-1)*n by XCMPLX_1:8;
hence contradiction by A4;
end;
hence thesis by A5,AXIOMS:22;
end;
end;
Lm23:
for f being Real_Sequence, b being Real, N being Nat st
(f.0 = 0 & (for n st n > 0 holds f.n = b))
holds for M being Nat holds Sum(f, N, M) = b*(N-M)
proof
let f be Real_Sequence, b be Real, N be Nat such that
A1: f.0 = 0 & (for n st n > 0 holds f.n = b);
defpred _P[Nat] means Sum(f, N, $1) = b*(N-$1);
A2: _P[0] proof
Sum(f, 0) = (Partial_Sums(f)).0 by BHSP_4:def 6
.= 0 by A1,SERIES_1:def 1;
then Sum(f, N, 0) = Sum(f, N) - 0 by BHSP_4:def 7
.= b*(N-0) by A1,Lm19;
hence thesis;
end;
A3: for M st _P[M] holds _P[M+1] proof let M; assume
A4: Sum(f, N, M) = b*(N-M);
Sum(f, N, M+1) = Sum(f, N) - Sum(f, M+1) by BHSP_4:def 7
.= Sum(f, N) - (Partial_Sums(f)).(M+1) by BHSP_4:def 6
.= Sum
(f, N) - ((Partial_Sums(f)).M + f.(M+1)) by SERIES_1:def 1
.= Sum
(f, N) + -((Partial_Sums(f)).M + f.(M+1)) by XCMPLX_0:def 8
.= Sum(f, N) + (-(Partial_Sums(f)).M + -f.(M+1)) by XCMPLX_1:
140
.= Sum(f, N) + -(Partial_Sums(f)).M + -f.(M+1) by XCMPLX_1:1
.= (Sum
(f, N) - (Partial_Sums(f)).M) + -f.(M+1) by XCMPLX_0:def 8
.= (Sum(f, N) - Sum(f, M)) + -f.(M+1) by BHSP_4:def 6
.= b*(N-M) + -f.(M+1) by A4,BHSP_4:def 7
.= b*(N-M) + -b by A1
.= b*(N-M) + (-1)*b by XCMPLX_1:180
.= b*(N-M+-1) by XCMPLX_1:8
.= b*(N+-M+-1) by XCMPLX_0:def 8
.= b*(N+(-M+-1)) by XCMPLX_1:1
.= b*(N+-(M+1)) by XCMPLX_1:140
.= b*(N-(M+1)) by XCMPLX_0:def 8;
hence thesis;
end;
for M being Nat holds _P[M] from Ind(A2, A3);
hence thesis;
end;
theorem
for f being Real_Sequence, k being Nat st
(for n holds f.n = Sum(seq_n^(k), n))
holds f in Big_Theta(seq_n^(k+1))
proof
let f be Real_Sequence, k be Nat such that
A1: for n holds f.n = Sum(seq_n^(k), n);
set g = seq_n^(k+1);
A2: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 }
by ASYMPT_0:def 12;
A3: Big_Omega(g) = { t where t is Element of Funcs(NAT, REAL) :
ex d,N st d > 0 & for n st n >= N holds t.n>=d*g.n & t.n>=0 }
by ASYMPT_0:def 13;
A4: f is Element of Funcs(NAT, REAL) by FUNCT_2:11;
2 to_power (k+1) > 0 by POWER:39;
then A5: (2 to_power (k+1))" > 0 by REAL_1:72;
now let n; assume A6: n >= 1;
set p = seq_n^(k);
ex s being Real_Sequence st s.0 = 0 &
(for m st m > 0 holds s.m = (n to_power k)) proof
defpred P[Nat,Real] means
($1 = 0 implies $2 = 0) &
($1 > 0 implies $2 = (n to_power k));
A7: for x being Element of NAT ex y being Element of REAL st P[x,y] proof
let n;
per cases;
suppose n = 0; hence thesis;
suppose n > 0; hence thesis;
end;
consider h being Function of NAT,REAL such that
A8: for x being Element of NAT holds P[x,h.x] from FuncExD(A7);
take h;
thus h.0 = 0 by A8;
let n; thus thesis by A8;
end;
then consider q being Real_Sequence such that
A9: q.0 = 0 & (for m st m > 0 holds q.m = n to_power k);
A10: f.n = Sum(p, n) by A1;
now let m; assume
A11: m <= n;
per cases;
suppose m = 0;
hence p.m <= q.m by A9,Def3;
suppose
A12: m > 0;
then A13: p.m = m to_power k by Def3;
q.m = n to_power k by A9,A12;
hence p.m <= q.m by A11,A12,A13,Lm6;
end;
then A14: Sum(p, n) <= Sum(q, n) by Lm18;
Sum(q, n) = (n to_power k)*n by A9,Lm19
.= (n to_power k)*(n to_power 1) by POWER:30
.= n to_power (k+1) by A6,POWER:32
.= g.n by A6,Def3;
hence f.n <= 1*g.n by A1,A14;
now let m; assume m <= n;
per cases;
suppose m = 0;
hence p.m >= 0 by Def3;
suppose
m > 0;
then p.m = m to_power k by Def3;
hence p.m >= 0;
end;
hence f.n >= 0 by A10,Lm17;
end;
then A15: f in Big_Oh(g) by A2,A4;
now let n; assume
A16: n >= 1;
set p = seq_n^(k);
ex s being Real_Sequence st s.0 = 0 &
(for m st m > 0 holds s.m = ((n/2) to_power k)) proof
defpred P[Nat,Real] means
($1 = 0 implies $2 = 0) &
($1 > 0 implies $2 = ((n/2) to_power k));
A17: for x being Element of NAT ex y being Element of REAL st P[x,y] proof
let n;
per cases;
suppose n = 0; hence thesis;
suppose n > 0; hence thesis;
end;
consider h being Function of NAT,REAL such that
A18: for x being Element of NAT holds P[x,h.x] from FuncExD(A17);
take h;
thus h.0 = 0 by A18;
let n; thus thesis by A18;
end;
then consider q being Real_Sequence such that
A19: q.0 = 0 & (for m st m > 0 holds q.m = (n/2) to_power k);
A20: f.n = Sum(p, n) by A1;
A21: g.n = n to_power (k+1) by A16,Def3;
set n1 = [/n/2\];
A22: n*2" > 0*2" by A16,REAL_1:70;
then A23: n/2 > 0 by XCMPLX_0:def 9;
A24: [/n/2\] >= n/2 by INT_1:def 5;
then reconsider n1 as Nat by INT_1:16;
set n2 = n1-1;
now assume n2 < 0;
then n1-1 <= -1 by INT_1:21;
then (n1-1)+1 <= -1+1 by AXIOMS:24;
then (n1+-1)+1 <= 0 by XCMPLX_0:def 8;
then n1+(-1+1) <= 0 by XCMPLX_1:1;
hence contradiction by A22,A24,XCMPLX_0:def 9;
end;
then reconsider n2 as Nat by INT_1:16;
A25: now let m; assume m <= n;
per cases;
suppose m = 0;
hence p.m >= 0 by Def3;
suppose
m > 0;
then p.m = m to_power k by Def3;
hence p.m >= 0;
end;
then A26: Sum(p,n) >= 0 by Lm17;
A27: Sum(p,n,n2) = Sum(p,n) - Sum(p,n2) by BHSP_4:def 7;
now let m; assume
A28: m <= n2;
n1 <= n1+1 by NAT_1:29;
then n2 <= n1 by REAL_1:86;
then A29: m <= n1 by A28,AXIOMS:22;
n1 <= n by Lm22;
then m <= n by A29,AXIOMS:22;
hence p.m >= 0 by A25;
end;
then Sum(p,n2) >= 0 by Lm17;
then Sum(p,n) + Sum(p,n2) >= Sum(p,n) + 0 by REAL_1:55;
then A30: Sum(p,n) >= Sum(p,n,n2) by A27,REAL_1:86;
A31: n1 = n2+1 by XCMPLX_1:27;
A32: for N0 st n1 <= N0 & N0 <= n holds q.N0 <= p.N0 proof
let N0; assume
A33: n1 <= N0 & N0 <= n;
then A34: N0 > 0 by A22,A24,XCMPLX_0:def 9;
then A35: q.N0 = (n/2) to_power k by A19;
A36: p.N0 = N0 to_power k by A34,Def3;
N0 >= n/2 by A24,A33,AXIOMS:22;
hence q.N0 <= p.N0 by A23,A35,A36,Lm6;
end;
n >= n1 by Lm22;
then n+-1 >= n1+-1 by AXIOMS:24;
then n-1 >= n1+-1 by XCMPLX_0:def 8;
then n-1 >= n2 by XCMPLX_0:def 8;
then n >= n2 + 1 by REAL_1:84;
then A37: Sum(p,n,n2) >= Sum(q,n,n2) by A31,A32,Lm21;
A38: Sum(q,n,n2) = (n-n2)*((n/2) to_power k) by A19,Lm23;
A39: now assume n-n2 < n/2;
then A40: n < n/2 + n2 by REAL_1:84;
[/n/2\] < n/2 + 1 by INT_1:def 5;
then n2 < n/2 by REAL_1:84;
then n/2 + n2 < n/2 + n/2 by REAL_1:53;
then n < 1*(n/2) + 1*(n/2) by A40,AXIOMS:22;
then n < (1+1)*(n/2) by XCMPLX_1:8;
then n < 2*(n*2") by XCMPLX_0:def 9;
then n < (2*2")*n by XCMPLX_1:4;
hence contradiction;
end;
((n/2) to_power k) > 0 by A23,POWER:39;
then Sum(q,n,n2) >= (n/2) * ((n/2) to_power k) by A38,A39,AXIOMS:25;
then Sum(q,n,n2) >= ((n/2) to_power 1) * ((n/2) to_power k) by POWER:30;
then Sum(q,n,n2) >= ((n/2) to_power (k+1)) by A23,POWER:32;
then Sum(q,n,n2) >= (n to_power (k+1))/(2 to_power (k+1)) by A16,POWER:36
;
then Sum
(q,n,n2) >= (n to_power (k+1))*(2 to_power (k+1))" by XCMPLX_0:def 9;
then Sum(p,n,n2) >= (n to_power (k+1))*(2 to_power (k+1))" by A37,AXIOMS:
22;
hence (2 to_power (k+1))"*g.n <= f.n by A20,A21,A30,AXIOMS:22;
thus f.n >= 0 by A1,A26;
end;
then f in Big_Omega(g) by A3,A4,A5;
then f in Big_Oh(g) /\ Big_Omega(g) by A15,XBOOLE_0:def 3;
hence thesis by ASYMPT_0:def 14;
end;
:: Example p. 89
theorem
for f being Real_Sequence st
(f.0 = 0 & (for n st n > 0 holds f.n = (n to_power log(2,n))))
holds ex s being eventually-positive Real_Sequence st
s = f & not s is smooth
proof
let f be Real_Sequence such that
A1: f.0 = 0 & (for n st n > 0 holds f.n = (n to_power log(2,n)));
set g = f taken_every 2;
f is eventually-positive proof
take 1;
let n; assume A2: n >= 1;
then f.n = n to_power log(2,n) by A1;
hence f.n > 0 by A2,POWER:39;
end;
then reconsider f as eventually-positive Real_Sequence;
take f;
A3: Big_Oh(f) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 }
by ASYMPT_0:def 12;
now assume f is smooth;
then f is_smooth_wrt 2 by ASYMPT_0:def 20;
then g in Big_Oh(f) by ASYMPT_0:def 19;
then consider t being Element of Funcs(NAT, REAL) such that
A4: t = g and
A5: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A3;
consider c,N such that
A6: c > 0 and
A7: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A5;
set N0 = [/sqrt c / sqrt 2\];
reconsider N2=max(N, N0) as Integer by SQUARE_1:49;
set N1 = max( N2, 2 );
A8: N1 >= N2 & N1 >= 2 by SQUARE_1:46;
N2 >= N & N2 >= N0 by SQUARE_1:46;
then A9: N1 >= N & N1 >= N0 by A8,AXIOMS:22;
N1 is Integer by SQUARE_1:49;
then reconsider N1 as Nat by A8,INT_1:16;
set n = N1 + 1;
n > N1 + 0 by REAL_1:67;
then A10: n > N0 & n > N & n > 2 by A8,A9,AXIOMS:22;
A11: n to_power log(2,n) > 0 by POWER:39;
A12: 2*n > 2*0 by REAL_1:70;
A13: (2*n^2)*(n to_power log(2,n)) = (2*n) to_power log(2,2*n) proof
thus (2*n^2)*(n to_power log(2,n))
= (2*(n*n))*(n to_power log(2,n)) by SQUARE_1:def 3
.= ((2*n)*n)*(n to_power log(2,n)) by XCMPLX_1:4
.= ((2*n)*(2 to_power (log(2,n))))*(n to_power log(2,n))
by POWER:def 3
.= (2*n)*((2 to_power (log(2,n)))*(n to_power log(2,n))) by XCMPLX_1:4
.= (2*n)*((2*n) to_power log(2,n)) by POWER:35
.= ((2*n) to_power 1)*((2*n) to_power log(2,n)) by POWER:30
.= (2*n) to_power (1 + log(2,n)) by A12,POWER:32
.= (2*n) to_power (log(2,2) + log(2,n)) by POWER:60
.= (2*n) to_power log(2,2*n) by POWER:61;
end;
A14: sqrt 2 > 0 by SQUARE_1:93;
A15: sqrt 2 <> 0 by SQUARE_1:93;
A16: sqrt c > 0 by A6,SQUARE_1:93;
N0 >= sqrt c / sqrt 2 by INT_1:def 5;
then n > sqrt c / sqrt 2 by A10,AXIOMS:22;
then n*sqrt 2 > (sqrt c / sqrt 2) * sqrt 2 by A14,REAL_1:70;
then n*sqrt 2 > sqrt c by A15,XCMPLX_1:88;
then (n*sqrt 2)^2 > (sqrt c)^2 by A16,SQUARE_1:78;
then (n*sqrt 2)^2 > c by A6,SQUARE_1:def 4;
then n^2*(sqrt 2)^2 > c by SQUARE_1:68;
then 2*n^2 > c by SQUARE_1:def 4;
then (2*n) to_power log(2,2*n) > c*(n to_power log(2,n)) by A11,A13,REAL_1:
70;
then f.(2*n) > c*(n to_power log(2,n)) by A1,A12;
then t.n > c*(n to_power log(2,n)) by A4,ASYMPT_0:def 18;
then t.n > c*f.n by A1;
hence contradiction by A7,A10;
end;
hence thesis;
end;
:: Example p. 92
definition
let b be Real;
func seq_const(b) -> Real_Sequence equals :Def4:
NAT --> b;
coherence proof
dom (NAT --> b) = NAT & rng (NAT --> b) = {b} by FUNCOP_1:14,19;
hence NAT --> b is Real_Sequence by FUNCT_2:def 1,RELSET_1:11;
end;
end;
definition
cluster seq_const(1) -> eventually-nonnegative;
coherence proof
take 0; let n; assume n >= 0;
(seq_const(1)).n = (NAT --> 1).n by Def4 .= 1 by FUNCOP_1:13;
hence (seq_const(1)).n >= 0;
end;
end;
Lm24:
for a,b,c being Real holds
a>1 & b>=a & c>=1 implies log(a,c) >= log(b,c)
proof
let a,b,c be Real;
assume that
A1: a > 1 and
A2: b >= a and
A3: c >= 1;
A4: b > 1 by A1,A2,AXIOMS:22;
A5: b > 0 & b <> 1 by A1,A2;
log(b,c) >= log(b,1) by A3,A4,PRE_FF:12;
then A6: log(b,c) >= 0 by A4,POWER:59;
log(a,b) >= log(a,a) by A1,A2,PRE_FF:12;
then log(a,b) >= 1 by A1,POWER:60;
then log(a,b)*log(b,c) >= 1*log(b,c) by A6,AXIOMS:25;
hence thesis by A1,A3,A5,POWER:64;
end;
theorem Th9:
for f being eventually-nonnegative Real_Sequence
holds ex F being FUNCTION_DOMAIN of NAT,REAL st F = { seq_n^(1) } &
(f in F to_power Big_Oh(seq_const(1))
iff ex N,c,k st c>0 & for n st n >= N holds 1 <= f.n & f.n <=
c*(seq_n^(k)).n)
proof
let h be eventually-nonnegative Real_Sequence;
reconsider F = { seq_n^(1) } as FUNCTION_DOMAIN of NAT,REAL by FRAENKEL:10;
take F;
thus F = { seq_n^(1) };
set G = Big_Oh(seq_const(1));
set p = seq_const(1);
A1: F to_power G =
{ t where t is Element of Funcs(NAT,REAL) :
ex f,g being Element of Funcs(NAT,REAL), N being Element of NAT st
f in F & g in G &
for n being Element of NAT st n >= N holds t.n = (f.n) to_power (g.n) }
by ASYMPT_0:def 23;
A2:G = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*p.n & t.n >= 0 }
by ASYMPT_0:def 12;
now
hereby assume h in F to_power Big_Oh(seq_const(1));
then consider t being Element of Funcs(NAT,REAL) such that
A3: h = t and
A4: ex f,g being Element of Funcs(NAT,REAL), N being Element of NAT st
f in F & g in G &
for n being Element of NAT st n>=N holds t.n=(f.n) to_power (g.n) by A1
;
consider f,g being Element of Funcs(NAT,REAL),
N0 being Element of NAT such that
A5: f in F and
A6: g in G and
A7: for n being Element of NAT st n>=N0 holds t.n = (f.n) to_power (g.n) by
A4;
A8:f = seq_n^(1) by A5,TARSKI:def 1;
consider g' being Element of Funcs(NAT, REAL) such that
A9: g = g' and
A10: ex c,N st c > 0 & for n st n >= N holds g'.n <= c*p.n & g'.n >= 0 by A2,
A6;
consider c,N1 such that
A11: c > 0 and
A12: for n st n >= N1 holds g'.n <= c*p.n & g'.n >= 0 by A10;
set N = max(2,max(N0,N1));
max(N0,N1) >= N0 & max(N0,N1) >= N1 & N >= max(N0,N1) by SQUARE_1:46;
then A13: N >= N0 & N >= N1 & N >= 2 by AXIOMS:22,SQUARE_1:46;
set k = [/c\];
A14: k >= c by INT_1:def 5;
k > 0 by A11,INT_1:def 5;
then reconsider k as Nat by INT_1:16;
reconsider i = 1 as Nat;
take N,i,k;
thus i > 0;
let n; assume A15: n >= N;
then A16: n >= N0 & n >= N1 & n >= 2 by A13,AXIOMS:22;
then A17: g'.n <= c*p.n & g'.n >= 0 by A12;
A18: p.n = (NAT --> 1).n by Def4 .= 1 by FUNCOP_1:13;
A19: n > 0 & n > 1 by A16,AXIOMS:22;
f.n = n to_power 1 by A8,A13,A15,Def3 .= n by POWER:30;
then A20: h.n = n to_power (g.n) by A3,A7,A16;
n to_power (g.n) >= n to_power 0 by A9,A17,A19,PRE_FF:10;
hence 1 <= h.n by A20,POWER:29;
g.n <= c*p.n by A9,A12,A16;
then A21: h.n <= n to_power (c*1) by A18,A19,A20,PRE_FF:10;
n to_power c <= n to_power k by A14,A19,PRE_FF:10;
then h.n <= n to_power k by A21,AXIOMS:22;
hence h.n <= i*(seq_n^(k)).n by A13,A15,Def3;
end;
given N0,c,k such that
c > 0 and
A22: for n st n >= N0 holds 1 <= h.n & h.n <= c*(seq_n^(k)).n;
reconsider t = h as Element of Funcs(NAT,REAL) by FUNCT_2:11;
A23: G = { s where s is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds s.n <= c*(seq_const(1)).n & s.n>=
0 }
by ASYMPT_0:def 12;
set N = max(N0,2);
A24: N >= N0 & N >= 2 by SQUARE_1:46;
then A25:N > 1 by AXIOMS:22;
A26:N > 0 & N <> 1 by SQUARE_1:46;
set c1= max(c,2);
A27: c1 >= c & c1 >= 2 by SQUARE_1:46;
then A28:c1 > 0 & c1 > 1 by AXIOMS:22;
set a = log(N,c1);
set b = k+a;
reconsider f = seq_n^(1) as Element of Funcs(NAT,REAL) by FUNCT_2:11;
defpred Q[Nat,Real] means
($1 < N implies $2 = 1) & ($1 >= N implies $2 = log($1,t.$1));
A29:for x being Element of NAT ex y being Element of REAL st Q[x,y] proof
let n; per cases;
suppose n < N; hence thesis;
suppose n >= N; hence thesis;
end;
consider g being Function of NAT,REAL such that
A30:for x being Element of NAT holds Q[x,g.x] from FuncExD(A29);
A31:g is Element of Funcs(NAT,REAL) by FUNCT_2:11;
A32: now let n be Element of NAT; assume
A33: n >= N;
then n >= N0 by A24,AXIOMS:22;
then A34: t.n >= 1 by A22;
thus (f.n) to_power (g.n) = (n to_power 1) to_power (g.n) by A24,A33,Def3
.= n to_power (g.n) by POWER:30
.= n to_power (1*log(n,t.n)) by A30,A33
.= t.n by A24,A25,A33,A34,POWER:def 3;
end;
A35: f in F by TARSKI:def 1;
now
log(N,1) = 0 by A26,POWER:59;
then a > 0 by A25,A28,POWER:65;
then k+a > k+0 by REAL_1:53;
hence b > 0;
let n; assume
A36:n >= N;
then A37: n >= N0 & n >= 2 by A24,AXIOMS:22;
then A38: n > 1 by AXIOMS:22;
A39: n > 0 & n <> 1 by A24,A36,AXIOMS:22;
A40: a >= log(n,c1) by A25,A28,A36,Lm24;
A41: 1 <= t.n & t.n <= c*(seq_n^(k)).n by A22,A37;
A42:(seq_n^(k)).n = n to_power k by A24,A36,Def3;
then A43:(seq_n^(k)).n > 0 by A24,A36,POWER:39;
c*(seq_n^(k)).n <= c1*(seq_n^(k)).n by A27,A42,AXIOMS:25;
then t.n <= c1*(seq_n^(k)).n by A41,AXIOMS:22;
then A44: log(n,t.n) <= log(n,c1*(seq_n^(k)).n) by A38,A41,PRE_FF:12;
t.n = (f.n) to_power (g.n) by A32,A36
.= (n to_power 1) to_power (g.n) by A24,A36,Def3
.= n to_power (g.n) by POWER:30;
then A45: log(n,t.n) = g.n*log(n,n) by A39,POWER:63 .= g.n*1 by A39,POWER:
60;
A46: log(n,c1*(seq_n^(k)).n)
= log(n,c1) + log(n,n to_power k) by A27,A39,A42,A43,POWER:61
.= log(n,c1) + k*log(n,n) by A39,POWER:63
.= log(n,c1) + k*1 by A39,POWER:60;
A47: log(n,c1) + k <= a + k by A40,AXIOMS:24;
(seq_const(1)).n = (NAT --> 1).n by Def4 .= 1 by FUNCOP_1:13;
hence g.n <= b*(seq_const(1)).n by A44,A45,A46,A47,AXIOMS:22;
g.n = log(n,t.n) by A30,A36;
then g.n >= log(n,1) by A38,A41,PRE_FF:12;
hence g.n >= 0 by A39,POWER:59;
end;
then g in G by A23,A31;
hence h in F to_power Big_Oh(seq_const(1)) by A1,A31,A32,A35;
end;
hence thesis;
end;
begin :: Problem 3.1
theorem
for f being Real_Sequence st
(for n holds f.n = 3*(10 to_power 6) - 18*(10 to_power 3)*n + 27*n^2)
holds f in Big_Oh(seq_n^(2))
proof
let f be Real_Sequence such that
A1: for n holds f.n = 3*(10 to_power 6) - 18*(10 to_power 3)*n + 27*n^2;
set g = seq_n^(2);
A2: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 }
by ASYMPT_0:def 12;
A3: f is Element of Funcs(NAT, REAL) by FUNCT_2:11;
consider t1 being Nat such that
A4: t1 = 10*10*10;
consider t2 being Nat such that
A5: t2 = t1*t1;
t1 = 10*10^2 by A4,SQUARE_1:def 3;
then t1 = 10*(10 to_power 2) by POWER:53;
then t1 = (10 to_power 1)*(10 to_power 2) by POWER:30;
then A6: t1 = 10 to_power (1+2) by POWER:32;
then A7: t2 = 10 to_power (3+3) by A5,POWER:32
.= 10 to_power 6;
A8: 10 to_power 3 = 10 to_power (2+1)
.= (10 to_power 2)*(10 to_power 1) by POWER:32
.= (10 to_power 2)*10 by POWER:30
.= (10^2)*10 by POWER:53
.= (10*10)*10 by SQUARE_1:def 3
.= 1000;
A9: t1 > 0 by A6,POWER:39;
A10: for n st n >= 400 holds f.n <= 27*n^2 proof
let n such that
A11: n >= 400;
now assume f.n > 27*n^2;
then 3*t2 - 18*(10 to_power 3)*n + 27*n^2 > 27*n^2 by A1,A7;
then 3*t2 + -18*t1*n + 27*n^2 > 27*n^2 by A6,XCMPLX_0:def 8;
then 3*t2 + -18*t1*n > 27*n^2 - 27*n^2 by REAL_1:84;
then 3*t2 + -18*t1*n > 0 by XCMPLX_1:14;
then 3*t2 - 18*t1*n > 0 by XCMPLX_0:def 8;
then A12: 3*t2 > 0 + 18*t1*n by REAL_1:86;
(18*t1)*n >= (18*t1)*400 by A11,AXIOMS:25;
then 3*t2 > (18*t1)*400 by A12,AXIOMS:22;
then 3*t2 > t1*(18*400) by XCMPLX_1:4;
then 3*(10 to_power (3+3)) > t1*7200 by A7;
then 3*((10 to_power 3)*(10 to_power 3)) > t1*7200 by POWER:32;
then (3*1000)*t1 > t1*7200 by A6,A8,XCMPLX_1:4;
hence contradiction by A9,REAL_1:70;
end;
hence thesis;
end;
A13: for n st n >= 400 holds 18*t1*n - 3*t2 < 27*n^2 proof
defpred _P[Nat] means 18*t1*$1 - 3*t2 < 27*$1^2;
A14: _P[400] proof
A15: 18*t1*400 - 3*t2 = 7200*t1 - (3*1000)*t1 by A5,A6,A8,XCMPLX_1:4
.= (7200 - 3000)*t1 by XCMPLX_1:40
.= 4200*t1;
27*400^2 = 27*(400*400) by SQUARE_1:def 3
.= 27*((4*40)*t1) by A6,A8
.= (27*160)*t1 by XCMPLX_1:4
.= 4320*t1;
hence thesis by A9,A15,REAL_1:70;
end;
A16: for k st k >= 400 & _P[k] holds _P[k+1] proof let k such that
A17: k >= 400 and
A18: 18*t1*k - 3*t2 < 27*k^2;
18*t1*(k+1) - 3*t2 = (18*t1*k + 18*t1*1) - 3*t2 by XCMPLX_1:8
.= (18*t1*k + 18*t1*1) + -3*t2 by XCMPLX_0:def 8
.= (18*t1*k + -3*t2) + 18*t1 by XCMPLX_1:1
.= (18*t1*k - 3*t2) + 18*t1 by XCMPLX_0:def 8;
then A19: 18*t1*(k+1) - 3*t2 < 27*k^2 + 18*t1 by A18,REAL_1:53;
54*400 <= 54*k by A17,AXIOMS:25;
then A20: 18*t1 < 54*k by A6,A8,AXIOMS:22;
54*k + 0 <= 54*k + 27 by REAL_1:55;
then 18*t1 < 54*k + 27 by A20,AXIOMS:22;
then A21: 27*k^2 + 18*t1 < 27*k^2 + (54*k + 27) by REAL_1:53;
27*k^2 + (54*k + 27) = 27*k^2 + ((27*2)*k + 27)
.= 27*k^2 + (27*(2*k) + 27*1) by XCMPLX_1:4
.= 27*k^2 + 27*(2*k + 1) by XCMPLX_1:8
.= 27*(k^2 + (2*k + 1)) by XCMPLX_1:8
.= 27*(k^2 + 2*k*1 + 1*1) by XCMPLX_1:1
.= 27*(k^2 + 2*k*1 + 1^2) by SQUARE_1:def 3
.= 27*(k+1)^2 by SQUARE_1:63;
hence thesis by A19,A21,AXIOMS:22;
end;
for n st n >= 400 holds _P[n]from Ind1(A14, A16);
hence thesis;
end;
now let n; assume
A22: n >= 400;
then f.n <= 27*n^2 by A10;
then f.n <= 27*(n to_power 2) by POWER:53;
hence f.n <= 27*g.n by A22,Def3;
0 + (18*t1*n - 3*t2) < 27*n^2 by A13,A22;
then 0 < 27*n^2 - (18*t1*n - 3*t2) by REAL_1:86;
then 0 < 27*n^2 - 18*t1*n + 3*t2 by XCMPLX_1:37;
then 0 < 27*n^2 + -18*t1*n + 3*t2 by XCMPLX_0:def 8;
then 0 < 3*t2 + -18*t1*n + 27*n^2 by XCMPLX_1:1;
then 0 < 3*(10 to_power 6) - 18*t1*n + 27*n^2 by A7,XCMPLX_0:def 8;
hence f.n >= 0 by A1,A6;
end;
hence thesis by A2,A3;
end;
:: Problem 3.2 -- omitted
:: Problem 3.3 -- omitted
:: Problem 3.4 -- omitted
begin :: Problem 3.5
theorem :: Part 1
seq_n^(2) in Big_Oh(seq_n^(3))
proof
set f = seq_n^(2);
set g = seq_n^(3);
A1: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 &
for n st n >= N holds t.n <= c*g.n & t.n >= 0 } by ASYMPT_0:def 12;
A2: f is Element of Funcs(NAT, REAL) by FUNCT_2:11;
now let n; assume
A3: n >= 2;
then A4: n > 1 by AXIOMS:22;
A5: f.n = n to_power 2 by A3,Def3;
g.n = n to_power 3 by A3,Def3;
hence f.n <= 1*g.n by A4,A5,POWER:44;
thus f.n >= 0 by A5;
end;
hence thesis by A1,A2;
end;
theorem :: Part 2
not seq_n^(2) in Big_Omega(seq_n^(3))
proof
set f = seq_n^(2);
set g = seq_n^(3);
A1: Big_Omega(g) = { s where s is Element of Funcs(NAT, REAL) :
ex d,N st d > 0 & for n st n >= N holds d*g.n <= s.n&s.n >= 0 }
by ASYMPT_0:def 13;
now assume seq_n^(2) in Big_Omega(seq_n^(3));
then consider s being Element of Funcs(NAT, REAL) such that
A2: s = f and
A3: ex d,N st d > 0 & for n st n >= N holds d*g.n <= s.n & s.n >= 0 by A1;
consider d,N such that
A4: d > 0 and
A5: for n st n >= N holds d*g.n <= s.n & s.n >= 0 by A3;
A6: N+2 > 1+0 by REAL_1:67;
ex n st n >= N & d*g.n > s.n proof
take n = max( N, [/(N+2)/d\] );
A7: n >= [/(N+2)/d\] & n >= N by SQUARE_1:46;
d" > 0 by A4,REAL_1:72;
then A8: (N+2)*d" > 0*d" by REAL_1:70;
A9: [/(N+2)/d\] >= (N+2)/d by INT_1:def 5;
then A10: n > 0 by A7,A8,XCMPLX_0:def 9;
n is Integer by SQUARE_1:49;
then reconsider n as Nat by A7,INT_1:16;
A11: (d*g.n)*(n to_power -2) = d*(n to_power 3)*(n to_power -2)
by A10,Def3
.= d*((n to_power 3)*(n to_power -2)) by XCMPLX_1:4
.= d*(n to_power (3+(-2))) by A10,POWER:32
.= d*n by POWER:30;
A12: f.n*(n to_power -2)
= (n to_power 2)*(n to_power -2) by A10,Def3
.= (n to_power (2+(-2))) by A10,POWER:32
.= 1 by POWER:29;
A13: d*([/(N+2)/d\]) >= d*((N+2)/d) by A4,A9,AXIOMS:25;
d*n >= d*([/(N+2)/d\]) by A4,A7,AXIOMS:25;
then d*n >= ((N+2)/d)*d by A13,AXIOMS:22;
then d*n >= N+2 by A4,XCMPLX_1:88;
then A14: (d*g.n)*(n to_power -2) > f.n*(n to_power -2) by A6,A11,A12,
AXIOMS:22;
(n to_power -2) > 0 by A10,POWER:39;
hence thesis by A2,A14,AXIOMS:25,SQUARE_1:46;
end;
hence contradiction by A5;
end;
hence thesis;
end;
Lm25:
for a being positive Real, b,c being Real
holds seq_a^(a,b,c) is eventually-positive;
theorem :: Part 3
ex s being eventually-positive Real_Sequence
st s = seq_a^(2,1,1) & seq_a^(2,1,0) in Big_Theta(s)
proof
set f = seq_a^(2,1,0);
reconsider g = seq_a^(2,1,1) as eventually-positive Real_Sequence;
take g;
thus g = seq_a^(2,1,1);
A1: Big_Theta(g) = { s where s is Element of Funcs(NAT, REAL) :
ex c,d,N st c > 0 & d > 0 &
for n st n >= N holds d*g.n <= s.n & s.n <= c*g.n } by ASYMPT_0:27;
A2: f is Element of Funcs(NAT, REAL) by FUNCT_2:11;
A3: (2 to_power -1) > 0 by POWER:39;
now let n; assume n >= 2;
A4: f.n = 2 to_power (1*n+0) by Def1;
A5: g.n = 2 to_power (1*n+1) by Def1;
then (2 to_power -1)*g.n = 2 to_power ((-1)+(n+1)) by POWER:32
.= 2 to_power (n+(1+-1)) by XCMPLX_1:1
.= f.n by A4;
hence (2 to_power -1)*g.n <= f.n;
n+0 <= n+1 by REAL_1:55;
hence f.n <= 1*g.n by A4,A5,PRE_FF:10;
end;
hence thesis by A1,A2,A3;
end;
definition let a be Nat;
func seq_n!(a) -> Real_Sequence means :Def5:
it.n = (n+a)!;
existence proof
deffunc _F(Nat) = ($1+a)!;
consider h being Function of NAT, REAL such that
A1: for n being Nat holds h.n = _F(n) from LambdaD;
take h; let n; thus h.n = (n+a)! by A1;
end;
uniqueness proof let j,k be Real_Sequence such that
A2: for n holds j.n = (n+a)! and
A3: for n holds k.n = (n+a)!;
now let n; thus j.n = (n+a)! by A2 .= k.n by A3; end;
hence j = k by FUNCT_2:113;
end;
end;
definition let a be Nat;
cluster seq_n!(a) -> eventually-positive;
coherence proof
set f = seq_n!(a);
take 0;
let n; assume n >= 0;
f.n = (n+a)! by Def5;
hence f.n > 0 by NEWTON:23;
end;
end;
theorem :: Part 4
not seq_n!(0) in Big_Theta(seq_n!(1))
proof
set f = seq_n!(0);
set g = seq_n!(1);
A1: Big_Theta(g) = { s where s is Element of Funcs(NAT, REAL) :
ex c,d,N st c > 0 & d > 0 &
for n st n >= N holds d*g.n <= s.n & s.n <= c*g.n } by ASYMPT_0:27;
now assume f in Big_Theta(g);
then consider s being Element of Funcs(NAT, REAL) such that
A2: s = f and
A3: ex c,d,N st c > 0 & d > 0 &
for n st n >= N holds d*g.n <= s.n & s.n <= c*g.n by A1;
consider c,d,N such that
c > 0 and
A4: d > 0 and
A5: for n st n >= N holds d*g.n <= s.n & s.n <= c*g.n by A3;
ex n st n >= N & d*g.n > f.n proof
take n = max( N, [/(N+1)/d\] );
A6: n >= N & n >= [/(N+1)/d\] by SQUARE_1:46;
n is Integer by SQUARE_1:49;
then reconsider n as Nat by A6,INT_1:16;
n! > 0 by NEWTON:23;
then A7: (n!)" > 0 by REAL_1:72;
A8: n! <> 0 by NEWTON:23;
A9: (d*g.n)*(n!)" = (d*((n+1)!))*(n!)" by Def5
.= (d*((n+1)*(n!)))*(n!)" by NEWTON:21
.= ((d*(n+1))*(n!))*(n!)" by XCMPLX_1:4
.= (d*(n+1)*((n!)*(n!)")) by XCMPLX_1:4
.= (d*(n+1))*1 by A8,XCMPLX_0:def 7
.= d*(n+1);
[/(N+1)/d\] >= (N+1)/d by INT_1:def 5;
then [/(N+1)/d\] + 1 >= (N+1)/d + 1 by AXIOMS:24;
then A10: d*([/(N+1)/d\] + 1) >= d*((N+1)/d + 1) by A4,AXIOMS:25;
n+1 >= [/(N+1)/d\]+1 by A6,AXIOMS:24;
then d*(n+1) >= d*([/(N+1)/d\]+1) by A4,AXIOMS:25;
then A11: d*(n+1) >= d*(((N+1)/d) + 1) by A10,AXIOMS:22;
A12: d*(((N+1)/d) + 1) = d*((N+1)/d) + d*1 by XCMPLX_1:8
.= (N+1) + d by A4,XCMPLX_1:88;
N+1 >= 1+0 by AXIOMS:24;
then d*(((N+1)/d) + 1) > 1 by A4,A12,REAL_1:67;
then A13: (d*g.n)*(n!)" > 1 by A9,A11,AXIOMS:22;
f.n*(n!)" = (n+0)!*(n!)" by Def5
.= 1 by A8,XCMPLX_0:def 7;
hence thesis by A7,A13,AXIOMS:25,SQUARE_1:46;
end;
hence contradiction by A2,A5;
end;
hence thesis;
end;
begin :: Problem 3.6
Lm26:
now let a,b,c,d be Real;
assume 0 <= b & a <= b & 0 <= c & c <= d;
then a*c <= b*c & b*c <= b*d by AXIOMS:25;
hence a*c <= b*d by AXIOMS:22;
end;
theorem
for f being Real_Sequence
st f in Big_Oh(seq_n^(1)) holds f(#)f in Big_Oh(seq_n^(2))
proof
set g = seq_n^(1);
set h = seq_n^(2);
let f be Real_Sequence;
assume
A1: f in Big_Oh(g);
A2: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 }
by ASYMPT_0:def 12;
A3: Big_Oh(h) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*h.n & t.n >= 0 }
by ASYMPT_0:def 12;
consider t being Element of Funcs(NAT, REAL) such that
A4: t = f and
A5: ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A1,A2;
consider c, N such that
A6: c > 0 and
A7: for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A5;
set d = max( c, c*c );
A8: d >= c & d >= c*c by SQUARE_1:46;
A9: d > 0 by A6,SQUARE_1:46;
A10: t(#)t is Element of Funcs(NAT, REAL) by FUNCT_2:11;
A11: 0 to_power 1 = 0 by POWER:def 2;
now take N; let n; assume n >= N;
then A12: t.n <= c*g.n & t.n >= 0 by A7;
A13: g.n >= 0 proof
per cases;
suppose n = 0;
hence thesis by Def3;
suppose
n > 0;
then g.n = n to_power 1 by Def3
.= n by POWER:30;
hence thesis;
end;
A14: for n holds g.n <= h.n proof
let n;
per cases;
suppose
A15: n = 0;
then g.n = 0 by Def3;
hence g.n <= h.n by A15,Def3;
suppose
n > 0;
then A16: n >= 0+1 by NAT_1:38;
thus g.n <= h.n proof
per cases by A16,REAL_1:def 5;
suppose
A17: n = 1;
(1 to_power 1) = 1 & (1 to_power 2) = 1 by POWER:31;
then g.n = (1 to_power 2) by A17,Def3;
hence g.n <= h.n by A17,Def3;
suppose
A18: n > 1;
then (n to_power 1) < (n to_power 2) by POWER:44;
then g.n < (n to_power 2) by A18,Def3;
hence g.n <= h.n by A18,Def3;
end;
end;
t.n*t.n <= (c*g.n)*(c*g.n) by A12,Lm26;
then t.n*t.n <= (c*(g.n*c*g.n)) by XCMPLX_1:4;
then A19: t.n*t.n <= (c*(c*(g.n*g.n))) by XCMPLX_1:4;
A20: (n to_power 1)*(n to_power 1) = (n to_power (1+1)) proof
per cases;
suppose
n = 0;
hence thesis by A11,POWER:def 2;
suppose n > 0;
hence thesis by POWER:32;
end;
g.n*g.n = h.n proof
per cases;
suppose
A21: n = 0;
hence g.n*g.n = 0*g.n by Def3
.= h.n by A21,Def3;
suppose
A22: n > 0;
hence g.n*g.n = (n to_power 1)*g.n by Def3
.= (n to_power (1+1)) by A20,A22,Def3
.= h.n by A22,Def3;
end;
then A23: t.n*t.n <= (c*c)*h.n by A19,XCMPLX_1:4;
h.n >= g.n by A14;
then (c*c)*h.n <= d*h.n by A8,A13,AXIOMS:25;
then t.n*t.n <= d*h.n by A23,AXIOMS:22;
hence (t(#)t).n <= d*h.n by SEQ_1:12;
t.n*t.n >= t.n*0 by A12,AXIOMS:25;
hence (t(#)t).n >= 0 by SEQ_1:12;
end;
hence thesis by A3,A4,A9,A10;
end;
begin :: Problem 3.7
theorem
ex s being eventually-positive Real_Sequence
st s = seq_a^(2,1,0) & 2(#)seq_n^(1) in Big_Oh( seq_n^(1) ) &
not seq_a^(2,2,0) in Big_Oh(s)
proof
set f = 2(#)seq_n^(1);
set g = seq_n^(1);
set p = seq_a^(2,2,0);
reconsider q = seq_a^(2,1,0) as eventually-positive Real_Sequence;
take q;
thus q = seq_a^(2,1,0);
A1: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 }
by ASYMPT_0:def 12;
A2: Big_Oh(q) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*q.n & t.n >= 0 }
by ASYMPT_0:def 12;
A3: f is Element of Funcs(NAT, REAL) by FUNCT_2:11;
now let n; assume
n >= 0;
thus f.n <= 2*g.n by SEQ_1:13;
A4: g.n = n proof
per cases;
suppose n = 0;
hence thesis by Def3;
suppose n > 0;
hence g.n = n to_power 1 by Def3
.= n by POWER:30;
end;
2*n >= 2*0;
hence f.n >= 0 by A4,SEQ_1:13;
end;
hence f in Big_Oh(g) by A1,A3;
now assume p in Big_Oh(q);
then consider t being Element of Funcs(NAT, REAL) such that
A5: t = p and
A6: ex c,N st c > 0 & for n st n >= N holds t.n <= c*q.n & t.n >= 0 by A2;
consider c,N such that
A7: c > 0 and
A8: for n st n >= N holds t.n <= c*q.n & t.n >= 0 by A6;
ex n st n >= N & t.n > c*q.n proof
take n = max( N, [/log(2,c)+1\] );
A9: n >= N & n >= [/log(2,c)+1\] by SQUARE_1:46;
n is Integer by SQUARE_1:49;
then reconsider n as Nat by A9,INT_1:16;
A10: (c*q.n)*(2 to_power -n)
= (c*(2 to_power (1*n+0)))*(2 to_power -n) by Def1
.= c*((2 to_power n)*(2 to_power -n)) by XCMPLX_1:4
.= c*(2 to_power (n+-n)) by POWER:32
.= c*(2 to_power 0) by XCMPLX_0:def 6
.= c*1 by POWER:29;
A11: p.n*(2 to_power -n) = (2 to_power (2*n+0))*(2 to_power -n) by Def1
.= (2 to_power (2*n+-(1*n))) by POWER:32
.= (2 to_power (2*n+(-1)*n)) by XCMPLX_1:175
.= (2 to_power ((2+-1)*n)) by XCMPLX_1:8
.= (2 to_power (1*n));
A12: 2 to_power n >= 2 to_power [/log(2,c)+1\] by A9,PRE_FF:10;
[/log(2,c)+1\] >= log(2,c)+1 by INT_1:def 5;
then A13: 2 to_power [/log(2,c)+1\] >= 2 to_power (log(2,c)+1) by PRE_FF:10
;
2 to_power (log(2,c)+1)
= (2 to_power log(2,c))*(2 to_power 1) by POWER:32
.= c*(2 to_power 1) by A7,POWER:def 3
.= c*2 by POWER:30;
then 2 to_power (log(2,c)+1) > (c*q.n)*(2 to_power -n)
by A7,A10,REAL_1:70;
then 2 to_power [/log(2,c)+1\] > (c*q.n)*(2 to_power -n) by A13,AXIOMS:
22;
then A14: p.n*(2 to_power -n) > (c*q.n)*(2 to_power -n) by A11,A12,AXIOMS:
22;
2 to_power -n > 0 by POWER:39;
hence thesis by A5,A14,AXIOMS:25,SQUARE_1:46;
end;
hence contradiction by A8;
end;
hence thesis;
end;
begin :: Problem 3.8
theorem
log(2,3) < 159/100 implies
seq_n^(log(2,3)) in Big_Oh(seq_n^(159/100)) &
not seq_n^(log(2,3)) in Big_Omega(seq_n^(159/100)) &
not seq_n^(log(2,3)) in Big_Theta(seq_n^(159/100))
proof
assume
A1: log(2,3) < 159/100;
set f = seq_n^(log(2,3));
set g = seq_n^(159/100);
set h = f/"g;
set c = 159/100 - log(2,3);
log(2,3) - log(2,3) < 159/100 - log(2,3) by A1,REAL_1:54;
then A2: 0 < c by XCMPLX_1:14;
then A3: c*2" > 0*2" by REAL_1:70;
then A4: c/2 > 0 by XCMPLX_0:def 9;
A5: c/2 <> 0 by A3,XCMPLX_0:def 9;
A6: now let p be real number such that
A7: p > 0;
reconsider p1 = p as Real by XREAL_0:def 1;
set N1 = max([/((1/p1) to_power (1/(c/2)))\], 2);
A8: N1 >= [/((1/p) to_power (1/(c/2)))\] & N1 >= 2 by SQUARE_1:46;
then A9: N1 > 1 by AXIOMS:22;
N1 is Integer by SQUARE_1:49;
then reconsider N1 as Nat by A8,INT_1:16;
take N1; let n; assume
A10: n >= N1;
p" > 0 by A7,REAL_1:72;
then A11: 1/p > 0 by XCMPLX_1:217;
[/((1/p) to_power (1/(c/2)))\]>=
((1/p) to_power (1/(c/2))) by INT_1:def 5;
then A12: N1 >= ((1/p) to_power (1/(c/2))) by A8,AXIOMS:22;
A13: ((1/p1) to_power (1/(c/2))) > 0 by A11,POWER:39;
A14: n > 1 by A9,A10,AXIOMS:22;
A15: h.n = f.n/g.n by Lm4;
f.n = (n to_power log(2,3)) by A8,A10,Def3;
then A16: h.n = (n to_power log(2,3)) / (n to_power (159/100)) by A8,A10,A15,
Def3
.= (n to_power (log(2,3) - (159/100))) by A8,A10,POWER:34
.= (n to_power -c) by XCMPLX_1:143;
n >= ((1/p) to_power (1/(c/2))) by A10,A12,AXIOMS:22;
then n to_power (c/2) >=
((1/p) to_power (1/(c/2))) to_power (c/2) by A4,A13,Lm6;
then n to_power (c/2) >=
(1/p1) to_power ((1/(c/2))*(c/2)) by A11,POWER:38;
then n to_power (c/2) >= (1/p) to_power 1 by A5,XCMPLX_1:88;
then n to_power (c/2) >= 1/p1 by POWER:30;
then 1 / (n to_power (c/2)) <= 1 / (1/p) by A11,REAL_2:152;
then 1 / (n to_power (c/2)) <= 1 / (p") by XCMPLX_1:217;
then 1 / (n to_power (c/2)) <= p by XCMPLX_1:218;
then A17: n to_power -(c/2) <= p by A8,A10,POWER:33;
A18: n to_power (c/2) > 0 by A8,A10,POWER:39;
c*(1/2) < c*1 by A2,REAL_1:70;
then c/2 < c by XCMPLX_1:100;
then n to_power (c/2) < n to_power c by A14,POWER:44;
then 1 / (n to_power (c/2)) > 1 / (n to_power c) by A18,REAL_2:151;
then n to_power -(c/2) > 1 / (n to_power c) by A8,A10,POWER:33;
then h.n < n to_power -(c/2) by A8,A10,A16,POWER:33;
then A19: h.n < p by A17,AXIOMS:22;
h.n > 0 by A8,A10,A16,POWER:39;
hence abs(h.n-0) < p by A19,ABSVALUE:def 1;
end;
then A20: h is convergent by SEQ_2:def 6;
then A21:lim h = 0 by A6,SEQ_2:def 7;
then A22: f in Big_Oh(g) & not g in Big_Oh(f) by A20,ASYMPT_0:16;
then A23: f in Big_Oh(g) & not f in Big_Omega(g) by ASYMPT_0:19;
A24: now assume f in Big_Theta(g);
then f in Big_Oh(g) /\ Big_Omega(g) by ASYMPT_0:def 14;
hence contradiction by A23,XBOOLE_0:def 3;
end;
thus f in Big_Oh(g) by A20,A21,ASYMPT_0:16;
thus not f in Big_Omega(g) by A22,ASYMPT_0:19;
thus not f in Big_Theta(g) by A24;
end;
:: Problem 3.9 -- Proven in theorem ASYMPT_0:10
:: Problem 3.10 -- Proven in theorem ASYMPT_0:12
begin :: Problem 3.11
theorem
for f,g being Real_Sequence st
(for n holds f.n = n mod 2) & (for n holds g.n = n+1 mod 2)
holds ex s,s1 being eventually-nonnegative Real_Sequence
st s = f & s1 = g & not s in Big_Oh(s1) & not s1 in Big_Oh(s)
proof
let f,g be Real_Sequence such that
A1: for n holds f.n = n mod 2 and
A2: for n holds g.n = n+1 mod 2;
f is eventually-nonnegative proof
take 0;
let n; assume n >= 0;
A3: f.n = n mod 2 by A1;
per cases by A3,GROUP_4:100;
suppose f.n = 0;
hence f.n >= 0;
suppose f.n = 1;
hence f.n >= 0;
end;
then reconsider f as eventually-nonnegative Real_Sequence;
g is eventually-nonnegative proof
take 0;
let n; assume n >= 0;
A4: g.n = n+1 mod 2 by A2;
per cases by A4,GROUP_4:100;
suppose g.n = 0;
hence g.n >= 0;
suppose g.n = 1;
hence g.n >= 0;
end;
then reconsider g as eventually-nonnegative Real_Sequence;
take f,g;
A5: Big_Oh(f) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 }
by ASYMPT_0:def 12;
A6: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 }
by ASYMPT_0:def 12;
A7: now assume f in Big_Oh(g);
then consider t being Element of Funcs(NAT, REAL) such that
A8: t = f and
A9: ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A6;
consider c,N such that
c > 0 and
A10: for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A9;
ex n st n >= N & t.n > c*g.n proof
per cases by GROUP_4:100;
suppose
A11: N mod 2 = 0;
A12: N+1 >= N by NAT_1:38;
A13: t.(N+1) = (N+1) mod 2 by A1,A8
.= (0+(1 mod 2)) mod 2 by A11,EULER_2:8
.= (0+1) mod 2 by GROUP_4:102
.= 1 by GROUP_4:102;
g.(N+1) = ((N+1)+1) mod 2 by A2
.= (N+(1+1)) mod 2 by XCMPLX_1:1
.= (0+(2 mod 2)) mod 2 by A11,EULER_2:8
.= (0+0) mod 2 by GR_CY_1:5
.= 0 by GR_CY_1:6;
then c*g.(N+1) = 0;
hence thesis by A12,A13;
suppose
A14: N mod 2 = 1;
then A15: t.N = 1 by A1,A8;
g.N = (N+1) mod 2 by A2
.= (1+(1 mod 2)) mod 2 by A14,EULER_2:8
.= (1+1) mod 2 by GROUP_4:102
.= 0 by GR_CY_1:5;
then c*g.N = 0;
hence thesis by A15;
end;
hence contradiction by A10;
end;
now assume g in Big_Oh(f);
then consider t being Element of Funcs(NAT, REAL) such that
A16: t = g and
A17: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A5;
consider c,N such that
c > 0 and
A18: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A17;
ex n st n >= N & t.n > c*f.n proof
per cases by GROUP_4:100;
suppose
A19: N mod 2 = 0;
A20: t.N = (N+1) mod 2 by A2,A16
.= (0+(1 mod 2)) mod 2 by A19,EULER_2:8
.= (0+1) mod 2 by GROUP_4:102
.= 1 by GROUP_4:102;
f.N = 0 by A1,A19;
then c*f.N = 0;
hence thesis by A20;
suppose
A21: N mod 2 = 1;
A22: N+1 >= N by NAT_1:38;
A23: t.(N+1) = ((N+1)+1) mod 2 by A2,A16
.= (N+(1+1)) mod 2 by XCMPLX_1:1
.= (1+(2 mod 2)) mod 2 by A21,EULER_2:8
.= (1+0) mod 2 by GR_CY_1:5
.= 1 by GROUP_4:102;
f.(N+1) = (N+1) mod 2 by A1
.= (1+(1 mod 2)) mod 2 by A21,EULER_2:8
.= (1+1) mod 2 by GROUP_4:102
.= 0 by GR_CY_1:5;
then c*f.(N+1) = 0;
hence thesis by A22,A23;
end;
hence contradiction by A18;
end;
hence thesis by A7;
end;
:: Problem 3.12 -- Proven in theorems ASYMPT_0:20, ASYMPT_0:21
:: Problem 3.13 -- omitted (uses a notation that we do not support)
:: Problem 3.14 -- omitted (cannot Mizar an incorrect proof)
:: Problem 3.15 -- omitted (cannot Mizar an incorrect proof)
:: Problem 3.16 -- omitted (maximum rule over multiple functions can be
:: reduced to repeated applications of the binary
:: maximum rule)
:: Problem 3.17 -- omitted (cannot Mizar an incorrect proof)
:: Problem 3.18 -- Proven in theorems ASYMPT_0:28, ASYMPT_0:29, ASYMPT_0:30
begin :: Problem 3.19
theorem :: Part 1
for f,g being eventually-nonnegative Real_Sequence holds
Big_Oh(f) = Big_Oh(g) iff f in Big_Theta(g)
proof
let f,g be eventually-nonnegative Real_Sequence;
A1: Big_Oh(f) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 }
by ASYMPT_0:def 12;
A2: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 }
by ASYMPT_0:def 12;
hereby assume
A3: Big_Oh(f) = Big_Oh(g);
then A4: f in Big_Oh(g) by ASYMPT_0:10;
g in Big_Oh(f) by A3,ASYMPT_0:10;
then f in Big_Omega(g) by ASYMPT_0:19;
then f in Big_Oh(g) /\ Big_Omega(g) by A4,XBOOLE_0:def 3;
hence f in Big_Theta(g) by ASYMPT_0:def 14;
end;
assume
A5: f in Big_Theta(g);
now let x be set;
hereby assume x in Big_Oh(f);
then consider t being Element of Funcs(NAT, REAL) such that
A6: x = t and
A7: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A1;
consider c,N such that
c > 0 and
A8: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A7;
now take N; let n; assume n >= N;
hence t.n >= 0 by A8;
end;
then A9: t is eventually-nonnegative by ASYMPT_0:def 4;
A10: t in Big_Oh(f) by A1,A7;
f in Big_Oh(g) /\ Big_Omega(g) by A5,ASYMPT_0:def 14;
then f in Big_Oh(g) by XBOOLE_0:def 3;
hence x in Big_Oh(g) by A6,A9,A10,ASYMPT_0:12;
end;
assume x in Big_Oh(g);
then consider t being Element of Funcs(NAT, REAL) such that
A11: x = t and
A12: ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A2;
consider c,N such that
c > 0 and
A13: for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A12;
now take N; let n; assume n >= N;
hence t.n >= 0 by A13;
end;
then A14: t is eventually-nonnegative by ASYMPT_0:def 4;
A15: t in Big_Oh(g) by A2,A12;
f in Big_Oh(g) /\ Big_Omega(g) by A5,ASYMPT_0:def 14;
then f in Big_Omega(g) by XBOOLE_0:def 3;
then g in Big_Oh(f) by ASYMPT_0:19;
hence x in Big_Oh(f) by A11,A14,A15,ASYMPT_0:12;
end;
hence Big_Oh(f) = Big_Oh(g) by TARSKI:2;
end;
theorem :: Part 2
for f,g being eventually-nonnegative Real_Sequence holds
f in Big_Theta(g) iff Big_Theta(f) = Big_Theta(g)
proof
let f,g be eventually-nonnegative Real_Sequence;
A1: Big_Theta(f) = { s where s is Element of Funcs(NAT, REAL) :
ex c,d,N st c > 0 & d > 0 &
for n st n >= N holds d*f.n <= s.n & s.n <= c*f.n } by ASYMPT_0:27;
A2: Big_Theta(g) = { s where s is Element of Funcs(NAT, REAL) :
ex c,d,N st c > 0 & d > 0 &
for n st n >= N holds d*g.n <= s.n & s.n <= c*g.n } by ASYMPT_0:27;
consider N1 such that
A3: for n st n >= N1 holds f.n >= 0 by ASYMPT_0:def 4;
consider N2 such that
A4: for n st n >= N2 holds g.n >= 0 by ASYMPT_0:def 4;
hereby assume
A5: f in Big_Theta(g);
now let x be set;
hereby assume x in Big_Theta(f);
then consider s being Element of Funcs(NAT, REAL) such that
A6: s = x and
A7: ex c,d,N st c > 0 & d > 0 &
for n st n >= N holds d*f.n <= s.n & s.n <= c*f.n by A1;
consider c,d,N3 such that
c > 0 and
A8: d > 0 and
A9: for n st n >= N3 holds d*f.n <= s.n & s.n <= c*f.n by A7;
set N = max( N1, N3 );
A10: N >= N1 & N >= N3 by SQUARE_1:46;
now take N; let n; assume n >= N;
then A11: n >= N1 & n >= N3 by A10,AXIOMS:22;
then f.n >= 0 by A3;
then d*f.n >= d*0 by A8,AXIOMS:25;
hence s.n >= 0 by A9,A11;
end;
then A12: s is eventually-nonnegative by ASYMPT_0:def 4;
s in Big_Theta(f) by A1,A7;
hence x in Big_Theta(g) by A5,A6,A12,ASYMPT_0:30;
end;
assume x in Big_Theta(g);
then consider s being Element of Funcs(NAT, REAL) such that
A13: s = x and
A14: ex c,d,N st c > 0 & d > 0 &
for n st n >= N holds d*g.n <= s.n & s.n <= c*g.n by A2;
consider c,d,N3 such that
c > 0 and
A15: d > 0 and
A16: for n st n >= N3 holds d*g.n <= s.n & s.n <= c*g.n by A14;
set N = max( N2, N3 );
A17: N >= N2 & N >= N3 by SQUARE_1:46;
now take N; let n; assume n >= N;
then A18: n >= N2 & n >= N3 by A17,AXIOMS:22;
then g.n >= 0 by A4;
then d*g.n >= d*0 by A15,AXIOMS:25;
hence s.n >= 0 by A16,A18;
end;
then A19: s is eventually-nonnegative by ASYMPT_0:def 4;
A20: s in Big_Theta(g) by A2,A14;
g in Big_Theta(f) by A5,ASYMPT_0:29;
hence x in Big_Theta(f) by A13,A19,A20,ASYMPT_0:30;
end;
hence Big_Theta(f) = Big_Theta(g) by TARSKI:2;
end;
assume Big_Theta(f) = Big_Theta(g);
hence f in Big_Theta(g) by ASYMPT_0:28;
end;
:: Problem 3.20 -- Proven above in theorem ASYMPT_1:?????
begin :: Problem 3.21
Lm27:
for n holds (n^2 - n + 1) > 0
proof defpred _P[Nat] means ($1^2 - $1 + 1) > 0;
A1: _P[0] proof 0^2 -0 + 1 = 0*0 - 0 + 1 by SQUARE_1:def 3 .= 1;
hence thesis;
end;
A2: for k st _P[k] holds _P[k+1] proof let k such that
A3: (k^2 - k + 1) > 0;
A4: ((k+1)^2 - (k+1) + 1) = ((k^2 + 2*k*1 + 1^2) - (k+1) + 1) by SQUARE_1:63
.= ((k^2 + 2*k + 1*1) - (k+1) + 1) by SQUARE_1:def 3
.= ((k^2 + 2*k + 1) - k - 1 + 1) by XCMPLX_1:36
.= ((k^2 + 2*k + 1) - k + -1 + 1) by XCMPLX_0:def 8
.= ((k^2 + 2*k + 1) + -k + -1 + 1) by XCMPLX_0:def 8
.= ((k^2 + 2*k + 1) + -k + (-1 + 1)) by XCMPLX_1:1
.= ((k^2 + (2*k + 1)) + -k) by XCMPLX_1:1
.= (k^2 + ((1 + 2*k) + -k)) by XCMPLX_1:1
.= (k^2 + ((1 + -k) + 2*k)) by XCMPLX_1:1
.= ((k^2 + (1 + -k)) + 2*k) by XCMPLX_1:1
.= ((k^2 + -k + 1) + 2*k) by XCMPLX_1:1
.= ((k^2 -k + 1) + 2*k) by XCMPLX_0:def 8;
(k^2 - k + 1) + 2*k > 0+0 by A3,REAL_1:67;
hence thesis by A4;
end;
for n holds _P[n] from Ind(A1, A2);
hence thesis;
end;
Lm28:
for f,g being Real_Sequence, N being Nat, c being Real
st f is convergent & lim f = c & for n st n >= N holds f.n = g.n
holds g is convergent & lim g = c
proof
let f,g be Real_Sequence, N be Nat, c be Real such that
A1: f is convergent and
A2: lim f = c and
A3: for n st n >= N holds f.n = g.n;
A4: now let p be real number; assume
p > 0;
then consider M such that
A5: for n st n >= M holds abs(f.n-c) < p by A1,A2,SEQ_2:def 7;
set N1 = max(N, M);
A6: N1 >= N & N1 >= M by SQUARE_1:46;
take N1; let n; assume
n >= N1;
then A7: n >= N & n >= M by A6,AXIOMS:22;
then abs(f.n-c) < p by A5;
hence abs(g.n-c) < p by A3,A7;
end;
hence g is convergent by SEQ_2:def 6;
hence lim g = c by A4,SEQ_2:def 7;
end;
Lm29:
for n st n >= 1 holds (n^2 -n + 1) <= n^2
proof
let n such that
A1: n >= 1;
now assume (n^2 -n + 1) > n^2;
then (n^2 + -n + 1) > n^2 by XCMPLX_0:def 8;
then n^2 + (-n + 1) > n^2 by XCMPLX_1:1;
then -n^2 + (n^2 + (-n + 1)) > n^2 + -n^2 by REAL_1:53;
then (-n^2 + n^2) + (-n + 1) > n^2 + -n^2 by XCMPLX_1:1;
then 0 + (-n + 1) > n^2 + -n^2 by XCMPLX_0:def 6;
then -n + 1 > 0 by XCMPLX_0:def 6;
then 1 > 0 -(-n) by REAL_1:84;
then 1 > 0 + -(-n) by XCMPLX_0:def 8;
hence contradiction by A1;
end;
hence thesis;
end;
Lm30:
for n st n >= 1 holds n^2 <= 2*(n^2 -n + 1)
proof
defpred _P[Nat] means $1^2 <= 2*($1^2 -$1 + 1);
A1: _P[1] proof 1^2 = 1*1 by SQUARE_1:def 3 .= 1; hence thesis; end;
A2: for k st k>=1 & _P[k] holds _P[k+1] proof let k such that
A3: k >= 1 and
A4: k^2 <= 2*(k^2 -k + 1);
A5: (k+1)^2 = k^2 + 2*k*1 + 1^2 by SQUARE_1:63
.= k^2 + 2*k + 1*1 by SQUARE_1:def 3
.= k^2 + 2*k + 1;
k^2 + (2*k + 1) <= 2*(k^2 -k + 1) + (2*k + 1) by A4,AXIOMS:24;
then A6: (k+1)^2 <= 2*(k^2 -k + 1) + (2*k + 1) by A5,XCMPLX_1:1;
A7: 2*(k^2 -k + 1) + (2*k + 1) = 2*(k^2
+ -k + 1) + (2*k + 1) by XCMPLX_0:def 8
.= (2*(k^2 + -k) + 2*1) + (2*k + 1) by XCMPLX_1:8
.= ((2*k^2 + 2*(-k)) + 2) + (2*k + 1) by XCMPLX_1:8
.= (2*k^2 + (2*(-k) + 2)) + (2*k + 1) by XCMPLX_1:1
.= (2*k^2 + (-2*k + 2)) + (2*k + 1) by XCMPLX_1:175
.= ((2*k^2 + 2) + -2*k) + (2*k + 1) by XCMPLX_1:1
.= (2*k^2 + 2) + (-2*k + (2*k + 1)) by XCMPLX_1:1
.= (2*k^2 + 2) + ((-2*k + 2*k) + 1) by XCMPLX_1:1
.= (2*k^2 + 2) + (0 + 1) by XCMPLX_0:def 6
.= 2*k^2 + (2 + 1) by XCMPLX_1:1
.= 2*k^2 + 3;
2*k >= 2*1 by A3,AXIOMS:25;
then A8: 2*k + 2 >= 2 + 2 by AXIOMS:24;
A9: 2*k^2 + 3 <= 2*k^2 + 4 by AXIOMS:24;
2*k^2 + 4 <= 2*k^2 + (2*k + 2) by A8,AXIOMS:24;
then A10: 2*(k^2 -k + 1) + (2*k + 1) <= 2*k^2
+ (2*k + 2) by A7,A9,AXIOMS:22;
2*k^2 + (2*k + 2) = 2*k^2 + (2*k + 2*1)
.= 2*k^2 + (2*(k + 1)) by XCMPLX_1:8
.= 2*(k^2 + (k + 1)) by XCMPLX_1:8
.= 2*(k^2 + (2+-1)*k + 1) by XCMPLX_1:1
.= 2*(k^2 + (2*k + (-1)*k) + 1) by XCMPLX_1:8
.= 2*(((k^2 + 2*k) + (-1)*k) + 1) by XCMPLX_1:1
.= 2*((k^2 + 2*k) + (1 + -1) + ((-1)*k + 1)) by XCMPLX_1:1
.= 2*((((k^2 + 2*k) + 1) + -1) + ((-1)*k + 1)) by XCMPLX_1:1
.= 2*(((k^2 + 2*k) + 1) + (-1 + ((-1)*k + 1))) by XCMPLX_1:1
.= 2*((k^2 + 2*k*1 + 1*1) + (((-1)*k + -1) + 1)) by XCMPLX_1:1
.= 2*((k^2 + 2*k*1 + 1^2) + (((-1)*k + -1) + 1)) by SQUARE_1:
def 3
.= 2*((k+1)^2 + (((-1)*k + (-1)*1) + 1)) by SQUARE_1:63
.= 2*((k+1)^2 + ((-1)*(k + 1) + 1)) by XCMPLX_1:8
.= 2*((k+1)^2 + (-(k + 1) + 1)) by XCMPLX_1:180
.= 2*((k+1)^2 + -(k + 1) + 1) by XCMPLX_1:1
.= 2*((k+1)^2 -(k + 1) + 1) by XCMPLX_0:def 8;
hence thesis by A6,A10,AXIOMS:22;
end;
for n st n >= 1 holds _P[n] from Ind1(A1, A2);
hence thesis;
end;
Lm31:
for e being Real st 0 < e & e < 1 holds
ex N st for n st n >= N holds n*log(2,1+e) - 8*log(2,n) > 8*log(2,n)
proof
let e be Real such that
A1: 0 < e and
A2: e < 1;
set f = seq_logn;
set g = seq_n^(e);
set h = f/"g;
A3: h is convergent & lim h = 0 by A1,Lm16;
set d = log(2,1+e);
0+1 < e+1 by A1,REAL_1:53;
then log(2,1) < log(2,e+1) by POWER:65;
then A4: d > 0 by POWER:59;
then d*(1/16) > d*0 by REAL_1:70;
then d/16 > 0 by XCMPLX_1:100;
then consider N such that
A5: for n st n >= N holds abs(h.n-0) < d/16 by A3,SEQ_2:def 7;
ex N st for n st n >= N holds n*log(2,1+e) - 8*log(2,n) > 8*log(2,n) proof
set N1 = max(2, N);
A6: N1 >= 2 & N1 >= N by SQUARE_1:46;
now take N1; let n; assume A7: n >= N1;
then A8: n >= 2 & n >= N by A6,AXIOMS:22;
then A9: abs(h.n-0) < d/16 by A5;
log(2,2) <= log(2,n) by A8,PRE_FF:12;
then A10: 1 <= log(2,n) by POWER:60;
A11: h.n = f.n / g.n by Lm4
.= log(2,n) / g.n by A6,A7,Def2
.= log(2,n) / (n to_power e) by A6,A7,Def3;
A12: n to_power e > 0 by A6,A7,POWER:39;
then (n to_power e)" > 0 by REAL_1:72;
then log(2,n)*(n to_power e)" > 0*(n to_power e)" by A10,REAL_1:70;
then h.n > 0 by A11,XCMPLX_0:def 9;
then A13: h.n < d/16 by A9,ABSVALUE:def 1;
n > 1 by A8,AXIOMS:22;
then n to_power 1 > n to_power e by A2,POWER:44;
then 1 / (n to_power 1) < 1 / (n to_power e) by A12,REAL_2:151;
then 1 / n < 1 / (n to_power e) by POWER:30;
then log(2,n) * (1 / n) <
log(2,n) * (1 / (n to_power e)) by A10,REAL_1:70;
then log(2,n) / n < log(2,n) * (1/(n to_power e)) by XCMPLX_1:100;
then log(2,n) / n < h.n by A11,XCMPLX_1:100;
then A14: log(2,n) / n < d / 16 by A13,AXIOMS:22;
n" > 0 by A6,A7,REAL_1:72;
then log(2,n)*n" > 0*n" by A10,REAL_1:70;
then log(2,n) / n > 0 by XCMPLX_0:def 9;
then 1 / (log(2,n) / n) > 1 / (d / 16) by A14,REAL_2:151;
then n / log(2,n) > 1 / (d / 16) by XCMPLX_1:57;
then n / log(2,n) > 16 / d by XCMPLX_1:57;
then d * (n / log(2,n)) > 16 / d * d by A4,REAL_1:70;
then d * (n / log(2,n)) > 16 by A4,XCMPLX_1:88;
then d * (n / log(2,n)) * log(2,n) > 16*log(2,n) by A10,REAL_1:70;
then d * ((n / log(2,n)) * log(2,n)) > 16*log(2,n) by XCMPLX_1:4;
then d*n > (8+8)*log(2,n) by A10,XCMPLX_1:88;
then d*n > 8*log(2,n) + 8*log(2,n) by XCMPLX_1:8;
then d*n - 8*log(2,n) >
(8*log(2,n) + 8*log(2,n)) - 8*log(2,n) by REAL_1:54;
then d*n - 8*log(2,n) >
(8*log(2,n) + 8*log(2,n)) + -8*log(2,n) by XCMPLX_0:def 8;
then d*n - 8*log(2,n) >
8*log(2,n) + (8*log(2,n) + -8*log(2,n)) by XCMPLX_1:1;
then d*n - 8*log(2,n) >
8*log(2,n) + (8*log(2,n) - 8*log(2,n)) by XCMPLX_0:def 8;
then d*n - 8*log(2,n) > 8*log(2,n) + 0 by XCMPLX_1:14;
hence n*d - 8*log(2,n) > 8*log(2,n);
end;
hence thesis;
end;
hence thesis;
end;
theorem :: (Part 1, O(nlogn) c O(n^(1+e))), slightly generalized
for e being Real, f being Real_Sequence
st 0 < e & (f.0 = 0 & (for n st n > 0 holds f.n = n*log(2,n)))
holds ex s being eventually-positive Real_Sequence st
s = f & Big_Oh(s) c= Big_Oh(seq_n^(1+e)) &
not Big_Oh(s) = Big_Oh(seq_n^(1+e))
proof
let e be Real, f be Real_Sequence such that
A1: 0 < e and
A2: (f.0 = 0 & (for n st n > 0 holds f.n = n*log(2,n)));
f is eventually-positive proof
take 2;
let n; assume
A3: n >= 2;
then log(2,n) >= log(2,2) by PRE_FF:12;
then log(2,n) >= 1 by POWER:60;
then n*log(2,n) > n*0 by A3,REAL_1:70;
hence f.n > 0 by A2,A3;
end;
then reconsider f as eventually-positive Real_Sequence;
take f;
set g = seq_n^(1+e);
set h = f /" g;
set seq = seq_logn;
set seq1 = seq_n^(e);
set p = seq /" seq1;
A4: p is convergent & lim p = 0 by A1,Lm16;
for n st n >= 1 holds h.n = p.n proof
let n; assume A5: n >= 1;
h.n = f.n / g.n by Lm4
.= n*log(2,n) / g.n by A2,A5
.= n*log(2,n) / (n to_power (1+e)) by A5,Def3
.= (n to_power 1)*log(2,n) / (n to_power (1+e)) by POWER:30
.= (n to_power 1)*log(2,n) * (n to_power (1+e))" by XCMPLX_0:def 9
.= log(2,n)*((n to_power 1)*(n to_power (1+e))") by XCMPLX_1:4
.= log(2,n)*((n to_power 1)/(n to_power (1+e))) by XCMPLX_0:def 9
.= log(2,n)*(n to_power (1-(1+e))) by A5,POWER:34
.= log(2,n)*(n to_power (1+-(1+e))) by XCMPLX_0:def 8
.= log(2,n)*(n to_power (1+(-1+-e))) by XCMPLX_1:140
.= log(2,n)*(n to_power ((1+-1)+-e)) by XCMPLX_1:1
.= log(2,n)*(1/(n to_power e)) by A5,POWER:33
.= log(2,n)/(n to_power e) by XCMPLX_1:100
.= seq.n / (n to_power e) by A5,Def2
.= seq.n / seq1.n by A5,Def3
.= p.n by Lm4;
hence h.n = p.n;
end;
then h is convergent & lim h = 0 by A4,Lm28;
then f in Big_Oh(g) & not g in Big_Oh(f) by ASYMPT_0:16;
then f in Big_Oh(g) & not f in Big_Omega(g) by ASYMPT_0:19;
hence thesis by Th4;
end;
theorem :: (Part 2, O(n^(1+e)) c O(n^2/logn))
for e being Real, g being Real_Sequence
st 0 < e & e < 1 &
(g.0 = 0 & g.1 = 0 & (for n st n > 1 holds g.n = (n to_power 2)/log(2,n)))
holds ex s being eventually-positive Real_Sequence st
s = g & Big_Oh(seq_n^(1+e)) c= Big_Oh(s) &
not Big_Oh(seq_n^(1+e)) = Big_Oh(s)
proof
let e be Real, g be Real_Sequence such that 0 < e and
A1: e < 1 and
A2: (g.0 = 0 & g.1 = 0 & (for n st n > 1 holds g.n = (n to_power 2)/log(2,n)));
set f = seq_n^(1+e);
set h = f /" g;
set seq = seq_logn;
set seq1 = seq_n^(1-e);
set p = seq /" seq1;
g is eventually-positive proof
take 2;
let n; assume
A3: n >= 2;
then n > 1 by AXIOMS:22;
then A4: g.n = (n to_power 2)/log(2,n) by A2
.= (n to_power 2)*(log(2,n))" by XCMPLX_0:def 9;
A5: n to_power 2 > 0 by A3,POWER:39;
log(2,n) >= log(2,2) by A3,PRE_FF:12;
then log(2,n) >= 1 by POWER:60;
then (log(2,n))" > 0 by REAL_1:72;
then (n to_power 2)*(log(2,n))" > (n to_power 2)*0 by A5,REAL_1:70;
hence g.n > 0 by A4;
end;
then reconsider g as eventually-positive Real_Sequence;
take g;
0+e < 1 by A1;
then 0 < 1-e by REAL_1:86;
then A6: p is convergent & lim p = 0 by Lm16;
A7: (1+e)-2 = (e+1)+-2 by XCMPLX_0:def 8
.= e+(1+-2) by XCMPLX_1:1
.= e+-1
.= e-1 by XCMPLX_0:def 8;
for n st n >= 2 holds h.n = p.n proof
let n; assume
A8: n >= 2;
then A9: n > 1 by AXIOMS:22;
h.n = f.n / g.n by Lm4
.= (n to_power (1+e)) / g.n by A8,Def3
.= (n to_power (1+e)) /
((n to_power 2) / log(2,n)) by A2,A9
.= (n to_power (1+e)) * ((n to_power 2) / log(2,n))" by XCMPLX_0:def
9
.= (n to_power (1+e)) * (log(2,n) / (n to_power 2)) by XCMPLX_1:215
.= (n to_power (1+e)) * (log(2,n) * (n to_power 2)") by XCMPLX_0:def
9
.= ((n to_power (1+e)) * (n to_power 2)") * log(2,n) by XCMPLX_1:4
.= ((n to_power (1+e)) / (n to_power 2)) * log(2,n) by XCMPLX_0:def 9
.= (n to_power (e-1)) * log(2,n) by A7,A8,POWER:34
.= (n to_power -(1-e)) * log(2,n) by XCMPLX_1:143
.= log(2,n) * (1 / (n to_power (1-e))) by A8,POWER:33
.= log(2,n) / (n to_power (1-e)) by XCMPLX_1:100
.= seq.n / (n to_power (1-e)) by A8,Def2
.= seq.n / seq1.n by A8,Def3
.= p.n by Lm4;
hence thesis;
end;
then h is convergent & lim h = 0 by A6,Lm28;
then f in Big_Oh(g) & not g in Big_Oh(f) by ASYMPT_0:16;
then f in Big_Oh(g) & not f in Big_Omega(g) by ASYMPT_0:19;
hence thesis by Th4;
end;
theorem :: (Part 3, O(n^2/logn) c O(n^8))
for f being Real_Sequence st
(f.0 = 0 & f.1 = 0 & (for n st n > 1 holds f.n = (n to_power 2)/log(2,n)))
holds ex s being eventually-positive Real_Sequence st
s = f & Big_Oh(s) c= Big_Oh(seq_n^(8)) &
not Big_Oh(s) = Big_Oh(seq_n^(8))
proof
let f be Real_Sequence such that
A1: (f.0 = 0 & f.1 = 0 & (for n st n > 1 holds f.n = (n to_power 2)/log(2,n)));
set g = seq_n^(8);
set h = f/"g;
f is eventually-positive proof
take 2;
let n; assume
A2: n >= 2;
then n > 1 by AXIOMS:22;
then A3: f.n = (n to_power 2)/log(2,n) by A1
.= (n to_power 2)*(log(2,n))" by XCMPLX_0:def 9;
A4: n to_power 2 > 0 by A2,POWER:39;
log(2,n) >= log(2,2) by A2,PRE_FF:12;
then log(2,n) >= 1 by POWER:60;
then (log(2,n))" > 0 by REAL_1:72;
then (n to_power 2)*(log(2,n))" > (n to_power 2)*0 by A4,REAL_1:70;
hence f.n > 0 by A3;
end;
then reconsider f as eventually-positive Real_Sequence;
take f;
A5: now let p be real number; assume
A6: p > 0;
reconsider p1 = p as Real by XREAL_0:def 1;
set N = max(3,[/(p1 to_power -(1/6))\]);
A7: N >= 3 & N >= [/(p to_power -(1/6))\] by SQUARE_1:46;
N is Integer by SQUARE_1:49;
then reconsider N as Nat by A7,INT_1:16;
take N; let n; assume A8: n >= N;
then A9: n >= 3 & n >= [/(p to_power -(1/6))\] by A7,AXIOMS:22;
then A10: log(2,n) >= log(2,3) by PRE_FF:12;
log(2,3) > log(2,2) by POWER:65;
then log(2,n) > log(2,2) by A10,AXIOMS:22;
then A11: log(2,n) > 1 by POWER:60;
A12: n > 1 by A9,AXIOMS:22;
A13: n to_power 6 > 0 by A7,A8,POWER:39;
A14: h.n = f.n/g.n by Lm4
.= ((n to_power 2)/log(2,n)) / g.n by A1,A12
.= ((n to_power 2)/log(2,n)) / (n to_power 8) by A7,A8,Def3
.= ((n to_power 2)*(log(2,n))") / (n to_power 8) by XCMPLX_0:def 9
.= ((log(2,n))"*(n to_power 2)) * (n to_power 8)" by XCMPLX_0:def 9
.= (log(2,n))"*((n to_power 2)*(n to_power 8)") by XCMPLX_1:4
.= (log(2,n))"*((n to_power 2)/(n to_power 8)) by XCMPLX_0:def 9
.= (log(2,n))"*(n to_power (2-8)) by A7,A8,POWER:34
.= (log(2,n))"*(n to_power -6)
.= (log(2,n))"*(1/(n to_power 6)) by A7,A8,POWER:33
.= (1/(n to_power 6))*(1/log(2,n)) by XCMPLX_1:217
.= 1/((n to_power 6)*log(2,n)) by XCMPLX_1:103;
(n to_power 6)*1 < (n to_power 6)*log(2,n) by A11,A13,REAL_1:70;
then A15: h.n < 1/(n to_power 6) by A13,A14,REAL_2:151;
A16: (p1 to_power -(1/6)) > 0 by A6,POWER:39;
[/(p to_power -(1/6))\] >= (p to_power -(1/6)) by INT_1:def 5;
then n >= (p to_power -(1/6)) by A9,AXIOMS:22;
then n to_power 6 >= (p to_power -(1/6)) to_power 6 by A16,Lm6;
then A17: n to_power 6 >= p1 to_power ((-(1/6))*6) by A6,POWER:38;
p1 to_power -1 > 0 by A6,POWER:39;
then 1/(n to_power 6) <= 1/(p to_power -1) by A17,REAL_2:152;
then 1/(n to_power 6) <= 1/(1/(p1 to_power 1)) by A6,POWER:33;
then 1/(n to_power 6) <= 1/(1/p1) by POWER:30;
then 1/(n to_power 6) <= p by XCMPLX_1:56;
then A18: h.n < p by A15,AXIOMS:22;
(n to_power 6)*log(2,n) > (n to_power 6)*0 by A11,A13,REAL_1:70;
then ((n to_power 6)*log(2,n))" > 0 by REAL_1:72;
then h.n > 0 by A14,XCMPLX_1:217;
hence abs(h.n-0) < p by A18,ABSVALUE:def 1;
end;
then A19: h is convergent by SEQ_2:def 6;
then lim h = 0 by A5,SEQ_2:def 7;
then f in Big_Oh(g) & not g in Big_Oh(f) by A19,ASYMPT_0:16;
then f in Big_Oh(g) & not f in Big_Omega(g) by ASYMPT_0:19;
hence thesis by Th4;
end;
theorem :: (Part 4, O(n^8) = O((n^2-n+1)^4))
for g being Real_Sequence st (for n holds g.n = (n^2 - n + 1) to_power 4)
holds ex s being eventually-positive Real_Sequence st
s = g & Big_Oh(seq_n^(8)) = Big_Oh(s)
proof
let g be Real_Sequence such that
A1: (for n holds g.n = (n^2 - n + 1) to_power 4);
set f = seq_n^(8);
g is eventually-positive proof
take 0;
let n; assume n >= 0;
A2: g.n = (n^2 - n + 1) to_power 4 by A1;
n^2 - n + 1 > 0 by Lm27;
hence g.n > 0 by A2,POWER:39;
end;
then reconsider g as eventually-positive Real_Sequence;
take g;
A3: Big_Oh(f) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 }
by ASYMPT_0:def 12;
A4: Big_Oh(g) = { t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0 }
by ASYMPT_0:def 12;
A5: f is Element of Funcs(NAT, REAL) by FUNCT_2:11;
A6: g is Element of Funcs(NAT, REAL) by FUNCT_2:11;
now let n; assume
A7: n >= 1;
then A8: f.n = n to_power (2*4) by Def3
.= n to_power 2 to_power 4 by A7,POWER:38
.= n^2 to_power 4 by POWER:53;
A9: g.n = (n^2 -n + 1) to_power 4 by A1;
A10: n^2 -n + 1 <= n^2 by A7,Lm29;
A11: n^2 -n + 1 > 0 by Lm27;
hence g.n <= 1*f.n by A8,A9,A10,Lm6;
thus g.n >= 0 by A9,A11,POWER:39;
end;
then A12: g in Big_Oh(f) by A3,A6;
now let n; assume
A13: n >= 1;
then A14: f.n = n to_power (2*4) by Def3
.= n to_power 2 to_power 4 by A13,POWER:38
.= n^2 to_power 4 by POWER:53;
A15: g.n = (n^2 -n + 1) to_power 4 by A1;
A16: n^2 <= 2*(n^2 -n + 1) by A13,Lm30;
A17: (n^2 -n + 1) > 0 by Lm27;
n*n > n*0 by A13,REAL_1:70;
then A18: n^2 > 0 by SQUARE_1:def 3;
then f.n <= (2*(n^2 -n + 1)) to_power 4 by A14,A16,Lm6;
hence f.n <= 16*g.n by A15,A17,Lm9,POWER:35;
thus f.n >= 0 by A14,A18,POWER:39;
end;
then f in Big_Oh(g) by A4,A5;
hence thesis by A12,Lm5;
end;
theorem :: (Part 5, O(n^8) c O((1+e)^n))
for e being Real st 0 < e & e < 1 holds
ex s being eventually-positive Real_Sequence st s = seq_a^(1+e,1,0) &
Big_Oh(seq_n^(8)) c= Big_Oh(s) & not Big_Oh(seq_n^(8)) = Big_Oh(s)
proof
let e be Real such that
A1: 0 < e and
A2: e < 1;
set f = seq_n^(8);
set g = seq_a^(1+e,1,0);
set h = f/"g;
A3: 1 + e > 0 + 0 by A1,REAL_1:67;
then reconsider g as eventually-positive Real_Sequence by Lm25;
take g;
thus g = seq_a^(1+e,1,0);
consider N such that
A4: for n st n >= N holds n*log(2,1+e) - 8*log(2,n) > 8*log(2,n)
by A1,A2,Lm31;
A5: now let p be real number such that
A6: p > 0;
reconsider p1 = p as Real by XREAL_0:def 1;
set N1 = max( N, max([/((1/p1) to_power (1/8))\], 2) );
A7: N1 >= N & N1 >= max([/((1/p) to_power (1/8))\], 2) by SQUARE_1:46;
A8: max([/((1/p) to_power (1/8))\], 2) >= [/((1/p) to_power (1/8))\] &
max([/((1/p) to_power (1/8))\], 2) >= 2 by SQUARE_1:46;
then A9: N1 >= [/((1/p) to_power (1/8))\] & N1 >= 2 by A7,AXIOMS:22;
N1 is Integer proof
per cases by SQUARE_1:49;
suppose N1 = N;
hence thesis;
suppose N1 = max([/((1/p) to_power (1/8))\], 2);
hence thesis by SQUARE_1:49;
end;
then reconsider N1 as Nat by A7,INT_1:16;
take N1; let n; assume
A10: n >= N1;
p" > 0 by A6,REAL_1:72;
then A11: 1/p > 0 by XCMPLX_1:217;
[/((1/p) to_power (1/8))\] >= ((1/p) to_power (1/8)) by INT_1:def 5;
then A12: N1 >= ((1/p) to_power (1/8)) by A9,AXIOMS:22;
A13: ((1/p1) to_power (1/8)) > 0 by A11,POWER:39;
A14: n >= N by A7,A10,AXIOMS:22;
A15: h.n = f.n/g.n by Lm4;
g.n = ((1+e) to_power (1*n + 0)) by Def1;
then A16: h.n = (n to_power 8) / ((1+e) to_power n) by A7,A8,A10,A15,Def3
.= (2 to_power (8*log(2,n))) / ((1+e) to_power n) by A7,A8,A10,Lm3
.= (2 to_power (8*log(2,n))) /
(2 to_power (n*log(2,1+e))) by A3,Lm3
.= (2 to_power ((8*log(2,n)) - (n*log(2,1+e)))) by POWER:34
.= (2 to_power -((n*log(2,1+e)) - (8*log(2,n)))) by XCMPLX_1:143;
n >= ((1/p) to_power (1/8)) by A10,A12,AXIOMS:22;
then n to_power 8 >= ((1/p) to_power (1/8)) to_power 8 by A13,Lm6;
then n to_power 8 >= (1/p1) to_power ((1/8)*8) by A11,POWER:38;
then n to_power 8 >= 1/p1 by POWER:30;
then 1 / (n to_power 8) <= 1 / (1/p) by A11,REAL_2:152;
then 1 / (n to_power 8) <= 1 / (p") by XCMPLX_1:217;
then 1 / (n to_power 8) <= p by XCMPLX_1:218;
then 1 / (2 to_power (8*log(2,n))) <= p by A7,A8,A10,Lm3;
then A17: 2 to_power -(8*log(2,n)) <= p by POWER:33;
((n*log(2,1+e)) - (8*log(2,n))) > (8*log(2,n)) by A4,A14;
then A18: 2 to_power ((n*log(2,1+e)) - (8*log(2,n))) >
2 to_power (8*log(2,n)) by POWER:44;
2 to_power (8*log(2,n)) > 0 by POWER:39;
then 1 / (2 to_power ((n*log(2,1+e)) - (8*log(2,n)))) <
1 / (2 to_power (8*log(2,n))) by A18,REAL_2:151;
then 2 to_power -((n*log(2,1+e)) - (8*log(2,n))) <
1 / (2 to_power (8*log(2,n))) by POWER:33;
then h.n < 2 to_power -(8*log(2,n)) by A16,POWER:33;
then A19: h.n < p by A17,AXIOMS:22;
h.n > 0 by A16,POWER:39;
hence abs(h.n-0) < p by A19,ABSVALUE:def 1;
end;
then A20: h is convergent by SEQ_2:def 6;
then lim h = 0 by A5,SEQ_2:def 7;
then f in Big_Oh(g) & not g in Big_Oh(f) by A20,ASYMPT_0:16;
then f in Big_Oh(g) & not f in Big_Omega(g) by ASYMPT_0:19;
hence thesis by Th4;
end;
begin :: Problem 3.22
Lm32:
2 to_power 12 = 4096
proof
thus 2 to_power 12 = 2 to_power (6+6)
.= 64*64 by Lm11,POWER:32
.= 4096;
end;
Lm33:
for n st n >= 3 holds n^2 > 2*n + 1
proof
defpred _P[Nat] means $1^2 > 2*$1 + 1;
3^2 = 3*3 by SQUARE_1:def 3
.= 9;
then A1: _P[3];
A2: for n st n >= 3 & _P[n] holds _P[n+1] proof let n; assume that
A3: n >= 3 and
A4: n^2 > 2*n + 1;
A5: (n+1)^2 = (n+1)*(n+1) by SQUARE_1:def 3
.= (n+1)*n + (n+1)*1 by XCMPLX_1:8
.= n*n + 1*n + (n+1) by XCMPLX_1:8
.= n^2 + n + (n+1) by SQUARE_1:def 3;
n^2 + (n + (n+1)) > 2*n + 1 + (n + (n+1)) by A4,REAL_1:53;
then (n+1)^2 > 2*n + 1 + (n + (n+1)) by A5,XCMPLX_1:1;
then (n+1)^2 > 2*n + (1 + (n + (n+1))) by XCMPLX_1:1;
then (n+1)^2 > 2*n + ((n+1) + (n+1)) by XCMPLX_1:1;
then A6: (n+1)^2 > 2*n + 2*(n+1) by XCMPLX_1:11;
n > 0 & n > 1 by A3,AXIOMS:22;
then n + n > 1 + 0 by REAL_1:67;
then 2*n > 1 by XCMPLX_1:11;
then 2*n + 2*(n+1) > 1 + 2*(n+1) by REAL_1:53;
hence (n+1)^2 > 2*(n+1) + 1 by A6,AXIOMS:22;
end;
for n st n >= 3 holds _P[n] from Ind1(A1, A2);
hence thesis;
end;
Lm34:
for n st n >= 10 holds 2 to_power (n-1) > (2*n)^2
proof
defpred _P[Nat] means 2 to_power ($1-1) > (2*$1)^2;
A1: _P[10] proof
A2: 2 to_power (10-1) = 2 to_power (6+3)
.= 64*(2 to_power (2+1)) by Lm11,POWER:32
.= 64*((2 to_power 2)*(2 to_power 1)) by POWER:32
.= 64*((2 to_power (1+1))*2) by POWER:30
.= 64*(((2 to_power 1)*(2 to_power 1))*2) by POWER:32
.= 64*((2*(2 to_power 1))*2) by POWER:30
.= 64*((2*2)*2) by POWER:30
.= 512;
(2*10)^2 = 20*20 by SQUARE_1:def 3
.= 400;
hence thesis by A2;
end;
A3: for n st n >= 10 & _P[n] holds _P[n+1] proof let n; assume that
A4: n >= 10 and
A5: 2 to_power (n-1) > (2*n)^2;
2 to_power ((n+1)-1) = 2 to_power ((n+1)+-1) by XCMPLX_0:def 8
.= 2 to_power ((n+-1)+1) by XCMPLX_1:1
.= 2 to_power ((n-1)+1) by XCMPLX_0:def 8
.= (2 to_power (n-1))*(2 to_power 1) by POWER:32
.= (2 to_power (n-1))*2 by POWER:30;
then A6: 2 to_power ((n+1)-1) > ((2*n)^2)*2 by A5,REAL_1:70;
A7: (2*(n+1))^2 = (2*n + 2*1)^2 by XCMPLX_1:8
.= (2*n)^2 + 2*(2*n)*2 + 2^2 by SQUARE_1:63
.= (2*n)*(2*n) + 2*(2*n)*2 + 2^2 by SQUARE_1:def 3
.= (2*n)*(2*n) + (2*2)*(2*n) + 2^2 by XCMPLX_1:4
.= (2*n)*(2*n) + (2*2)*(2*n) + 2*2 by SQUARE_1:def 3
.= ((2*n)*2)*n + (2*2)*(2*n) + 2*2 by XCMPLX_1:4
.= (n*(2*2))*n + (2*2)*(2*n) + 2*2 by XCMPLX_1:4
.= (2*2)*(n*n) + (2*2)*(2*n) + 2*2 by XCMPLX_1:4
.= (2*2)*(n*n + 2*n) + 2*2*1 by XCMPLX_1:8
.= (2*2)*(n*n + 2*n + 1) by XCMPLX_1:8;
now assume ((2*n)^2)*2 <= (2*2)*(n*n + 2*n + 1);
then ((2*n)*(2*n))*2 <= (2*2)*(n*n + 2*n + 1) by SQUARE_1:def 3;
then (2*(n*(2*n)))*2 <= (2*2)*(n*n + 2*n + 1) by XCMPLX_1:4;
then (2*(2*(n*n)))*2 <= (2*2)*(n*n + 2*n + 1) by XCMPLX_1:4;
then ((2*2)*(n*n))*2 <= (2*2)*(n*n + 2*n + 1) by XCMPLX_1:4;
then ((2*2)*(n*n))*2 <= (2*2)*(n*n + (2*n + 1)) by XCMPLX_1:1;
then ((2*2)*(n*n))*2 <= (2*2)*(n*n) + (2*2)*(2*n + 1) by XCMPLX_1:8;
then ((2*2)*(n*n))*2 - (2*2)*(n*n) <= (2*2)*(2*n + 1) by REAL_1:86;
then ((2*2)*(n*n))*2 + -((2*2)*(n*n)) <=
(2*2)*(2*n + 1) by XCMPLX_0:def 8;
then ((2*2)*(n*n))*2 + (-1)*((2*2)*(n*n)) <=
(2*2)*(2*n + 1) by XCMPLX_1:180;
then ((2*2)*(n*n))*(2+-1) <= (2*2)*(2*n + 1) by XCMPLX_1:8;
then (2*2)"*((2*2)*(n*n)) <=
(2*2)"*((2*2)*(2*n + 1)) by AXIOMS:25;
then ((2*2)"*(2*2))*(n*n) <= (2*2)"*((2*2)*(2*n + 1)) by XCMPLX_1:4;
then n*n <= ((2*2)"*(2*2))*(2*n + 1) by XCMPLX_1:4;
then A8: n^2 <= 2*n + 1 by SQUARE_1:def 3;
n >= 3 by A4,AXIOMS:22;
hence contradiction by A8,Lm33;
end;
hence 2 to_power ((n+1)-1) > (2*(n+1))^2 by A6,A7,AXIOMS:22;
end;
for n st n >= 10 holds _P[n] from Ind1(A1, A3);
hence thesis;
end;
Lm35:
for n st n >= 9 holds (n+1) to_power 6 < 2*(n to_power 6)
proof
defpred _P[Nat] means ($1+1) to_power 6 < 2*($1 to_power 6);
A1: _P[9] proof
A2: 9 to_power 2 = 9 to_power (1+1)
.= (9 to_power 1)*(9 to_power 1) by POWER:32
.= 9*(9 to_power 1) by POWER:30
.= 9*9 by POWER:30
.= 81;
A3: 2*(9 to_power 4) = 2*(9 to_power (2+2))
.= 2*(81*81) by A2,POWER:32
.= 13122;
consider t1 being Nat such that
A4: t1 = 10;
consider t2 being Nat such that
A5: t2 = 10*10;
consider t3 being Nat such that
A6: t3 = 10*10*10;
consider t4 being Nat such that
A7: t4 = 10*10*10*10;
consider t5 being Nat such that
A8: t5 = 10*10*10*10*10;
consider t6 being Nat such that
A9: t6 = 10*10*10*10*10*10;
A10: 10 to_power 3 = 10 to_power (2+1)
.= (10 to_power 2)*(10 to_power 1) by POWER:32
.= (10 to_power (1+1))*10 by POWER:30
.= ((10 to_power 1)*(10 to_power 1))*10 by POWER:32
.= (10*(10 to_power 1))*10 by POWER:30
.= (10*10)*10 by POWER:30;
A11: 10 to_power 6 = 10 to_power (3+3)
.= (10*10*10)*(10*10*10) by A10,POWER:32
.= (10*10*10*10)*(10*10)
.= t6 by A9,XCMPLX_1:4;
A12: now thus 13122*9 = ((t4 + 3*t3 + t2) + (2*t1 + 2))*9 by A4,A5,A6,A7
.= (t4 + 3*t3 + t2)*9 + (2*t1 + 2)*9 by XCMPLX_1:8
.= (t4 + (3*t3 + t2))*9 + (2*t1 + 2)*9 by XCMPLX_1:1
.= 9*t4 + (3*t3 + t2)*9 + (2*t1 + 2)*9 by XCMPLX_1:8
.= 9*t4 + (9*(3*t3) + 9*t2) + (2*t1 + 2)*9 by XCMPLX_1:8
.= 9*t4 + ((9*3)*t3 + 9*t2) + (2*t1 + 2)*9 by XCMPLX_1:4
.= 9*t4 + (2*10 + 7)*t3 + 9*t2 + (2*t1 + 2)*9 by XCMPLX_1:1
.= 9*t4 + ((2*10)*t3 + 7*t3) + 9*t2 + (2*t1 + 2)*9 by XCMPLX_1:8
.= 9*t4 + 2*t4 + 7*t3 + 9*t2 + (2*t1 + 2)*9 by A6,A7,XCMPLX_1:1
.= (9+2)*t4 + 7*t3 + 9*t2 + (2*t1 + 2)*9 by XCMPLX_1:8
.= (10 + 1)*t4 + 7*t3 + 9*t2 + (2*t1 + 2)*9
.= 10*t4 + 1*t4 + 7*t3 + 9*t2 + (2*t1 + 2)*9 by XCMPLX_1:8
.= (t5 + t4 + 7*t3) + (9*t2 + (2*t1 + 2)*9) by A7,A8,XCMPLX_1:1
.= t5 + t4 + 7*t3 + (t3 + (8*t1 + 2*9)) by A4,A5,A6
.= (t5 + t4 + 7*t3 + t3) + (8*t1 + 2*9) by XCMPLX_1:1
.= (t5 + t4 + (7*t3 + 1*t3)) + (8*t1 + 2*9) by XCMPLX_1:1
.= (t5 + t4 + ((7+1)*t3)) + (8*t1 + 2*9) by XCMPLX_1:8
.= (t5 + t4 + 8*t3) + ((8+1)*t1 + 8) by A4
.= t5 + t4 + 8*t3 + 9*t1 + 8 by XCMPLX_1:1;
end;
now thus (13122*9)*9 = ((t5 + t4 + 8*t3) + (9*t1 + 8))*9 by A12,XCMPLX_1
:1
.= (t5 + t4 + 8*t3)*9 + (9*t1 +8 )*9 by XCMPLX_1:8
.= (t5 + (t4 + 8*t3))*9 + (9*t1 + 8)*9 by XCMPLX_1:1
.= (9*t5 + (t4 + 8*t3)*9) + (9*t1 + 8)*9 by XCMPLX_1:8
.= (9*t5 + (9*t4 + 9*(8*t3))) + (9*t1 + 8)*9 by XCMPLX_1:8
.= (9*t5 + (9*t4 + (9*8)*t3)) + (9*t1 + 8)*9 by XCMPLX_1:4
.= (9*t5 + (9*t4 + (70+2)*t3)) + (9*t1 + 8)*9
.= (9*t5 + (9*t4 + ((7*10)*t3 + 2*t3))) + (9*t1 + 8)*9 by XCMPLX_1:8
.= (9*t5 + ((9*t4 + 7*t4) + 2*t3)) + (9*t1 + 8)*9 by A6,A7,XCMPLX_1:1
.= (9*t5 + (((9+7)*t4) + 2*t3)) + (9*t1 + 8)*9 by XCMPLX_1:8
.= ((9*t5 + (10+6)*t4) + 2*t3) + (9*t1 + 8)*9 by XCMPLX_1:1
.= ((9*t5 + (t5 + 6*t4)) + 2*t3) + (9*t1 + 8)*9 by A7,A8,XCMPLX_1:8;
end;
then A13: (13122*9)*9 =
(((9*t5 + 1*t5) + 6*t4) + 2*t3) + (9*t1 + 8)*9 by XCMPLX_1:1
.= ((((9+1)*t5) + 6*t4) + 2*t3) + (9*t1 + 8)*9 by XCMPLX_1:8
.= ((t6 + 6*t4) + 2*t3) + (8*t2 + (8*t1 + 2)) by A4,A5,A8,A9
.= (t6 + 6*t4 + 2*t3 + 8*t2) + (8*t1 + 2) by XCMPLX_1:1
.= t6 + 6*t4 + 2*t3 + 8*t2 + 8*t1 + 2 by XCMPLX_1:1;
t6 < t6 + ((6*t4 + 2*t3 + 8*t2) + (8*t1 + 2)) by REAL_1:69;
then t6 < (t6 + (6*t4 + 2*t3 + 8*t2)) + (8*t1 + 2) by XCMPLX_1:1;
then t6 < (t6 + (6*t4 + (2*t3 + 8*t2))) + (8*t1 + 2) by XCMPLX_1:1;
then t6 < ((t6 + 6*t4) + (2*t3 + 8*t2)) + (8*t1 + 2) by XCMPLX_1:1;
then A14: t6 < (t6 + 6*t4 + 2*t3 + 8*t2) + (8*t1 + 2) by XCMPLX_1:1;
(13122*9)*9 = (2*((9 to_power 4)*9))*9 by A3,XCMPLX_1:4
.= (2*((9 to_power 4)*(9 to_power 1)))*9 by POWER:30
.= (2*(9 to_power (4+1)))*9 by POWER:32
.= 2*((9 to_power 5)*9) by XCMPLX_1:4
.= 2*((9 to_power 5)*(9 to_power 1)) by POWER:30
.= 2*(9 to_power (5+1)) by POWER:32
.= 2*(9 to_power 6);
hence thesis by A11,A13,A14,XCMPLX_1:1;
end;
A15: for n st n >= 9 & _P[n] holds _P[n+1] proof let n; assume that
A16: n >= 9 and
A17: (n+1) to_power 6 < 2*(n to_power 6);
A18: n to_power 6 > 0 by A16,POWER:39;
A19: (n+1) to_power 6 > 0 by POWER:39;
(n+1)" > 0 by REAL_1:72;
then (n+2)*((n+1)") > 0*((n+1)") by REAL_1:70;
then A20: ((n+2) / (n+1)) > 0 by XCMPLX_0:def 9;
now assume (n+2) / (n+1) >= (n+1) / n;
then (n+2) / (n+1) * (n+1) >= (n+1) / n * (n+1) by AXIOMS:25;
then (n+2) >= (n+1) / n * (n+1) by XCMPLX_1:88;
then (n+2)*n >= (n+1) / n * (n+1) * n by AXIOMS:25;
then (n+2)*n >= ((n+1) / n * n) * (n+1) by XCMPLX_1:4;
then (n+2)*n >= (n+1)*(n+1) by A16,XCMPLX_1:88;
then n*n + 2*n >= (n+1)*(n+1) by XCMPLX_1:8;
then n^2 + 2*n >= (n+1)*(n+1) by SQUARE_1:def 3;
then n^2 + 2*n >= (n+1)^2 by SQUARE_1:def 3;
then n^2 + 2*n >= n^2 + 2*n*1 + 1^2 by SQUARE_1:63;
then n^2 + 2*n >= n^2 + 2*n + 1*1 by SQUARE_1:def 3;
then (n^2 + 2*n) - (n^2 + 2*n) >= 1 by REAL_1:84;
hence contradiction by XCMPLX_1:14;
end;
then A21: ((n+2) / (n+1)) to_power 6 < ((n+1) / n) to_power 6 by A20,POWER
:42;
(n+1) to_power 6 / n to_power 6 < 2 by A17,A18,REAL_2:178;
then ((n+1) / n) to_power 6 < 2 by A16,POWER:36;
then ((n+2) / (n+1)) to_power 6 < 2 by A21,AXIOMS:22;
then ((n+2) to_power 6) / ((n+1) to_power 6) < 2 by POWER:36;
then ((n+2) to_power 6) / ((n+1) to_power 6) * ((n+1) to_power 6) <
2*((n+1) to_power 6) by A19,REAL_1:70;
then (n+(1+1)) to_power 6 < 2*((n+1) to_power 6) by A19,XCMPLX_1:88;
hence thesis by XCMPLX_1:1;
end;
for n st n >= 9 holds _P[n] from Ind1(A1, A15);
hence thesis;
end;
Lm36:
for n st n &