set seq = seq_logn ;
let e be Real; :: thesis: 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 )
let g be Real_Sequence; :: thesis: ( e < 1 & ( 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
A1: e < 1 and
A2: 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 seq1 = seq_n^ (1 - e);
set p = seq_logn /" (seq_n^ (1 - e));
set f = seq_n^ (1 + e);
set h = (seq_n^ (1 + e)) /" g;
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 log 2,n >= log 2,2 by PRE_FF:12;
then A4: log 2,n >= 1 by POWER:60;
n > 1 by A3, XXREAL_0:2;
then A5: g . n = (n to_power 2) / (log 2,n) by A2
.= (n to_power 2) * ((log 2,n) " ) ;
n to_power 2 > 0 by A3, POWER:39;
then (n to_power 2) * ((log 2,n) " ) > (n to_power 2) * 0 by A4, XREAL_1:70;
hence not g . n <= 0 by A5; :: thesis: verum

end;

then reconsider g = g as eventually-positive Real_Sequence ;
A6: (1 + e) - 2 = e - 1 ;
A7: 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 A6, 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;

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 A10: 0 < 1 - e by XREAL_1:22;
then A11: seq_logn /" (seq_n^ (1 - e)) is convergent by Lm11;
A12: lim (seq_logn /" (seq_n^ (1 - e))) = 0 by A10, Lm11;
then A13: lim ((seq_n^ (1 + e)) /" g) = 0 by A11, A7, Lm22;
A14: (seq_n^ (1 + e)) /" g is convergent by A11, A12, A7, Lm22;
then not g in Big_Oh (seq_n^ (1 + e)) by A13, ASYMPT_0:16;
then A15: not seq_n^ (1 + e) in Big_Omega g by ASYMPT_0:19;
seq_n^ (1 + e) in Big_Oh g by A14, A13, ASYMPT_0:16;
hence ( g = g & Big_Oh (seq_n^ (1 + e)) c= Big_Oh g & not Big_Oh (seq_n^ (1 + e)) = Big_Oh g ) by A15, Th4; :: thesis: verum