:: by Hiroyuki Okazaki and Yuichi Futa

::

:: Received June 30, 2015

:: Copyright (c) 2015-2016 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) ;

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 ;

not f is polynomially-bounded ;

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

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;
let y be Real_Sequence;

:: original: (#)

redefine func x (#) y -> XFinSequence of REAL ;

correctness

coherence

x (#) y is XFinSequence of REAL ;

by LMXFIN1;

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)

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 ;

ex b_{1} being Real_Sequence st

for x being Nat holds b_{1} . x = Sum (c (#) (seq_a^ (x,1,0)))

for b_{1}, b_{2} being Real_Sequence st ( for x being Nat holds b_{1} . x = Sum (c (#) (seq_a^ (x,1,0))) ) & ( for x being Nat holds b_{2} . x = Sum (c (#) (seq_a^ (x,1,0))) ) holds

b_{1} = b_{2}

end;
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 for x being Nat holds it . x = Sum (c (#) (seq_a^ (x,1,0)));

ex b

for x being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defseqp defines seq_p ASYMPT_2:def 2 :

for c being XFinSequence of REAL

for b_{2} being Real_Sequence holds

( b_{2} = seq_p c iff for x being Nat holds b_{2} . x = Sum (c (#) (seq_a^ (x,1,0))) );

for c being XFinSequence of REAL

for b

( b

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

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

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)

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)

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

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

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

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)

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

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

( 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

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)

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

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

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

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

for c being XFinSequence of REAL st len c = k + 1 & 0 < c . k holds

seq_p c is polynomially-bounded

proof end;