:: 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 b₁ being Real_Sequence st
for x being Nat holds b₁ . x = Sum (c (#) (seq_a^ (x,1,0)))

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for x being Nat holds b₁ . x = Sum (c (#) (seq_a^ (x,1,0))) ) & ( for x being Nat holds b₂ . x = Sum (c (#) (seq_a^ (x,1,0))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defseqp defines seq_p ASYMPT_2:def 2 :
for c being XFinSequence of REAL
for b₂ being Real_Sequence holds
( b₂ = seq_p c iff for x being Nat holds b₂ . 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;