let e be Real; :: thesis: for g being Real_Sequence st 0 < e & e < 1 & g . 0 = 0 & g . 1 = 0 & ( 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 )
let g be Real_Sequence; :: thesis: ( 0 < e & e < 1 & g . 0 = 0 & g . 1 = 0 & ( for n being Element of NAT st n > 1 holds
g . n = (n to_power 2) / (log 2,n) ) implies 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 ) )
assume that
0 < e and
A1: e < 1 and
A2: ( g . 0 = 0 & g . 1 = 0 & ( for n being Element of NAT st n > 1 holds
g . n = (n to_power 2) / (log 2,n) ) ) ; :: thesis: 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 )
set f = seq_n^ (1 + e);
set h = (seq_n^ (1 + e)) /" g;
set seq = seq_logn ;
set seq1 = seq_n^ (1 - e);
set p = seq_logn /" (seq_n^ (1 - e));
g 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 g . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 2 <= n or not g . n <= 0 )
assume A3: n >= 2 ; :: thesis: not g . n <= 0
then n > 1 by XXREAL_0:2;
then A4: g . n = (n to_power 2) / (log 2,n) by A2
.= (n to_power 2) * ((log 2,n) " ) ;
A5: n to_power 2 > 0 by A3, POWER:39;
log 2,n >= log 2,2 by A3, 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 A5, XREAL_1:70;
hence not g . n <= 0 by A4; :: thesis: verum

end;

then reconsider g = g as eventually-positive Real_Sequence ;
take g ; :: thesis: ( g = g & Big_Oh (seq_n^ (1 + e)) c= Big_Oh g & not Big_Oh (seq_n^ (1 + e)) = Big_Oh g )
0 + e < 1 by A1;
then 0 < 1 - e by XREAL_1:22;
then A6: ( seq_logn /" (seq_n^ (1 - e)) is convergent & lim (seq_logn /" (seq_n^ (1 - e))) = 0 ) by Lm16;
A7: (1 + e) - 2 = e - 1 ;
for n being Element of NAT st n >= 2 holds
((seq_n^ (1 + e)) /" g) . n = (seq_logn /" (seq_n^ (1 - e))) . n

proof

let n be Element of NAT ; :: thesis: ( n >= 2 implies ((seq_n^ (1 + e)) /" g) . n = (seq_logn /" (seq_n^ (1 - e))) . n )
assume A8: n >= 2 ; :: thesis: ((seq_n^ (1 + e)) /" g) . n = (seq_logn /" (seq_n^ (1 - e))) . n
then A9: n > 1 by XXREAL_0:2;
((seq_n^ (1 + e)) /" g) . n = ((seq_n^ (1 + e)) . n) / (g . n) by Lm4
.= (n to_power (1 + e)) / (g . n) by A8, Def3
.= (n to_power (1 + e)) / ((n to_power 2) / (log 2,n)) by A2, A9
.= (n to_power (1 + e)) * (((n to_power 2) / (log 2,n)) " )
.= (n to_power (1 + e)) * ((log 2,n) / (n to_power 2)) by XCMPLX_1:215
.= (n to_power (1 + e)) * ((log 2,n) * ((n to_power 2) " ))
.= ((n to_power (1 + e)) * ((n to_power 2) " )) * (log 2,n)
.= ((n to_power (1 + e)) / (n to_power 2)) * (log 2,n)
.= (n to_power (- (1 - e))) * (log 2,n) by A7, A8, POWER:34
.= (log 2,n) * (1 / (n to_power (1 - e))) by A8, POWER:33
.= (log 2,n) / (n to_power (1 - e))
.= (seq_logn . n) / (n to_power (1 - e)) by A8, Def2
.= (seq_logn . n) / ((seq_n^ (1 - e)) . n) by A8, Def3
.= (seq_logn /" (seq_n^ (1 - e))) . n by Lm4 ;
hence ((seq_n^ (1 + e)) /" g) . n = (seq_logn /" (seq_n^ (1 - e))) . n ; :: thesis: verum

end;

then ( (seq_n^ (1 + e)) /" g is convergent & lim ((seq_n^ (1 + e)) /" g) = 0 ) by A6, Lm28;
then ( seq_n^ (1 + e) in Big_Oh g & not g in Big_Oh (seq_n^ (1 + e)) ) by ASYMPT_0:16;
then ( seq_n^ (1 + e) in Big_Oh g & not seq_n^ (1 + e) in Big_Omega g ) by ASYMPT_0:19;
hence ( g = g & Big_Oh (seq_n^ (1 + e)) c= Big_Oh g & not Big_Oh (seq_n^ (1 + e)) = Big_Oh g ) by Th4; :: thesis: verum