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 set holds
( not 1 <= b₁ or not g . b₁ <= 0 )
let n be Nat; :: thesis: ( not 1 <= n or not g . n <= 0 )
A3: n in NAT by ORDINAL1:def 12;
assume A4: n >= 1 ; :: thesis: not g . n <= 0
then g . n = n to_power (sqrt n) by A2, A3;
hence not g . n <= 0 by A4, 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 set holds
( not 1 <= b₁ or not f . b₁ <= 0 )
let n be Nat; :: thesis: ( not 1 <= n or not f . n <= 0 )
A5: n in NAT by ORDINAL1:def 12;
assume A6: n >= 1 ; :: thesis: not f . n <= 0
then f . n = n to_power (log (2,n)) by A1, A5;
hence not f . n <= 0 by A6, 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
A7: for n being Element of NAT st n >= N holds
(sqrt n) - (log (2,n)) > 1 by Lm32;

A8: now :: thesis: for p being Real st p > 0 holds
ex N1 being Nat st
for n being Nat st n >= N1 holds
|.(((f /" g) . n) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex N1 being Nat st
for n being Nat st n >= N1 holds
|.(((f /" g) . n) - 0).| < p )
assume A9: p > 0 ; :: thesis: ex N1 being Nat st
for n being Nat st n >= N1 holds
|.(((f /" g) . n) - 0).| < p
set N1 = max (N,(max ([/(1 / p)\],2)));
A10: max (N,(max ([/(1 / p)\],2))) >= N by XXREAL_0:25;
A11: 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;

A12: 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 A13: max (N,(max ([/(1 / p)\],2))) >= [/(1 / p)\] by A12, XXREAL_0:2;
A14: max ([/(1 / p)\],2) >= 2 by XXREAL_0:25;
then max (N,(max ([/(1 / p)\],2))) >= 2 by A12, XXREAL_0:2;
then A15: max (N,(max ([/(1 / p)\],2))) > 1 by XXREAL_0:2;
max (N,(max ([/(1 / p)\],2))) in NAT by A10, A11, INT_1:3;
then reconsider N1 = max (N,(max ([/(1 / p)\],2))) as Nat ;
take N1 = N1; :: thesis: for n being Nat st n >= N1 holds
|.(((f /" g) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N1 implies |.(((f /" g) . n) - 0).| < p )
A16: n in NAT by ORDINAL1:def 12;
A17: (f /" g) . n = (f . n) / (g . n) by Lm4;
assume A18: n >= N1 ; :: thesis: |.(((f /" g) . n) - 0).| < p
then f . n = n to_power (log (2,n)) by A1, A12, A14, A16;
then A19: (f /" g) . n = (n to_power (log (2,n))) / (n to_power (sqrt n)) by A2, A12, A14, A18, A17, A16
.= n to_power ((log (2,n)) - (sqrt n)) by A12, A14, A18, POWER:29
.= n to_power (- ((sqrt n) - (log (2,n)))) ;
then A20: (f /" g) . n > 0 by A12, A14, A18, POWER:34;
n >= N by A10, A18, XXREAL_0:2;
then (sqrt n) - (log (2,n)) > 1 by A7, A16;
then A21: (- 1) * ((sqrt n) - (log (2,n))) < (- 1) * 1 by XREAL_1:69;
n > 1 by A15, A18, XXREAL_0:2;
then A22: n to_power (- ((sqrt n) - (log (2,n)))) < n to_power (- 1) by A21, POWER:39;
[/(1 / p)\] >= 1 / p by INT_1:def 7;
then N1 >= 1 / p by A13, XXREAL_0:2;
then n >= 1 / p by A18, XXREAL_0:2;
then A23: 1 / n <= 1 / (1 / p) by A9, XREAL_1:85;
n to_power (- 1) = 1 / (n to_power 1) by A12, A14, A18, POWER:28
.= 1 / n by POWER:25 ;
then (f /" g) . n < p by A19, A22, A23, XXREAL_0:2;
hence |.(((f /" g) . n) - 0).| < p by A20, ABSVALUE:def 1; :: thesis: verum

end;

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