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

proof

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

end;

then reconsider f = f as eventually-positive Real_Sequence ;
g is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 6 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not g . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not g . n <= 0 )
assume A4: n >= 1 ; :: thesis: not g . n <= 0
then g . n = n to_power (sqrt n) by A2;
hence not g . n <= 0 by A4, POWER:39; :: thesis: verum

end;

then reconsider g = g as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = f & s1 = g & Big_Oh f c= Big_Oh s1 & not Big_Oh f = Big_Oh s1 )
take g ; :: thesis: ( f = f & g = g & Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g )
consider N being Element of NAT such that
A5: for n being Element of NAT st n >= N holds
(sqrt n) - (log 2,n) > 1 by Lm38;

A6: now

let p be real number ; :: thesis: ( p > 0 implies ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs (((f /" g) . n) - 0 ) < p )
assume A7: p > 0 ; :: thesis: ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs (((f /" g) . n) - 0 ) < p
set N1 = max N,(max [/(1 / p)\],2);
A8: ( max N,(max [/(1 / p)\],2) >= N & max N,(max [/(1 / p)\],2) >= max [/(1 / p)\],2 ) by XXREAL_0:25;
A9: ( max [/(1 / p)\],2 >= [/(1 / p)\] & max [/(1 / p)\],2 >= 2 ) by XXREAL_0:25;
then A10: ( max N,(max [/(1 / p)\],2) >= [/(1 / p)\] & max N,(max [/(1 / p)\],2) >= 2 ) by A8, XXREAL_0:2;
then A11: max N,(max [/(1 / p)\],2) > 1 by XXREAL_0:2;
max N,(max [/(1 / p)\],2) is Integer

proof

per cases ( max N,(max [/(1 / p)\],2) = N or max N,(max [/(1 / p)\],2) = max [/(1 / p)\],2 ) by XXREAL_0:16;

suppose max N,(max [/(1 / p)\],2) = N ; :: thesis: max N,(max [/(1 / p)\],2) is Integer

hence max N,(max [/(1 / p)\],2) is Integer ; :: thesis: verum

end;

suppose max N,(max [/(1 / p)\],2) = max [/(1 / p)\],2 ; :: thesis: max N,(max [/(1 / p)\],2) is Integer

hence max N,(max [/(1 / p)\],2) is Integer by XXREAL_0:16; :: thesis: verum

end;

end;

end;

then reconsider N1 = max N,(max [/(1 / p)\],2) as Element of NAT by A8, INT_1:16;
take N1 = N1; :: thesis: for n being Element of NAT st n >= N1 holds
abs (((f /" g) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N1 implies abs (((f /" g) . n) - 0 ) < p )
assume A12: n >= N1 ; :: thesis: abs (((f /" g) . n) - 0 ) < p
p " > 0 by A7;
then A13: 1 / p > 0 ;
[/(1 / p)\] >= 1 / p by INT_1:def 5;
then A14: N1 >= 1 / p by A10, XXREAL_0:2;
A15: n > 1 by A11, A12, XXREAL_0:2;
A16: (f /" g) . n = (f . n) / (g . n) by Lm4;
f . n = n to_power (log 2,n) by A1, A8, A9, A12;
then A17: (f /" g) . n = (n to_power (log 2,n)) / (n to_power (sqrt n)) by A2, A8, A9, A12, A16
.= n to_power ((log 2,n) - (sqrt n)) by A8, A9, A12, POWER:34
.= n to_power (- ((sqrt n) - (log 2,n))) ;
n >= N by A8, A12, XXREAL_0:2;
then (sqrt n) - (log 2,n) > 1 by A5;
then (- 1) * ((sqrt n) - (log 2,n)) < (- 1) * 1 by XREAL_1:71;
then A18: n to_power (- ((sqrt n) - (log 2,n))) < n to_power (- 1) by A15, POWER:44;
A19: n to_power (- 1) = 1 / (n to_power 1) by A8, A9, A12, POWER:33
.= 1 / n by POWER:30 ;
n >= 1 / p by A12, A14, XXREAL_0:2;
then 1 / n <= 1 / (1 / p) by A13, XREAL_1:87;
then n to_power (- 1) <= p by A19;
then A20: (f /" g) . n < p by A17, A18, XXREAL_0:2;
(f /" g) . n > 0 by A8, A9, A12, A17, POWER:39;
hence abs (((f /" g) . n) - 0 ) < p by A20, ABSVALUE:def 1; :: thesis: verum

end;

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