let f 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) ) implies ex s being eventually-positive Real_Sequence st
( s = f & not s is smooth ) )
assume A1: ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = n to_power (log 2,n) ) ) ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = f & not s is smooth )
set g = f taken_every 2;
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 (log 2,n) by A1;
hence not f . n <= 0 by A2, POWER:39; :: thesis: verum

end;

then reconsider f = f as eventually-positive Real_Sequence ;
take f ; :: thesis: ( f = f & not f is smooth )

now

assume f is smooth ; :: thesis: contradiction
then f is_smooth_wrt 2 by ASYMPT_0:def 20;
then f taken_every 2 in Big_Oh f by ASYMPT_0:def 19;
then consider t being Element of Funcs NAT ,REAL such that
A3: t = f taken_every 2 and
A4: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A5: c > 0 and
A6: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A4;
set N0 = [/((sqrt c) / (sqrt 2))\];
reconsider N2 = max N,[/((sqrt c) / (sqrt 2))\] as Integer by XXREAL_0:16;
set N1 = max N2,2;
A7: ( max N2,2 >= N2 & max N2,2 >= 2 ) by XXREAL_0:25;
( N2 >= N & N2 >= [/((sqrt c) / (sqrt 2))\] ) by XXREAL_0:25;
then A8: ( max N2,2 >= N & max N2,2 >= [/((sqrt c) / (sqrt 2))\] ) by A7, XXREAL_0:2;
max N2,2 is Integer by XXREAL_0:16;
then reconsider N1 = max N2,2 as Element of NAT by A7, INT_1:16;
set n = N1 + 1;
N1 + 1 > N1 + 0 by XREAL_1:10;
then A9: ( N1 + 1 > [/((sqrt c) / (sqrt 2))\] & N1 + 1 > N & N1 + 1 > 2 ) by A7, A8, XXREAL_0:2;
A10: (N1 + 1) to_power (log 2,(N1 + 1)) > 0 by POWER:39;
A11: 2 * (N1 + 1) > 2 * 0 by XREAL_1:70;
A12: (2 * ((N1 + 1) ^2 )) * ((N1 + 1) to_power (log 2,(N1 + 1))) = (2 * (N1 + 1)) to_power (log 2,(2 * (N1 + 1)))

proof

thus (2 * ((N1 + 1) ^2 )) * ((N1 + 1) to_power (log 2,(N1 + 1))) = ((2 * (N1 + 1)) * (N1 + 1)) * ((N1 + 1) to_power (log 2,(N1 + 1)))
.= ((2 * (N1 + 1)) * (2 to_power (log 2,(N1 + 1)))) * ((N1 + 1) to_power (log 2,(N1 + 1))) by POWER:def 3
.= (2 * (N1 + 1)) * ((2 to_power (log 2,(N1 + 1))) * ((N1 + 1) to_power (log 2,(N1 + 1))))
.= (2 * (N1 + 1)) * ((2 * (N1 + 1)) to_power (log 2,(N1 + 1))) by POWER:35
.= ((2 * (N1 + 1)) to_power 1) * ((2 * (N1 + 1)) to_power (log 2,(N1 + 1))) by POWER:30
.= (2 * (N1 + 1)) to_power (1 + (log 2,(N1 + 1))) by A11, POWER:32
.= (2 * (N1 + 1)) to_power ((log 2,2) + (log 2,(N1 + 1))) by POWER:60
.= (2 * (N1 + 1)) to_power (log 2,(2 * (N1 + 1))) by POWER:61 ; :: thesis: verum

end;

A13: sqrt 2 > 0 by SQUARE_1:93;
A14: sqrt 2 <> 0 by SQUARE_1:93;
A15: sqrt c > 0 by A5, SQUARE_1:93;
[/((sqrt c) / (sqrt 2))\] >= (sqrt c) / (sqrt 2) by INT_1:def 5;
then N1 + 1 > (sqrt c) / (sqrt 2) by A9, XXREAL_0:2;
then (N1 + 1) * (sqrt 2) > ((sqrt c) / (sqrt 2)) * (sqrt 2) by A13, XREAL_1:70;
then (N1 + 1) * (sqrt 2) > sqrt c by A14, XCMPLX_1:88;
then ((N1 + 1) * (sqrt 2)) ^2 > (sqrt c) ^2 by A15, SQUARE_1:78;
then ((N1 + 1) ^2 ) * ((sqrt 2) ^2 ) > c by A5, SQUARE_1:def 4;
then 2 * ((N1 + 1) ^2 ) > c by SQUARE_1:def 4;
then (2 * (N1 + 1)) to_power (log 2,(2 * (N1 + 1))) > c * ((N1 + 1) to_power (log 2,(N1 + 1))) by A10, A12, XREAL_1:70;
then f . (2 * (N1 + 1)) > c * ((N1 + 1) to_power (log 2,(N1 + 1))) by A1, A11;
then t . (N1 + 1) > c * ((N1 + 1) to_power (log 2,(N1 + 1))) by A3, ASYMPT_0:def 18;
then t . (N1 + 1) > c * (f . (N1 + 1)) by A1;
hence contradiction by A6, A9; :: thesis: verum

end;

hence ( f = f & not f is smooth ) ; :: thesis: verum