:: Polynomially Bounded Sequences and Polynomial Sequences
:: by Hiroyuki Okazaki and Yuichi Futa
::
:: Received June 30, 2015
:: Copyright (c) 2015-2021 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 being Real_Sequence st ( for k being Nat holds not f in Big_Oh (seq_n^ k) ) holds
not f is polynomially-bounded ;

theorem :: ASYMPT_2:22
for a being positive Real holds seq_a^ (a,1,0) is positive
proof end;

theorem :: ASYMPT_2:23
for a being Real st 1 <= a holds
seq_a^ (a,1,0) is V51()
proof end;

theorem :: ASYMPT_2:24
for a being Real st 1 < a holds
seq_a^ (a,1,0) is V49()
proof end;

theorem :: ASYMPT_2:25
for a being Nat st 1 < a holds
not seq_a^ (a,1,0) is polynomially-bounded
proof end;

theorem LMXFIN1: :: ASYMPT_2:26
for x being XFinSequence of REAL
for y being Real_Sequence holds
( x (#) y is finite Sequence of REAL & dom (x (#) y) = dom x & ( for i being object st i in dom x holds
(x (#) y) . i = (x . i) * (y . i) ) )
proof end;

definition
let x be XFinSequence of REAL ;
let y be Real_Sequence;
:: original: (#)
redefine func x (#) y -> XFinSequence of REAL ;
correctness
coherence
x (#) y is XFinSequence of REAL
;
by LMXFIN1;
end;

theorem LMXFIN2: :: ASYMPT_2:27
for d being XFinSequence of REAL
for x, i being Nat st i in dom d holds
(d (#) (seq_a^ (x,1,0))) . i = (d . i) * (x to_power i)
proof end;

definition
let c be XFinSequence of REAL ;
func seq_p c -> Real_Sequence means :defseqp: :: ASYMPT_2:def 2
for x being Nat holds it . x = Sum (c (#) (seq_a^ (x,1,0)));
existence
ex b1 being Real_Sequence st
for x being Nat holds b1 . x = Sum (c (#) (seq_a^ (x,1,0)))
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for x being Nat holds b1 . x = Sum (c (#) (seq_a^ (x,1,0))) ) & ( for x being Nat holds b2 . x = Sum (c (#) (seq_a^ (x,1,0))) ) holds
b1 = b2
proof end;
end;

:: deftheorem defseqp defines seq_p ASYMPT_2:def 2 :
for c being XFinSequence of REAL
for b2 being Real_Sequence holds
( b2 = seq_p c iff for x being Nat holds b2 . x = Sum (c (#) (seq_a^ (x,1,0))) );

LMXFIN3: for d being XFinSequence of REAL
for k being Nat st len d = k + 1 holds
ex a being Real ex d1 being XFinSequence of REAL st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> )

proof end;

theorem LMXFIN4: :: ASYMPT_2:28
for d being XFinSequence of REAL
for k being Nat st len d = k + 1 holds
ex a being Real ex d1 being XFinSequence of REAL ex y being Real_Sequence st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> & seq_p d = (seq_p d1) + y & ( for i being Nat holds y . i = a * (i to_power k) ) )
proof end;

theorem LMXFIN5: :: ASYMPT_2:29
for d being XFinSequence of REAL
for k being Nat st len d = 1 holds
ex a being Real st
( a = d . 0 & ( for x being Nat holds (seq_p d) . x = a ) )
proof end;

theorem LMXFIN6: :: ASYMPT_2:30
for d being XFinSequence of REAL
for k being Nat st len d = 1 & d is nonnegative-yielding holds
seq_p d in Big_Oh (seq_n^ k)
proof end;

LMXFIN7: for k being Nat
for x, y being Real_Sequence st x in Big_Oh (seq_n^ k) & y in Big_Oh (seq_n^ k) holds
x + y in Big_Oh (seq_n^ k)

proof end;

theorem LMXFIN8: :: ASYMPT_2:31
for k being Nat
for a being Real
for y being Real_Sequence st 0 <= a & ( for i being Nat holds y . i = a * (i to_power k) ) holds
y in Big_Oh (seq_n^ k)
proof end;

LMXFIN9: for k being Nat holds Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ (k + 1))
proof end;

theorem :: ASYMPT_2:32
for k, n being Nat st k <= n holds
Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ n)
proof end;

theorem LMXFIN10: :: ASYMPT_2:33
for k being Nat
for c being nonnegative-yielding XFinSequence of REAL st len c = k + 1 holds
seq_p c in Big_Oh (seq_n^ k)
proof end;

theorem LMXFIN15: :: ASYMPT_2:34
for k being Nat
for c being XFinSequence of REAL ex d being XFinSequence of REAL st
( len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) )
proof end;

theorem LMXFIN17: :: ASYMPT_2:35
for c, d being XFinSequence of REAL st len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) holds
for n being Nat holds (seq_p c) . n <= (seq_p d) . n
proof end;

theorem LMXFIN20A: :: ASYMPT_2:36
for k being Nat
for c being XFinSequence of REAL st len c = k + 1 & seq_p c is eventually-nonnegative holds
seq_p c in Big_Oh (seq_n^ k)
proof end;

theorem TPOWSUCC: :: ASYMPT_2:37
for k, n being Nat st 0 < n holds
n * ((seq_n^ k) . n) = (seq_n^ (k + 1)) . n
proof end;

theorem TLNEG1: :: ASYMPT_2:38
for c being XFinSequence of REAL st len c = 0 holds
for x being Nat holds (seq_p c) . x = 0
proof end;

theorem :: ASYMPT_2:39
for f being eventually-nonnegative Real_Sequence
for k being Nat st f in Big_Oh (seq_n^ k) holds
ex N being Nat st
for n being Nat st N <= n holds
f . n <= (seq_n^ (k + 1)) . n
proof end;

theorem :: ASYMPT_2:40
for c being XFinSequence of REAL ex absc being XFinSequence of REAL st
( absc = |.c.| & ( for n being Nat holds (seq_p c) . n <= (seq_p absc) . n ) )
proof end;

theorem TLNEG41: :: ASYMPT_2:41
for c, absc being XFinSequence of REAL st absc = |.c.| holds
for n being Nat holds |.((seq_p c) . n).| <= (seq_p absc) . n
proof end;

TLNEG42: for d being XFinSequence of REAL st ( for i being Nat st i in dom d holds
0 <= d . i ) holds
ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) )

proof end;

theorem TLNEG36: :: ASYMPT_2:42
for a being Real st 0 < a holds
for k being Nat
for d being nonnegative-yielding XFinSequence of REAL st len d = k holds
ex N being Nat st
for x being Nat st N <= x holds
for i being Nat st i in dom d holds
((d . i) * (x to_power i)) * k <= a * (x to_power k)
proof end;

theorem TLNEG35: :: ASYMPT_2:43
for k being Nat
for d being XFinSequence of REAL
for a being Real
for y being Real_Sequence st 0 < a & len d = k & ( for x being Nat holds y . x = a * (x to_power k) ) holds
ex N being Nat st
for x being Nat st N <= x holds
|.((seq_p d) . x).| <= y . x
proof end;

theorem TLNEG3: :: ASYMPT_2:44
for k being Nat
for d being XFinSequence of REAL st len d = k + 1 & 0 < d . k holds
seq_p d is eventually-nonnegative
proof end;

theorem :: ASYMPT_2:45
for k being Nat
for c being XFinSequence of REAL st len c = k + 1 & 0 < c . k holds
seq_p c in Big_Oh (seq_n^ k) by LMXFIN20A, TLNEG3;

theorem :: ASYMPT_2:46
for k being Nat
for c being XFinSequence of REAL st len c = k + 1 & 0 < c . k holds
seq_p c is polynomially-bounded
proof end;