set seq = seq_logn ;
let e be Real; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: 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

proof

take 2 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being set holds
( not 2 <= b₁ or not f . b₁ <= 0 )
let n be Nat; :: thesis: ( not 2 <= n or not f . n <= 0 )
A4: n in NAT by ORDINAL1:def 12;
assume A5: n >= 2 ; :: thesis: not f . n <= 0
then log (2,n) >= log (2,2) by PRE_FF:10;
then log (2,n) >= 1 by POWER:52;
then n * (log (2,n)) > n * 0 by A5, XREAL_1:68;
hence not f . n <= 0 by A2, A5, A4; :: thesis: verum

end;

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 ; :: thesis: ( n >= 1 implies (f /" (seq_n^ (1 + e))) . n = (seq_logn /" (seq_n^ e)) . n )
assume A7: n >= 1 ; :: thesis: (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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum