:: by Hiroyuki Okazaki and Yuichi Futa

::

:: Received June 30, 2015

:: Copyright (c) 2015-2018 Association of Mizar Users

LMC31X: for m, n being Nat st 2 <= m holds

n < m to_power n

by NEWTON:86;

Lm5: ( dom (id ([#] REAL)) = [#] REAL & ( for x being Real holds (id ([#] REAL)) . x = x ) & ( for x being Real holds

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 ) ) )

proof end;

LEMC01: for x, n, a being Nat st 0 < a & a <= x holds

a to_power n <= x to_power n

by PREPOWER:9;

theorem Lm6: :: ASYMPT_2:10

ex g being PartFunc of REAL,REAL st

( dom g = right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

g . x = log (2,x) ) & g is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

( g is_differentiable_in x & diff (g,x) = (log (2,number_e)) / x & 0 < diff (g,x) ) ) )

( dom g = right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

g . x = log (2,x) ) & g is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds

( g is_differentiable_in x & diff (g,x) = (log (2,number_e)) / x & 0 < diff (g,x) ) ) )

proof end;

theorem LMC31H2: :: ASYMPT_2:11

ex f being PartFunc of REAL,REAL st

( right_open_halfline number_e = dom f & ( for x being Real st x in dom f holds

f . x = x / (log (2,x)) ) & f is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds

0 <= diff (f,x0) ) & f is non-decreasing )

( right_open_halfline number_e = dom f & ( for x being Real st x in dom f holds

f . x = x / (log (2,x)) ) & f is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds

0 <= diff (f,x0) ) & f is non-decreasing )

proof end;

theorem LMC31H: :: ASYMPT_2:13

for k being Nat st number_e < k holds

ex N being Nat st

for n being Nat st N <= n holds

2 to_power k <= n / (log (2,n))

ex N being Nat st

for n being Nat st N <= n holds

2 to_power k <= n / (log (2,n))

proof end;

LMC31: for r being Real ex N being Element of NAT st

for n being Nat st N <= n holds

r < n / (log (2,n))

proof end;

LMC31HC: ex N being Element of NAT st

for n being Nat st N <= n holds

4 < n / (log (2,n))

proof end;

theorem :: ASYMPT_2:14

for x being Nat st 1 < x holds

ex N being Nat st

for n being Nat st N <= n holds

4 < n / (log (x,n))

ex N being Nat st

for n being Nat st N <= n holds

4 < n / (log (x,n))

proof end;

theorem :: ASYMPT_2:15

for x being Nat st 1 < x holds

ex N, c being Nat st

for n being Nat st N <= n holds

n to_power x <= c * (x to_power n)

ex N, c being Nat st

for n being Nat st N <= n holds

n to_power x <= c * (x to_power n)

proof end;

theorem N2POWINPOLY: :: ASYMPT_2:16

for x being Nat st 1 < x holds

for N, c being Nat ex n being Nat st

( N <= n & not 2 to_power n <= c * (n to_power x) )

for N, c being Nat ex n being Nat st

( N <= n & not 2 to_power n <= c * (n to_power x) )

proof end;

FROMASYMPT1t11: for a, b being Nat st a < b holds

seq_n^ a in Big_Oh (seq_n^ b)

proof end;

theorem :: ASYMPT_2:18

for x being Nat st 1 < x holds

for N, c being Nat ex n being Nat st

( N <= n & not x to_power n <= c * (n to_power x) )

for N, c being Nat ex n being Nat st

( N <= n & not x to_power n <= c * (n to_power x) )

proof end;

:: deftheorem defines polynomially-bounded ASYMPT_2:def 1 :

for p being Real_Sequence holds

( p is polynomially-bounded iff ex k being Nat st p in Big_Oh (seq_n^ k) );

for p being Real_Sequence holds

( p is polynomially-bounded iff ex k being Nat st p in Big_Oh (seq_n^ k) );

theorem :: ASYMPT_2:20

for f being Real_Sequence st not f is polynomially-bounded holds

for k being Nat holds not f in Big_Oh (seq_n^ k) ;

for k being Nat holds not f in Big_Oh (seq_n^ k) ;