set g = seq_a^ (2,1,0);
let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n > 0 holds
f . n = n to_power (sqrt n) ) implies ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = seq_a^ (2,1,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 ) )
assume A1: for n being Element of NAT st n > 0 holds
f . n = n to_power (sqrt n) ; :: thesis: ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = seq_a^ (2,1,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )
A2: 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 (sqrt n) by A1;
hence not f . n <= 0 by A3, POWER:39; :: thesis: verum

end;

set h = f /" (seq_a^ (2,1,0));
reconsider f = f as eventually-positive Real_Sequence by A2;
reconsider g = seq_a^ (2,1,0) as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = f & s1 = seq_a^ (2,1,0) & Big_Oh f c= Big_Oh s1 & not Big_Oh f = Big_Oh s1 )
take g ; :: thesis: ( f = f & g = seq_a^ (2,1,0) & Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g )
consider N being Element of NAT such that
A4: for n being Element of NAT st n >= N holds
n - ((sqrt n) * (log (2,n))) > n / 2 by Lm40;

A5: 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 /" (seq_a^ (2,1,0))) . n) - 0) < p )
assume A6: p > 0 ; :: thesis: ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs (((f /" (seq_a^ (2,1,0))) . n) - 0) < p
set N1 = max (N,(max ((2 * [/(log (2,(1 / p)))\]),2)));
A7: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) >= N by XXREAL_0:25;
A8: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) is Integer

proof

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

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

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

end;

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

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

end;

end;

end;

A9: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) >= max ((2 * [/(log (2,(1 / p)))\]),2) by XXREAL_0:25;
max ((2 * [/(log (2,(1 / p)))\]),2) >= 2 * [/(log (2,(1 / p)))\] by XXREAL_0:25;
then A10: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) >= 2 * [/(log (2,(1 / p)))\] by A9, XXREAL_0:2;
reconsider N1 = max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) as Element of NAT by A7, A8, INT_1:16;
take N1 = N1; :: thesis: for n being Element of NAT st n >= N1 holds
abs (((f /" (seq_a^ (2,1,0))) . n) - 0) < p
let n be Element of NAT ; :: thesis: ( n >= N1 implies abs (((f /" (seq_a^ (2,1,0))) . n) - 0) < p )
A11: (f /" (seq_a^ (2,1,0))) . n = (f . n) / (g . n) by Lm4;
A12: [/(log (2,(1 / p)))\] >= log (2,(1 / p)) by INT_1:def 5;
assume A13: n >= N1 ; :: thesis: abs (((f /" (seq_a^ (2,1,0))) . n) - 0) < p
then n >= 2 * [/(log (2,(1 / p)))\] by A10, XXREAL_0:2;
then n / 2 >= [/(log (2,(1 / p)))\] by XREAL_1:79;
then n / 2 >= log (2,(1 / p)) by A12, XXREAL_0:2;
then - (n / 2) <= - (log (2,(1 / p))) by XREAL_1:26;
then 2 to_power (- (n / 2)) <= 2 to_power (- (log (2,(1 / p)))) by PRE_FF:10;
then 2 to_power (- (n / 2)) <= 1 / (2 to_power (log (2,(1 / p)))) by POWER:33;
then A14: 2 to_power (- (n / 2)) <= 1 / (1 / p) by A6, POWER:def 3;
A15: g . n = 2 to_power ((1 * n) + 0) by Def1
.= 2 to_power n ;
A16: max ((2 * [/(log (2,(1 / p)))\]),2) >= 2 by XXREAL_0:25;
then f . n = n to_power (sqrt n) by A1, A9, A13
.= 2 to_power ((sqrt n) * (log (2,n))) by A9, A16, A13, Lm3 ;
then A17: (f /" (seq_a^ (2,1,0))) . n = 2 to_power (((sqrt n) * (log (2,n))) - n) by A11, A15, POWER:34
.= 2 to_power (- (n - ((sqrt n) * (log (2,n))))) ;
then A18: (f /" (seq_a^ (2,1,0))) . n > 0 by POWER:39;
n >= N by A7, A13, XXREAL_0:2;
then n - ((sqrt n) * (log (2,n))) > n / 2 by A4;
then - (n - ((sqrt n) * (log (2,n)))) < - (n / 2) by XREAL_1:26;
then 2 to_power (- (n - ((sqrt n) * (log (2,n))))) < 2 to_power (- (n / 2)) by POWER:44;
then (f /" (seq_a^ (2,1,0))) . n < p by A17, A14, XXREAL_0:2;
hence abs (((f /" (seq_a^ (2,1,0))) . n) - 0) < p by A18, ABSVALUE:def 1; :: thesis: verum

end;

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