let f be Real_Sequence; :: thesis: ( f . 0 = 0 & f . 1 = 0 & ( for n being Element of NAT st n > 1 holds
f . n = (n to_power 2) / (log 2,n) ) implies ex s being eventually-positive Real_Sequence st
( s = f & Big_Oh s c= Big_Oh (seq_n^ 8) & not Big_Oh s = Big_Oh (seq_n^ 8) ) )
assume A1: ( f . 0 = 0 & f . 1 = 0 & ( for n being Element of NAT st n > 1 holds
f . n = (n to_power 2) / (log 2,n) ) ) ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = f & Big_Oh s c= Big_Oh (seq_n^ 8) & not Big_Oh s = Big_Oh (seq_n^ 8) )
set g = seq_n^ 8;
set h = f /" (seq_n^ 8);
f is eventually-positive

proof

take 2 ; :: according to ASYMPT_0:def 6 :: thesis: for b₁ being Element of NAT holds
( not 2 <= b₁ or not f . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 2 <= n or not f . n <= 0 )
assume A2: n >= 2 ; :: thesis: not f . n <= 0
then n > 1 by XXREAL_0:2;
then A3: f . n = (n to_power 2) / (log 2,n) by A1
.= (n to_power 2) * ((log 2,n) " ) ;
A4: n to_power 2 > 0 by A2, POWER:39;
log 2,n >= log 2,2 by A2, PRE_FF:12;
then log 2,n >= 1 by POWER:60;
then (log 2,n) " > 0 ;
then (n to_power 2) * ((log 2,n) " ) > (n to_power 2) * 0 by A4, XREAL_1:70;
hence not f . n <= 0 by A3; :: thesis: verum

end;

then reconsider f = f as eventually-positive Real_Sequence ;
take f ; :: thesis: ( f = f & Big_Oh f c= Big_Oh (seq_n^ 8) & not Big_Oh f = Big_Oh (seq_n^ 8) )

A5: now

let p be real number ; :: thesis: ( p > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ 8)) . n) - 0 ) < p )
assume A6: p > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ 8)) . n) - 0 ) < p
reconsider p1 = p as Real by XREAL_0:def 1;
set N = max 3,[/(p1 to_power (- (1 / 6)))\];
A7: ( max 3,[/(p1 to_power (- (1 / 6)))\] >= 3 & max 3,[/(p1 to_power (- (1 / 6)))\] >= [/(p to_power (- (1 / 6)))\] ) by XXREAL_0:25;
max 3,[/(p1 to_power (- (1 / 6)))\] is Integer by XXREAL_0:16;
then reconsider N = max 3,[/(p1 to_power (- (1 / 6)))\] as Element of NAT by A7, INT_1:16;
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ 8)) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N implies abs (((f /" (seq_n^ 8)) . n) - 0 ) < p )
assume A8: n >= N ; :: thesis: abs (((f /" (seq_n^ 8)) . n) - 0 ) < p
then A9: ( n >= 3 & n >= [/(p to_power (- (1 / 6)))\] ) by A7, XXREAL_0:2;
then A10: log 2,n >= log 2,3 by PRE_FF:12;
log 2,3 > log 2,2 by POWER:65;
then log 2,n > log 2,2 by A10, XXREAL_0:2;
then A11: log 2,n > 1 by POWER:60;
A12: n > 1 by A9, XXREAL_0:2;
A13: n to_power 6 > 0 by A7, A8, POWER:39;
A14: (f /" (seq_n^ 8)) . n = (f . n) / ((seq_n^ 8) . n) by Lm4
.= ((n to_power 2) / (log 2,n)) / ((seq_n^ 8) . n) by A1, A12
.= ((n to_power 2) / (log 2,n)) / (n to_power 8) by A7, A8, Def3
.= ((n to_power 2) * ((log 2,n) " )) / (n to_power 8)
.= (((log 2,n) " ) * (n to_power 2)) * ((n to_power 8) " )
.= ((log 2,n) " ) * ((n to_power 2) * ((n to_power 8) " ))
.= ((log 2,n) " ) * ((n to_power 2) / (n to_power 8))
.= ((log 2,n) " ) * (n to_power (2 - 8)) by A7, A8, POWER:34
.= ((log 2,n) " ) * (n to_power (- 6))
.= ((log 2,n) " ) * (1 / (n to_power 6)) by A7, A8, POWER:33
.= (1 / (n to_power 6)) * (1 / (log 2,n))
.= 1 / ((n to_power 6) * (log 2,n)) by XCMPLX_1:103 ;
(n to_power 6) * 1 < (n to_power 6) * (log 2,n) by A11, A13, XREAL_1:70;
then A15: (f /" (seq_n^ 8)) . n < 1 / (n to_power 6) by A13, A14, XREAL_1:90;
A16: p1 to_power (- (1 / 6)) > 0 by A6, POWER:39;
[/(p to_power (- (1 / 6)))\] >= p to_power (- (1 / 6)) by INT_1:def 5;
then n >= p to_power (- (1 / 6)) by A9, XXREAL_0:2;
then n to_power 6 >= (p to_power (- (1 / 6))) to_power 6 by A16, Lm6;
then A17: n to_power 6 >= p1 to_power ((- (1 / 6)) * 6) by A6, POWER:38;
p1 to_power (- 1) > 0 by A6, POWER:39;
then 1 / (n to_power 6) <= 1 / (p to_power (- 1)) by A17, XREAL_1:87;
then 1 / (n to_power 6) <= 1 / (1 / (p1 to_power 1)) by A6, POWER:33;
then 1 / (n to_power 6) <= 1 / (1 / p1) by POWER:30;
then 1 / (n to_power 6) <= p ;
then A18: (f /" (seq_n^ 8)) . n < p by A15, XXREAL_0:2;
(n to_power 6) * (log 2,n) > (n to_power 6) * 0 by A11, A13, XREAL_1:70;
then ((n to_power 6) * (log 2,n)) " > 0 ;
then (f /" (seq_n^ 8)) . n > 0 by A14;
hence abs (((f /" (seq_n^ 8)) . n) - 0 ) < p by A18, ABSVALUE:def 1; :: thesis: verum

end;

then A19: f /" (seq_n^ 8) is convergent by SEQ_2:def 6;
then lim (f /" (seq_n^ 8)) = 0 by A5, SEQ_2:def 7;
then ( f in Big_Oh (seq_n^ 8) & not seq_n^ 8 in Big_Oh f ) by A19, ASYMPT_0:16;
then ( f in Big_Oh (seq_n^ 8) & not f in Big_Omega (seq_n^ 8) ) by ASYMPT_0:19;
hence ( f = f & Big_Oh f c= Big_Oh (seq_n^ 8) & not Big_Oh f = Big_Oh (seq_n^ 8) ) by Th4; :: thesis: verum