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