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 )