:: Asymptotic notation. Part II: Examples and Problems
:: by Richard Krueger, Piotr Rudnicki and Paul Shelley
::
:: Received November 4, 1999
:: Copyright (c) 1999 Association of Mizar Users
Lm1:
for n being Nat st n >= 2 holds
2 to_power n > n + 1
theorem :: ASYMPT_1:1
Lm2:
for a being logbase Real
for f being Real_Sequence st a > 1 & f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log a,n ) holds
f is eventually-positive
theorem :: ASYMPT_1:2
:: deftheorem Def1 defines seq_a^ ASYMPT_1:def 1 :
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))
theorem :: ASYMPT_1:3
:: deftheorem Def2 defines seq_logn ASYMPT_1:def 2 :
:: deftheorem Def3 defines seq_n^ ASYMPT_1:def 3 :
Lm4:
for f, g being Real_Sequence
for n being Element of NAT holds (f /" g) . n = (f . n) / (g . n)
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 )
theorem Th4: :: ASYMPT_1:4
Lm6:
for a, b, c being real number st 0 < a & a <= b & c >= 0 holds
a to_power c <= b to_power c
Lm8:
2 to_power 3 = 8
by POWER:69;
Lm9:
2 to_power 4 = 16
by POWER:70;
Lm10:
2 to_power 5 = 32
by POWER:71;
Lm11:
2 to_power 6 = 64
by POWER:72;
Lm12:
for n being Nat st n >= 4 holds
(2 * n) + 3 < 2 to_power n
Lm13:
for n being Element of NAT st n >= 6 holds
(n + 1) ^2 < 2 to_power n
Lm14:
for c being Real st c > 6 holds
c ^2 < 2 to_power c
Lm15:
for e being positive Real
for f being Real_Sequence st f . 0 = 0 & ( 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 )
Lm16:
for e being Real st e > 0 holds
( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 )
theorem Th5: :: ASYMPT_1:5
theorem :: ASYMPT_1:6
Lm17:
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
Lm18:
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
Lm19:
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
Lm20:
for f being Real_Sequence
for N, M being Nat holds (Sum f,N,M) + (f . (N + 1)) = Sum f,(N + 1),M
Lm21:
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
Lm22:
for n being Element of NAT holds [/(n / 2)\] <= n
Lm23:
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)
theorem :: ASYMPT_1:7
theorem :: ASYMPT_1:8
:: deftheorem defines seq_const ASYMPT_1:def 4 :
Lm24:
for a, b, c being Real st a > 1 & b >= a & c >= 1 holds
log a,c >= log b,c
theorem Th9: :: ASYMPT_1:9
theorem :: ASYMPT_1:10
theorem :: ASYMPT_1:11
theorem :: ASYMPT_1:12
theorem :: ASYMPT_1:13
:: deftheorem Def5 defines seq_n! ASYMPT_1:def 5 :
theorem :: ASYMPT_1:14
theorem :: ASYMPT_1:15
theorem :: ASYMPT_1:16
theorem :: ASYMPT_1:17
theorem :: ASYMPT_1:18
theorem :: ASYMPT_1:19
theorem :: ASYMPT_1:20
Lm27:
for n being Element of NAT holds ((n ^2 ) - n) + 1 > 0
Lm28:
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 )
Lm29:
for n being Element of NAT st n >= 1 holds
((n ^2 ) - n) + 1 <= n ^2
Lm30:
for n being Element of NAT st n >= 1 holds
n ^2 <= 2 * (((n ^2 ) - n) + 1)
Lm31:
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)
theorem :: ASYMPT_1:21
theorem :: ASYMPT_1:22
theorem :: ASYMPT_1:23
theorem :: ASYMPT_1:24
theorem :: ASYMPT_1:25
Lm32:
2 to_power 12 = 4096
Lm33:
for n being Nat st n >= 3 holds
n ^2 > (2 * n) + 1
Lm34:
for n being Element of NAT st n >= 10 holds
2 to_power (n - 1) > (2 * n) ^2
Lm35:
for n being Nat st n >= 9 holds
(n + 1) to_power 6 < 2 * (n to_power 6)
Lm36:
for n being Element of NAT st n >= 30 holds
2 to_power n > n to_power 6
Lm37:
for x being Real st x > 9 holds
2 to_power x > (2 * x) ^2
Lm38:
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(sqrt n) - (log 2,n) > 1
Lm39:
(4 + 1) ! = 120
Lm40:
for n being Element of NAT st n >= 10 holds
(2 to_power (2 * n)) / (n ! ) < 1 / (2 to_power (n - 9))
Lm41:
for n being Element of NAT st n >= 3 holds
2 * (n - 2) >= n - 1
Lm42:
5 to_power 5 = 3125
Lm43:
4 to_power 4 = 256
Lm44:
for a, b, d, e being Real holds (a / b) / (d / e) = (a / d) * (e / b)
Lm45:
for x being real number st x >= 0 holds
sqrt x = x to_power (1 / 2)
Lm46:
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
Lm47:
for s being Real_Sequence st ( for n being Element of NAT holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) holds
s is non-decreasing
Lm48:
for n being Element of NAT st n >= 1 holds
((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1)
theorem :: ASYMPT_1:26
theorem :: ASYMPT_1:27
theorem :: ASYMPT_1:28
theorem :: ASYMPT_1:29
theorem :: ASYMPT_1:30
theorem :: ASYMPT_1:31
theorem :: ASYMPT_1:32
Lm49:
for k, n being Element of NAT st k <= n holds
n choose k >= ((n + 1) choose k) / (n + 1)
theorem :: ASYMPT_1:33
Lm50:
for f being Real_Sequence st ( for n being Element of NAT holds f . n = log 2,(n ! ) ) holds
for n being Element of NAT holds f . n = Sum seq_logn ,n
Lm51:
for n being Element of NAT st n >= 4 holds
n * (log 2,n) >= 2 * n
theorem :: ASYMPT_1:34
theorem :: ASYMPT_1:35
Lm53:
for n being Element of NAT st n >= 2 holds
[/(n / 2)\] < n
:: deftheorem ASYMPT_1:def 6 :
canceled;
:: deftheorem ASYMPT_1:def 7 :
canceled;
:: deftheorem defines POWEROF2SET ASYMPT_1:def 8 :
Lm55:
for n being Element of NAT st n >= 2 holds
n ^2 > n + 1
Lm56:
for n being Element of NAT st n >= 1 holds
(2 to_power (n + 1)) - (2 to_power n) > 1
Lm57:
for n being Element of NAT st n >= 2 holds
not (2 to_power n) - 1 in POWEROF2SET
theorem :: ASYMPT_1:36
canceled;
theorem :: ASYMPT_1:37
theorem :: ASYMPT_1:38
theorem :: ASYMPT_1:39
Lm58:
for n being Element of NAT st n >= 2 holds
n ! > 1
Lm59:
for n1, n being Element of NAT st n <= n1 holds
n ! <= n1 !
Lm60:
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 ) )
:: deftheorem Def9 defines Step1 ASYMPT_1:def 9 :
Lm61:
for n being Element of NAT st n >= 3 holds
n ! > n
theorem :: ASYMPT_1:40
Lm62:
(seq_n^ 1) - (seq_const 1) is eventually-positive
theorem :: ASYMPT_1:41
theorem :: ASYMPT_1:42
theorem :: ASYMPT_1:43
theorem :: ASYMPT_1:44
canceled;
theorem :: ASYMPT_1:45
canceled;
theorem :: ASYMPT_1:46
canceled;
theorem :: ASYMPT_1:47
canceled;
theorem :: ASYMPT_1:48
canceled;
theorem :: ASYMPT_1:49
theorem :: ASYMPT_1:50
theorem :: ASYMPT_1:51
theorem :: ASYMPT_1:52
theorem :: ASYMPT_1:53
theorem :: ASYMPT_1:54
theorem :: ASYMPT_1:55
theorem :: ASYMPT_1:56
theorem :: ASYMPT_1:57
theorem :: ASYMPT_1:58
theorem :: ASYMPT_1:59
theorem :: ASYMPT_1:60
theorem :: ASYMPT_1:61
theorem :: ASYMPT_1:62
theorem :: ASYMPT_1:63
theorem :: ASYMPT_1:64
theorem :: ASYMPT_1:65
theorem :: ASYMPT_1:66
theorem :: ASYMPT_1:67
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:75
theorem :: ASYMPT_1:76
theorem :: ASYMPT_1:77
theorem :: ASYMPT_1:78
theorem :: ASYMPT_1:79
theorem :: ASYMPT_1:80
theorem :: ASYMPT_1:81
theorem :: ASYMPT_1:82
theorem :: ASYMPT_1:83
theorem :: ASYMPT_1:84
theorem :: ASYMPT_1:85
theorem :: ASYMPT_1:86
theorem :: ASYMPT_1:87
theorem :: ASYMPT_1:88
theorem :: ASYMPT_1:89
theorem :: ASYMPT_1:90
theorem :: ASYMPT_1:91
theorem :: ASYMPT_1:92
theorem :: ASYMPT_1:93
theorem :: ASYMPT_1:94
theorem :: ASYMPT_1:95
theorem :: ASYMPT_1:96
canceled;
theorem :: ASYMPT_1:97
theorem :: ASYMPT_1:98
theorem :: ASYMPT_1:99
theorem :: ASYMPT_1:100
theorem :: ASYMPT_1:101