ASYMPT

:: 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

:: ASYMPT_1 semantic presentation

Lm1: for n being Nat st n >= 2 holds
2 to_power n > n + 1

proof end;

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 ) & t1 . 0 = 0 & ( 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 )

proof end;

Lm2: 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

proof end;

theorem :: ASYMPT_1:2

for a, b being logbase Real
for f, g being Real_Sequence st a > 1 & b > 1 & f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log a,n ) & g . 0 = 0 & ( 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 )

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines seq_a^ ASYMPT_1:def 1 :

registration

let a be positive Real;
let b, c be Real;
cluster seq_a^ a,b,c -> eventually-positive ;
coherence

proof 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 end;

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 )

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines seq_logn ASYMPT_1:def 2 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines seq_n^ ASYMPT_1:def 3 :

registration

cluster seq_logn -> eventually-positive ;
coherence

proof end;

end;

registration

let a be Real;
cluster seq_n^ a -> eventually-positive ;
coherence

proof end;

end;

Lm4: for f, g being Real_Sequence
for n being Element of NAT holds (f /" g) . n = (f . n) / (g . n)

proof 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 end;

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 ) )

proof 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 end;

Lm7: 2 to_power 2 = 4

proof end;

Lm8: 2 to_power 3 = 8

proof end;

Lm9: 2 to_power 4 = 16

proof end;

Lm10: 2 to_power 5 = 32

proof end;

Lm11: 2 to_power 6 = 64

proof end;

Lm12: for n being Nat st n >= 4 holds
(2 * n) + 3 < 2 to_power n

proof end;

Lm13: for n being Element of NAT st n >= 6 holds
(n + 1) ^2 < 2 to_power n

proof end;

Lm14: for c being Real st c > 6 holds
c ^2 < 2 to_power c

proof end;

Lm15: 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 )

proof 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 end;

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)) )

proof end;

theorem :: ASYMPT_1:6

( seq_n^ (1 / 2) in Big_Omega seq_logn & not seq_logn in Big_Omega (seq_n^ (1 / 2)) )

proof end;

Lm17: 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

proof end;

Lm18: 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

proof end;

Lm19: 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

proof end;

Lm20: for f being Real_Sequence
for N, M being Nat holds (Sum f,N,M) + (f . (N + 1)) = Sum f,(N + 1),M

proof end;

Lm21: 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

proof end;

Lm22: for n being Element of NAT holds [/(n / 2)\] <= n

proof end;

Lm23: 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)

proof end;

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))

proof end;

theorem :: ASYMPT_1:8

for f being Real_Sequence st f . 0 = 0 & ( 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 )

proof end;

definition

let b be Real;
func seq_const b -> Real_Sequence equals :: ASYMPT_1:def 4
NAT --> b;
coherence

proof end;

end;

:: deftheorem defines seq_const ASYMPT_1:def 4 :

registration

cluster seq_const 1 -> eventually-nonnegative ;
coherence

proof end;

end;

Lm24: for a, b, c being Real st a > 1 & b >= a & c >= 1 holds
log a,c >= log b,c

proof end;

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)) ) )

proof end;

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)

proof end;

theorem :: ASYMPT_1:11

seq_n^ 2 in Big_Oh (seq_n^ 3)

proof end;

theorem :: ASYMPT_1:12

not seq_n^ 2 in Big_Omega (seq_n^ 3)

proof end;

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 )

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines seq_n! ASYMPT_1:def 5 :

registration

let a be Element of NAT ;
cluster seq_n! a -> eventually-positive ;
coherence

proof end;

end;

theorem :: ASYMPT_1:14

not seq_n! 0 in Big_Theta (seq_n! 1)

proof end;

Lm26: now

let a, b, c, d be Real; :: thesis:
assume ( 0 <= b & a <= b & 0 <= c & c <= d ) ; :: thesis:
then ( a * c <= b * c & b * c <= b * d ) by XREAL_1:66;
hence a * c <= b * d by XXREAL_0:2; :: thesis:

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)

proof end;

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 )

proof end;

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)) ) )

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

Lm27: for n being Element of NAT holds ((n ^2 ) - n) + 1 > 0

proof end;

Lm28: 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 )

proof end;

Lm29: for n being Element of NAT st n >= 1 holds
((n ^2 ) - n) + 1 <= n ^2

proof end;

Lm30: for n being Element of NAT st n >= 1 holds
n ^2 <= 2 * (((n ^2 ) - n) + 1)

proof end;

Lm31: 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)

proof end;

theorem :: ASYMPT_1:21

for e being Real
for f being Real_Sequence st 0 < e & f . 0 = 0 & ( 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)) )

proof end;

theorem :: ASYMPT_1:22

for e being Real
for g being Real_Sequence st 0 < e & e < 1 & g . 0 = 0 & g . 1 = 0 & ( 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 )

proof end;

theorem :: ASYMPT_1:23

for f being Real_Sequence st f . 0 = 0 & f . 1 = 0 & ( 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) )

proof end;

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 )

proof end;

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 )

proof end;

Lm32: 2 to_power 12 = 4096

proof end;

Lm33: for n being Nat st n >= 3 holds
n ^2 > (2 * n) + 1

proof end;

Lm34: for n being Element of NAT st n >= 10 holds
2 to_power (n - 1) > (2 * n) ^2

proof end;

Lm35: for n being Nat st n >= 9 holds
(n + 1) to_power 6 < 2 * (n to_power 6)

proof end;

Lm36: for n being Element of NAT st n >= 30 holds
2 to_power n > n to_power 6

proof end;

Lm37: for x being Real st x > 9 holds
2 to_power x > (2 * x) ^2

proof end;

Lm38: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(sqrt n) - (log 2,n) > 1

proof end;

Lm39: (4 + 1) ! = 120

proof end;

Lm40: for n being Element of NAT st n >= 10 holds
(2 to_power (2 * n)) / (n ! ) < 1 / (2 to_power (n