let f, g be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n > 0 holds
f . n = n to_power (log (2,n)) ) & ( 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: for n being Element of NAT st n > 0 holds
f . n = n to_power (log (2,n)) and
A2: 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;
g is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 4 :: 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 A3: n >= 1 ; :: thesis: not g . n <= 0
then g . n = n to_power (sqrt n) by A2;
hence not g . n <= 0 by A3, POWER:34; :: thesis: verum

end;

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

proof

take 1 ; :: according to ASYMPT_0:def 4 :: 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 A4: n >= 1 ; :: thesis: not f . n <= 0
then f . n = n to_power (log (2,n)) by A1;
hence not f . n <= 0 by A4, POWER:34; :: thesis: verum

end;

then reconsider f = f 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 Lm32;

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 by XXREAL_0:25;
A9: 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;

A10: max (N,(max ([/(1 / p)\],2))) >= max ([/(1 / p)\],2) by XXREAL_0:25;
max ([/(1 / p)\],2) >= [/(1 / p)\] by XXREAL_0:25;
then A11: max (N,(max ([/(1 / p)\],2))) >= [/(1 / p)\] by A10, XXREAL_0:2;
A12: max ([/(1 / p)\],2) >= 2 by XXREAL_0:25;
then max (N,(max ([/(1 / p)\],2))) >= 2 by A10, XXREAL_0:2;
then A13: max (N,(max ([/(1 / p)\],2))) > 1 by XXREAL_0:2;
reconsider N1 = max (N,(max ([/(1 / p)\],2))) as Element of NAT by A8, A9, INT_1:3;
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 )
A14: (f /" g) . n = (f . n) / (g . n) by Lm4;
assume A15: n >= N1 ; :: thesis: abs (((f /" g) . n) - 0) < p
then f . n = n to_power (log (2,n)) by A1, A10, A12;
then A16: (f /" g) . n = (n to_power (log (2,n))) / (n to_power (sqrt n)) by A2, A10, A12, A15, A14
.= n to_power ((log (2,n)) - (sqrt n)) by A10, A12, A15, POWER:29
.= n to_power (- ((sqrt n) - (log (2,n)))) ;
then A17: (f /" g) . n > 0 by A10, A12, A15, POWER:34;
n >= N by A8, A15, XXREAL_0:2;
then (sqrt n) - (log (2,n)) > 1 by A5;
then A18: (- 1) * ((sqrt n) - (log (2,n))) < (- 1) * 1 by XREAL_1:69;
n > 1 by A13, A15, XXREAL_0:2;
then A19: n to_power (- ((sqrt n) - (log (2,n)))) < n to_power (- 1) by A18, POWER:39;
[/(1 / p)\] >= 1 / p by INT_1:def 7;
then N1 >= 1 / p by A11, XXREAL_0:2;
then n >= 1 / p by A15, XXREAL_0:2;
then A20: 1 / n <= 1 / (1 / p) by A7, XREAL_1:85;
n to_power (- 1) = 1 / (n to_power 1) by A10, A12, A15, POWER:28
.= 1 / n by POWER:25 ;
then (f /" g) . n < p by A16, A19, A20, XXREAL_0:2;
hence abs (((f /" g) . n) - 0) < p by A17, ABSVALUE:def 1; :: thesis: verum

end;

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