:: Asymptotic notation. Part II: Examples and Problems :: by Richard Krueger, Piotr Rudnicki and Paul Shelley :: :: Received November 4, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin Lm1: for n being Nat st n >= 2 holds 2 to_power n > n + 1 proofend; theorem :: ASYMPT_1:1 for t, t1 being Real_Sequence st t . 0 = 0 & ( for n being Element of NAT st n > 0 holds t . n = ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 ) & ( for n being Element of NAT st n > 0 holds t1 . n = (n to_power 3) * (log (2,n)) ) holds ex s, s1 being eventually-positive Real_Sequence st ( s = t & s1 = t1 & s in Big_Oh s1 ) proofend; Lm2: for a being logbase Real for f being Real_Sequence st a > 1 & ( for n being Element of NAT st n > 0 holds f . n = log (a,n) ) holds f is eventually-positive proofend; theorem :: ASYMPT_1:2 for a, b being logbase Real for f, g being Real_Sequence st a > 1 & b > 1 & ( for n being Element of NAT st n > 0 holds f . n = log (a,n) ) & ( for n being Element of NAT 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 ) proofend; definition let a, b, c be Real; func seq_a^ (a,b,c) -> Real_Sequence means :Def1: :: ASYMPT_1:def 1 for n being Element of NAT holds it . n = a to_power ((b * n) + c); existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = a to_power ((b * n) + c) proofend; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = a to_power ((b * n) + c) ) & ( for n being Element of NAT holds b2 . n = a to_power ((b * n) + c) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines seq_a^ ASYMPT_1:def_1_:_ for a, b, c being Real for b4 being Real_Sequence holds ( b4 = seq_a^ (a,b,c) iff for n being Element of NAT holds b4 . n = a to_power ((b * n) + c) ); registration let a be positive Real; let b, c be Real; cluster seq_a^ (a,b,c) -> eventually-positive ; coherence seq_a^ (a,b,c) is eventually-positive proofend; 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))) proofend; theorem :: ASYMPT_1:3 for a, b being positive Real st a < b holds not seq_a^ (b,1,0) in Big_Oh (seq_a^ (a,1,0)) proofend; :: Example p. 84 definition func seq_logn -> Real_Sequence means :Def2: :: ASYMPT_1:def 2 ( it . 0 = 0 & ( for n being Element of NAT st n > 0 holds it . n = log (2,n) ) ); existence ex b1 being Real_Sequence st ( b1 . 0 = 0 & ( for n being Element of NAT st n > 0 holds b1 . n = log (2,n) ) ) proofend; uniqueness for b1, b2 being Real_Sequence st b1 . 0 = 0 & ( for n being Element of NAT st n > 0 holds b1 . n = log (2,n) ) & b2 . 0 = 0 & ( for n being Element of NAT st n > 0 holds b2 . n = log (2,n) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines seq_logn ASYMPT_1:def_2_:_ for b1 being Real_Sequence holds ( b1 = seq_logn iff ( b1 . 0 = 0 & ( for n being Element of NAT st n > 0 holds b1 . n = log (2,n) ) ) ); definition let a be Real; func seq_n^ a -> Real_Sequence means :Def3: :: ASYMPT_1:def 3 ( it . 0 = 0 & ( for n being Element of NAT st n > 0 holds it . n = n to_power a ) ); existence ex b1 being Real_Sequence st ( b1 . 0 = 0 & ( for n being Element of NAT st n > 0 holds b1 . n = n to_power a ) ) proofend; uniqueness for b1, b2 being Real_Sequence st b1 . 0 = 0 & ( for n being Element of NAT st n > 0 holds b1 . n = n to_power a ) & b2 . 0 = 0 & ( for n being Element of NAT st n > 0 holds b2 . n = n to_power a ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines seq_n^ ASYMPT_1:def_3_:_ for a being Real for b2 being Real_Sequence holds ( b2 = seq_n^ a iff ( b2 . 0 = 0 & ( for n being Element of NAT st n > 0 holds b2 . n = n to_power a ) ) ); registration cluster seq_logn -> eventually-positive ; coherence seq_logn is eventually-positive proofend; end; registration let a be Real; cluster seq_n^ a -> eventually-positive ; coherence seq_n^ a is eventually-positive proofend; end; Lm4: for f, g being Real_Sequence for n being Element of NAT holds (f /" g) . n = (f . n) / (g . n) proofend; 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 ) proofend; theorem Th4: :: ASYMPT_1:4 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 ) ) proofend; Lm6: for a, b, c being real number st 0 < a & a <= b & c >= 0 holds a to_power c <= b to_power c proofend; Lm7: for n being Nat st n >= 4 holds (2 * n) + 3 < 2 to_power n proofend; Lm8: for n being Element of NAT st n >= 6 holds (n + 1) ^2 < 2 to_power n proofend; Lm9: for c being Real st c > 6 holds c ^2 < 2 to_power c proofend; Lm10: for e being positive Real for f being Real_Sequence st ( for n being Element of NAT 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 ) proofend; Lm11: for e being Real st e > 0 holds ( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 ) proofend; theorem Th5: :: ASYMPT_1:5 ( Big_Oh seq_logn c= Big_Oh (seq_n^ (1 / 2)) & not Big_Oh seq_logn = Big_Oh (seq_n^ (1 / 2)) ) proofend; :: Example p. 86 theorem :: ASYMPT_1:6 ( seq_n^ (1 / 2) in Big_Omega seq_logn & not seq_logn in Big_Omega (seq_n^ (1 / 2)) ) proofend; Lm12: for f being Real_Sequence for N being Element of NAT st ( for n being Element of NAT st n <= N holds f . n >= 0 ) holds Sum (f,N) >= 0 proofend; Lm13: for f, g being Real_Sequence for N being Element of NAT st ( for n being Element of NAT st n <= N holds f . n <= g . n ) holds Sum (f,N) <= Sum (g,N) proofend; Lm14: for f being Real_Sequence for b being Real st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds f . n = b ) holds for N being Element of NAT holds Sum (f,N) = b * N proofend; Lm15: for f being Real_Sequence for N, M being Nat holds (Sum (f,N,M)) + (f . (N + 1)) = Sum (f,(N + 1),M) proofend; Lm16: for f, g being Real_Sequence for M, N being Element of NAT st N >= M + 1 & ( for n being Element of NAT st M + 1 <= n & n <= N holds f . n <= g . n ) holds Sum (f,N,M) <= Sum (g,N,M) proofend; Lm17: for n being Element of NAT holds [/(n / 2)\] <= n proofend; Lm18: for f being Real_Sequence for b being Real for N being Element of NAT st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds f . n = b ) holds for M being Element of NAT holds Sum (f,N,M) = b * (N - M) proofend; theorem :: ASYMPT_1:7 for f being Real_Sequence for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds f in Big_Theta (seq_n^ (k + 1)) proofend; :: Example p. 89 theorem :: ASYMPT_1:8 for f being Real_Sequence st ( for n being Element of NAT 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 ) proofend; :: Example p. 92 definition let b be Real; func seq_const b -> Real_Sequence equals :: ASYMPT_1:def 4 NAT --> b; coherence NAT --> b is Real_Sequence ; end; :: deftheorem defines seq_const ASYMPT_1:def_4_:_ for b being Real holds seq_const b = NAT --> b; registration cluster seq_const 1 -> eventually-nonnegative ; coherence seq_const 1 is eventually-nonnegative proofend; end; Lm19: for a, b, c being Real st a > 1 & b >= a & c >= 1 holds log (a,c) >= log (b,c) proofend; theorem Th9: :: ASYMPT_1:9 for f being eventually-nonnegative Real_Sequence ex F being FUNCTION_DOMAIN of NAT , REAL st ( F = {(seq_n^ 1)} & ( f in F to_power (Big_Oh (seq_const 1)) implies ex N being Element of NAT ex c being Real ex k being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( 1 <= f . n & f . n <= c * ((seq_n^ k) . n) ) ) ) ) & ( ex N being Element of NAT ex c being Real ex k being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( 1 <= f . n & f . n <= c * ((seq_n^ k) . n) ) ) ) implies f in F to_power (Big_Oh (seq_const 1)) ) ) proofend; begin theorem :: ASYMPT_1:10 for f being Real_Sequence st ( for n being Element of NAT 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) proofend; begin theorem :: ASYMPT_1:11 seq_n^ 2 in Big_Oh (seq_n^ 3) proofend; theorem :: ASYMPT_1:12 not seq_n^ 2 in Big_Omega (seq_n^ 3) proofend; theorem :: ASYMPT_1:13 ex s being eventually-positive Real_Sequence st ( s = seq_a^ (2,1,1) & seq_a^ (2,1,0) in Big_Theta s ) proofend; definition let a be Element of NAT ; func seq_n! a -> Real_Sequence means :Def5: :: ASYMPT_1:def 5 for n being Element of NAT holds it . n = (n + a) ! ; existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = (n + a) ! proofend; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (n + a) ! ) & ( for n being Element of NAT holds b2 . n = (n + a) ! ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines seq_n! ASYMPT_1:def_5_:_ for a being Element of NAT for b2 being Real_Sequence holds ( b2 = seq_n! a iff for n being Element of NAT holds b2 . n = (n + a) ! ); registration let a be Element of NAT ; cluster seq_n! a -> eventually-positive ; coherence seq_n! a is eventually-positive proofend; end; theorem :: ASYMPT_1:14 not seq_n! 0 in Big_Theta (seq_n! 1) proofend; begin Lm20: now__::_thesis:_for_a,_b,_c,_d_being_Real_st_0_<=_b_&_a_<=_b_&_0_<=_c_&_c_<=_d_holds_ a_*_c_<=_b_*_d let a, b, c, d be Real; ::_thesis: ( 0 <= b & a <= b & 0 <= c & c <= d implies a * c <= b * d ) assume that A1: 0 <= b and A2: a <= b and A3: 0 <= c and A4: c <= d ; ::_thesis: a * c <= b * d A5: b * c <= b * d by A1, A4, XREAL_1:64; a * c <= b * c by A2, A3, XREAL_1:64; hence a * c <= b * d by A5, XXREAL_0:2; ::_thesis: verum end; theorem :: ASYMPT_1:15 for f being Real_Sequence st f in Big_Oh (seq_n^ 1) holds f (#) f in Big_Oh (seq_n^ 2) proofend; begin theorem :: ASYMPT_1:16 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 ) proofend; begin theorem :: ASYMPT_1:17 ( 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)) ) ) proofend; begin theorem :: ASYMPT_1:18 for f, g being Real_Sequence st ( for n being Element of NAT holds f . n = n mod 2 ) & ( for n being Element of NAT 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 ) proofend; begin theorem :: ASYMPT_1:19 for f, g being eventually-nonnegative Real_Sequence holds ( Big_Oh f = Big_Oh g iff f in Big_Theta g ) proofend; theorem :: ASYMPT_1:20 for f, g being eventually-nonnegative Real_Sequence holds ( f in Big_Theta g iff Big_Theta f = Big_Theta g ) proofend; begin Lm21: for n being Element of NAT holds ((n ^2) - n) + 1 > 0 proofend; Lm22: for f, g being Real_Sequence for N being Element of NAT for c being Real st f is convergent & lim f = c & ( for n being Element of NAT st n >= N holds f . n = g . n ) holds ( g is convergent & lim g = c ) proofend; Lm23: for n being Element of NAT st n >= 1 holds ((n ^2) - n) + 1 <= n ^2 proofend; Lm24: for n being Element of NAT st n >= 1 holds n ^2 <= 2 * (((n ^2) - n) + 1) proofend; Lm25: for e being Real st 0 < e & e < 1 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds (n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) proofend; theorem :: ASYMPT_1:21 for e being Real for f being Real_Sequence st 0 < e & ( for n being Element of NAT 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)) ) proofend; theorem :: ASYMPT_1:22 for e being Real for g being Real_Sequence st e < 1 & ( for n being Element of NAT 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 ) proofend; theorem :: ASYMPT_1:23 for f being Real_Sequence st ( for n being Element of NAT 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) ) proofend; theorem :: ASYMPT_1:24 for g being Real_Sequence st ( for n being Element of NAT 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 ) proofend; theorem :: ASYMPT_1:25 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 ) proofend; begin Lm26: 2 to_power 12 = 4096 proofend; Lm27: for n being Nat st n >= 3 holds n ^2 > (2 * n) + 1 proofend; Lm28: for n being Element of NAT st n >= 10 holds 2 to_power (n - 1) > (2 * n) ^2 proofend; Lm29: for n being Nat st n >= 9 holds (n + 1) to_power 6 < 2 * (n to_power 6) proofend; Lm30: for n being Element of NAT st n >= 30 holds 2 to_power n > n to_power 6 proofend; Lm31: for x being Real st x > 9 holds 2 to_power x > (2 * x) ^2 proofend; Lm32: ex N being Element of NAT st for n being Element of NAT st n >= N holds (sqrt n) - (log (2,n)) > 1 proofend; Lm33: 5 ! = 120 proofend; Lm34: for n being Element of NAT st n >= 10 holds (2 to_power (2 * n)) / (n !) < 1 / (2 to_power (n - 9)) proofend; Lm35: for n being Element of NAT st n >= 3 holds 2 * (n - 2) >= n - 1 proofend; Lm36: 5 to_power 5 = 3125 proofend; Lm37: 4 to_power 4 = 256 proofend; Lm38: for a, b, d, e being Real holds (a / b) / (d / e) = (a / d) * (e / b) proofend; Lm39: for x being real number st x >= 0 holds sqrt x = x to_power (1 / 2) proofend; Lm40: ex N being Element of NAT st for n being Element of NAT st n >= N holds n - ((sqrt n) * (log (2,n))) > n / 2 proofend; Lm41: for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds s is V41() proofend; Lm42: for n being Element of NAT st n >= 1 holds ((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1) proofend; theorem :: ASYMPT_1:26 for f, g being Real_Sequence st ( for n being Element of NAT st n > 0 holds f . n = n to_power (log (2,n)) ) & ( for n being Element of NAT 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 ) proofend; theorem :: ASYMPT_1:27 for f being Real_Sequence st ( for n being Element of NAT 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 ) proofend; theorem :: ASYMPT_1:28 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 ) proofend; theorem :: ASYMPT_1:29 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 ) proofend; theorem :: ASYMPT_1:30 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) ) proofend; theorem :: ASYMPT_1:31 ( Big_Oh (seq_n! 0) c= Big_Oh (seq_n! 1) & not Big_Oh (seq_n! 0) = Big_Oh (seq_n! 1) ) proofend; theorem :: ASYMPT_1:32 for g being Real_Sequence st ( for n being Element of NAT st n > 0 holds g . n = n to_power n ) holds ex s being eventually-positive Real_Sequence st ( s = g & Big_Oh (seq_n! 1) c= Big_Oh s & not Big_Oh (seq_n! 1) = Big_Oh s ) proofend; begin Lm43: for k, n being Element of NAT st k <= n holds n choose k >= ((n + 1) choose k) / (n + 1) proofend; theorem :: ASYMPT_1:33 for n being Element of NAT st n >= 1 holds for f being Real_Sequence for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds f . n >= (n to_power (k + 1)) / (k + 1) proofend; begin Lm44: for f being Real_Sequence st ( for n being Element of NAT holds f . n = log (2,(n !)) ) holds for n being Element of NAT holds f . n = Sum (seq_logn,n) proofend; Lm45: for n being Element of NAT st n >= 4 holds n * (log (2,n)) >= 2 * n proofend; theorem :: ASYMPT_1:34 for f, g being Real_Sequence st ( for n being Element of NAT st n > 0 holds g . n = n * (log (2,n)) ) & ( for n being Element of NAT holds f . n = log (2,(n !)) ) holds ex s being eventually-nonnegative Real_Sequence st ( s = g & f in Big_Theta s ) proofend; begin :: For a "natural" example of an algorithm that would take time in :: O(t(n)), consider a naive algorithm that tries to find at least one :: factor of a given Nat. For all even numbers, the task is trivial, :: and for all odd numbers, the algorithm might try dividing the number by all :: numbers smaller than it, giving a running time of n. theorem :: ASYMPT_1:35 for f being eventually-nonnegative eventually-nondecreasing Real_Sequence for t being Real_Sequence st ( for n being Element of NAT holds ( ( n mod 2 = 0 implies t . n = 1 ) & ( n mod 2 = 1 implies t . n = n ) ) ) holds not t in Big_Theta f proofend; begin Lm46: for n being Element of NAT st n >= 2 holds [/(n / 2)\] < n proofend; begin definition func POWEROF2SET -> non empty Subset of NAT equals :: ASYMPT_1:def 6 { (2 to_power n) where n is Element of NAT : verum } ; coherence { (2 to_power n) where n is Element of NAT : verum } is non empty Subset of NAT proofend; end; :: deftheorem defines POWEROF2SET ASYMPT_1:def_6_:_ POWEROF2SET = { (2 to_power n) where n is Element of NAT : verum } ; Lm47: for n being Element of NAT st n >= 2 holds n ^2 > n + 1 proofend; Lm48: for n being Element of NAT st n >= 1 holds (2 to_power (n + 1)) - (2 to_power n) > 1 proofend; Lm49: for n being Element of NAT st n >= 2 holds not (2 to_power n) - 1 in POWEROF2SET proofend; theorem :: ASYMPT_1:36 for f being Real_Sequence st ( for n being Element of NAT holds ( ( n in POWEROF2SET implies f . n = n ) & ( not n in POWEROF2SET implies f . n = 2 to_power n ) ) ) holds ( f in Big_Theta ((seq_n^ 1),POWEROF2SET) & not f in Big_Theta (seq_n^ 1) & seq_n^ 1 is smooth & not f is eventually-nondecreasing ) proofend; theorem :: ASYMPT_1:37 for f, g being Real_Sequence st ( for n being Element of NAT st n > 0 holds f . n = n to_power (2 to_power [\(log (2,n))/]) ) & ( for n being Element of NAT st n > 0 holds g . n = n to_power n ) holds ex s being eventually-positive Real_Sequence st ( s = g & f in Big_Theta (s,POWEROF2SET) & not f in Big_Theta s & f is eventually-nondecreasing & s is eventually-nondecreasing & not s is_smooth_wrt 2 ) proofend; theorem :: ASYMPT_1:38 for g being Real_Sequence st ( for n being Element of NAT holds ( ( n in POWEROF2SET implies g . n = n ) & ( not n in POWEROF2SET implies g . n = n to_power 2 ) ) ) holds ex s being eventually-positive Real_Sequence st ( s = g & seq_n^ 1 in Big_Theta (s,POWEROF2SET) & not seq_n^ 1 in Big_Theta s & s taken_every 2 in Big_Oh s & seq_n^ 1 is eventually-nondecreasing & not s is eventually-nondecreasing ) proofend; begin Lm50: for n being Element of NAT st n >= 2 holds n ! > 1 proofend; Lm51: for n1, n being Element of NAT st n <= n1 holds n ! <= n1 ! proofend; Lm52: for k being Element of NAT st k >= 1 holds ex n being Element of NAT st ( n ! <= k & k < (n + 1) ! & ( for m being Element of NAT st m ! <= k & k < (m + 1) ! holds m = n ) ) proofend; definition let x be Element of NAT ; func Step1 x -> Element of NAT means :Def7: :: ASYMPT_1:def 7 ex n being Element of NAT st ( n ! <= x & x < (n + 1) ! & it = n ! ) if x <> 0 otherwise it = 0 ; consistency for b1 being Element of NAT holds verum ; existence ( ( x <> 0 implies ex b1, n being Element of NAT st ( n ! <= x & x < (n + 1) ! & b1 = n ! ) ) & ( not x <> 0 implies ex b1 being Element of NAT st b1 = 0 ) ) proofend; uniqueness for b1, b2 being Element of NAT holds ( ( x <> 0 & ex n being Element of NAT st ( n ! <= x & x < (n + 1) ! & b1 = n ! ) & ex n being Element of NAT st ( n ! <= x & x < (n + 1) ! & b2 = n ! ) implies b1 = b2 ) & ( not x <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proofend; end; :: deftheorem Def7 defines Step1 ASYMPT_1:def_7_:_ for x, b2 being Element of NAT holds ( ( x <> 0 implies ( b2 = Step1 x iff ex n being Element of NAT st ( n ! <= x & x < (n + 1) ! & b2 = n ! ) ) ) & ( not x <> 0 implies ( b2 = Step1 x iff b2 = 0 ) ) ); Lm53: for n being Element of NAT st n >= 3 holds n ! > n proofend; theorem :: ASYMPT_1:39 for f being Real_Sequence st ( for n being Element of NAT holds f . n = Step1 n ) holds ex s being eventually-positive Real_Sequence st ( s = f & f is eventually-nondecreasing & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & not s is smooth ) proofend; begin Lm54: (seq_n^ 1) - (seq_const 1) is eventually-positive proofend; :: This is to show that Big_Theta(n-1) + Big_Theta(n) = Big_Theta(n). :: Note that it is not true that Big_Theta(n) = Big_Theta(n) - Big_Theta(n-1). :: Consider n and n. The function n - n = 0, which is not in Big_Theta(n). theorem :: ASYMPT_1:40 for F being eventually-nonnegative Real_Sequence st F = (seq_n^ 1) - (seq_const 1) holds (Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1) proofend; begin theorem :: ASYMPT_1:41 ex F being FUNCTION_DOMAIN of NAT , REAL st ( F = {(seq_n^ 1)} & ( for n being Element of NAT holds (seq_n^ (- 1)) . n <= (seq_n^ 1) . n ) & not seq_n^ (- 1) in F to_power (Big_Oh (seq_const 1)) ) proofend; begin :: In theorem ASYMPT_0:14, if we restrict our attentions to functions that :: do not have a subsequence that converges to 0, then the reverse implication :: is true. theorem :: ASYMPT_1:42 for c being non negative Real for x, f being eventually-nonnegative Real_Sequence st ex e being Real ex N being Element of NAT st ( e > 0 & ( for n being Element of NAT st n >= N holds f . n >= e ) ) & x in Big_Oh (c + f) holds x in Big_Oh f proofend; begin theorem :: ASYMPT_1:43 2 to_power 12 = 4096 by Lm26; theorem :: ASYMPT_1:44 for n being Element of NAT st n >= 3 holds n ^2 > (2 * n) + 1 by Lm27; theorem :: ASYMPT_1:45 for n being Element of NAT st n >= 10 holds 2 to_power (n - 1) > (2 * n) ^2 by Lm28; theorem :: ASYMPT_1:46 for n being Element of NAT st n >= 9 holds (n + 1) to_power 6 < 2 * (n to_power 6) by Lm29; theorem :: ASYMPT_1:47 for n being Element of NAT st n >= 30 holds 2 to_power n > n to_power 6 by Lm30; theorem :: ASYMPT_1:48 for x being Real st x > 9 holds 2 to_power x > (2 * x) ^2 by Lm31; theorem :: ASYMPT_1:49 ex N being Element of NAT st for n being Element of NAT st n >= N holds (sqrt n) - (log (2,n)) > 1 by Lm32; theorem :: ASYMPT_1:50 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))) by Lm3; theorem :: ASYMPT_1:51 5 ! = 120 by Lm33; theorem :: ASYMPT_1:52 5 to_power 5 = 3125 by Lm36; theorem :: ASYMPT_1:53 4 to_power 4 = 256 by Lm37; theorem :: ASYMPT_1:54 for n being Element of NAT holds ((n ^2) - n) + 1 > 0 by Lm21; theorem :: ASYMPT_1:55 for n being Element of NAT st n >= 2 holds n ! > 1 by Lm50; theorem :: ASYMPT_1:56 for n1, n being Element of NAT st n <= n1 holds n ! <= n1 ! by Lm51; theorem :: ASYMPT_1:57 for k being Element of NAT st k >= 1 holds ex n being Element of NAT st ( n ! <= k & k < (n + 1) ! & ( for m being Element of NAT st m ! <= k & k < (m + 1) ! holds m = n ) ) by Lm52; theorem :: ASYMPT_1:58 for n being Element of NAT st n >= 2 holds [/(n / 2)\] < n by Lm46; theorem :: ASYMPT_1:59 for n being Element of NAT st n >= 3 holds n ! > n by Lm53; theorem :: ASYMPT_1:60 (seq_n^ 1) - (seq_const 1) is eventually-positive by Lm54; theorem :: ASYMPT_1:61 for n being Element of NAT st n >= 2 holds 2 to_power n > n + 1 by Lm1; theorem :: ASYMPT_1:62 for a being logbase Real for f being Real_Sequence st a > 1 & f . 0 = 0 & ( for n being Element of NAT st n > 0 holds f . n = log (a,n) ) holds f is eventually-positive by Lm2; theorem :: ASYMPT_1:63 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 ) by Lm5; theorem :: ASYMPT_1:64 for a, b, c being Real st 0 < a & a <= b & c >= 0 holds a to_power c <= b to_power c by Lm6; theorem :: ASYMPT_1:65 for n being Element of NAT st n >= 4 holds (2 * n) + 3 < 2 to_power n by Lm7; theorem :: ASYMPT_1:66 for n being Element of NAT st n >= 6 holds (n + 1) ^2 < 2 to_power n by Lm8; theorem :: ASYMPT_1:67 for c being Real st c > 6 holds c ^2 < 2 to_power c by Lm9; theorem :: ASYMPT_1:68 for e being positive Real for f being Real_Sequence st f . 0 = 0 & ( for n being Element of NAT 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 ) by Lm10; theorem :: ASYMPT_1:69 for e being Real st e > 0 holds ( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 ) by Lm11; theorem :: ASYMPT_1:70 for f being Real_Sequence for N being Element of NAT st ( for n being Element of NAT st n <= N holds f . n >= 0 ) holds Sum (f,N) >= 0 by Lm12; theorem :: ASYMPT_1:71 for f, g being Real_Sequence for N being Element of NAT st ( for n being Element of NAT st n <= N holds f . n <= g . n ) holds Sum (f,N) <= Sum (g,N) by Lm13; theorem :: ASYMPT_1:72 for f being Real_Sequence for b being Real st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds f . n = b ) holds for N being Element of NAT holds Sum (f,N) = b * N by Lm14; theorem :: ASYMPT_1:73 for f being Real_Sequence for N, M being Element of NAT holds (Sum (f,N,M)) + (f . (N + 1)) = Sum (f,(N + 1),M) by Lm15; theorem :: ASYMPT_1:74 for f, g being Real_Sequence for M, N being Element of NAT st N >= M + 1 & ( for n being Element of NAT st M + 1 <= n & n <= N holds f . n <= g . n ) holds Sum (f,N,M) <= Sum (g,N,M) by Lm16; theorem :: ASYMPT_1:75 for n being Element of NAT holds [/(n / 2)\] <= n by Lm17; theorem :: ASYMPT_1:76 for f being Real_Sequence for b being Real for N being Element of NAT st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds f . n = b ) holds for M being Element of NAT holds Sum (f,N,M) = b * (N - M) by Lm18; theorem :: ASYMPT_1:77 for f, g being Real_Sequence for N being Element of NAT for c being Real st f is convergent & lim f = c & ( for n being Element of NAT st n >= N holds f . n = g . n ) holds ( g is convergent & lim g = c ) by Lm22; theorem :: ASYMPT_1:78 for n being Element of NAT st n >= 1 holds ((n ^2) - n) + 1 <= n ^2 by Lm23; theorem :: ASYMPT_1:79 for n being Element of NAT st n >= 1 holds n ^2 <= 2 * (((n ^2) - n) + 1) by Lm24; theorem :: ASYMPT_1:80 for e being Real st 0 < e & e < 1 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds (n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) by Lm25; theorem :: ASYMPT_1:81 for n being Element of NAT st n >= 10 holds (2 to_power (2 * n)) / (n !) < 1 / (2 to_power (n - 9)) by Lm34; theorem :: ASYMPT_1:82 for n being Element of NAT st n >= 3 holds 2 * (n - 2) >= n - 1 by Lm35; theorem :: ASYMPT_1:83 for c being real number st c >= 0 holds c to_power (1 / 2) = sqrt c by Lm39; theorem :: ASYMPT_1:84 ex N being Element of NAT st for n being Element of NAT st n >= N holds n - ((sqrt n) * (log (2,n))) > n / 2 by Lm40; :: The proof of this theorem has been taken directly from the :: article POWER.miz (with very slight modifications to fit this new theorem). theorem :: ASYMPT_1:85 for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds s is V41() by Lm41; :: (1 + 1/n)^n is non-decreasing theorem :: ASYMPT_1:86 for n being Element of NAT st n >= 1 holds ((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1) by Lm42; theorem :: ASYMPT_1:87 for k, n being Element of NAT st k <= n holds n choose k >= ((n + 1) choose k) / (n + 1) by Lm43; theorem :: ASYMPT_1:88 for f being Real_Sequence st ( for n being Element of NAT holds f . n = log (2,(n !)) ) holds for n being Element of NAT holds f . n = Sum (seq_logn,n) by Lm44; theorem :: ASYMPT_1:89 for n being Element of NAT st n >= 4 holds n * (log (2,n)) >= 2 * n by Lm45; theorem :: ASYMPT_1:90 for n being Element of NAT st n >= 2 holds n ^2 > n + 1 by Lm47; theorem :: ASYMPT_1:91 for n being Element of NAT st n >= 1 holds (2 to_power (n + 1)) - (2 to_power n) > 1 by Lm48; theorem :: ASYMPT_1:92 for n being Element of NAT st n >= 2 holds not (2 to_power n) - 1 in POWEROF2SET by Lm49; theorem :: ASYMPT_1:93 for n, k being Element of NAT st k >= 1 & n ! <= k & k < (n + 1) ! holds Step1 k = n ! by Def7; theorem :: ASYMPT_1:94 for a, b, c being Real st a > 1 & b >= a & c >= 1 holds log (a,c) >= log (b,c) by Lm19;