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 4 :: 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:10;
then A4: log (2,n) >= 1 by POWER:52;
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:34;
then (n to_power 2) * ((log (2,n)) ") > (n to_power 2) * 0 by A4, XREAL_1:68;
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:213
.= (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:29
.= (log (2,n)) * (1 / (n to_power (1 - e))) by A8, POWER:28
.= (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:20;
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