:: Polynomially Bounded Sequences and Polynomial Sequences
:: by Hiroyuki Okazaki and Yuichi Futa
::
:: Received June 30, 2015
:: Copyright (c) 2015-2018 Association of Mizar Users


theorem :: ASYMPT_2:1
for m, k being Nat st 1 <= m holds
1 <= m to_power k
proof end;

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

by NEWTON:86;

theorem LMC31B: :: ASYMPT_2:2
for m, n being Nat holds m <= m to_power (n + 1)
proof end;

theorem :: ASYMPT_2:3
for m, n being Nat st 2 <= m holds
n + 1 <= m to_power n by NEWTON:85;

theorem LMC31D: :: ASYMPT_2:4
for k being Nat holds 2 * k <= 2 to_power k
proof end;

theorem LMC31E: :: ASYMPT_2:5
for k, n being Nat st k <= n holds
n + k <= 2 to_power n
proof end;

theorem LMC31G: :: ASYMPT_2:6
for k, m being Nat st (2 * k) + 1 <= m holds
2 to_power k <= (2 to_power m) / m
proof end;

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;

theorem CPOWER57: :: ASYMPT_2:7
for a, b, c being Real st 1 < a & 0 < b & b <= c holds
log (a,b) <= log (a,c)
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 LC5aa: :: ASYMPT_2:8
for n being Nat
for a being Real st 1 < a holds
a to_power n < a to_power (n + 1)
proof end;

theorem LC5a: :: ASYMPT_2:9
for n being Nat
for a being Real st 1 <= a holds
a to_power n <= a to_power (n + 1)
proof end;

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

theorem LMC31H1: :: ASYMPT_2:12
for x, y being Real st number_e < x & x <= y holds
x / (log (2,x)) <= y / (log (2,y))
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))
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))
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)
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) )
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:17
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) )
proof end;

theorem LC4: :: ASYMPT_2:19
for a being non negative Real
for n being Nat st 1 <= n holds
0 < (seq_n^ a) . n
proof end;

definition
let p be Real_Sequence;
attr p is polynomially-bounded means :: ASYMPT_2:def 1
ex k being Nat st p in Big_Oh (seq_n^ k);
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) );

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

theorem :: ASYMPT_2:21
for f