:: by Richard Krueger, Piotr Rudnicki and Paul Shelley

::

:: Received November 4, 1999

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

Lm1: for n being Nat st n >= 2 holds

2 to_power n > n + 1

proof end;

reconsider zz = 0 as Element of REAL by XREAL_0:def 1;

theorem :: ASYMPT_1:1

for t, t1 being Real_Sequence st t . 0 = 0 & ( for n being Element of NAT st n > 0 holds

t . n = ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 ) & ( for n being Element of NAT st n > 0 holds

t1 . n = (n to_power 3) * (log (2,n)) ) holds

ex s, s1 being eventually-positive Real_Sequence st

( s = t & s1 = t1 & s in Big_Oh s1 )

t . n = ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 ) & ( for n being Element of NAT st n > 0 holds

t1 . n = (n to_power 3) * (log (2,n)) ) holds

ex s, s1 being eventually-positive Real_Sequence st

( s = t & s1 = t1 & s in Big_Oh s1 )

proof end;

Lm2: for a being logbase Real

for f being Real_Sequence st a > 1 & ( for n being Element of NAT st n > 0 holds

f . n = log (a,n) ) holds

f is eventually-positive

proof end;

theorem :: ASYMPT_1:2

for a, b being logbase Real

for f, g being Real_Sequence st a > 1 & b > 1 & ( for n being Element of NAT st n > 0 holds

f . n = log (a,n) ) & ( for n being Element of NAT st n > 0 holds

g . n = log (b,n) ) holds

ex s, s1 being eventually-positive Real_Sequence st

( s = f & s1 = g & Big_Oh s = Big_Oh s1 )

for f, g being Real_Sequence st a > 1 & b > 1 & ( for n being Element of NAT st n > 0 holds

f . n = log (a,n) ) & ( for n being Element of NAT st n > 0 holds

g . n = log (b,n) ) holds

ex s, s1 being eventually-positive Real_Sequence st

( s = f & s1 = g & Big_Oh s = Big_Oh s1 )

proof end;

definition

let a, b, c be Real;

ex b_{1} being Real_Sequence st

for n being Element of NAT holds b_{1} . n = a to_power ((b * n) + c)

for b_{1}, b_{2} being Real_Sequence st ( for n being Element of NAT holds b_{1} . n = a to_power ((b * n) + c) ) & ( for n being Element of NAT holds b_{2} . n = a to_power ((b * n) + c) ) holds

b_{1} = b_{2}

end;
func seq_a^ (a,b,c) -> Real_Sequence means :Def1: :: ASYMPT_1:def 1

for n being Element of NAT holds it . n = a to_power ((b * n) + c);

existence for n being Element of NAT holds it . n = a to_power ((b * n) + c);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines seq_a^ ASYMPT_1:def 1 :

for a, b, c being Real

for b_{4} being Real_Sequence holds

( b_{4} = seq_a^ (a,b,c) iff for n being Element of NAT holds b_{4} . n = a to_power ((b * n) + c) );

for a, b, c being Real

for b

