let f be Real_Sequence; :: thesis: ( ( 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: 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 )
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 (log 2,n) by A1;
hence not f . n <= 0 by A3, POWER:39; :: thesis: verum

end;

set g = f taken_every 2;
reconsider f = f as eventually-positive Real_Sequence by A2;
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
A4: t = f taken_every 2 and
A5: 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
A6: c > 0 and
A7: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A5;
A8: sqrt c > 0 by A6, SQUARE_1:93;
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;
A9: max N2,2 >= N2 by XXREAL_0:25;
N2 >= [/((sqrt c) / (sqrt 2))\] by XXREAL_0:25;
then A10: max N2,2 >= [/((sqrt c) / (sqrt 2))\] by A9, XXREAL_0:2;
A11: max N2,2 is Integer by XXREAL_0:16;
N2 >= N by XXREAL_0:25;
then A12: max N2,2 >= N by A9, XXREAL_0:2;
max N2,2 >= 2 by XXREAL_0:25;
then reconsider N1 = max N2,2 as Element of NAT by A11, INT_1:16;
set n = N1 + 1;
A13: (N1 + 1) to_power (log 2,(N1 + 1)) > 0 by POWER:39;
A14: 2 * (N1 + 1) > 2 * 0 by XREAL_1:70;
A15: sqrt 2 <> 0 by SQUARE_1:93;
A16: sqrt 2 > 0 by SQUARE_1:93;
A17: [/((sqrt c) / (sqrt 2))\] >= (sqrt c) / (sqrt 2) by INT_1:def 5;
A18: N1 + 1 > N1 + 0 by XREAL_1:10;
then N1 + 1 > [/((sqrt c) / (sqrt 2))\] by A10, XXREAL_0:2;
then N1 + 1 > (sqrt c) / (sqrt 2) by A17, XXREAL_0:2;
then (N1 + 1) * (sqrt 2) > ((sqrt c) / (sqrt 2)) * (sqrt 2) by A16, XREAL_1:70;
then (N1 + 1) * (sqrt 2) > sqrt c by A15, XCMPLX_1:88;
then ((N1 + 1) * (sqrt 2)) ^2 > (sqrt c) ^2 by A8, SQUARE_1:78;
then ((N1 + 1) ^2 ) * ((sqrt 2) ^2 ) > c by A6, SQUARE_1:def 4;
then A19: 2 * ((N1 + 1) ^2 ) > c by SQUARE_1:def 4;
(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 A14, 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 ;
then (2 * (N1 + 1)) to_power (log 2,(2 * (N1 + 1))) > c * ((N1 + 1) to_power (log 2,(N1 + 1))) by A13, A19, XREAL_1:70;
then f . (2 * (N1 + 1)) > c * ((N1 + 1) to_power (log 2,(N1 + 1))) by A1, A14;
then t . (N1 + 1) > c * ((N1 + 1) to_power (log 2,(N1 + 1))) by A4, ASYMPT_0:def 18;
then A20: t . (N1 + 1) > c * (f . (N1 + 1)) by A1;
N1 + 1 > N by A12, A18, XXREAL_0:2;
hence contradiction by A7, A20; :: thesis: verum

end;

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