:: Asymptotic notation. Part II: Examples and Problems :: by Richard Krueger, Piotr Rudnicki and Paul Shelley :: :: Received November 4, 1999 :: Copyright (c) 1999 Association of Mizar Users environ vocabularies ASYMPT_0, 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; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_1, PARTFUN1, FUNCT_2, FRAENKEL, INT_1, NAT_1, VALUED_1, SEQ_1, SEQ_2, RELAT_1, NEWTON, POWER, SERIES_1, PRE_CIRC, SQUARE_1, SEQM_3, FINSEQ_1, FINSEQ_2, RVSUM_1, ASYMPT_0; constructors PARTFUN1, DOMAIN_1, REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_2, SEQM_3, RVSUM_1, NEWTON, PREPOWER, SERIES_1, PRE_CIRC, SEQ_1, ASYMPT_0; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_2, ASYMPT_0, SQUARE_1, VALUED_0, VALUED_1, FUNCT_2, POWER; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions ASYMPT_0, SQUARE_1, VALUED_1; theorems TARSKI, FUNCT_2, INT_1, NAT_1, REAL_1, SEQ_1, SQUARE_1, SEQ_2, ABSVALUE, REAL_2, FUNCOP_1, POWER, NEWTON, EULER_2, SERIES_1, SEQM_3, FINSEQ_1, PRE_FF, RVSUM_1, FINSEQ_2, ASYMPT_0, FRAENKEL, RELSET_1, XREAL_0, XBOOLE_0, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, VALUED_1; schemes FUNCT_2, SEQ_1, NAT_1; begin :: Examples from the text reserve c, c1, c2, d, d1, d2, e for Real, i, k, n, m, N, n1, n2, N0, N1, N2, N3, M for Element of NAT, x for set; Lm1: for n be Nat 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 .= 4; then A1: P[2]; A2: for k be Nat st k >= 2 & P[k] holds P[k+1] proof let k be Nat 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); then A4: 2 to_power (k+1) > (k+1) + (2 to_power k) by A3,XREAL_1:8; reconsider k as Element of NAT by ORDINAL1:def 13; 2 to_power k >= 0 + 1 by INT_1:20,POWER:39; then (k+1) + (2 to_power k) >= (k+1) + 1 by XREAL_1:8; hence thesis by A4,XXREAL_0:2; end; for n be Nat st n >= 2 holds P[n] from NAT_1:sch 8(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 XXREAL_0:2; 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,XXREAL_0:2; 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^2 + 0 by POWER:53; then 12*(n to_power 3)*log(2,n) - 5*n^2 > 0 by XREAL_1:22; then (12*(n to_power 3)*log(2,n)-5*n^2)+(log(2,n))^2>0+0 by XREAL_1:10,65; then (12*(n to_power 3)*log(2,n)-5*n^2)+(log(2,n))^2+36 > 0+0; 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 A7: n >= 2; then log(2,n) >= log(2,2) by PRE_FF:12; then A8: log(2,n) >= 1 by POWER:60; n to_power 3 > 0 by A7,POWER:39; then (n to_power 3)*log(2,n) > (n to_power 3)*0 by A8,XREAL_1:70; hence g.n > 0 by A2,A7; 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[Element of NAT,Real] means ($1 = 0 implies $2 = 0) & ($1 > 0 implies $2 = 12*($1 to_power 3)*log(2,$1) - 5*($1)^2); A9: 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 A10: for x being Element of NAT holds P[x,h.x] from FUNCT_2:sch 3(A9); take h; thus h.0 = 0 by A10; let n; thus thesis by A10; end; then consider p being Real_Sequence such that A11: 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 A12: n >= 3; then n > 1 by XXREAL_0:2; then A13: n to_power 3 > n to_power 2 by POWER:44; A14: n to_power 2 > 0 by A12,POWER:39; A15: log(2,n) >= log(2,3) by A12,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 A15,XXREAL_0:2; then (n to_power 3)*log(2,n) > (n to_power 2)*1 by A13,A14,REAL_2:199; then 12*((n to_power 3)*log(2,n)) > 5*(n to_power 2) by A14,REAL_2:199; 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 XREAL_1:22; hence p.n > 0 by A11,A12; 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[Element of NAT,Real] means ($1 = 0 implies $2 = 0) & ($1 > 0 implies $2 = (log(2,$1))^2 + 36); A16: 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 A17: for x being Element of NAT holds P[x,h.x] from FUNCT_2:sch 3(A16); take h; thus thesis by A17; end; then consider q being Real_Sequence such that A18: 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 A19: n >= 1; (log(2,n))^2 + 36 > 0+0 by XREAL_1:10,65; hence q.n > 0 by A18,A19; 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,A11,A18; end; suppose A20: n > 0; then p.n = 12*(n to_power 3)*log(2,n) - 5*n^2 by A11; then p.n + q.n = (12*(n to_power 3)*log(2,n)-5*n^2)+((log(2,n))^2 +36) by A18,A20 .= 12*(n to_power 3)*log(2,n)-5*n^2+(log(2,n))^2 +36; hence thesis by A1,A20; end; end; end; then A21: Big_Oh(f) = Big_Oh(p+q) by SEQ_1:11 .= Big_Oh(t) by ASYMPT_0:9; 4 = 2^2 .= 2 to_power 2 by POWER:53; then A22: log(2,4) = 2*log(2,2) by POWER:63 .= 2*1 by POWER:60 .= 2; A23: for n st n >= 4 holds 7*n^2 > q.n proof defpred P[Nat] means 7*$1^2 > q.$1; A24: P[4] proof q.4 = 2^2 + 36 by A18,A22 .= 40; hence thesis; end; A25: for k be Nat st k >= 4 & P[k] holds P[k+1] proof let k be Nat such that A26: k >= 4 and A27: 7*k^2 > q.k; k in NAT by ORDINAL1:def 13; then A28: q.k = (log(2,k))^2 + 36 by A18,A26; 7*(k+1)^2 = 7*k^2 + (7*(2*k) + 7*1); then A29: 7*(k+1)^2 > q.k + (7*(2*k) + 7*1) by A27,XREAL_1:8; A30: q.(k+1) = (log(2,k+1))^2 + 36 by A18; k >= 1 by A26,XXREAL_0:2; then k+k >= k+1 by XREAL_1:8; then A31: log(2,k+k) >= log(2,k+1) by PRE_FF:12; k+1 >= 4+0 by A26,XREAL_1:10; then log(2,k+1) >= 2 by A22,PRE_FF:12; then (log(2,k+k))^2 >= (log(2,k+1))^2 by A31,SQUARE_1:77; then A32: q.(k+1) <= (log(2,k+k))^2 + 36 by A30,XREAL_1:8; log(2,k+k) = log(2,2*k); then log(2,k+k) = log(2,k) + log(2,2) by A26,POWER:61; then A33: (log(2,k+k))^2 = (log(2,k) + 1)^2 by POWER:60 .= (log(2,k))^2 + 2*log(2,k) + 1; k >= 2 by A26,XXREAL_0:2; then A34: 2 to_power k > k + 1 by Lm1; A35: log(2,k) >= 2 by A22,A26,PRE_FF:12; k+1 > k+0 by XREAL_1:10; then 2 to_power k > k by A34,XXREAL_0:2; then log(2,2 to_power k) > log(2,k) by A26,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 A35,REAL_2:199; then (7*2)*k + 7 > 2*log(2,k) + 1 by XREAL_1:10; then (log(2,k))^2 + (2*log(2,k) + 1) < (log(2,k))^2 + (7*(2*k) + 7) by XREAL_1:8; then (log(2,k+k))^2 + 36 < ((log(2,k))^2 + (7*(2*k) + 7)) + 36 by A33,XREAL_1:8; then q.k + (7*(2*k) + 7*1) > q.(k+1) by A28,A32,XXREAL_0:2; hence thesis by A29,XXREAL_0:2; end; for n be Nat st n >= 4 holds P[n] from NAT_1:sch 8(A24, A25); hence thesis; end; A36: for n st n >= 4 holds p.n > 7*n^2 proof let n; assume A37: n >= 4; then A38: p.n = 12*(n to_power 3)*log(2,n) - 5*n^2 by A11; n > 1 by A37,XXREAL_0:2; then A39: n to_power 3 > n to_power 2 by POWER:44; A40: n to_power 2 > 0 by A37,POWER:39; log(2,n) >= log(2,4) by A37,PRE_FF:12; then log(2,n) > 1 by A22,XXREAL_0:2; then (n to_power 3)*log(2,n) > (n to_power 2)*1 by A39,A40,REAL_2:199; then 12*((n to_power 3)*log(2,n)) > 12*(n to_power 2) by XREAL_1:70; 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 A38,XREAL_1:11; hence p.n > 7*n^2; end; A41: for n st n >= 4 holds p.n > q.n proof let n; assume A42: n >= 4; then A43: p.n > 7*n^2 by A36; 7*n^2 > q.n by A23,A42; hence thesis by A43,XXREAL_0:2; end; A44: for n st n >= 4 holds t.n = p.n proof let n; assume n >= 4; then A45: p.n > q.n by A41; thus t.n = max( p.n, q.n ) by ASYMPT_0:def 10 .= p.n by A45,XXREAL_0:def 9; end; A46: t is Element of Funcs(NAT, REAL) by FUNCT_2:11; consider N such that A47: for n st n >= N holds t.n > 0 by ASYMPT_0:def 6; now let n; assume A48: n >= max(4,N); A49: max(4,N) >= 4 & max(4,N) >= N by XXREAL_0:25; then A50: n >= 4 & n >= N by A48,XXREAL_0:2; A51: t.n = p.n by A44,A48,A49,XXREAL_0:2 .= 12*(n to_power 3)*log(2,n) - 5*n^2 by A11,A48,A49; t.n <= 12*(n to_power 3)*log(2,n) - 0 by A51,REAL_1:92; then t.n <= 12*((n to_power 3)*log(2,n)); hence t.n <= 12*g.n by A2,A48,A49; thus t.n >= 0 by A47,A50; end; then A52: t in Big_Oh(g) by A46; f in Big_Oh(f) by ASYMPT_0:10; hence thesis by A21,A52,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 Element of NAT by INT_1:16; now let n; assume A6: n >= N+1; N+1 > N+0 by XREAL_1:10; then n > N by A6,XXREAL_0:2; 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) > 0 by A3,A7,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; now let x be set; hereby assume x in Big_Oh(f); then consider t being Element of Funcs(NAT, REAL) such that A7: x = t and A8: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0; consider c,N such that A9: c > 0 and A10: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A8; log(a,b) > log(a,1) by A1,A2,POWER:65; then log(a,b) > 0 by A5,POWER:59; then A11: c*log(a,b) > c*0 by A9,XREAL_1:70; now take N1 = N+1; let n; assume A12: n >= N1; N+1 > N+0 by XREAL_1:10; then A13: n > N by A12,XXREAL_0:2; then A14: t.n <= c*f.n by A10; f.n = log(a,n) by A3,A12 .= log(a,b)*log(b,n) by A5,A6,A12,POWER:64; then t.n <= (c*log(a,b))*log(b,n) by A14; hence t.n <= (c*log(a,b))*g.n by A4,A12; thus t.n >= 0 by A10,A13; end; hence x in Big_Oh(g) by A7,A11; end; assume x in Big_Oh(g); then consider t being Element of Funcs(NAT, REAL) such that A15: x = t and A16: ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0; consider c,N such that A17: c > 0 and A18: for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A16; log(b,a) > log(b,1) by A1,A2,POWER:65; then log(b,a) > 0 by A6,POWER:59; then A19: c*log(b,a) > c*0 by A17,XREAL_1:70; now take N1 = N+1; let n; assume A20: n >= N1; N+1 > N+0 by XREAL_1:10; then A21: n > N by A20,XXREAL_0:2; then A22: t.n <= c*g.n by A18; g.n = log(b,n) by A4,A20 .= log(b,a)*log(a,n) by A5,A6,A20,POWER:64; then t.n <= (c*log(b,a))*log(a,n) by A22; hence t.n <= (c*log(b,a))*f.n by A3,A20; thus t.n >= 0 by A18,A21; end; hence x in Big_Oh(f) by A15,A19; 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(Element of NAT) = a to_power (b*$1+c); consider h being Function of NAT, REAL such that A1: for n being Element of NAT holds h.n = F(n) from FUNCT_2:sch 4; 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; registration 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); hereby assume f in Big_Oh(g); then consider s being Element of Funcs(NAT, REAL) such that A2: s = f and A3: ex c,N st c > 0 & for n st n >= N holds s.n <= c*g.n & s.n >= 0; consider c,N such that A4: c > 0 and A5: for n st n >= N holds s.n <= c*g.n & s.n >= 0 by A3; set d = (log(2,b) - log(2,a)); log(2,b) > log(2,a) + 0 by A1,POWER:65; then A6: d > 0 by XREAL_1:22; set N0 = [/log(2,c) / d\]; set N1 = max( N, N0 ); A7: N1 >= N & N1 >= N0 by XXREAL_0:25; N1 = N or N1 = N0 by XXREAL_0:16; then reconsider N1 as Element of NAT by A7,INT_1:16; set n = N1 + 1; set e = (2 to_power (n*log(2,a))); A8: e > 0 by POWER:39; N1 + 1 > N1 + 0 by XREAL_1:10; then A9: n > N & n > N0 by A7,XXREAL_0:2; N0 >= log(2,c) / d by INT_1:def 5; then n > log(2,c) / d by A9,XXREAL_0:2; then n*d > (log(2,c) / d)*d by A6,XREAL_1:70; then n*d > log(2,c) by A6,XCMPLX_1:88; then 2 to_power (n*d) > 2 to_power log(2,c) by POWER:44; then 2 to_power (n*log(2,b) - n*log(2,a)) > c by A4,POWER:def 3; 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 A8,XREAL_1:70; then 2 to_power (n*log(2,b)) > c*e by A8,XCMPLX_1:88; then b to_power n > c*(2 to_power (n*log(2,a))) by Lm3; then A10: b to_power n > c*(a to_power n) by Lm3; f.n <= c*g.n by A2,A5,A9; then b to_power (1*n + 0) <= c*g.n by Def1; hence contradiction by A10,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[Element of 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; end; suppose n > 0; hence thesis; end; end; consider h being Function of NAT,REAL such that A2: for x being Element of NAT holds P[x,h.x] from FUNCT_2:sch 3(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; end; suppose A5: n > 0; then j.n = log(2,n) by A3; hence j.n = k.n by A4,A5; end; 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[Element of 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; end; suppose n > 0; hence thesis; end; end; consider h being Function of NAT,REAL such that A2: for x being Element of NAT holds P[x,h.x] from FUNCT_2:sch 3(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; end; suppose A5: n > 0; then j.n = n to_power a by A3; hence j.n = k.n by A4,A5; end; end; hence j = k by FUNCT_2:113; end; end; registration 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; registration 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 Element of NAT holds (f/"g).n = f.n/g.n proof let f,g be Real_Sequence, n be Element of NAT; thus (f/"g).n = f.n*g".n by SEQ_1:12 .= f.n*(g.n)" by VALUED_1:10 .= 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; hereby assume A1: Big_Oh(f) c= Big_Oh(g) & not Big_Oh(f) = Big_Oh(g); A2: 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 A1,A2,Lm5; end; hence f in Big_Oh(g) & not f in Big_Omega(g) by A1,A2; end; assume A3: 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 A4: x = t and A5: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0; consider c,N such that c > 0 and A6: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A5; now take N; let n; assume n >= N; hence t.n >= 0 by A6; end; then A7: t is eventually-nonnegative by ASYMPT_0:def 4; t in Big_Oh(f) by A5; hence x in Big_Oh(g) by A3,A4,A7,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 A3,ASYMPT_0:19; end; Lm6: for a, b, c being real number st 0 < a & a <= b & c >= 0 holds a to_power c <= b to_power c proof let a, b, c be real number; 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; end; suppose A4: c > 0; per cases by A2,REAL_1:def 5; suppose a = b; hence thesis; end; suppose a < b; hence thesis by A1,A4,POWER:42; end; end; end; Lm7: 2 to_power 2 = 4 proof thus 2 to_power 2 = 2^2 by POWER:53 .= 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; 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 be Nat 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 be Nat st k >= 4 & P[k] holds P[k+1] proof let k be Nat such that A3: k >= 4 and A4: 2*k + 3 < 2 to_power k; 2*(k+1) + 3 = 2 + (2*k + 3); then A5: 2*(k+1) + 3 < 2 + (2 to_power k) by A4,XREAL_1:8; k > 1 by A3,XXREAL_0:2; 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 XREAL_1:8; then 2*(k+1) + 3 < 2*(2 to_power k) by A5,XXREAL_0:2; then 2*(k+1) + 3 < (2 to_power 1)*(2 to_power k) by POWER:30; hence thesis by POWER:32; end; for n be Nat st n >= 4 holds P[n] from NAT_1:sch 8(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; A1: P[6] by Lm11; A2: for k be Nat st k >= 6 & P[k] holds P[k+1] proof let k be Nat such that A3: k >= 6 and A4: (k+1)^2 < 2 to_power k; k >= 4 by A3,XXREAL_0:2; then 2*k + 3 < 2 to_power k by Lm12; then A5: (k+1)^2 + (2*k + 3) < (k+1)^2 + (2 to_power k) by XREAL_1:8; (k+1)^2 + (2 to_power k) < (2 to_power k) + (2 to_power k) by A4,XREAL_1:8; then ((k+1)+1)^2 < 2*(2 to_power k) by A5,XXREAL_0:2; then ((k+1)+1)^2 < (2 to_power 1)*(2 to_power k) by POWER:30; hence thesis by POWER:32; end; for n be Nat st n >= 6 holds P[n] from NAT_1:sch 8(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; set i0 = [\c/], i1 = [/c\]; per cases; suppose i0 = i1; then c is Integer by INT_1:59; then reconsider c as Element of NAT by A1,INT_1:16; A3: (c+1)^2 < 2 to_power c by A1,Lm13; c+0 < c+1 by XREAL_1:10; then c^2 < (c+1)^2 by SQUARE_1:78; hence thesis by A3,XXREAL_0:2; end; suppose not i0 = i1; then A4: i0 + 1 = i1 by INT_1:66; then A5: i0 = i1 - 1; A6: i1 >= c by INT_1:def 5; then reconsider i1 as Element of NAT by A1,INT_1:16; i1 > 6 by A1,A6,XXREAL_0:2; then A7: i0 > 5 by A2,A5,XREAL_1:11; then reconsider i0 as Element of NAT by INT_1:16; i0 >= 5 + 1 by A7,INT_1:20; then A8: i1^2 < 2 to_power i0 by A4,Lm13; i1 >= c by INT_1:def 5; then i1^2 >= c^2 by A1,SQUARE_1:77; then A9: c^2 < 2 to_power i0 by A8,XXREAL_0:2; i0 <= c by INT_1:def 4; then 2 to_power i0 <= 2 to_power c by PRE_FF:10; hence thesis by A9,XXREAL_0:2; end; 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 XXREAL_0:25; max(i0, i1) >= i0 & max(i0, i1) >= i1 by XXREAL_0:25; then A5: N >= i0 & N >= i1 by A4,XXREAL_0:2; N is Integer proof per cases by XXREAL_0:16; suppose N = max(i0, i1); hence thesis by XXREAL_0:16; end; suppose N = 2; hence thesis; end; end; then reconsider N as Element of NAT by A4,INT_1:16; p" > 0 by A3,XREAL_1:124; then 7*p" > 7*0 by XREAL_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,XXREAL_0:2; i0 >= (7/p) to_power (1/e) by INT_1:def 5; then A9: n >= (7/p) to_power (1/e) by A8,XXREAL_0:2; (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,XREAL_1:66; then p*(n to_power e) >= 7 by A3,XCMPLX_1:88; then p*(n to_power e) > 6 by XXREAL_0:2; 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 XREAL_1:124; p*(n to_power e) > p*0 by A3,A11,XREAL_1:70; then c < (2 to_power c)/c by A10,REAL_2:178; then n to_power e < ((2 to_power c)/c)/p by A3,REAL_2:178; then A13: n to_power e < (2 to_power c)/(c*p) by XCMPLX_1:79; A14: p1 to_power 2 > 0 by A3,POWER:39; A15: 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 XREAL_1:10; then i1 > (p to_power -(2/e)) by A15,XXREAL_0:2; then A16: n > p to_power -(2/e) by A8,XXREAL_0:2; p1 to_power -(2/e) > 0 by A3,POWER:39; then n to_power e > p to_power (-(2/e)) to_power e by A16,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); 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 A14,XREAL_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 A17: 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 A17,XREAL_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 A13,XXREAL_0:2; 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 A18: log(2,n to_power e)/(n to_power e) < p by A11,REAL_2:178; n > 1 by A8,XXREAL_0:2; 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,XREAL_1:70; then A19: 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 A18,A19,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[Element of 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; end; suppose n > 0; hence thesis; end; end; consider h being Function of NAT,REAL such that A3: for x being Element of NAT holds P[x,h.x] from FUNCT_2:sch 3(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; per cases; suppose A9: n = 0; then h.n = 0 / g.n by A7,Def2 .= 0*(1/e); hence thesis by A4,A8,A9; end; 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)") .= (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[Element of 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 SERIES_1: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 XREAL_1:9; 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; then (Partial_Sums(f)).N + f.(N+1) >= 0 by SERIES_1:def 6; then (Partial_Sums(f)).(N+1) >= 0 by SERIES_1:def 1; hence Sum(f,N+1) >= 0 by SERIES_1:def 6; end; for N holds P[N] from NAT_1:sch 1(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[Element of 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 SERIES_1:def 6; hence Sum(f,0) <= Sum(g,0) by SERIES_1: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 XREAL_1:9; 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,XREAL_1:9; then (Partial_Sums(f)).N + f.(N+1) <= Sum(g,N) + g.(N+1) by SERIES_1: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 SERIES_1:def 6; then Sum(f,N+1) <= (Partial_Sums(g)).N + g.(N+1) by SERIES_1: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 SERIES_1:def 6; end; for N holds P[N] from NAT_1:sch 1(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 Element of NAT holds Sum(f,N) = b*N proof let f be Real_Sequence, b be Real; defpred P[Element of 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 SERIES_1: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 SERIES_1:def 6 .= (Partial_Sums(f)).N + f.(N+1) by SERIES_1:def 1 .= b*N + f.(N+1) by A4,SERIES_1:def 6 .= b*N + b*1 by A1 .= b*(N+1); hence thesis; end; for N holds P[N] from NAT_1:sch 1( A2, A3 ); hence thesis; end; Lm20: for f being Real_Sequence, N,M being Nat holds Sum(f,N,M) + f.(N+1) = Sum(f,N+1,M) proof let f be Real_Sequence, N,M be Nat; A1: N in NAT by ORDINAL1:def 13; Sum(f,N,M) + f.(N+1) = Sum(f,N) - Sum(f,M) + f.(N+1) by SERIES_1:def 7 .= Sum(f,N) + f.(N+1) + -Sum(f,M) .= (Partial_Sums(f)).N + f.(N+1) + -Sum (f,M) by SERIES_1:def 6 .= (Partial_Sums(f)).(N+1) + -Sum(f,M) by A1,SERIES_1:def 1 .= Sum(f,N+1) + -Sum(f,M) by SERIES_1:def 6 .= Sum(f,N+1) - Sum(f,M) .= Sum(f,N+1,M) by SERIES_1: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 Element of 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 Element of 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 SERIES_1:def 7 .= (Partial_Sums(f)).(M+1) - Sum(f,M) by SERIES_1: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 SERIES_1:def 6 .= f.(M+1) + 0; Sum(g,M+1,M) = Sum(g,M+1) - Sum(g,M) by SERIES_1:def 7 .= (Partial_Sums(g)).(M+1) - Sum(g,M) by SERIES_1: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 SERIES_1:def 6 .= g.(M+1) + 0; hence Sum(f,M+1,M) <= Sum(g,M+1,M) by A2,A3; end; A4: for N1 be Nat st N1 >= M+1 & P[N1] holds P[N1+1] proof let N1 be Nat; 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 XREAL_1:9; hence f.n <= g.n by A7,A9; end; N1+1 >= M+1+0 by A5,XREAL_1:9; 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,XREAL_1:9; 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 be Nat st N >= M+1 holds P[N] from NAT_1:sch 8(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; end; suppose n > 0; then A1: n >= 0+1 by NAT_1:13; 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,XXREAL_0:2; end; hence thesis by A2; end; suppose n > 1; then A4: n >= 1+1 by NAT_1:13; 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 XREAL_1:70; then 2*(n/2) + 2*1 > 2*n; then 2 > 2*n - n by XREAL_1:21; hence contradiction by A4; end; hence thesis by A5,XXREAL_0:2; end; end; end; Lm23: for f being Real_Sequence, b being Real, N being Element of NAT st (f.0 = 0 & (for n st n > 0 holds f.n = b)) holds for M being Element of NAT holds Sum(f, N, M) = b*(N-M) proof let f be Real_Sequence, b be Real, N be Element of NAT such that A1: f.0 = 0 & (for n st n > 0 holds f.n = b); defpred P[Element of NAT] means Sum(f, N, $1) = b*(N-$1); A2: P[0] proof Sum(f, 0) = (Partial_Sums(f)).0 by SERIES_1:def 6 .= 0 by A1,SERIES_1:def 1; then Sum(f, N, 0) = Sum(f, N) - 0 by SERIES_1: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 SERIES_1:def 7 .= Sum(f, N) - (Partial_Sums(f)).(M+1) by SERIES_1: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) .= (Sum(f, N) - Sum(f, M)) + -f.(M+1) by SERIES_1:def 6 .= b*(N-M) + -f.(M+1) by A4,SERIES_1:def 7 .= b*(N-M) + -b by A1 .= b*(N-(M+1)); hence thesis; end; for M being Element of NAT holds P[M] from NAT_1:sch 1(A2, A3); hence thesis; end; theorem for f being Real_Sequence, k being Element of 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 Element of NAT such that A1: for n holds f.n = Sum(seq_n^(k), n); set g = seq_n^(k+1); A2: f is Element of Funcs(NAT, REAL) by FUNCT_2:11; 2 to_power (k+1) > 0 by POWER:39; then A3: (2 to_power (k+1))" > 0 by XREAL_1:124; now let n; assume A4: 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[Element of NAT,Real] means ($1 = 0 implies $2 = 0) & ($1 > 0 implies $2 = (n to_power k)); A5: 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; end; suppose n > 0; hence thesis; end; end; consider h being Function of NAT,REAL such that A6: for x being Element of NAT holds P[x,h.x] from FUNCT_2:sch 3(A5); take h; thus h.0 = 0 by A6; let n; thus thesis by A6; end; then consider q being Real_Sequence such that A7: q.0 = 0 & (for m st m > 0 holds q.m = n to_power k); A8: f.n = Sum(p, n) by A1; now let m; assume A9: m <= n; per cases; suppose m = 0; hence p.m <= q.m by A7,Def3; end; suppose A10: m > 0; then A11: p.m = m to_power k by Def3; q.m = n to_power k by A7,A10; hence p.m <= q.m by A9,A10,A11,Lm6; end; end; then A12: Sum(p, n) <= Sum(q, n) by Lm18; Sum(q, n) = (n to_power k)*n by A7,Lm19 .= (n to_power k)*(n to_power 1) by POWER:30 .= n to_power (k+1) by A4,POWER:32 .= g.n by A4,Def3; hence f.n <= 1*g.n by A1,A12; now let m; assume m <= n; per cases; suppose m = 0; hence p.m >= 0 by Def3; end; suppose m > 0; then p.m = m to_power k by Def3; hence p.m >= 0; end; end; hence f.n >= 0 by A8,Lm17; end; then A13: f in Big_Oh(g) by A2; now let n; assume A14: 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[Element of NAT,Real] means ($1 = 0 implies $2 = 0) & ($1 > 0 implies $2 = ((n/2) to_power k)); A15: 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; end; suppose n > 0; hence thesis; end; end; consider h being Function of NAT,REAL such that A16: for x being Element of NAT holds P[x,h.x] from FUNCT_2:sch 3(A15); take h; thus h.0 = 0 by A16; let n; thus thesis by A16; end; then consider q being Real_Sequence such that A17: q.0 = 0 & (for m st m > 0 holds q.m = (n/2) to_power k); A18: f.n = Sum(p, n) by A1; A19: g.n = n to_power (k+1) by A14,Def3; set n1 = [/n/2\]; A20: n*2" > 0*2" by A14,XREAL_1:70; A21: [/n/2\] >= n/2 by INT_1:def 5; then reconsider n1 as Element of 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 XREAL_1:8; hence contradiction by A20,INT_1:def 5; end; then reconsider n2 as Element of NAT by INT_1:16; A22: now let m; assume m <= n; per cases; suppose m = 0; hence p.m >= 0 by Def3; end; suppose m > 0; then p.m = m to_power k by Def3; hence p.m >= 0; end; end; then A23: Sum(p,n) >= 0 by Lm17; A24: Sum(p,n,n2) = Sum(p,n) - Sum(p,n2) by SERIES_1:def 7; now let m; assume A25: m <= n2; n1 <= n1+1 by NAT_1:11; then n2 <= n1 by XREAL_1:22; then A26: m <= n1 by A25,XXREAL_0:2; n1 <= n by Lm22; then m <= n by A26,XXREAL_0:2; hence p.m >= 0 by A22; end; then Sum(p,n2) >= 0 by Lm17; then Sum(p,n) + Sum(p,n2) >= Sum(p,n) + 0 by XREAL_1:9; then A27: Sum(p,n) >= Sum(p,n,n2) by A24,XREAL_1:22; A28: for N0 st n1 <= N0 & N0 <= n holds q.N0 <= p.N0 proof let N0; assume A29: n1 <= N0 & N0 <= n; then A30: q.N0 = (n/2) to_power k by A17,A20,A21; A31: p.N0 = N0 to_power k by A20,A21,A29,Def3; N0 >= n/2 by A21,A29,XXREAL_0:2; hence q.N0 <= p.N0 by A20,A30,A31,Lm6; end; n >= n1 by Lm22; then n+-1 >= n1+-1 by XREAL_1:8; then n-1 >= n1+-1; then n >= n2 + 1 by XREAL_1:21; then A32: Sum(p,n,n2) >= Sum(q,n,n2) by A28,Lm21; A33: Sum(q,n,n2) = (n-n2)*((n/2) to_power k) by A17,Lm23; A34: now assume A35: n-n2 < n/2; [/n/2\] < n/2 + 1 by INT_1:def 5; then n2 < n/2 by XREAL_1:21; then n/2 + n2 < n/2 + n/2 by XREAL_1:8; hence contradiction by A35,XREAL_1:21; end; ((n/2) to_power k) > 0 by A20,POWER:39; then Sum(q,n,n2) >= (n/2) * ((n/2) to_power k) by A33,A34,XREAL_1:66; 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 A20,POWER:32; then Sum(q,n,n2) >= (n to_power (k+1))/(2 to_power (k+1)) by A14,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 A32, XXREAL_0:2; hence (2 to_power (k+1))"*g.n <= f.n by A18,A19,A27,XXREAL_0:2; thus f.n >= 0 by A1,A23; end; then f in Big_Omega(g) by A2,A3; hence thesis by A13,XBOOLE_0:def 3; 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; 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 A3: t = g and A4: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0; consider c,N such that A5: c > 0 and A6: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A4; set N0 = [/sqrt c / sqrt 2\]; reconsider N2=max(N, N0) as Integer by XXREAL_0:16; set N1 = max( N2, 2 ); A7: N1 >= N2 & N1 >= 2 by XXREAL_0:25; N2 >= N & N2 >= N0 by XXREAL_0:25; then A8: N1 >= N & N1 >= N0 by A7,XXREAL_0:2; N1 is Integer by XXREAL_0:16; then reconsider N1 as Element of NAT by A7,INT_1:16; set n = N1 + 1; n > N1 + 0 by XREAL_1:10; then A9: n > N0 & n > N & n > 2 by A7,A8,XXREAL_0:2; A10: n to_power log(2,n) > 0 by POWER:39; A11: 2*n > 2*0 by XREAL_1:70; A12: (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)) .= ((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))) .= (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 A11,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; A13: sqrt 2 > 0 by SQUARE_1:93; A14: sqrt 2 <> 0 by SQUARE_1:93; A15: sqrt c > 0 by A5,SQUARE_1:93; N0 >= sqrt c / sqrt 2 by INT_1:def 5; then n > sqrt c / sqrt 2 by A9,XXREAL_0:2; then n*sqrt 2 > (sqrt c / sqrt 2) * sqrt 2 by A13,XREAL_1:70; then n*sqrt 2 > sqrt c by A14,XCMPLX_1:88; then (n*sqrt 2)^2 > (sqrt c)^2 by A15,SQUARE_1:78; then n^2*(sqrt 2)^2 > c by A5,SQUARE_1:def 4; 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 A10,A12, XREAL_1:70; then f.(2*n) > c*(n to_power log(2,n)) by A1,A11; then t.n > c*(n to_power log(2,n)) by A3,ASYMPT_0:def 18; then t.n > c*f.n by A1; hence contradiction by A6,A9; end; hence thesis; end; :: Example p. 92 definition let b be Real; func seq_const(b) -> Real_Sequence equals 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; registration cluster seq_const(1) -> eventually-nonnegative; coherence proof take 0; let n; assume n >= 0; thus (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; b > 1 by A1,A2,XXREAL_0:2; then log(b,c) >= log(b,1) by A3,PRE_FF:12; then A4: log(b,c) >= 0 by A1,A2,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 A4,XREAL_1:66; hence thesis by A1,A2,A3,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); now hereby assume h in F to_power Big_Oh(seq_const(1)); then consider t being Element of Funcs(NAT,REAL) such that A1: h = t and A2: 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); consider f,g being Element of Funcs(NAT,REAL), N0 being Element of NAT such that A3: f in F and A4: g in G and A5: for n being Element of NAT st n>=N0 holds t.n = (f.n) to_power (g.n) by A2; A6: f = seq_n^(1) by A3,TARSKI:def 1; consider g' being Element of Funcs(NAT, REAL) such that A7: g = g' and A8: ex c,N st c > 0 & for n st n >= N holds g'.n <= c*p.n & g'.n >= 0 by A4; consider c,N1 such that A9: c > 0 and A10: for n st n >= N1 holds g'.n <= c*p.n & g'.n >= 0 by A8; set N = max(2,max(N0,N1)); max(N0,N1) >= N0 & max(N0,N1) >= N1 & N >= max(N0,N1) by XXREAL_0:25; then A11: N >= N0 & N >= N1 & N >= 2 by XXREAL_0:2,25; set k = [/c\]; A12: k >= c by INT_1:def 5; k > 0 by A9,INT_1:def 5; then reconsider k as Element of NAT by INT_1:16; reconsider i = 1 as Element of NAT; take N,i,k; thus i > 0; let n; assume A13: n >= N; then A14: n >= N0 & n >= N1 & n >= 2 by A11,XXREAL_0:2; then A15: g'.n <= c*p.n & g'.n >= 0 by A10; A16: p.n = 1 by FUNCOP_1:13; A17: n > 0 & n > 1 by A14,XXREAL_0:2; f.n = n to_power 1 by A6,A11,A13,Def3 .= n by POWER:30; then A18: h.n = n to_power (g.n) by A1,A5,A11,A13,XXREAL_0:2; n to_power (g.n) >= n to_power 0 by A7,A15,A17,PRE_FF:10; hence 1 <= h.n by A18,POWER:29; g.n <= c*p.n by A7,A10,A14; then A19: h.n <= n to_power (c*1) by A16,A17,A18,PRE_FF:10; n to_power c <= n to_power k by A12,A17,PRE_FF:10; then h.n <= n to_power k by A19,XXREAL_0:2; hence h.n <= i*(seq_n^(k)).n by A11,A13,Def3; end; given N0,c,k such that c > 0 and A20: 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; set N = max(N0,2); A21: N >= N0 & N >= 2 by XXREAL_0:25; then A22: N > 1 by XXREAL_0:2; A23: N > 0 & N <> 1 by XXREAL_0:25; set c1= max(c,2); A24: c1 >= c & c1 >= 2 by XXREAL_0:25; then A25: c1 > 0 & c1 > 1 by XXREAL_0:2; 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[Element of NAT,Real] means ($1 < N implies $2 = 1) & ($1 >= N implies $2 = log($1,t.$1)); A26: 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; end; suppose n >= N; hence thesis; end; end; consider g being Function of NAT,REAL such that A27: for x being Element of NAT holds Q[x,g.x] from FUNCT_2:sch 3(A26); A28: g is Element of Funcs(NAT,REAL) by FUNCT_2:11; A29: now let n be Element of NAT; assume A30: n >= N; then n >= N0 by A21,XXREAL_0:2; then A31: t.n >= 1 by A20; thus (f.n) to_power (g.n) = (n to_power 1) to_power (g.n) by A21,A30,Def3 .= n to_power (g.n) by POWER:30 .= n to_power (1*log(n,t.n)) by A27,A30 .= t.n by A22,A30,A31,POWER:def 3; end; A32: f in F by TARSKI:def 1; now log(N,1) = 0 by A23,POWER:59; then a > 0 by A22,A25,POWER:65; then k+a > k+0 by XREAL_1:8; hence b > 0; let n; assume A33: n >= N; then A34: n >= N0 & n >= 2 by A21,XXREAL_0:2; then A35: n > 1 by XXREAL_0:2; A36: n > 0 & n <> 1 by A21,A33,XXREAL_0:2; A37: a >= log(n,c1) by A22,A25,A33,Lm24; A38: 1 <= t.n & t.n <= c*(seq_n^(k)).n by A20,A34; A39: (seq_n^(k)).n = n to_power k by A21,A33,Def3; then A40: (seq_n^(k)).n > 0 by A21,A33,POWER:39; c*(seq_n^(k)).n <= c1*(seq_n^(k)).n by A39,XREAL_1:66,XXREAL_0:25; then t.n <= c1*(seq_n^(k)).n by A38,XXREAL_0:2; then A41: log(n,t.n) <= log(n,c1*(seq_n^(k)).n) by A35,A38,PRE_FF:12; t.n = (f.n) to_power (g.n) by A29,A33 .= (n to_power 1) to_power (g.n) by A21,A33,Def3 .= n to_power (g.n) by POWER:30; then A42: log(n,t.n) = g.n*log(n,n) by A36,POWER:63 .= g.n*1 by A36,POWER:60; A43: log(n,c1*(seq_n^(k)).n) = log(n,c1) + log(n,n to_power k) by A24,A36,A39,A40,POWER:61 .= log(n,c1) + k*log(n,n) by A36,POWER:63 .= log(n,c1) + k*1 by A36,POWER:60; A44: log(n,c1) + k <= a + k by A37,XREAL_1:8; (seq_const(1)).n = 1 by FUNCOP_1:13; hence g.n <= b*(seq_const(1)).n by A41,A42,A43,A44,XXREAL_0:2; g.n = log(n,t.n) by A27,A33; then g.n >= log(n,1) by A35,A38,PRE_FF:12; hence g.n >= 0 by A36,POWER:59; end; then g in G by A28; hence h in F to_power Big_Oh(seq_const(1)) by A28,A29,A32; 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: f is Element of Funcs(NAT, REAL) by FUNCT_2:11; consider t1 being Element of NAT such that A3: t1 = 10*10*10; consider t2 being Element of NAT such that A4: t2 = t1*t1; t1 = 10*10^2 by A3; then t1 = 10*(10 to_power 2) by POWER:53; then t1 = (10 to_power 1)*(10 to_power 2) by POWER:30; then A5: t1 = 10 to_power (1+2) by POWER:32; then A6: t2 = 10 to_power (3+3) by A4,POWER:32 .= 10 to_power 6; A7: 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 .= 1000; A8: for n st n >= 400 holds f.n <= 27*n^2 proof let n such that A9: 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,A6; then 3*t2 + -18*t1*n > 27*n^2 - 27*n^2 by A5,XREAL_1:21; then 3*t2 - 18*t1*n > 0; then A10: 3*t2 > 0 + 18*t1*n by XREAL_1:22; (18*t1)*n >= (18*t1)*400 by A9,XREAL_1:66; then 3*(10 to_power (3+3)) > t1*7200 by A6,A10,XXREAL_0:2; then 3*((10 to_power 3)*(10 to_power 3)) > t1*7200 by POWER:32; hence contradiction by A5,A7; end; hence thesis; end; A11: 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; A12: P[400] by A4,A5,A7; A13: for k be Nat st k >= 400 & P[k] holds P[k+1] proof let k be Nat such that A14: k >= 400 and A15: 18*t1*k - 3*t2 < 27*k^2; 18*t1*(k+1) - 3*t2 = (18*t1*k - 3*t2) + 18*t1; then A16: 18*t1*(k+1) - 3*t2 < 27*k^2 + 18*t1 by A15,XREAL_1:8; 54*400 <= 54*k by A14,XREAL_1:66; then A17: 18*t1 < 54*k by A5,A7,XXREAL_0:2; 54*k + 0 <= 54*k + 27 by XREAL_1:9; then 18*t1 < 54*k + 27 by A17,XXREAL_0:2; then 27*k^2 + 18*t1 < 27*k^2 + (54*k + 27) by XREAL_1:8; hence thesis by A16,XXREAL_0:2; end; for n be Nat st n >= 400 holds P[n]from NAT_1:sch 8(A12, A13); hence thesis; end; now let n; assume A18: n >= 400; then f.n <= 27*n^2 by A8; then f.n <= 27*(n to_power 2) by POWER:53; hence f.n <= 27*g.n by A18,Def3; 0 + (18*t1*n - 3*t2) < 27*n^2 by A11,A18; then 0 < 27*n^2 - (18*t1*n - 3*t2) by XREAL_1:22; then 0 < 3*(10 to_power 6) - 18*t1*n + 27*n^2 by A6; hence f.n >= 0 by A1,A5; end; hence thesis by A2; 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: f is Element of Funcs(NAT, REAL) by FUNCT_2:11; now let n; assume A2: n >= 2; then A3: n > 1 by XXREAL_0:2; A4: f.n = n to_power 2 by A2,Def3; g.n = n to_power 3 by A2,Def3; hence f.n <= 1*g.n by A3,A4,POWER:44; thus f.n >= 0 by A4; end; hence thesis by A1; 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); now assume seq_n^(2) in Big_Omega(seq_n^(3)); then consider s being Element of Funcs(NAT, REAL) such that A1: s = f and A2: ex d,N st d > 0 & for n st n >= N holds d*g.n <= s.n & s.n >= 0; consider d,N such that A3: d > 0 and A4: for n st n >= N holds d*g.n <= s.n & s.n >= 0 by A2; A5: N+2 > 1+0 by XREAL_1:10; ex n st n >= N & d*g.n > s.n proof take n = max( N, [/(N+2)/d\] ); A6: n >= [/(N+2)/d\] & n >= N by XXREAL_0:25; d" > 0 by A3,XREAL_1:124; then A7: (N+2)*d" > 0*d" by XREAL_1:70; A8: [/(N+2)/d\] >= (N+2)/d by INT_1:def 5; then A9: n > 0 by A6,A7,XCMPLX_0:def 9; n is Integer by XXREAL_0:16; then reconsider n as Element of NAT by A6,INT_1:16; A10: (d*g.n)*(n to_power -2) = d*(n to_power 3)*(n to_power -2) by A9,Def3 .= d*((n to_power 3)*(n to_power -2)) .= d*(n to_power (3+(-2))) by A9,POWER:32 .= d*n by POWER:30; A11: f.n*(n to_power -2) = (n to_power 2)*(n to_power -2) by A9,Def3 .= (n to_power (2+(-2))) by A9,POWER:32 .= 1 by POWER:29; A12: d*([/(N+2)/d\]) >= d*((N+2)/d) by A3,A8,XREAL_1:66; d*n >= d*([/(N+2)/d\]) by A3,XREAL_1:66,XXREAL_0:25; then d*n >= ((N+2)/d)*d by A12,XXREAL_0:2; then d*n >= N+2 by A3,XCMPLX_1:88; then A13: (d*g.n)*(n to_power -2) > f.n*(n to_power -2) by A5,A10,A11,XXREAL_0:2; (n to_power -2) > 0 by A9,POWER:39; hence thesis by A1,A13,XREAL_1:66,XXREAL_0:25; end; hence contradiction by A4; end; hence thesis; end; 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 .= f.n by A4; hence (2 to_power -1)*g.n <= f.n; n+0 <= n+1 by XREAL_1:9; hence f.n <= 1*g.n by A4,A5,PRE_FF:10; end; hence thesis by A1,A2,A3; end; definition let a be Element of NAT; func seq_n!(a) -> Real_Sequence means :Def5: it.n = (n+a)!; existence proof deffunc F(Element of NAT) = ($1+a)!; consider h being Function of NAT, REAL such that A1: for n being Element of NAT holds h.n = F(n) from FUNCT_2:sch 4; 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; registration let a be Element of 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 XXREAL_0:25; n is Integer by XXREAL_0:16; then reconsider n as Element of NAT by A6,INT_1:16; A7: n! <> 0 by NEWTON:23; A8: (d*g.n)*(n!)" = (d*((n+1)!))*(n!)" by Def5 .= (d*((n+1)*(n!)))*(n!)" by NEWTON:21 .= (d*(n+1)*((n!)*(n!)")) .= (d*(n+1))*1 by A7,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 XREAL_1:8; then A9: d*([/(N+1)/d\] + 1) >= d*((N+1)/d + 1) by A4,XREAL_1:66; n+1 >= [/(N+1)/d\]+1 by A6,XREAL_1:8; then d*(n+1) >= d*([/(N+1)/d\]+1) by A4,XREAL_1:66; then A10: d*(n+1) >= d*(((N+1)/d) + 1) by A9,XXREAL_0:2; A11: d*(((N+1)/d) + 1) = d*((N+1)/d) + d*1 .= (N+1) + d by A4,XCMPLX_1:88; N+1 >= 1+0 by XREAL_1:8; then d*(((N+1)/d) + 1) > 1 by A4,A11,XREAL_1:10; then A12: (d*g.n)*(n!)" > 1 by A8,A10,XXREAL_0:2; f.n*(n!)" = (n+0)!*(n!)" by Def5 .= 1 by A7,XCMPLX_0:def 7; hence thesis by A12,XREAL_1:66,XXREAL_0:25; 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 XREAL_1:66; hence a*c <= b*d by XXREAL_0:2; 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 f in Big_Oh(g); then consider t being Element of Funcs(NAT, REAL) such that A1: t = f and A2: ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0; consider c, N such that A3: c > 0 and A4: for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A2; set d = max( c, c*c ); A5: d > 0 by A3,XXREAL_0:25; A6: t(#)t is Element of Funcs(NAT, REAL) by FUNCT_2:11; A7: 0 to_power 1 = 0 by POWER:def 2; now take N; let n; assume n >= N; then A8: t.n <= c*g.n & t.n >= 0 by A4; A9: g.n >= 0 proof per cases; suppose n = 0; hence thesis by Def3; end; suppose n > 0; then g.n = n to_power 1 by Def3 .= n by POWER:30; hence thesis; end; end; A10: for n holds g.n <= h.n proof let n; per cases; suppose A11: n = 0; then g.n = 0 by Def3; hence g.n <= h.n by A11,Def3; end; suppose n > 0; then A12: n >= 0+1 by NAT_1:13; thus g.n <= h.n proof per cases by A12,REAL_1:def 5; suppose A13: n = 1; (1 to_power 1) = 1 & (1 to_power 2) = 1 by POWER:31; then g.n = (1 to_power 2) by A13,Def3; hence g.n <= h.n by A13,Def3; end; suppose A14: n > 1; then (n to_power 1) < (n to_power 2) by POWER:44; then g.n < (n to_power 2) by A14,Def3; hence g.n <= h.n by A14,Def3; end; end; end; end; A15: t.n*t.n <= (c*g.n)*(c*g.n) by A8,Lm26; A16: (n to_power 1)*(n to_power 1) = (n to_power (1+1)) proof per cases; suppose n = 0; hence thesis by A7,POWER:def 2; end; suppose n > 0; hence thesis by POWER:32; end; end; A17: g.n*g.n = h.n proof per cases; suppose A18: n = 0; hence g.n*g.n = 0*g.n by Def3 .= h.n by A18,Def3; end; suppose A19: n > 0; hence g.n*g.n = (n to_power 1)*g.n by Def3 .= (n to_power (1+1)) by A16,A19,Def3 .= h.n by A19,Def3; end; end; h.n >= g.n by A10; then (c*c)*h.n <= d*h.n by A9,XREAL_1:66,XXREAL_0:25; then t.n*t.n <= d*h.n by A15,A17,XXREAL_0:2; hence (t(#)t).n <= d*h.n by SEQ_1:12; t.n*t.n >= t.n*0 by A8; hence (t(#)t).n >= 0 by SEQ_1:12; end; hence thesis by A1,A5,A6; 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: 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; A2: g.n = n proof per cases; suppose n = 0; hence thesis by Def3; end; suppose n > 0; hence g.n = n to_power 1 by Def3 .= n by POWER:30; end; end; 2*n >= 2*0; hence f.n >= 0 by A2,SEQ_1:13; end; hence f in Big_Oh(g) by A1; now assume p in Big_Oh(q); then consider t being Element of Funcs(NAT, REAL) such that A3: t = p and A4: ex c,N st c > 0 & for n st n >= N holds t.n <= c*q.n & t.n >= 0; consider c,N such that A5: c > 0 and A6: for n st n >= N holds t.n <= c*q.n & t.n >= 0 by A4; ex n st n >= N & t.n > c*q.n proof take n = max( N, [/log(2,c)+1\] ); A7: n >= N & n >= [/log(2,c)+1\] by XXREAL_0:25; n is Integer by XXREAL_0:16; then reconsider n as Element of NAT by A7,INT_1:16; A8: (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)) .= c*(2 to_power (n+-n)) by POWER:32 .= c*1 by POWER:29; A9: 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 (1*n)); A10: 2 to_power n >= 2 to_power [/log(2,c)+1\] by PRE_FF:10,XXREAL_0:25; [/log(2,c)+1\] >= log(2,c)+1 by INT_1:def 5; then A11: 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 A5,POWER:def 3 .= c*2 by POWER:30; then 2 to_power (log(2,c)+1) > (c*q.n)*(2 to_power -n) by A5,A8,XREAL_1:70; then 2 to_power [/log(2,c)+1\] > (c*q.n)*(2 to_power -n) by A11, XXREAL_0:2; then A12: p.n*(2 to_power -n) > (c*q.n)*(2 to_power -n) by A9,A10,XXREAL_0:2; 2 to_power -n > 0 by POWER:39; hence thesis by A3,A12,XREAL_1:66,XXREAL_0:25; end; hence contradiction by A6; 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); A2: log(2,3) - log(2,3) < 159/100 - log(2,3) by A1,XREAL_1:11; then A3: c*2" > 0*2" by XREAL_1:70; A4: c/2 <> 0 by A1; 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([/((1/p1) to_power (1/(c/2)))\], 2); A7: N1 >= [/((1/p) to_power (1/(c/2)))\] & N1 >= 2 by XXREAL_0:25; then A8: N1 > 1 by XXREAL_0:2; N1 is Integer by XXREAL_0:16; then reconsider N1 as Element of NAT by A7,INT_1:16; take N1; let n; assume A9: n >= N1; p" > 0 by A6,XREAL_1:124; then A10: 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 A11: N1 >= ((1/p) to_power (1/(c/2))) by A7,XXREAL_0:2; A12: ((1/p1) to_power (1/(c/2))) > 0 by A10,POWER:39; A13: n > 1 by A8,A9,XXREAL_0:2; A14: h.n = f.n/g.n by Lm4; f.n = (n to_power log(2,3)) by A7,A9,Def3; then A15: h.n = (n to_power log(2,3)) / (n to_power (159/100)) by A7,A9,A14,Def3 .= (n to_power (log(2,3) - (159/100))) by A7,A9,POWER:34 .= (n to_power -c); n >= ((1/p) to_power (1/(c/2))) by A9,A11,XXREAL_0:2; then n to_power (c/2) >= ((1/p) to_power (1/(c/2))) to_power (c/2) by A3,A12,Lm6; then n to_power (c/2) >= (1/p1) to_power ((1/(c/2))*(c/2)) by A10,POWER:38; then n to_power (c/2) >= (1/p) to_power 1 by A4,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 A10,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 A16: n to_power -(c/2) <= p by A7,A9,POWER:33; A17: n to_power (c/2) > 0 by A7,A9,POWER:39; c*(1/2) < c*1 by A2,XREAL_1:70; then n to_power (c/2) < n to_power c by A13,POWER:44; then 1 / (n to_power (c/2)) > 1 / (n to_power c) by A17,REAL_2:151; then n to_power -(c/2) > 1 / (n to_power c) by A7,A9,POWER:33; then h.n < n to_power -(c/2) by A7,A9,A15,POWER:33; then A18: h.n < p by A16,XXREAL_0:2; h.n > 0 by A7,A9,A15,POWER:39; hence abs(h.n-0) < p by A18,ABSVALUE:def 1; end; then A19: h is convergent by SEQ_2:def 6; then A20: lim h = 0 by A5,SEQ_2:def 7; then A21: f in Big_Oh(g) & not g in Big_Oh(f) by A19,ASYMPT_0:16; then A22: f in Big_Oh(g) & not f in Big_Omega(g) by ASYMPT_0:19; thus f in Big_Oh(g) by A19,A20,ASYMPT_0:16; thus not f in Big_Omega(g) by A21,ASYMPT_0:19; thus not f in Big_Theta(g) by A22,XBOOLE_0:def 3; 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,NAT_D:12; suppose f.n = 0; hence f.n >= 0; end; suppose f.n = 1; hence f.n >= 0; end; 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,NAT_D:12; suppose g.n = 0; hence g.n >= 0; end; suppose g.n = 1; hence g.n >= 0; end; end; then reconsider g as eventually-nonnegative Real_Sequence; take f,g; A5: now assume f in Big_Oh(g); then consider t being Element of Funcs(NAT, REAL) such that A6: t = f and A7: ex c,N st c > 0 & for n st n >= N holds t.n <= c*g.n & t.n >= 0; consider c,N such that c > 0 and A8: for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A7; ex n st n >= N & t.n > c*g.n proof per cases by NAT_D:12; suppose A9: N mod 2 = 0; A10: N+1 >= N by NAT_1:13; A11: t.(N+1) = (N+1) mod 2 by A1,A6 .= (0+(1 mod 2)) mod 2 by A9,EULER_2:8 .= (0+1) mod 2 by NAT_D:14 .= 1 by NAT_D:14; g.(N+1) = ((N+1)+1) mod 2 by A2 .= (N+(1+1)) mod 2 .= (0+(2 mod 2)) mod 2 by A9,EULER_2:8 .= (0+0) mod 2 by NAT_D:25 .= 0 by NAT_D:26; then c*g.(N+1) = 0; hence thesis by A10,A11; end; suppose A12: N mod 2 = 1; then A13: t.N = 1 by A1,A6; g.N = (N+1) mod 2 by A2 .= (1+(1 mod 2)) mod 2 by A12,EULER_2:8 .= (1+1) mod 2 by NAT_D:14 .= 0 by NAT_D:25; then c*g.N = 0; hence thesis by A13; end; end; hence contradiction by A8; end; now assume g in Big_Oh(f); then consider t being Element of Funcs(NAT, REAL) such that A14: t = g and A15: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0; consider c,N such that c > 0 and A16: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A15; ex n st n >= N & t.n > c*f.n proof per cases by NAT_D:12; suppose A17: N mod 2 = 0; A18: t.N = (N+1) mod 2 by A2,A14 .= (0+(1 mod 2)) mod 2 by A17,EULER_2:8 .= (0+1) mod 2 by NAT_D:14 .= 1 by NAT_D:14; f.N = 0 by A1,A17; then c*f.N = 0; hence thesis by A18; end; suppose A19: N mod 2 = 1; A20: N+1 >= N by NAT_1:13; A21: t.(N+1) = ((N+1)+1) mod 2 by A2,A14 .= (N+(1+1)) mod 2 .= (1+(2 mod 2)) mod 2 by A19,EULER_2:8 .= (1+0) mod 2 by NAT_D:25 .= 1 by NAT_D:14; f.(N+1) = (N+1) mod 2 by A1 .= (1+(1 mod 2)) mod 2 by A19,EULER_2:8 .= (1+1) mod 2 by NAT_D:14 .= 0 by NAT_D:25; then c*f.(N+1) = 0; hence thesis by A20,A21; end; end; hence contradiction by A16; end; hence thesis by A5; 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; hereby assume A1: Big_Oh(f) = Big_Oh(g); then A2: f in Big_Oh(g) by ASYMPT_0:10; g in Big_Oh(f) by A1,ASYMPT_0:10; then f in Big_Omega(g) by ASYMPT_0:19; hence f in Big_Theta(g) by A2,XBOOLE_0:def 3; end; assume A3: 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 A4: x = t and A5: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0; consider c,N such that c > 0 and A6: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A5; now take N; let n; assume n >= N; hence t.n >= 0 by A6; end; then A7: t is eventually-nonnegative by ASYMPT_0:def 4; A8: t in Big_Oh(f) by A5; f in Big_Oh(g) by A3,XBOOLE_0:def 3; hence x in Big_Oh(g) by A4,A7,A8,ASYMPT_0:12; end; assume x in Big_Oh(g); 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*g.n & t.n >= 0; consider c,N such that c > 0 and A11: for n st n >= N holds t.n <= c*g.n & t.n >= 0 by A10; now take N; let n; assume n >= N; hence t.n >= 0 by A11; end; then A12: t is eventually-nonnegative by ASYMPT_0:def 4; A13: t in Big_Oh(g) by A10; f in Big_Omega(g) by A3,XBOOLE_0:def 3; then g in Big_Oh(f) by ASYMPT_0:19; hence x in Big_Oh(f) by A9,A12,A13,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 XXREAL_0:25; now take N; let n; assume n >= N; then A11: n >= N1 & n >= N3 by A10,XXREAL_0:2; then f.n >= 0 by A3; then d*f.n >= d*0 by A8; 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 XXREAL_0:25; now take N; let n; assume n >= N; then A18: n >= N2 & n >= N3 by A17,XXREAL_0:2; then g.n >= 0 by A4; then d*g.n >= d*0 by A15; 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[Element of NAT] means ($1^2 - $1 + 1) > 0; A1: P[0]; A2: for k st P[k] holds P[k+1] proof let k such that A3: (k^2 - k + 1) > 0; (k^2 - k + 1) + 2*k > 0+0 by A3; hence thesis; end; for n holds P[n] from NAT_1:sch 1(A1, A2); hence thesis; end; Lm28: for f,g being Real_Sequence, N being Element of 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 Element of 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 XXREAL_0:25; take N1; let n; assume A7: n >= N1; then n >= N & n >= M by A6,XXREAL_0:2; then abs(f.n-c) < p by A5; hence abs(g.n-c) < p by A3,A6,A7,XXREAL_0:2; 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^2 + (-n + 1)) > n^2 + -n^2 by XREAL_1:8; then 1 > 0 -(-n) by XREAL_1:21; 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]; A2: for k be Nat st k>=1 & P[k] holds P[k+1] proof let k be Nat such that A3: k >= 1 and A4: k^2 <= 2*(k^2 -k + 1); A5: k^2 + (2*k + 1) <= 2*(k^2 -k + 1) + (2*k + 1) by A4,XREAL_1:8; 2*k >= 2*1 by A3,XREAL_1:66; then A6: 2*k + 2 >= 2 + 2 by XREAL_1:8; A7: 2*k^2 + 3 <= 2*k^2 + 4 by XREAL_1:8; 2*k^2 + 4 <= 2*k^2 + (2*k + 2) by A6,XREAL_1:8; then 2*(k^2 -k + 1) + (2*k + 1) <= 2*k^2 + (2*k + 2) by A7,XXREAL_0:2; hence thesis by A5,XXREAL_0:2; end; for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8(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,XREAL_1:8; 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 XREAL_1:70; 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 XXREAL_0:25; now take N1; let n; assume A7: n >= N1; then A8: n >= 2 & n >= N by A6,XXREAL_0:2; 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 XREAL_1:124; then log(2,n)*(n to_power e)" > 0*(n to_power e)" by A10,XREAL_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,XXREAL_0:2; 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,XREAL_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,XXREAL_0:2; n" > 0 by A6,A7,XREAL_1:124; then log(2,n)*n" > 0*n" by A10,XREAL_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,XREAL_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,XREAL_1:70; then d * ((n / log(2,n)) * log(2,n)) > 16*log(2,n); then d*n > (8+8)*log(2,n) by A10,XCMPLX_1:88; then d*n - 8*log(2,n) > (8*log(2,n) + 8*log(2,n)) - 8*log(2,n) by XREAL_1:11; 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,XREAL_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))") .= 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))) .= 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 XXREAL_0:2; 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 XREAL_1:124; then (n to_power 2)*(log(2,n))" > (n to_power 2)*0 by A5,XREAL_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 XREAL_1:22; then A6: p is convergent & lim p = 0 by Lm16; A7: (1+e)-2 = e-1; for n st n >= 2 holds h.n = p.n proof let n; assume A8: n >= 2; then A9: n > 1 by XXREAL_0:2; 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) .= ((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) by A7,A8,POWER:34 .= 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 XXREAL_0:2; 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 XREAL_1:124; then (n to_power 2)*(log(2,n))" > (n to_power 2)*0 by A4,XREAL_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 XXREAL_0:25; N is Integer by XXREAL_0:16; then reconsider N as Element of 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,XXREAL_0:2; 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,XXREAL_0:2; then A11: log(2,n) > 1 by POWER:60; A12: n > 1 by A9,XXREAL_0:2; 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)") .= (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,XREAL_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,XXREAL_0:2; 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,XXREAL_0:2; (n to_power 6)*log(2,n) > (n to_power 6)*0 by A11,A13,XREAL_1:70; then ((n to_power 6)*log(2,n))" > 0 by XREAL_1:124; 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; g.n = (n^2 - n + 1) to_power 4 by A1; hence g.n > 0 by Lm27,POWER:39; end; then reconsider g as eventually-positive Real_Sequence; take g; A2: f is Element of Funcs(NAT, REAL) by FUNCT_2:11; A3: g is Element of Funcs(NAT, REAL) by FUNCT_2:11; now let n; assume A4: n >= 1; then A5: f.n = n to_power (2*4) by Def3 .= n to_power 2 to_power 4 by A4,POWER:38 .= n^2 to_power 4 by POWER:53; A6: g.n = (n^2 -n + 1) to_power 4 by A1; n^2 -n + 1 <= n^2 by A4,Lm29; hence g.n <= 1*f.n by A5,A6,Lm6,Lm27; thus g.n >= 0 by A6,Lm27,POWER:39; end; then A7: g in Big_Oh(f) by A3; now let n; assume A8: n >= 1; then A9: f.n = n to_power (2*4) by Def3 .= n to_power 2 to_power 4 by A8,POWER:38 .= n^2 to_power 4 by POWER:53; A10: g.n = (n^2 -n + 1) to_power 4 by A1; A11: n^2 <= 2*(n^2 -n + 1) by A8,Lm30; A12: (n^2 -n + 1) > 0 by Lm27; A13: n*n > n*0 by A8,XREAL_1:70; then f.n <= (2*(n^2 -n + 1)) to_power 4 by A9,A11,Lm6; hence f.n <= 16*g.n by A10,A12,Lm9,POWER:35; thus f.n >= 0 by A9,A13,POWER:39; end; then f in Big_Oh(g) by A2; hence thesis by A7,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; then reconsider g as eventually-positive Real_Sequence; 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 XXREAL_0:25; 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 XXREAL_0:25; then A9: N1 >= [/((1/p) to_power (1/8))\] & N1 >= 2 by A7,XXREAL_0:2; N1 is Integer proof per cases by XXREAL_0:16; suppose N1 = N; hence thesis; end; suppose N1 = max([/((1/p) to_power (1/8))\], 2); hence thesis by XXREAL_0:16; end; end; then reconsider N1 as Element of NAT by A7,INT_1:16; take N1; let n; assume A10: n >= N1; p" > 0 by A6,XREAL_1:124; 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,XXREAL_0:2; A13: ((1/p1) to_power (1/8)) > 0 by A11,POWER:39; A14: n >= N by A7,A10,XXREAL_0:2; 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)))); n >= ((1/p) to_power (1/8)) by A10,A12,XXREAL_0:2; 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,XXREAL_0:2; 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 be Nat st n >= 3 holds n^2 > 2*n + 1 proof defpred P[Nat] means $1^2 > 2*$1 + 1; A1: P[3]; A2: for n be Nat st n >= 3 & P[n] holds P[n+1] proof let n be Nat; assume that A3: n >= 3 and A4: n^2 > 2*n + 1; A5: n^2 + (n + (n+1)) > 2*n + 1 + (n + (n+1)) by A4,XREAL_1:8; n > 0 & n > 1 by A3,XXREAL_0:2; then n + n > 1 + 0 by XREAL_1:10; then 2*n + 2*(n+1) > 1 + 2*(n+1) by XREAL_1:8; hence (n+1)^2 > 2*(n+1) + 1 by A5,XXREAL_0:2; end; for n be Nat st n >= 3 holds P[n] from NAT_1:sch 8(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 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; hence thesis; end; A2: for n be Nat st n >= 10 & P[n] holds P[n+1] proof let n be Nat; assume that A3: n >= 10 and A4: 2 to_power (n-1) > (2*n)^2; 2 to_power ((n+1)-1) = 2 to_power ((n+-1)+1) .= (2 to_power (n-1))*(2 to_power 1) by POWER:32 .= (2 to_power (n-1))*2 by POWER:30; then A5: 2 to_power ((n+1)-1) > ((2*n)^2)*2 by A4,XREAL_1:70; now assume ((2*n)^2)*2 <= (2*2)*(n*n + 2*n + 1); then ((2*2)*(n*n))*2 <= (2*2)*(n*n) + (2*2)*(2*n + 1); then ((2*2)*(n*n))*2 - (2*2)*(n*n) <= (2*2)*(2*n + 1) by XREAL_1:22; then (2*2)"*((2*2)*(n*n)) <= (2*2)"*((2*2)*(2*n + 1)) by XREAL_1:66; then A6: n^2 <= 2*n + 1; n >= 3 by A3,XXREAL_0:2; hence contradiction by A6,Lm33; end; hence 2 to_power ((n+1)-1) > (2*(n+1))^2 by A5,XXREAL_0:2; end; for n be Nat st n >= 10 holds P[n] from NAT_1:sch 8(A1, A2); hence thesis; end; Lm35: for n be Nat 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 t6 being Element of NAT such that A4: t6 = 10*10*10*10*10*10; A5: 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; A6: 10 to_power 6 = 10 to_power (3+3) .= (10*10*10)*(10*10*10) by A5,POWER:32 .= t6 by A4; (13122*9)*9 = (2*((9 to_power 4)*9))*9 by A3 .= (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) .= 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 A4,A6; end; A7: for n be Nat st n >= 9 & P[n] holds P[n+1] proof let n be Nat; assume that A8: n >= 9 and A9: (n+1) to_power 6 < 2*(n to_power 6); A10: n to_power 6 > 0 by A8,POWER:39; A11: (n+1) to_power 6 > 0 by POWER:39; (n+1)" > 0 by XREAL_1:124; then (n+2)*((n+1)") > 0*((n+1)") by XREAL_1:70; then A12: ((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 XREAL_1:66; then (n+2) >= (n+1) / n * (n+1) by XCMPLX_1:88; then (n+2)*n >= (n+1) / n * (n+1) * n by XREAL_1:66; then (n+2)*n >= ((n+1) / n * n) * (n+1); then n^2 + 2*n >= (n+1)^2 by A8,XCMPLX_1:88; then n^2 + 2*n >= n^2 + 2*n + 1*1; then (n^2 + 2*n) - (n^2 + 2*n) >= 1 by XREAL_1:21; hence contradiction by XCMPLX_1:14; end; then A13: ((n+2) / (n+1)) to_power 6 < ((n+1) / n) to_power 6 by A12,POWER:42; (n+1) to_power 6 / n to_power 6 < 2 by A9,A10,REAL_2:178; then ((n+1) / n) to_power 6 < 2 by A8,POWER:36; then ((n+2) / (n+1)) to_power 6 < 2 by A13,XXREAL_0:2; 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 A11,XREAL_1:70; hence thesis by A11,XCMPLX_1:88; end; for n be Nat st n >= 9 holds P[n] from NAT_1:sch 8(A1, A7); hence thesis; end; Lm36: for n st n >= 30 holds 2 to_power n > n to_power 6 proof defpred P[Nat] means 2 to_power $1 > $1 to_power 6; A1: P[30] proof 2 to_power 30 = 2 to_power (5*6) .= 32 to_power 6 by Lm10,POWER:38; hence thesis by POWER:42; end; A2: for n be Nat st n >= 30 & P[n] holds P[n+1] proof let n be Nat; assume that A3: n >= 30 and A4: 2 to_power n > n to_power 6; A5: 2 to_power (n+1) = (2 to_power n)*(2 to_power 1) by POWER:32 .= (2 to_power n)*2 by POWER:30; A6: (2 to_power n)*2 > (n to_power 6)*2 by A4,XREAL_1:70; n >= 9 by A3,XXREAL_0:2; then (n+1) to_power 6 < 2*(n to_power 6) by Lm35; hence thesis by A5,A6,XXREAL_0:2; end; for n be Nat st n >= 30 holds P[n] from NAT_1:sch 8(A1, A2); hence thesis; end; Lm37: for x being Real st x > 9 holds 2 to_power x > (2*x)^2 proof let x be Real such that A1: x > 9; set n = [/x\]; A2: n >= x by INT_1:def 5; then reconsider n as Element of NAT by A1,INT_1:16; x >= [\x/] by INT_1:def 4; then A3: 2 to_power x >= 2 to_power [\x/] by PRE_FF:10; [/x\] - [\x/] <= 1 proof per cases; suppose x is Integer; then [\x/] = [/x\] by INT_1:59; hence thesis; end; suppose not x is Integer; then not [\x/] = [/x\] by INT_1:59; then [\x/] + 1 = [/x\] by INT_1:66; hence thesis; end; end; then [/x\] <= 1 + [\x/] by XREAL_1:22; then [\x/] >= n-1 by XREAL_1:22; then 2 to_power [\x/] >= 2 to_power (n-1) by PRE_FF:10; then A4: 2 to_power x >= 2 to_power (n-1) by A3,XXREAL_0:2; n > 9 by A1,A2,XXREAL_0:2; then n >= 9+1 by NAT_1:13; then 2 to_power (n-1) > (2*n)^2 by Lm34; then A5: 2 to_power x > (2*n)^2 by A4,XXREAL_0:2; A6: 2*n >= 2*x by A2,XREAL_1:66; 2*x >= 0*x by A1; then (2*n)^2 >= (2*x)*(2*x) by A6,Lm26; hence 2 to_power x > (2*x)^2 by A5,XXREAL_0:2; end; Lm38: ex N st for n st n >= N holds sqrt n - log(2, n) > 1 proof ex N st for n st n >= N holds n/6 > 1 proof now take N = 7; let n; assume n >= N; then n > 6 by XXREAL_0:2; then n/6 > 6/6 by REAL_1:73; hence n/6 > 1; end; hence thesis; end; then consider N1 such that A1: for n st n >= N1 holds n/6 > 1; ex N st for n st n >= N holds n/3 > 2*log(2,n) proof now take N = 30; let n; assume A2: n >= N; then A3: 2 to_power n > n to_power 6 by Lm36; n to_power 6 > 0 by A2,POWER:39; then log(2,2 to_power n) > log(2,n to_power 6) by A3,POWER:65; then n*log(2,2) > log(2,n to_power 6) by POWER:63; then n*1 > log(2,n to_power 6) by POWER:60; then n > (3*2)*log(2,n) by A2,POWER:63; then n > 3*(2*log(2,n)); hence n/3 > 2*log(2,n) by REAL_2:178; end; hence thesis; end; then consider N2 such that A4: for n st n >= N2 holds n/3 > 2*log(2,n); ex N st for n st n >= N holds n/2 > log(2,n)*log(2,n) proof reconsider N = 2 to_power 10 as Element of NAT; now take N; let n; assume A5: n >= N; set x = log(2,n); A6: n > 0 by A5,POWER:39; A7: 2 to_power 9 > 0 by POWER:39; 2 to_power 10 > 2 to_power 9 by POWER:44; then n > 2 to_power 9 by A5,XXREAL_0:2; then log(2,n) > log(2,2 to_power 9) by A7,POWER:65; then x > 9*log(2,2) by POWER:63; then A8: x > 9*1 by POWER:60; then A9: 2*x > 0*x by XREAL_1:70; then (2*x)*(2*x) > 0*(2*x) by XREAL_1:70; then log(2, 2 to_power x) > log(2,(2*x)^2) by A8,Lm37,POWER:65; then x*log(2,2) > log(2,(2*x)^2) by POWER:63; then x*1 > log(2,(2*x)^2) by POWER:60; then x > log(2,(2*x) to_power 2) by POWER:53; then x > 2*log(2,2*x) by A9,POWER:63; then log(2,n) > 2*log(2,log(2,n to_power 2)) by A6,POWER:63; then A10: log(2,n) > 2*log(2,log(2,n^2)) by POWER:53; 2 to_power 10 > 2 to_power 1 by POWER:44; then n > 2 to_power 1 by A5,XXREAL_0:2; then A11: n > 2 by POWER:30; then A12: n*n > 2*n by XREAL_1:70; 2*n > 2*2 by A11,XREAL_1:70; then n^2 > 2*2 by A12,XXREAL_0:2; then log(2,n^2) > log(2,2^2) by POWER:65; then log(2,n^2) > log(2,2 to_power 2) by POWER:53; then log(2,n^2) > 2*log(2,2) by POWER:63; then A13: log(2,n^2) > 2*1 by POWER:60; 2 to_power log(2,n) > 2 to_power (2*log(2,log(2,n^2))) by A10,POWER:44; then n > 2 to_power (2*log(2,log(2,n^2))) by A6,POWER:def 3; then n > 2 to_power (log(2,log(2,n^2) to_power 2)) by A13,POWER:63; then A14: n > 2 to_power (log(2,(log(2,n^2))^2)) by POWER:53; (log(2,n^2))^2 > 0 by A13,SQUARE_1:74; then n > (log(2,n^2))^2 by A14,POWER:def 3; then n > (log(2,n to_power 2))^2 by POWER:53; then A15: n > (2*log(2,n))^2 by A6,POWER:63; 2 to_power 10 > 2 to_power 0 by POWER:44; then n > 2 to_power 0 by A5,XXREAL_0:2; then n > 1 by POWER:29; then log(2,n) > log(2,1) by POWER:65; then log(2,n) > 0 by POWER:59; then log(2,n)*log(2,n) > 0*log(2,n) by XREAL_1:70; then 4*(log(2,n)*log(2,n)) > 2*(log(2,n)*log(2,n)) by XREAL_1:70; then n > 2*(log(2,n)*log(2,n)) by A15,XXREAL_0:2; hence n/2 > log(2,n)*log(2,n) by REAL_2:178; end; hence thesis; end; then consider N3 such that A16: for n st n >= N3 holds n/2 > log(2,n)*log(2,n); set N = max( max(N1, 2), max( N2, N3 ) ); A17: N >= max(N1, 2) & N >= max( N2, N3 ) by XXREAL_0:25; A18: max( N2, N3 ) >= N2 & max( N2, N3 ) >= N3 by XXREAL_0:25; max(N1, 2) >= N1 & max(N1, 2) >= 2 by XXREAL_0:25; then A19: N >= N1 & N >= N2 & N >= N3 & N >= 2 by A17,A18,XXREAL_0:2; now let n; assume n >= N; then A20: n >= N1 & n >= N2 & n >= N3 & n >= 2 by A19,XXREAL_0:2; then A21: n/6 > 1 by A1; n/3 > 2*log(2,n) by A4,A20; then A22: n/6 + n/3 > 1 + 2*log(2,n) by A21,XREAL_1:10; A23: n/2 > log(2,n)*log(2,n) by A16,A20; A24: (n/6 + n/3) + n/2 = n; (1 + 2*log(2,n)) + log(2,n)*log(2,n) = (1 + log(2,n))^2; then A25: n > (1 + log(2,n))^2 by A22,A23,A24,XREAL_1:10; log(2,n) >= log(2,2) by A20,PRE_FF:12; then log(2,n) >= 1 by POWER:60; then A26: 1 + log(2,n) >= 1 + 0 by XREAL_1:9; sqrt n > sqrt((1 + log(2,n))^2) by A25,SQUARE_1:95,XREAL_1:65; then sqrt n > 1 + log(2,n) by A26,SQUARE_1:89; hence sqrt n - log(2,n) > 1 by XREAL_1:22; end; hence thesis; end; Lm39: (4+1)! = 120 proof (4+1)! = (4+1)*(4!) by NEWTON:21 .= 5*((3+1)*(3!)) by NEWTON:21 .= 5*(4*((2+1)*(2!))) by NEWTON:21 .= 120 by NEWTON:20; hence thesis; end; Lm40: for n st n >= 10 holds 2 to_power (2*n) / (n!) < 1/(2 to_power (n-9)) proof defpred P[Nat] means 2 to_power (2*$1) / ($1!) < 1/(2 to_power ($1-9)); A1: 7 = 8-1; A2: P[10] proof A3: 2 to_power (2*10) / (10!) = 2 to_power 20 / ((9+1)*(9!)) by NEWTON:21 .= 2 to_power (1+19) / (10*(9!)) .= ((2 to_power 1)*(2 to_power 19)) / (10*(9!)) by POWER:32 .= (2*(2 to_power 19)) / (2*(5*(9!))) by POWER:30 .= (2 to_power 19) / (5*(9!)) by XCMPLX_1:92 .= (2 to_power 19) / (5*((8+1)*(8!))) by NEWTON:21 .= (2 to_power 19) / ((5*9)*(8!)) .= (2 to_power 19) / (45*((7+1)*(7!))) by NEWTON:21 .= (2 to_power (3+16)) / (8*(45*(7!))) .= (8*(2 to_power 16)) / (8*(45*(7!))) by Lm8,POWER:32 .= (2 to_power 16) / (45*(7!)) by XCMPLX_1:92 .= (2 to_power (4+12)) / (45*((6+1)*(6!))) by NEWTON:21 .= ((2 to_power (3+1))*4096) / (45*((6+1)*(6!))) by Lm32,POWER:32 .= ((8*(2 to_power 1))*4096) / (45*((6+1)*(6!))) by Lm8,POWER:32 .= ((8*2)*4096) / (45*((6+1)*(6!))) by POWER:30 .= (16*4096) / ((45*7)*(6!)) .= (16*4096) / (315*((5+1)*(5!))) by NEWTON:21 .= 4096 / 14175 by Lm39; not 4096 / 14175 >= 1 / 2; hence thesis by A3,POWER:30; end; A4: for k be Nat st k >= 10 & P[k] holds P[k+1] proof let k be Nat; assume that A5: k >= 10 and A6: 2 to_power (2*k) / (k!) < 1/(2 to_power (k-9)); A7: (2 to_power 2) > 0 by POWER:39; (k+1)" > 0 by XREAL_1:124; then (2 to_power 2)*(k+1)" > 0*(k+1)" by A7,XREAL_1:70; then A8: ((2 to_power 2)/(k+1)) > 0 by XCMPLX_0:def 9; 2 to_power -(k-9) > 0 by POWER:39; then A9: (1/(2 to_power (k-9))) > 0 by POWER:33; 2 to_power (2*(k+1)) / ((k+1)!) = (2 to_power (2*k + 2*1)) / ((k+1)!) .= ((2 to_power (2*k))*(2 to_power 2)) / ((k+1)!) by POWER:32 .= ((2 to_power (2*k))*(2 to_power 2)) / ((k+1)*(k!)) by NEWTON:21 .= ((2 to_power 2)/(k+1))* ((2 to_power (2*k))/(k!)) by XCMPLX_1:77; then A10: 2 to_power (2*(k+1)) / ((k+1)!) < ((2 to_power 2)/(k+1))*(1/(2 to_power (k-9))) by A6,A8,XREAL_1:70; A11: 2 to_power 1 > 0 by POWER:39; now assume ((2 to_power 2)/(k+1)) >= (1/(2 to_power 1)); then (2 to_power 1)*((2 to_power 2)/(k+1)) >= (1/(2 to_power 1))*(2 to_power 1) by XREAL_1:66; then (2 to_power 1)*((2 to_power 2)*(k+1)") >= (1/(2 to_power 1))*(2 to_power 1) by XCMPLX_0:def 9; then ((2 to_power 1)*(2 to_power 2))*(k+1)" >= (1/(2 to_power 1))*(2 to_power 1); then (2 to_power (1+2))*(k+1)" >= (1/(2 to_power 1))*(2 to_power 1) by POWER:32; then 8/(k+1) >= (1/(2 to_power 1))*(2 to_power 1) by Lm8,XCMPLX_0:def 9; then 8/(k+1) >= 1 by A11,XCMPLX_1:107; then 8/(k+1)*(k+1) >= 1*(k+1) by XREAL_1:66; then 8 >= k+1 by XCMPLX_1:88; then 7 >= k by A1,XREAL_1:21; hence contradiction by A5,XXREAL_0:2; end; then ((2 to_power 2)/(k+1))*(1/(2 to_power (k-9))) < (1/(2 to_power 1))*(1/(2 to_power (k-9))) by A9,XREAL_1:70; then 2 to_power (2*(k+1)) / ((k+1)!) < (1/(2 to_power 1))*(1/(2 to_power (k-9))) by A10,XXREAL_0:2; then 2 to_power (2*(k+1)) / ((k+1)!) < (1/((2 to_power 1)*(2 to_power (k-9)))) by XCMPLX_1:103; then 2 to_power (2*(k+1)) / ((k+1)!) < (1/(2 to_power (1+(k+-9)))) by POWER:32; hence 2 to_power (2*(k+1)) / ((k+1)!) < (1/(2 to_power ((k+1)-9))); end; for n be Nat st n >= 10 holds P[n] from NAT_1:sch 8(A2, A4); hence thesis; end; Lm41: for n st n >= 3 holds 2*(n-2) >= n-1 proof defpred P[Nat] means 2*($1-2) >= $1-1; A1: P[3]; A2: for n be Nat st n >= 3 & P[n] holds P[n+1] proof let n be Nat; assume that n >= 3 and A3: 2*(n-2) >= n-1; 2*(n-2) + 2 >= (n+-1) +1 by A3,XREAL_1:9; hence 2*((n+1)-2) >= (n+1)-1; end; for n be Nat st n >= 3 holds P[n] from NAT_1:sch 8(A1, A2); hence thesis; end; Lm42: 5 to_power 5 = 3125 proof 5 to_power 5 = 5 to_power (4+1) .= (5 to_power 4)*(5 to_power 1) by POWER:32 .= (5 to_power (3+1))*5 by POWER:30 .= ((5 to_power 3)*(5 to_power 1))*5 by POWER:32 .= ((5 to_power (2+1))*5)*5 by POWER:30 .= (((5 to_power 2)*(5 to_power 1))*5)*5 by POWER:32 .= (((5 to_power (1+1))*5)*5)*5 by POWER:30 .= ((((5 to_power 1)*(5 to_power 1))*5)*5)*5 by POWER:32 .= ((((5 to_power 1)*5)*5)*5)*5 by POWER:30 .= (((5*5)*5)*5)*5 by POWER:30 .= 3125; hence thesis; end; Lm43: 4 to_power 4 = 256 proof 4 to_power 4 = 4 to_power (3+1) .= (4 to_power 3)*(4 to_power 1) by POWER:32 .= (4 to_power (2+1))*4 by POWER:30 .= ((4 to_power 2)*(4 to_power 1))*4 by POWER:32 .= ((4 to_power (1+1))*4)*4 by POWER:30 .= (((4 to_power 1)*(4 to_power 1))*4)*4 by POWER:32 .= (((4 to_power 1)*4)*4)*4 by POWER:30 .= ((4*4)*4)*4 by POWER:30 .= 256; hence thesis; end; Lm44: for a,b,d,e being Real holds (a/b) / (d/e) = (a/d) * (e/b) proof let a,b,d,e be Real; thus (a/b) / (d/e) = (a*e)/(b*d) by XCMPLX_1:85 .= (a/d) * (e/b) by XCMPLX_1:77; end; Lm45: for x being real number st x>=0 holds sqrt x = x to_power (1/2) proof let x be real number; assume A1: x >= 0; per cases by A1; suppose x = 0; hence thesis by POWER:def 2,SQUARE_1:82; end; suppose A2: x > 0; A3: (x to_power (1/2))^2=(x to_power (1/2)) to_power 2 by POWER:53 .=x to_power ((1/2)*2) by A2,POWER:38 .=x by POWER:30; x to_power (1/2)>0 by A2,POWER:39; hence thesis by A3,SQUARE_1:89; end; end; Lm46: ex N st for n st n >= N holds n - sqrt n*log(2,n) > n/2 proof set seq = seq_logn; set seq1 = seq_n^(1/2); set p = seq /" seq1; p is convergent & lim p = 0 by Lm16; then consider N such that A1: for n st n >= N holds abs(p.n-0) < 1/2 by SEQ_2:def 7; set N1 = max(2, N); A2: N1 >= 2 & N1 >= N by XXREAL_0:25; now let n; assume A3: n >= N1; then n >= 2 & n >= N by A2,XXREAL_0:2; then A4: abs(p.n-0) < 1/2 by A1; A5: p.n = seq.n / seq1.n by Lm4 .= log(2,n) / seq1.n by A2,A3,Def2 .= log(2,n) / (n to_power (1/2)) by A2,A3,Def3 .= log(2,n) / sqrt n by Lm45; A6: sqrt n > 0 by A2,A3,SQUARE_1:93; A7: p.n < 1/2 by A4,ABSVALUE:def 1; A8: sqrt n <> 0 by A2,A3,SQUARE_1:93; log(2,n) / sqrt n * sqrt n < sqrt n * (1/2) by A5,A6,A7,XREAL_1:70; then log(2,n) < sqrt n * (1/2) by A8,XCMPLX_1:88; then sqrt n*log(2,n) < sqrt n * (sqrt n * (1/2)) by A6,XREAL_1:70; then sqrt n*log(2,n) < ((sqrt n)^2) * (1/2); then sqrt n*log(2,n) < n * (1/2) by SQUARE_1:def 4; then n/2 + sqrt n*log(2,n) < n/2 + n/2 by XREAL_1:8; hence n/2 < n - sqrt n*log(2,n) by XREAL_1:22; end; hence thesis; end; Lm47: for s being Real_Sequence st for n holds s.n = (1 + 1/(n+1)) to_power (n+1) holds s is non-decreasing proof let s be Real_Sequence such that A1: for n holds s.n = (1 + 1/(n+1)) to_power (n+1); now let n; A2: (1+1/(n+1)) to_power (n+1) > 0 by POWER:39; A3: s.(n+1)/s.n =(1 + 1/(n+1+1)) to_power (n+1+1) / s.n by A1 .=(1 + 1/(n+1+1)) to_power (n+1+1)/(1+1/(n+1)) to_power (n+1)*1 by A1 .=(1 + 1/(n+1+1)) to_power (n+1+1)/(1 + 1/(n+1)) to_power (n+1) * ((1+1/(n+1))/(1+1/(n+1))) by XCMPLX_1:60 .=(1+1/(n+1)) * (1 + 1/(n+1+1)) to_power (n+1+1) / ((1 + 1/(n+1)) to_power (n+1) * (1+1/(n+1))) by XCMPLX_1:77 .=(1+1/(n+1)) * (1 + 1/(n+1+1)) to_power (n+1+1) / ((1 + 1/(n+1)) to_power (n+1) * (1+1/(n+1)) to_power 1) by POWER:30 .=(1+1/(n+1)) * (1 + 1/(n+1+1)) to_power (n+1+1) / (1 + 1/(n+1)) to_power (n+1+1) by POWER:32 .=(1+1/(n+1)) * ((1 + 1/(n+1+1)) to_power (n+1+1) / (1 + 1/(n+1)) to_power (n+1+1)) by XCMPLX_1:75 .=(1+1/(n+1)) * ((1 + 1/(n+1+1))/(1 + 1/(n+1))) to_power (n+1+1) by POWER:36; A4: (1 + 1/(n+1+1))/(1 + 1/(n+1)) = ((1*(n+1+1) + 1)/(n+1+1))/(1 + 1/(n+1)) by XCMPLX_1:114 .= ((n+1+1+1)/(n+1+1))/((1*(n+1) + 1)/(n+1)) by XCMPLX_1:114 .= ((n+(1+1)+1)*(n+1))/((n+2)*(n+2)) by XCMPLX_1:85 .= (n*n+n*2+2*n+3+1-1)/((n+2)*(n+2)) .= ((n+2)*(n+2))/((n+2)*(n+2)) - 1/((n+2)*(n+2)) by XCMPLX_1:121 .= 1 - 1/((n+2)*(n+2)) by XCMPLX_1:6,60; n+1+1>0+1 by XREAL_1:8; then (n+2)*(n+2)>1 by REAL_2:137; then 1/((n+2)*(n+2))<1 by SQUARE_1:2; then - 1/((n+2)*(n+2)) > -1 by XREAL_1:26; then (1 + -1/((n+2)*(n+2))) to_power (n+1+1) >= 1 + (n+1+1)*(-1/((n+2)*(n+2) )) by POWER:56; then (1 - 1/((n+2)*(n+2))) to_power (n+1+1) >= 1 - (n+2)*(1/((n+2)*(n+2))); then (1 - 1/((n+2)*(n+2))) to_power (n+1+1) >= 1 - (n+2)*1/((n+2)*(n+2)) by XCMPLX_1:75; then (1 - 1/((n+2)*(n+2))) to_power (n+1+1) >= 1 - ((n+2)/(n+2)*1)/(n+2) by XCMPLX_1:84; then (1 - 1/((n+2)*(n+2))) to_power (n+1+1) >= 1 - (1*1)/(n+2) by XCMPLX_1:60; then s.(n+1)/s.n >= (1 + 1/(n+1)) * (1 - 1/(n+2)) by A3,A4,XREAL_1:66; then s.(n+1)/s.n >= ((1*(n+1) + 1)/(n+1)) * (1 - 1/(n+2)) by XCMPLX_1:114; then s.(n+1)/s.n >= ((n+2)/(n+1)) * ((1*(n+2) - 1)/(n+2)) by XCMPLX_1:128; then s.(n+1)/s.n >= ((n+1)*(n+2))/((n+1)*(n+2)) by XCMPLX_1:77; then A5: s.(n+1)/s.n >= 1 by XCMPLX_1:6,60; s.n>0 by A1,A2; hence s.(n+1)>=s.n by A5,REAL_2:118; end; hence thesis by SEQM_3:def 13; end; Lm48: for n st n >= 1 holds ((n+1)/n) to_power n <= ((n+2)/(n+1)) to_power (n+1) proof let n; assume A1: n >= 1; deffunc F(Element of NAT) = (1 + 1/($1+1)) to_power ($1+1); consider seq being Real_Sequence such that A2: for n holds seq.n = F(n)from SEQ_1:sch 1; A3: seq is non-decreasing by A2,Lm47; n >= 0+1 by A1; then n-1 >= 0 by XREAL_1:21; then reconsider m = n-1 as Element of NAT by INT_1:16; seq.m <= seq.(m+1) by A3,SEQM_3:def 13; then (1 + 1/(m+1)) to_power (m+1) <= seq.(m+1) by A2; then (1 + 1/n) to_power n <= (1 + 1/(n+1)) to_power (n+1) by A2; then (n/n + 1/n) to_power n <= (1 + 1/(n+1)) to_power (n+1) by A1,XCMPLX_1:60; then ((n+1)/n) to_power n <= (1 + 1/(n+1)) to_power (n+1) by XCMPLX_1:63; then ((n+1)/n) to_power n <= ((n+1)/(n+1) + 1/(n+1)) to_power (n+1) by XCMPLX_1:60; then ((n+1)/n) to_power n <= (((n+1)+1)/(n+1)) to_power (n+1) by XCMPLX_1:63; hence ((n+1)/n) to_power n <= ((n+2)/(n+1)) to_power (n+1); end; theorem :: (Part 1, O(n^logn) c O(n^sqrt n)) for f,g being Real_Sequence st (f.0 = 0 & (for n st n > 0 holds f.n = (n to_power log(2,n)))) & (g.0 = 0 & (for n st n > 0 holds g.n = (n to_power sqrt n))) holds ex s,s1 being eventually-positive Real_Sequence st s = f & s1 = g & Big_Oh(s) c= Big_Oh(s1) & not Big_Oh(s) = Big_Oh(s1) proof let f,g be Real_Sequence such that A1: (f.0 = 0 & (for n st n > 0 holds f.n = (n to_power log(2,n)))) and A2: (g.0 = 0 & (for n st n > 0 holds g.n = (n to_power sqrt n))); set h = f/"g; f is eventually-positive proof take 1; let n; assume A3: n >= 1; then f.n = n to_power log(2,n) by A1; hence f.n > 0 by A3,POWER:39; end; then reconsider f as eventually-positive Real_Sequence; g is eventually-positive proof take 1; let n; assume A4: n >= 1; then g.n = n to_power sqrt n by A2; hence g.n > 0 by A4,POWER:39; end; then reconsider g as eventually-positive Real_Sequence; take f,g; consider N such that A5: for n st n >= N holds sqrt n - log(2, n) > 1 by Lm38; A6: now let p be real number such that A7: p > 0; set N1 = max( N, max([/1/p\], 2) ); A8: N1 >= N & N1 >= max([/1/p\], 2) by XXREAL_0:25; A9: max([/1/p\], 2) >= [/1/p\] & max([/1/p\], 2) >= 2 by XXREAL_0:25; then A10: N1 >= [/1/p\] & N1 >= 2 by A8,XXREAL_0:2; then A11: N1 > 1 by XXREAL_0:2; N1 is Integer proof per cases by XXREAL_0:16; suppose N1 = N; hence thesis; end; suppose N1 = max([/1/p\], 2); hence thesis by XXREAL_0:16; end; end; then reconsider N1 as Element of NAT by A8,INT_1:16; take N1; let n; assume A12: n >= N1; p" > 0 by A7,XREAL_1:124; then A13: 1/p > 0 by XCMPLX_1:217; [/1/p\] >= 1/p by INT_1:def 5; then A14: N1 >= 1/p by A10,XXREAL_0:2; A15: n > 1 by A11,A12,XXREAL_0:2; A16: h.n = f.n/g.n by Lm4; f.n = n to_power log(2,n) by A1,A8,A9,A12; then A17: h.n = (n to_power log(2,n)) / (n to_power sqrt n) by A2,A8,A9,A12,A16 .= n to_power (log(2,n) - sqrt n) by A8,A9,A12,POWER:34 .= n to_power -(sqrt n - log(2,n)); n >= N by A8,A12,XXREAL_0:2; then sqrt n - log(2, n) > 1 by A5; then (-1)*(sqrt n - log(2, n)) < (-1)*1 by XREAL_1:71; then A18: n to_power -(sqrt n - log(2,n)) < n to_power -1 by A15,POWER:44; A19: n to_power -1 = 1/(n to_power 1) by A8,A9,A12,POWER:33 .= 1/n by POWER:30; n >= 1/p by A12,A14,XXREAL_0:2; then 1/n <= 1/(1/p) by A13,REAL_2:152; then n to_power -1 <= p by A19,XCMPLX_1:56; then A20: h.n < p by A17,A18,XXREAL_0:2; h.n > 0 by A8,A9,A12,A17,POWER:39; hence abs(h.n-0) < p by A20,ABSVALUE:def 1; end; then A21: h is convergent by SEQ_2:def 6; then lim h = 0 by A6,SEQ_2:def 7; then f in Big_Oh(g) & not g in Big_Oh(f) by A21,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^sqrt n) c O(2^n)) for f being Real_Sequence st (f.0 = 0 & (for n st n > 0 holds f.n = (n to_power sqrt n))) holds ex s,s1 being eventually-positive Real_Sequence st s = f & s1 = seq_a^(2,1,0) & Big_Oh(s) c= Big_Oh(s1) & not Big_Oh(s) = Big_Oh(s1) proof let f be Real_Sequence such that A1: (f.0 = 0 & (for n st n > 0 holds f.n = (n to_power sqrt n))); set g = seq_a^(2,1,0); set h = f/"g; f is eventually-positive proof take 1; let n; assume A2: n >= 1; then f.n = n to_power sqrt n by A1; hence f.n > 0 by A2,POWER:39; end; then reconsider f as eventually-positive Real_Sequence; reconsider g as eventually-positive Real_Sequence; take f,g; consider N such that A3: for n st n >= N holds n - sqrt n*log(2,n) > n/2 by Lm46; A4: now let p be real number; assume p > 0; then p" > 0 by XREAL_1:124; then A5: 1/p > 0 by XCMPLX_1:217; set N1 = max( N, max(2*[/log(2,1/p)\], 2) ); A6: N1 >= N & N1 >= max(2*[/log(2,1/p)\], 2) by XXREAL_0:25; A7: max(2*[/log(2,1/p)\], 2) >= 2*[/log(2,1/p)\] & max(2*[/log(2,1/p)\], 2) >= 2 by XXREAL_0:25; then A8: N1 >= 2*[/log(2,1/p)\] & N1 >= 2 by A6,XXREAL_0:2; N1 is Integer proof per cases by XXREAL_0:16; suppose N1 = N; hence thesis; end; suppose N1 = max(2*[/log(2,1/p)\], 2); hence thesis by XXREAL_0:16; end; end; then reconsider N1 as Element of NAT by A6,INT_1:16; take N1; let n; assume A9: n >= N1; A10: h.n = f.n/g.n by Lm4; A11: f.n = n to_power sqrt n by A1,A6,A7,A9 .= 2 to_power (sqrt n*log(2,n)) by A6,A7,A9,Lm3; g.n = 2 to_power (1*n+0) by Def1 .= 2 to_power n; then A12: h.n = 2 to_power ((sqrt n*log(2,n)) - n) by A10,A11,POWER:34 .= 2 to_power -(n - sqrt n*log(2,n)); n >= N by A6,A9,XXREAL_0:2; then n - sqrt n*log(2,n) > n/2 by A3; then -(n - sqrt n*log(2,n)) < -(n/2) by XREAL_1:26; then A13: 2 to_power -(n - sqrt n*log(2,n)) < 2 to_power -(n/2) by POWER:44; A14: [/log(2,1/p)\] >= log(2,1/p) by INT_1:def 5; n >= 2*[/log(2,1/p)\] by A8,A9,XXREAL_0:2; then n/2 >= [/log(2,1/p)\] by REAL_2:177; then n/2 >= log(2,1/p) by A14,XXREAL_0:2; then -(n/2) <= -log(2,1/p) by XREAL_1:26; then 2 to_power -(n/2) <= 2 to_power -log(2,1/p) by PRE_FF:10; then 2 to_power -(n/2) <= 1/(2 to_power log(2,1/p)) by POWER:33; then 2 to_power -(n/2) <= 1/(1/p) by A5,POWER:def 3; then 2 to_power -(n/2) <= p by XCMPLX_1:56; then A15: h.n < p by A12,A13,XXREAL_0:2; h.n > 0 by A12,POWER:39; hence abs(h.n-0) < p by A15,ABSVALUE:def 1; end; then A16: h is convergent by SEQ_2:def 6; then lim h = 0 by A4,SEQ_2:def 7; then f in Big_Oh(g) & not g in Big_Oh(f) by A16,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(2^n+1) = O(2^n)) ex s, s1 being eventually-positive Real_Sequence st s = seq_a^(2,1,0) & s1 = seq_a^(2,1,1) & Big_Oh(s) = Big_Oh(s1) proof set f = seq_a^(2,1,0); set g = seq_a^(2,1,1); set h = f/"g; reconsider f as eventually-positive Real_Sequence; reconsider g as eventually-positive Real_Sequence; take f,g; thus f = seq_a^(2,1,0) & g = seq_a^(2,1,1); A1: 2" > 0; A2: for n holds h.n = 2" proof now let n; A3: f.n = 2 to_power (1*n + 0) by Def1; A4: g.n = 2 to_power (1*n + 1) by Def1; h.n = (2 to_power n)/g.n by A3,Lm4 .= 2 to_power (n-(n+1)) by A4,POWER:34 .= 2 to_power (0+-1) .= 1 / 2 to_power 1 by POWER:33 .= 1 / 2 by POWER:30 .= 2"; hence h.n = 2"; end; hence thesis; end; A5: now let p be real number such that A6: p > 0; take N = 0; let n; assume n >= N; abs(h.n-2") = abs(2"-2") by A2 .= 0 by ABSVALUE:7; hence abs(h.n-2") < p by A6; end; then A7: h is convergent by SEQ_2:def 6; then lim h > 0 by A1,A5,SEQ_2:def 7; hence thesis by A7,ASYMPT_0:15; end; theorem :: (Part 4, O(2^n) c O(2^2n)) ex s, s1 being eventually-positive Real_Sequence st s = seq_a^(2,1,0) & s1 = seq_a^(2,2,0) & Big_Oh(s) c= Big_Oh(s1) & not Big_Oh(s) = Big_Oh(s1) proof reconsider f = seq_a^(2,1,0) as eventually-positive Real_Sequence; reconsider g = seq_a^(2,2,0) as eventually-positive Real_Sequence; take f,g; thus f = seq_a^(2,1,0) & g = seq_a^(2,2,0); set h = f/"g; A1: for n holds h.n = (2 to_power -n) proof let n; h.n = f.n/g.n by Lm4 .= (2 to_power (1*n+0))/g.n by Def1 .= (2 to_power (1*n))/(2 to_power (2*n+0)) by Def1 .= 2 to_power (1*n-(2*n)) by POWER:34 .= 2 to_power -n; hence h.n = (2 to_power -n); end; A2: now let p be real number; assume A3: p > 0; then p" > 0 by XREAL_1:124; then A4: 1/p > 0 by XCMPLX_1:217; set N = max(1,[/log(2,1/p)\] + 1); A5: N >= 1 & N >= ([/log(2,1/p)\] + 1) by XXREAL_0:25; N is Integer by XXREAL_0:16; then reconsider N as Element of NAT by A5,INT_1:16; take N; let n; assume A6: n >= N; A7: abs(h.n-0) = abs((2 to_power -n)) by A1; (2 to_power -n) > 0 by POWER:39; then A8: abs(h.n-0) = (2 to_power -n) by A7,ABSVALUE:def 1; A9: 2 to_power n >= 2 to_power N by A6,PRE_FF:10; A10: 2 to_power N >= 2 to_power ([/log(2,1/p)\] + 1) by PRE_FF:10,XXREAL_0:25; A11: [/log(2,1/p)\] + 1 > [/log(2,1/p)\] by XREAL_1:31; [/log(2,1/p)\] >= log(2,1/p) by INT_1:def 5; then [/log(2,1/p)\] + 1 > log(2,1/p) by A11,XXREAL_0:2; then 2 to_power ([/log(2,1/p)\]+1) > 2 to_power log(2,1/p) by POWER:44; then 2 to_power N > 2 to_power log(2,1/p) by A10,XXREAL_0:2; then 2 to_power n > 2 to_power log(2,1/p) by A9,XXREAL_0:2; then 2 to_power n > 1/p by A4,POWER:def 3; then (2 to_power n)*p > 1/p*p by A3,XREAL_1:70; then A12: p*(2 to_power n) > 1 by A3,XCMPLX_1:88; 2 to_power n > 0 by POWER:39; then (2 to_power n)" > 0 by XREAL_1:124; then (p*(2 to_power n))*(2 to_power n)" > 1*(2 to_power n)" by A12,XREAL_1:70; then A13: p*((2 to_power n)*(2 to_power n)") > (2 to_power n)"; 2 to_power n <> 0 by POWER:39; then p*1 > (2 to_power n)" by A13,XCMPLX_0:def 7; then p > 1/(2 to_power n) by XCMPLX_1:217; hence abs(h.n-0) < p by A8,POWER:33; end; then A14: h is convergent by SEQ_2:def 6; then lim h = 0 by A2,SEQ_2:def 7; then f in Big_Oh(g) & not g in Big_Oh(f) by A14,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 5, O(2^2n) c O(n!)) ex s being eventually-positive Real_Sequence st s = seq_a^(2,2,0) & Big_Oh(s) c= Big_Oh(seq_n!(0)) & not Big_Oh(s) = Big_Oh(seq_n!(0)) proof set g = seq_n!(0); reconsider f = seq_a^(2,2,0)as eventually-positive Real_Sequence; take f; thus f = seq_a^(2,2,0); set h = f/"g; A1: now let p be real number; assume p > 0; then p" > 0 by XREAL_1:124; then A2: 1/p > 0 by XCMPLX_1:217; set N = max(10,[/9+log(2,1/p)\]); A3: N >= 10 & N >= [/9+log(2,1/p)\] by XXREAL_0:25; N is Integer by XXREAL_0:16; then reconsider N as Element of NAT by A3,INT_1:16; take N; let n; assume n >= N; then A4: n >= 10 & n >= [/9+log(2,1/p)\] by A3,XXREAL_0:2; A5: h.n = f.n/g.n by Lm4 .= (2 to_power (2*n+0)) / g.n by Def1 .= (2 to_power (2*n+0)) / ((n+0)!) by Def5 .= (2 to_power (2*n)) / (n!); then A6: h.n < 1 / (2 to_power (n-9)) by A4,Lm40; [/9+log(2,1/p)\] >= 9+log(2,1/p) by INT_1:def 5; then n >= 9+log(2,1/p) by A4,XXREAL_0:2; then n-9 >= log(2,1/p) by XREAL_1:21; then 2 to_power (n-9) >= 2 to_power log(2,1/p) by PRE_FF:10; then 2 to_power (n-9) >= 1/p by A2,POWER:def 3; then 1 / (2 to_power (n-9)) <= 1/(1/p) by A2,REAL_2:152; then 1 / (2 to_power (n-9)) <= p by XCMPLX_1:56; then h.n < p by A6,XXREAL_0:2; hence abs(h.n-0) < p by A5,ABSVALUE:def 1; end; then A7: h is convergent by SEQ_2:def 6; then lim h = 0 by A1,SEQ_2:def 7; then f in Big_Oh(g) & not g in Big_Oh(f) by A7,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 6, O(n!) c O((n+1)!)) Big_Oh(seq_n!(0)) c= Big_Oh(seq_n!(1)) & not Big_Oh(seq_n!(0)) = Big_Oh(seq_n!(1)) proof set f = seq_n!(0); set g = seq_n!(1); set h = f/"g; A1: for n holds h.n = 1/(n+1) proof let n; A2: n! <> 0 by NEWTON:23; h.n = f.n/g.n by Lm4 .= (n+0)!/g.n by Def5 .= (n!)/((n+1)!) by Def5 .= ((n!)*1)/((n+1)*(n!)) by NEWTON:21 .= (1/(n+1))*((n!)/(n!)) by XCMPLX_1:77 .= (1/(n+1))*1 by A2,XCMPLX_1:60; hence h.n = 1/(n+1); end; A3: now let p be real number; assume A4: p > 0; then p" > 0 by XREAL_1:124; then A5: 1/p > 0 by XCMPLX_1:217; set N = max( 1, [/1/p\] ); A6: N >= 1 & N >= ([/1/p\]) by XXREAL_0:25; N is Integer by XXREAL_0:16; then reconsider N as Element of NAT by A6,INT_1:16; take N; let n; assume n >= N; then A7: n+1 > N by NAT_1:13; A8: -p < -0 by A4,XREAL_1:26; 0 < (n+1)" by XREAL_1:124; then 0 < 1/(n+1) by XCMPLX_1:217; then A9: -p < h.n by A1,A8; [/1/p\] >= 1/p by INT_1:def 5; then N >= 1/p by A6,XXREAL_0:2; then (n+1) > 1/p by A7,XXREAL_0:2; then 1/(n+1) < 1/(1/p) by A5,REAL_2:151; then 1/(n+1) < p by XCMPLX_1:56; then A10: h.n < p by A1; abs(h.n) < p proof per cases; suppose h.n >= 0; hence thesis by A10,ABSVALUE:def 1; end; suppose h.n < 0; then A11: abs(h.n) = -h.n by ABSVALUE:def 1; (-1)*(-p) > (-1)*h.n by A9,XREAL_1:71; hence thesis by A11; end; end; hence abs(h.n-0) < p; end; then A12: h is convergent by SEQ_2:def 6; then lim h = 0 by A3,SEQ_2:def 7; then f in Big_Oh(g) & not g in Big_Oh(f) by A12,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 7, O((n+1)!) c O(n^n)) for g