( b

registration
end;

Lm3: for a, b, c being Real st a > 0 & c > 0 & c <> 1 holds

a to_power b = c to_power (b * (log (c,a)))

proof end;

:: Example p. 84

definition

ex b_{1} being Real_Sequence st

( b_{1} . 0 = 0 & ( for n being Element of NAT st n > 0 holds

b_{1} . n = log (2,n) ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = 0 & ( for n being Element of NAT st n > 0 holds

b_{1} . n = log (2,n) ) & b_{2} . 0 = 0 & ( for n being Element of NAT st n > 0 holds

b_{2} . n = log (2,n) ) holds

b_{1} = b_{2}
end;

func seq_logn -> Real_Sequence means :Def2: :: ASYMPT_1:def 2

( it . 0 = 0 & ( for n being Element of NAT st n > 0 holds

it . n = log (2,n) ) );

existence ( it . 0 = 0 & ( for n being Element of NAT st n > 0 holds

it . n = log (2,n) ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines seq_logn ASYMPT_1:def 2 :

for b_{1} being Real_Sequence holds

( b_{1} = seq_logn iff ( b_{1} . 0 = 0 & ( for n being Element of NAT st n > 0 holds

b_{1} . n = log (2,n) ) ) );

for b

( b

b

definition

let a be Real;

ex b_{1} being Real_Sequence st

( b_{1} . 0 = 0 & ( for n being Element of NAT st n > 0 holds

b_{1} . n = n to_power a ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = 0 & ( for n being Element of NAT st n > 0 holds

b_{1} . n = n to_power a ) & b_{2} . 0 = 0 & ( for n being Element of NAT st n > 0 holds

b_{2} . n = n to_power a ) holds

b_{1} = b_{2}

end;
func seq_n^ a -> Real_Sequence means :Def3: :: ASYMPT_1:def 3

( it . 0 = 0 & ( for n being Element of NAT st n > 0 holds

it . n = n to_power a ) );

existence ( it . 0 = 0 & ( for n being Element of NAT st n > 0 holds

it . n = n to_power a ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines seq_n^ ASYMPT_1:def 3 :

for a being Real

for b_{2} being Real_Sequence holds

( b_{2} = seq_n^ a iff ( b_{2} . 0 = 0 & ( for n being Element of NAT st n > 0 holds

b_{2} . n = n to_power a ) ) );

for a being Real

for b

( b

b

registration
end;

Lm4: for f, g being Real_Sequence

for n being Nat holds (f /" g) . n = (f . n) / (g . n)

proof end;

Lm5: for f, g being eventually-nonnegative Real_Sequence holds

( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g )

proof end;

theorem Th4: :: ASYMPT_1:4

for f, g being eventually-nonnegative Real_Sequence holds

( Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g iff ( f in Big_Oh g & not f in Big_Omega g ) )

( Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g iff ( f in Big_Oh g & not f in Big_Omega g ) )

proof end;

Lm6: for a, b, c being Real st 0 < a & a <= b & c >= 0 holds

a to_power c <= b to_power c

proof end;

Lm7: for n being Nat st n >= 4 holds

(2 * n) + 3 < 2 to_power n

proof end;

Lm8: for n being Element of NAT st n >= 6 holds

(n + 1) ^2 < 2 to_power n

proof end;

Lm9: for c being Real st c > 6 holds

c ^2 < 2 to_power c

proof end;

Lm10: for e being positive Real

for f being Real_Sequence st ( for n being Element of NAT st n > 0 holds

f . n = log (2,(n to_power e)) ) holds

( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 )

proof end;

Lm11: for e being Real st e > 0 holds

( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 )

proof end;

:: Example p. 86

Lm12: for f being Real_Sequence

for N being Element of NAT st ( for n being Element of NAT st n <= N holds

f . n >= 0 ) holds

Sum (f,N) >= 0

proof end;

Lm13: for f, g being Real_Sequence

for N being Element of NAT st ( for n being Element of NAT st n <= N holds

f . n <= g . n ) holds

Sum (f,N) <= Sum (g,N)

proof end;

Lm14: for f being Real_Sequence

for b being Real st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds

f . n = b ) holds

for N being Element of NAT holds Sum (f,N) = b * N

proof end;

Lm15: for f being Real_Sequence

for N, M being Nat holds (Sum (f,N,M)) + (f . (N + 1)) = Sum (f,(N + 1),M)

proof end;

Lm16: for f, g being Real_Sequence

for M, N being Element of NAT st N >= M + 1 & ( for n being Element of NAT st M + 1 <= n & n <= N holds

f . n <= g . n ) holds

Sum (f,N,M) <= Sum (g,N,M)

proof end;

Lm17: for n being Nat holds [/(n / 2)\] <= n

proof end;

Lm18: for f being Real_Sequence

for b being Real

for N being Element of NAT st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds

f . n = b ) holds

for M being Element of NAT holds Sum (f,N,M) = b * (N - M)

proof end;

theorem :: ASYMPT_1:7

for f being Real_Sequence

for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds

f in Big_Theta (seq_n^ (k + 1))

for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds

f in Big_Theta (seq_n^ (k + 1))

proof end;

:: Example p. 89

theorem :: ASYMPT_1:8

for f being Real_Sequence st ( for n being Element of NAT st n > 0 holds

f . n = n to_power (log (2,n)) ) holds

ex s being eventually-positive Real_Sequence st

( s = f & not s is smooth )

f . n = n to_power (log (2,n)) ) holds

ex s being eventually-positive Real_Sequence st

( s = f & not s is smooth )

proof end;

:: Example p. 92

definition
end;

Lm19: for a, b, c being Real st a > 1 & b >= a & c >= 1 holds

log (a,c) >= log (b,c)

proof end;

theorem Th9: :: ASYMPT_1:9

for f being eventually-nonnegative Real_Sequence ex F being FUNCTION_DOMAIN of NAT , REAL st

( F = {(seq_n^ 1)} & ( f in F to_power (Big_Oh (seq_const 1)) implies ex N being Element of NAT ex c being Real ex k being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( 1 <= f . n & f . n <= c * ((seq_n^ k) . n) ) ) ) ) & ( ex N being Element of NAT ex c being Real ex k being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( 1 <= f . n & f . n <= c * ((seq_n^ k) . n) ) ) ) implies f in F to_power (Big_Oh (seq_const 1)) ) )

( F = {(seq_n^ 1)} & ( f in F to_power (Big_Oh (seq_const 1)) implies ex N being Element of NAT ex c being Real ex k being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( 1 <= f . n & f . n <= c * ((seq_n^ k) . n) ) ) ) ) & ( ex N being Element of NAT ex c being Real ex k being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( 1 <= f . n & f . n <= c * ((seq_n^ k) . n) ) ) ) implies f in F to_power (Big_Oh (seq_const 1)) ) )

proof end;

theorem :: ASYMPT_1:10

for f being Real_Sequence st ( for n being Element of NAT holds f . n = ((3 * (10 to_power 6)) - ((18 * (10 to_power 3)) * n)) + (27 * (n ^2)) ) holds

f in Big_Oh (seq_n^ 2)

f in Big_Oh (seq_n^ 2)

proof end;

theorem :: ASYMPT_1:13

ex s being eventually-positive Real_Sequence st

( s = seq_a^ (2,1,1) & seq_a^ (2,1,0) in Big_Theta s )

( s = seq_a^ (2,1,1) & seq_a^ (2,1,0) in Big_Theta s )

proof end;

definition

let a be Element of NAT ;

ex b_{1} being Real_Sequence st

for n being Element of NAT holds b_{1} . n = (n + a) !

for b_{1}, b_{2} being Real_Sequence st ( for n being Element of NAT holds b_{1} . n = (n + a) ! ) & ( for n being Element of NAT holds b_{2} . n = (n + a) ! ) holds

b_{1} = b_{2}

end;
func seq_n! a -> Real_Sequence means :Def4: :: ASYMPT_1:def 5

for n being Element of NAT holds it . n = (n + a) ! ;

existence for n being Element of NAT holds it . n = (n + a) ! ;

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines seq_n! ASYMPT_1:def 5 :

for a being Element of NAT

for b_{2} being Real_Sequence holds

( b_{2} = seq_n! a iff for n being Element of NAT holds b_{2} . n = (n + a) ! );

for a being Element of NAT

for b

( b

Lm20: now :: thesis: for a, b, c, d being Real st 0 <= b & a <= b & 0 <= c & c <= d holds

a * c <= b * d

a * c <= b * d

let a, b, c, d be Real; :: thesis: ( 0 <= b & a <= b & 0 <= c & c <= d implies a * c <= b * d )

assume that

A1: 0 <= b and

A2: a <= b and

A3: 0 <= c and

A4: c <= d ; :: thesis: a * c <= b * d

A5: b * c <= b * d by A1, A4, XREAL_1:64;

a * c <= b * c by A2, A3, XREAL_1:64;

hence a * c <= b * d by A5, XXREAL_0:2; :: thesis: verum

end;
assume that

A1: 0 <= b and

A2: a <= b and

A3: 0 <= c and

A4: c <= d ; :: thesis: a * c <= b * d

A5: b * c <= b * d by A1, A4, XREAL_1:64;

a * c <= b * c by A2, A3, XREAL_1:64;

hence a * c <= b * d by A5, XXREAL_0:2; :: thesis: verum

theorem :: ASYMPT_1:16

ex s being eventually-positive Real_Sequence st

( s = seq_a^ (2,1,0) & 2 (#) (seq_n^ 1) in Big_Oh (seq_n^ 1) & not seq_a^ (2,2,0) in Big_Oh s )

( s = seq_a^ (2,1,0) & 2 (#) (seq_n^ 1) in Big_Oh (seq_n^ 1) & not seq_a^ (2,2,0) in Big_Oh s )

proof end;

theorem :: ASYMPT_1:17

( log (2,3) < 159 / 100 implies ( seq_n^ (log (2,3)) in Big_Oh (seq_n^ (159 / 100)) & not seq_n^ (log (2,3)) in Big_Omega (seq_n^ (159 / 100)) & not seq_n^ (log (2,3)) in Big_Theta (seq_n^ (159 / 100)) ) )

proof end;

theorem :: ASYMPT_1:18

for f, g being Real_Sequence st ( for n being Element of NAT holds f . n = n mod 2 ) & ( for n being Element of NAT holds g . n = (n + 1) mod 2 ) holds

ex s, s1 being eventually-nonnegative Real_Sequence st

( s = f & s1 = g & not s in Big_Oh s1 & not s1 in Big_Oh s )

ex s, s1 being eventually-nonnegative Real_Sequence st

( s = f & s1 = g & not s in Big_Oh s1 & not s1 in Big_Oh s )

proof end;

theorem :: ASYMPT_1:19

for f, g being eventually-nonnegative Real_Sequence holds

( Big_Oh f = Big_Oh g iff f in Big_Theta g )

( Big_Oh f = Big_Oh g iff f in Big_Theta g )

proof end;

theorem :: ASYMPT_1:20

for f, g being eventually-nonnegative Real_Sequence holds

( f in Big_Theta g iff Big_Theta f = Big_Theta g )

( f in Big_Theta g iff Big_Theta f = Big_Theta g )

proof end;

Lm21: for n being Element of NAT holds ((n ^2) - n) + 1 > 0

proof end;

Lm22: for f, g being Real_Sequence

for N being Element of NAT

for c being Real st f is convergent & lim f = c & ( for n being Element of NAT st n >= N holds

f . n = g . n ) holds

( g is convergent & lim g = c )

proof end;

Lm23: for n being Element of NAT st n >= 1 holds

((n ^2) - n) + 1 <= n ^2

proof end;

Lm24: for n being Element of NAT st n >= 1 holds

n ^2 <= 2 * (((n ^2) - n) + 1)

proof end;

Lm25: for e being Real st 0 < e & e < 1 holds

ex N being Element of NAT st

for n being Element of NAT st n >= N holds

(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n))

proof end;

theorem :: ASYMPT_1:21

for e being Real

for f being Real_Sequence st 0 < e & ( for n being Element of NAT st n > 0 holds

f . n = n * (log (2,n)) ) holds

ex s being eventually-positive Real_Sequence st

( s = f & Big_Oh s c= Big_Oh (seq_n^ (1 + e)) & not Big_Oh s = Big_Oh (seq_n^ (1 + e)) )

for f being Real_Sequence st 0 < e & ( for n being Element of NAT st n > 0 holds

f . n = n * (log (2,n)) ) holds

ex s being eventually-positive Real_Sequence st

( s = f & Big_Oh s c= Big_Oh (seq_n^ (1 + e)) & not Big_Oh s = Big_Oh (seq_n^ (1 + e)) )

proof end;

theorem :: ASYMPT_1:22

for e being Real

for g being Real_Sequence st e < 1 & ( for n being Element of NAT st n > 1 holds

g . n = (n to_power 2) / (log (2,n)) ) holds

ex s being eventually-positive Real_Sequence st

( s = g & Big_Oh (seq_n^ (1 + e)) c= Big_Oh s & not Big_Oh (seq_n^ (1 + e)) = Big_Oh s )

for g being Real_Sequence st e < 1 & ( for n being Element of NAT st n > 1 holds

g . n = (n to_power 2) / (log (2,n)) ) holds

ex s being eventually-positive Real_Sequence st

( s = g & Big_Oh (seq_n^ (1 + e)) c= Big_Oh s & not Big_Oh (seq_n^ (1 + e)) = Big_Oh s )

proof end;

theorem :: ASYMPT_1:23

for f being Real_Sequence st ( for n being Element of NAT st n > 1 holds

f . n = (n to_power 2) / (log (2,n)) ) holds

ex s being eventually-positive Real_Sequence st

( s = f & Big_Oh s c= Big_Oh (seq_n^ 8) & not Big_Oh s = Big_Oh (seq_n^ 8) )

f . n = (n to_power 2) / (log (2,n)) ) holds

ex s being eventually-positive Real_Sequence st

( s = f & Big_Oh s c= Big_Oh (seq_n^ 8) & not Big_Oh s = Big_Oh (seq_n^ 8) )

proof end;

theorem :: ASYMPT_1:24

for g being Real_Sequence st ( for n being Element of NAT holds g . n = (((n ^2) - n) + 1) to_power 4 ) holds

ex s being eventually-positive Real_Sequence st

( s = g & Big_Oh (seq_n^ 8) = Big_Oh s )

ex s being eventually-positive Real_Sequence st

( s = g & Big_Oh (seq_n^ 8) = Big_Oh s )

proof end;

theorem :: ASYMPT_1:25

for e being Real st 0 < e & e < 1 holds

ex s being eventually-positive Real_Sequence st

( s = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s )

ex s being eventually-positive Real_Sequence st

( s = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s )

proof end;

Lm26: 2 to_power 12 = 4096

proof end;

Lm27: for n being Nat st n >= 3 holds

n ^2 > (2 * n) + 1

proof end;

Lm28: for n being Element of NAT st n >= 10 holds

2 to_power (n - 1) > (2 * n) ^2

proof end;

Lm29: for n being Nat st n >= 9 holds

(n + 1) to_power 6 < 2 * (n to_power 6)

proof end;

Lm30: for n being Element of NAT st n >= 30 holds

2 to_power n > n to_power 6

proof end;

Lm31: for x being Real st x > 9 holds

2 to_power x > (2 * x) ^2

proof end;

Lm32: ex N being Element of NAT st

for n being Element of NAT st n >= N holds

(sqrt n) - (log (2,n)) > 1

proof end;

Lm33: 5 ! = 120

proof end;

Lm34: for n being Element of NAT st n >= 10 holds

(2 to_power (2 * n)) / (n !) < 1 / (2 to_power (n - 9))

proof end;

Lm35: for n being Element of NAT st n >= 3 holds

2 * (n - 2) >= n - 1

proof end;

Lm36: 5 to_power 5 = 3125

proof end;

Lm37: 4 to_power 4 = 256

proof end;

Lm38: for a, b, d, e being Real holds (a / b) / (d / e) = (a / d) * (e / b)

proof end;

Lm39: for x being Real st x >= 0 holds

sqrt x = x to_power (1 / 2)

proof end;

Lm40: ex N being Element of NAT st

for n being Element of NAT st n >= N holds

n - ((sqrt n) * (log (2,n))) > n / 2

proof end;

Lm41: for s being Real_Sequence st ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds

s is V48()

proof end;

Lm42: for n being Element of NAT st n >= 1 holds

((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1)

proof end;

theorem :: ASYMPT_1:26

for f, g being Real_Sequence st ( for n being Element of NAT st n > 0 holds

f . n = n to_power (log (2,n)) ) & ( for n being Element of NAT st n > 0 holds

g . n = n to_power (sqrt n) ) holds

ex s, s1 being eventually-positive Real_Sequence st

( s = f & s1 = g & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )

f . n = n to_power (log (2,n)) ) & ( for n being Element of NAT st n > 0 holds

g . n = n to_power (sqrt n) ) holds

ex s, s1 being eventually-positive Real_Sequence st

( s = f & s1 = g & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )

proof end;

theorem :: ASYMPT_1:27

for f being Real_Sequence st ( for n being Element of NAT st n > 0 holds

f . n = n to_power (sqrt n) ) holds

ex s, s1 being eventually-positive Real_Sequence st

( s = f & s1 = seq_a^ (2,1,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )

f . n = n to_power (sqrt n) ) holds

ex s, s1 being eventually-positive Real_Sequence st

( s = f & s1 = seq_a^ (2,1,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )

proof end;

theorem :: ASYMPT_1:28

ex s, s1 being eventually-positive Real_Sequence st

( s = seq_a^ (2,1,0) & s1 = seq_a^ (2,1,1) & Big_Oh s = Big_Oh s1 )

( s = seq_a^ (2,1,0) & s1 = seq_a^ (2,1,1) & Big_Oh s = Big_Oh s1 )

proof end;

theorem :: ASYMPT_1:29

ex s, s1 being eventually-positive Real_Sequence st

( s = seq_a^ (2,1,0) & s1 = seq_a^ (2,2,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )

( s = seq_a^ (2,1,0) & s1 = seq_a^ (2,2,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )

proof end;

theorem :: ASYMPT_1:30

ex s being eventually-positive Real_Sequence st

( s = seq_a^ (2,2,0) & Big_Oh s c= Big_Oh (seq_n! 0) & not Big_Oh s = Big_Oh (seq_n! 0) )

( s = seq_a^ (2,2,0) & Big_Oh s c= Big_Oh (seq_n! 0) & not Big_Oh s = Big_Oh (seq_n! 0) )

proof end;

theorem :: ASYMPT_1:32

for g being Real_Sequence st ( for n being Element of NAT st n > 0 holds

g . n = n to_power n ) holds

ex s being eventually-positive Real_Sequence st

( s = g & Big_Oh (seq_n! 1) c= Big_Oh s & not Big_Oh (seq_n! 1) = Big_Oh s )

g . n = n to_power n ) holds

ex s being eventually-positive Real_Sequence st

( s = g & Big_Oh (seq_n! 1) c= Big_Oh s & not Big_Oh (seq_n! 1) = Big_Oh s )

proof end;

Lm43: for k, n being Nat st k <= n holds

n choose k >= ((n + 1) choose k) / (n + 1)

proof end;

theorem :: ASYMPT_1:33

for n being Element of NAT st n >= 1 holds

for f being Real_Sequence

for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds

f . n >= (n to_power (k + 1)) / (k + 1)

for f being Real_Sequence

for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum ((seq_n^ k),n) ) holds

f . n >= (n to_power (k + 1)) / (k + 1)

proof end;

Lm44: for f being Real_Sequence st ( for n being Nat holds f . n = log (2,(n !)) ) holds

for n being Element of NAT holds f . n = Sum (seq_logn,n)

proof end;

Lm45: for n being Nat st n >= 4 holds

n * (log (2,n)) >= 2 * n

proof end;

theorem :: ASYMPT_1:34

for f, g being Real_Sequence st ( for n being Element of NAT st n > 0 holds

g . n = n * (log (2,n)) ) & ( for n being Nat holds f . n = log (2,(n !)) ) holds

ex s being eventually-nonnegative Real_Sequence st

( s = g & f in Big_Theta s )

g . n = n * (log (2,n)) ) & ( for n being Nat holds f . n = log (2,(n !)) ) holds

ex s being eventually-nonnegative Real_Sequence st

( s = g & f in Big_Theta s )

proof end;

:: For a "natural" example of an algorithm that would take time in

:: O(t(n)), consider a naive algorithm that tries to find at least one

:: factor of a given Nat. For all even numbers, the task is trivial,

:: and for all odd numbers, the algorithm might try dividing the number by all

:: numbers smaller than it, giving a running time of n.

:: O(t(n)), consider a naive algorithm that tries to find at least one

:: factor of a given Nat. For all even numbers, the task is trivial,

:: and for all odd numbers, the algorithm might try dividing the number by all

:: numbers smaller than it, giving a running time of n.

theorem :: ASYMPT_1:35

for f being eventually-nonnegative eventually-nondecreasing Real_Sequence

for t being Real_Sequence st ( for n being Element of NAT holds

( ( n mod 2 = 0 implies t . n = 1 ) & ( n mod 2 = 1 implies t . n = n ) ) ) holds

not t in Big_Theta f

for t being Real_Sequence st ( for n being Element of NAT holds

( ( n mod 2 = 0 implies t . n = 1 ) & ( n mod 2 = 1 implies t . n = n ) ) ) holds

not t in Big_Theta f

proof end;

Lm46: for n being Nat st n >= 2 holds

[/(n / 2)\] < n

proof end;

definition

{ (2 to_power n) where n is Element of NAT : verum } is non empty Subset of NAT
end;

func POWEROF2SET -> non empty Subset of NAT equals :: ASYMPT_1:def 6

{ (2 to_power n) where n is Element of NAT : verum } ;

coherence { (2 to_power n) where n is Element of NAT : verum } ;

{ (2 to_power n) where n is Element of NAT : verum } is non empty Subset of NAT

proof end;

:: deftheorem defines POWEROF2SET ASYMPT_1:def 6 :

POWEROF2SET = { (2 to_power n) where n is Element of NAT : verum } ;

POWEROF2SET = { (2 to_power n) where n is Element of NAT : verum } ;

Lm47: for n being Nat st n >= 2 holds

n ^2 > n + 1

proof end;

Lm48: for n being Nat st n >= 1 holds

(2 to_power (n + 1)) - (2 to_power n) > 1

proof end;

Lm49: for n being Nat st n >= 2 holds

not (2 to_power n) - 1 in POWEROF2SET

proof end;

theorem :: ASYMPT_1:36

for f being Real_Sequence st ( for n being Element of NAT holds

( ( n in POWEROF2SET implies f . n = n ) & ( not n in POWEROF2SET implies f . n = 2 to_power n ) ) ) holds

( f in Big_Theta ((seq_n^ 1),POWEROF2SET) & not f in Big_Theta (seq_n^ 1) & seq_n^ 1 is smooth & not f is eventually-nondecreasing )

( ( n in POWEROF2SET implies f . n = n ) & ( not n in POWEROF2SET implies f . n = 2 to_power n ) ) ) holds

( f in Big_Theta ((seq_n^ 1),POWEROF2SET) & not f in Big_Theta (seq_n^ 1) & seq_n^ 1 is smooth & not f is eventually-nondecreasing )

proof end;

theorem :: ASYMPT_1:37

for f, g being Real_Sequence st ( for n being Element of NAT st n > 0 holds

f . n = n to_power (2 to_power [\(log (2,n))/]) ) & ( for n being Element of NAT st n > 0 holds

g . n = n to_power n ) holds

ex s being eventually-positive Real_Sequence st

( s = g & f in Big_Theta (s,POWEROF2SET) & not f in Big_Theta s & f is eventually-nondecreasing & s is eventually-nondecreasing & not s is_smooth_wrt 2 )

f . n = n to_power (2 to_power [\(log (2,n))/]) ) & ( for n being Element of NAT st n > 0 holds

g . n = n to_power n ) holds

ex s being eventually-positive Real_Sequence st

( s = g & f in Big_Theta (s,POWEROF2SET) & not f in Big_Theta s & f is eventually-nondecreasing & s is eventually-nondecreasing & not s is_smooth_wrt 2 )

proof end;

theorem :: ASYMPT_1:38

for g being Real_Sequence st ( for n being Element of NAT holds

( ( n in POWEROF2SET implies g . n = n ) & ( not n in POWEROF2SET implies g . n = n to_power 2 ) ) ) holds

ex s being eventually-positive Real_Sequence st

( s = g & seq_n^ 1 in Big_Theta (s,POWEROF2SET) & not seq_n^ 1 in Big_Theta s & s taken_every 2 in Big_Oh s & seq_n^ 1 is eventually-nondecreasing & not s is eventually-nondecreasing )

( ( n in POWEROF2SET implies g . n = n ) & ( not n in POWEROF2SET implies g . n = n to_power 2 ) ) ) holds

ex s being eventually-positive Real_Sequence st

( s = g & seq_n^ 1 in Big_Theta (s,POWEROF2SET) & not seq_n^ 1 in Big_Theta s & s taken_every 2 in Big_Oh s & seq_n^ 1 is eventually-nondecreasing & not s is eventually-nondecreasing )

proof end;

Lm50: for n being Nat st n >= 2 holds

n ! > 1

proof end;

Lm51: for n1, n being Nat st n <= n1 holds

n ! <= n1 !

proof end;

Lm52: for k being Element of NAT st k >= 1 holds

ex n being Element of NAT st

( n ! <= k & k < (n + 1) ! & ( for m being Element of NAT st m ! <= k & k < (m + 1) ! holds

m = n ) )

proof end;

definition

let x be Nat;

for b_{1} being Element of NAT holds verum
;

existence

( ( x <> 0 implies ex b_{1}, n being Element of NAT st

( n ! <= x & x < (n + 1) ! & b_{1} = n ! ) ) & ( not x <> 0 implies ex b_{1} being Element of NAT st b_{1} = 0 ) )

for b_{1}, b_{2} being Element of NAT holds

( ( x <> 0 & ex n being Element of NAT st

( n ! <= x & x < (n + 1) ! & b_{1} = n ! ) & ex n being Element of NAT st

( n ! <= x & x < (n + 1) ! & b_{2} = n ! ) implies b_{1} = b_{2} ) & ( not x <> 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

end;
func Step1 x -> Element of NAT means :Def6: :: ASYMPT_1:def 7

ex n being Element of NAT st

( n ! <= x & x < (n + 1) ! & it = n ! ) if x <> 0

otherwise it = 0 ;

consistency ex n being Element of NAT st

( n ! <= x & x < (n + 1) ! & it = n ! ) if x <> 0

otherwise it = 0 ;

for b

existence

( ( x <> 0 implies ex b

( n ! <= x & x < (n + 1) ! & b

proof end;

uniqueness for b

( ( x <> 0 & ex n being Element of NAT st

( n ! <= x & x < (n + 1) ! & b

( n ! <= x & x < (n + 1) ! & b

proof end;

:: deftheorem Def6 defines Step1 ASYMPT_1:def 7 :

for x being Nat

for b_{2} being Element of NAT holds

( ( x <> 0 implies ( b_{2} = Step1 x iff ex n being Element of NAT st

( n ! <= x & x < (n + 1) ! & b_{2} = n ! ) ) ) & ( not x <> 0 implies ( b_{2} = Step1 x iff b_{2} = 0 ) ) );

for x being Nat

for b

( ( x <> 0 implies ( b

( n ! <= x & x < (n + 1) ! & b

Lm53: for n being Nat st n >= 3 holds

n ! > n

proof end;

theorem :: ASYMPT_1:39

for f being Real_Sequence st ( for n being Element of NAT holds f . n = Step1 n ) holds

ex s being eventually-positive Real_Sequence st

( s = f & not s is smooth & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing )

ex s being eventually-positive Real_Sequence st

( s = f & not s is smooth & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing )

proof end;

Lm54: (seq_n^ 1) - (seq_const 1) is eventually-positive

proof end;

:: This is to show that Big_Theta(n-1) + Big_Theta(n) = Big_Theta(n).

:: Note that it is not true that Big_Theta(n) = Big_Theta(n) - Big_Theta(n-1).

:: Consider n and n. The function n - n = 0, which is not in Big_Theta(n).

:: Note that it is not true that Big_Theta(n) = Big_Theta(n) - Big_Theta(n-1).

:: Consider n and n. The function n - n = 0, which is not in Big_Theta(n).

theorem :: ASYMPT_1:40

for F being eventually-nonnegative Real_Sequence st F = (seq_n^ 1) - (seq_const 1) holds

(Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1)

(Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1)

proof end;

theorem :: ASYMPT_1:41

ex F being FUNCTION_DOMAIN of NAT , REAL st

( F = {(seq_n^ 1)} & ( for n being Element of NAT holds (seq_n^ (- 1)) . n <= (seq_n^ 1) . n ) & not seq_n^ (- 1) in F to_power (Big_Oh (seq_const 1)) )

( F = {(seq_n^ 1)} & ( for n being Element of NAT holds (seq_n^ (- 1)) . n <= (seq_n^ 1) . n ) & not seq_n^ (- 1) in F to_power (Big_Oh (seq_const 1)) )

proof end;

:: In theorem ASYMPT_0:14, if we restrict our attentions to functions that

:: do not have a subsequence that converges to 0, then the reverse implication

:: is true.

:: do not have a subsequence that converges to 0, then the reverse implication

:: is true.

theorem :: ASYMPT_1:42

for c being non negative Real

for x, f being eventually-nonnegative Real_Sequence st ex e being Real ex N being Element of NAT st

( e > 0 & ( for n being Element of NAT st n >= N holds

f . n >= e ) ) & x in Big_Oh (c + f) holds

x in Big_Oh f

for x, f being eventually-nonnegative Real_Sequence st ex e being Real ex N being Element of NAT st

( e > 0 & ( for n being Element of NAT st n >= N holds

f . n >= e ) ) & x in Big_Oh (c + f) holds

x in Big_Oh f

proof end;

theorem :: ASYMPT_1:45

theorem :: ASYMPT_1:46

theorem :: ASYMPT_1:47

theorem :: ASYMPT_1:49

theorem :: ASYMPT_1:50

theorem :: ASYMPT_1:57

theorem :: ASYMPT_1:62

theorem :: ASYMPT_1:63

for f, g being eventually-nonnegative Real_Sequence holds

( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g ) by Lm5;

( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g ) by Lm5;

theorem :: ASYMPT_1:64

theorem :: ASYMPT_1:65

theorem :: ASYMPT_1:68

theorem :: ASYMPT_1:69

theorem :: ASYMPT_1:70

theorem :: ASYMPT_1:71

theorem :: ASYMPT_1:72

theorem :: ASYMPT_1:73

theorem :: ASYMPT_1:74

theorem :: ASYMPT_1:76

theorem :: ASYMPT_1:77

theorem :: ASYMPT_1:79

theorem :: ASYMPT_1:80

theorem :: ASYMPT_1:81

theorem :: ASYMPT_1:84

:: The proof of this theorem has been taken directly from the

:: article POWER.miz (with very slight modifications to fit this new theorem).

:: article POWER.miz (with very slight modifications to fit this new theorem).

theorem :: ASYMPT_1:85

:: (1 + 1/n)^n is non-decreasing

theorem :: ASYMPT_1:86

theorem :: ASYMPT_1:87

theorem :: ASYMPT_1:88

theorem :: ASYMPT_1:91

theorem :: ASYMPT_1:92

theorem :: ASYMPT_1:93

theorem :: ASYMPT_1:94