set seq = seq_logn ;
let e be 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)) )
let f be Real_Sequence; ( 0 < e & ( for n being Element of NAT st n > 0 holds
f . n = n * (log (2,n)) ) implies 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)) ) )
assume that
A1:
0 < e
and
A2:
for n being Element of NAT st n > 0 holds
f . n = n * (log (2,n))
; 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)) )
set seq1 = seq_n^ e;
set p = seq_logn /" (seq_n^ e);
A3:
lim (seq_logn /" (seq_n^ e)) = 0
by A1, Lm11;
f is eventually-positive
then reconsider f = f as eventually-positive Real_Sequence ;
set g = seq_n^ (1 + e);
set h = f /" (seq_n^ (1 + e));
A6:
for n being Element of NAT st n >= 1 holds
(f /" (seq_n^ (1 + e))) . n = (seq_logn /" (seq_n^ e)) . n
proof
let n be
Element of
NAT ;
( n >= 1 implies (f /" (seq_n^ (1 + e))) . n = (seq_logn /" (seq_n^ e)) . n )
assume A7:
n >= 1
;
(f /" (seq_n^ (1 + e))) . n = (seq_logn /" (seq_n^ e)) . n
(f /" (seq_n^ (1 + e))) . n =
(f . n) / ((seq_n^ (1 + e)) . n)
by Lm4
.=
(n * (log (2,n))) / ((seq_n^ (1 + e)) . n)
by A2, A7
.=
(n * (log (2,n))) / (n to_power (1 + e))
by A7, Def3
.=
((n to_power 1) * (log (2,n))) / (n to_power (1 + e))
by POWER:25
.=
((n to_power 1) * (log (2,n))) * ((n to_power (1 + e)) ")
.=
(log (2,n)) * ((n to_power 1) * ((n to_power (1 + e)) "))
.=
(log (2,n)) * ((n to_power 1) / (n to_power (1 + e)))
.=
(log (2,n)) * (n to_power (1 - (1 + e)))
by A7, POWER:29
.=
(log (2,n)) * (n to_power (1 + ((- 1) + (- e))))
.=
(log (2,n)) * (1 / (n to_power e))
by A7, POWER:28
.=
(log (2,n)) / (n to_power e)
.=
(seq_logn . n) / (n to_power e)
by A7, Def2
.=
(seq_logn . n) / ((seq_n^ e) . n)
by A7, Def3
.=
(seq_logn /" (seq_n^ e)) . n
by Lm4
;
hence
(f /" (seq_n^ (1 + e))) . n = (seq_logn /" (seq_n^ e)) . n
;
verum
end;
A8:
seq_logn /" (seq_n^ e) is convergent
by A1, Lm11;
then A9:
lim (f /" (seq_n^ (1 + e))) = 0
by A3, A6, Lm22;
A10:
f /" (seq_n^ (1 + e)) is convergent
by A8, A3, A6, Lm22;
then
not seq_n^ (1 + e) in Big_Oh f
by A9, ASYMPT_0:16;
then A11:
not f in Big_Omega (seq_n^ (1 + e))
by ASYMPT_0:19;
take
f
; ( f = f & Big_Oh f c= Big_Oh (seq_n^ (1 + e)) & not Big_Oh f = Big_Oh (seq_n^ (1 + e)) )
f in Big_Oh (seq_n^ (1 + e))
by A10, A9, ASYMPT_0:16;
hence
( f = f & Big_Oh f c= Big_Oh (seq_n^ (1 + e)) & not Big_Oh f = Big_Oh (seq_n^ (1 + e)) )
by A11, Th4; verum