let f be Real_Sequence; :: thesis: ( f . 0 = 0 & ( 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: ( f . 0 = 0 & ( 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 )
set g = seq_a^ 2,1,0 ;
set h = f /" (seq_a^ 2,1,0 );
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 A2: n >= 1 ; :: thesis: not f . n <= 0
then f . n = n to_power (sqrt n) by A1;
hence not f . n <= 0 by A2, POWER:39; :: thesis: verum

end;

then reconsider f = f as eventually-positive Real_Sequence ;
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
A3: for n being Element of NAT st n >= N holds
n - ((sqrt n) * (log 2,n)) > n / 2 by Lm46;

A4: 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 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
then p " > 0 ;
then A5: 1 / p > 0 ;
set N1 = max N,(max (2 * [/(log 2,(1 / p))\]),2);
A6: ( max N,(max (2 * [/(log 2,(1 / p))\]),2) >= N & max N,(max (2 * [/(log 2,(1 / p))\]),2) >= max (2 * [/(log 2,(1 / p))\]),2 ) by XXREAL_0:25;
A7: ( max (2 * [/(log 2,(1 / p))\]),2 >= 2 * [/(log 2,(1 / p))\] & max (2 * [/(log 2,(1 / p))\]),2 >= 2 ) by XXREAL_0:25;
then A8: ( max N,(max (2 * [/(log 2,(1 / p))\]),2) >= 2 * [/(log 2,(1 / p))\] & max N,(max (2 * [/(log 2,(1 / p))\]),2) >= 2 ) by A6, XXREAL_0:2;
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;

then reconsider N1 = max N,(max (2 * [/(log 2,(1 / p))\]),2) as Element of NAT by A6, 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 )
assume A9: n >= N1 ; :: thesis: abs (((f /" (seq_a^ 2,1,0 )) . n) - 0 ) < p
A10: (f /" (seq_a^ 2,1,0 )) . n = (f . n) / (g . n) by Lm4;
A11: f . n = n to_power (sqrt n) by A1, A6, A7, A9
.= 2 to_power ((sqrt n) * (log 2,n)) by A6, A7, A9, Lm3 ;
g . n = 2 to_power ((1 * n) + 0 ) by Def1
.= 2 to_power n ;
then A12: (f /" (seq_a^ 2,1,0 )) . n = 2 to_power (((sqrt n) * (log 2,n)) - n) by A10, A11, POWER:34
.= 2 to_power (- (n - ((sqrt n) * (log 2,n)))) ;
n >= N by A6, A9, XXREAL_0:2;
then n - ((sqrt n) * (log 2,n)) > n / 2 by A3;
then - (n - ((sqrt n) * (log 2,n))) < - (n / 2) by XREAL_1:26;
then A13: 2 to_power (- (n - ((sqrt n) * (log 2,n)))) < 2 to_power (- (n / 2)) by POWER:44;
A14: [/(log 2,(1 / p))\] >= log 2,(1 / p) by INT_1:def 5;
n >= 2 * [/(log 2,(1 / p))\] by A8, A9, XXREAL_0:2;
then n / 2 >= [/(log 2,(1 / p))\] by XREAL_1:79;
then n / 2 >= log 2,(1 / p) by A14, 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 2 to_power (- (n / 2)) <= 1 / (1 / p) by A5, POWER:def 3;
then 2 to_power (- (n / 2)) <= p ;
then A15: (f /" (seq_a^ 2,1,0 )) . n < p by A12, A13, XXREAL_0:2;
(f /" (seq_a^ 2,1,0 )) . n > 0 by A12, POWER:39;
hence abs (((f /" (seq_a^ 2,1,0 )) . n) - 0 ) < p by A15, ABSVALUE:def 1; :: thesis: verum

end;

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