set X = POWEROF2SET ;
let f, g be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n > 0 holds
f . n = n to_power (2 to_power [\(log (2,n))/]) ) & ( for n being Element of NAT st n > 0 holds
g . n = n to_power n ) implies ex s being eventually-positive Real_Sequence st
( s = g & f in Big_Theta (s,POWEROF2SET) & not f in Big_Theta s & f is eventually-nondecreasing & s is eventually-nondecreasing & not s is_smooth_wrt 2 ) )
assume that
A1: for n being Element of NAT st n > 0 holds
f . n = n to_power (2 to_power [\(log (2,n))/]) and
A2: for n being Element of NAT st n > 0 holds
g . n = n to_power n ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = g & f in Big_Theta (s,POWEROF2SET) & not f in Big_Theta s & f is eventually-nondecreasing & s is eventually-nondecreasing & not s is_smooth_wrt 2 )
A3: 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 )
A4: n in NAT by ORDINAL1:def 12;
assume A5: n >= 1 ; :: thesis: not g . n <= 0
then g . n = n to_power n by A2, A4;
hence not g . n <= 0 by A5, POWER:34; :: thesis: verum

end;

set h = g taken_every 2;
reconsider g = g as eventually-positive Real_Sequence by A3;

A6: now :: thesis: for n being Element of NAT st n >= 1 & n in POWEROF2SET holds
( 1 * (g . n) <= f . n & f . n <= 1 * (g . n) )

let n be Element of NAT ; :: thesis: ( n >= 1 & n in POWEROF2SET implies ( 1 * (g . n) <= f . n & f . n <= 1 * (g . n) ) )
assume that
A7: n >= 1 and
A8: n in POWEROF2SET ; :: thesis: ( 1 * (g . n) <= f . n & f . n <= 1 * (g . n) )
consider n1 being Element of NAT such that
A9: n = 2 to_power n1 by A8;
A10: f . n = n to_power (2 to_power [\(log (2,n))/]) by A1, A7;
log (2,n) = n1 * (log (2,2)) by A9, POWER:55
.= n1 * 1 by POWER:52 ;
then A11: f . n = n to_power n by A10, A9;
hence 1 * (g . n) <= f . n by A2, A7; :: thesis: f . n <= 1 * (g . n)
thus f . n <= 1 * (g . n) by A2, A7, A11; :: thesis: verum

end;

A12: Big_Theta g = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (g . n) <= t . n & t . n <= c * (g . n) ) ) ) } by ASYMPT_0:27;

A13: now :: thesis: not f in Big_Theta g

assume f in Big_Theta g ; :: thesis: contradiction
then consider t being Element of Funcs (NAT,REAL) such that
A14: t = f and
A15: ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (g . n) <= t . n & t . n <= c * (g . n) ) ) ) by A12;
consider c, d being Real, N being Element of NAT such that
c > 0 and
A16: d > 0 and
A17: for n being Element of NAT st n >= N holds
( d * (g . n) <= t . n & t . n <= c * (g . n) ) by A15;
set N1 = max ([/(1 / d)\],(max (N,2)));
A18: max ([/(1 / d)\],(max (N,2))) >= [/(1 / d)\] by XXREAL_0:25;
A19: max ([/(1 / d)\],(max (N,2))) is Integer by XXREAL_0:16;
A20: max ([/(1 / d)\],(max (N,2))) >= max (N,2) by XXREAL_0:25;
max (N,2) >= N by XXREAL_0:25;
then A21: max ([/(1 / d)\],(max (N,2))) >= N by A20, XXREAL_0:2;
max (N,2) >= 2 by XXREAL_0:25;
then A22: max ([/(1 / d)\],(max (N,2))) >= 2 by A20, XXREAL_0:2;
reconsider N1 = max ([/(1 / d)\],(max (N,2))) as Element of NAT by A20, A19, INT_1:3;
reconsider N2 = 2 to_power N1 as Element of NAT ;
A23: N2 > N1 + 1 by A22, Lm1;
N1 > 1 by A22, XXREAL_0:2;
then (2 to_power (N1 + 1)) - (2 to_power N1) > 1 by Lm48;
then 2 to_power (N1 + 1) > N2 + 1 by XREAL_1:20;
then log (2,(2 to_power (N1 + 1))) > log (2,(N2 + 1)) by POWER:57;
then (N1 + 1) * (log (2,2)) > log (2,(N2 + 1)) by POWER:55;
then A24: (N1 + 1) * 1 > log (2,(N2 + 1)) by POWER:52;

A25: now :: thesis: not [\(log (2,(N2 + 1)))/] > N1

assume [\(log (2,(N2 + 1)))/] > N1 ; :: thesis: contradiction
then A26: [\(log (2,(N2 + 1)))/] >= N1 + 1 by INT_1:7;
log (2,(N2 + 1)) >= [\(log (2,(N2 + 1)))/] by INT_1:def 6;
hence contradiction by A24, A26, XXREAL_0:2; :: thesis: verum

end;

A27: g . (N2 + 1) = (N2 + 1) to_power (N2 + 1) by A2;
then A28: g . (N2 + 1) > 0 by POWER:34;
N1 + 1 > N1 + 0 by XREAL_1:8;
then A29: N2 > N1 by A23, XXREAL_0:2;
A30: N2 + 1 > N2 + 0 by XREAL_1:8;
then N2 + 1 > N1 by A29, XXREAL_0:2;
then N2 + 1 > N by A21, XXREAL_0:2;
then A31: d * (g . (N2 + 1)) <= t . (N2 + 1) by A17;
[/(1 / d)\] >= 1 / d by INT_1:def 7;
then N1 >= 1 / d by A18, XXREAL_0:2;
then N2 >= 1 / d by A29, XXREAL_0:2;
then A32: N2 + 1 > (1 / d) + 0 by XREAL_1:8;
log (2,N2) = N1 * (log (2,2)) by POWER:55
.= N1 * 1 by POWER:52 ;
then log (2,(N2 + 1)) > N1 by A23, A30, POWER:57;
then [\(log (2,(N2 + 1)))/] >= [\N1/] by PRE_FF:9;
then A33: [\(log (2,(N2 + 1)))/] >= N1 ;
t . (N2 + 1) = (N2 + 1) to_power (2 to_power [\(log (2,(N2 + 1)))/]) by A1, A14;
then (g . (N2 + 1)) / (t . (N2 + 1)) = ((N2 + 1) to_power (N2 + 1)) / ((N2 + 1) to_power N2) by A27, A33, A25, XXREAL_0:1
.= (N2 + 1) to_power ((N2 + 1) - N2) by POWER:29
.= N2 + 1 by POWER:25 ;
then 1 / ((g . (N2 + 1)) / (t . (N2 + 1))) < 1 / (1 / d) by A16, A32, XREAL_1:88;
then (t . (N2 + 1)) / (g . (N2 + 1)) < d by XCMPLX_1:57;
then ((t . (N2 + 1)) / (g . (N2 + 1))) * (g . (N2 + 1)) < d * (g . (N2 + 1)) by A28, XREAL_1:68;
hence contradiction by A31, A28, XCMPLX_1:87; :: thesis: verum

end;

A34: now :: thesis: not g is_smooth_wrt 2

assume g is_smooth_wrt 2 ; :: thesis: contradiction
then consider t being Element of Funcs (NAT,REAL) such that
A35: t = g taken_every 2 and
A36: 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 * (g . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
c > 0 and
A37: for n being Element of NAT st n >= N holds
( t . n <= c * (g . n) & t . n >= 0 ) by A36;
set N0 = max ([/c\],(max (N,2)));
A38: max ([/c\],(max (N,2))) >= [/c\] by XXREAL_0:25;
A39: max ([/c\],(max (N,2))) is Integer by XXREAL_0:16;
A40: max ([/c\],(max (N,2))) >= max (N,2) by XXREAL_0:25;
max (N,2) >= N by XXREAL_0:25;
then A41: max ([/c\],(max (N,2))) >= N by A40, XXREAL_0:2;
A42: max (N,2) >= 2 by XXREAL_0:25;
then A43: 2 * (max ([/c\],(max (N,2)))) > 1 * (max ([/c\],(max (N,2)))) by A40, XREAL_1:68;
A44: max ([/c\],(max (N,2))) >= 2 by A40, A42, XXREAL_0:2;
then A45: max ([/c\],(max (N,2))) > 1 by XXREAL_0:2;
reconsider N0 = max ([/c\],(max (N,2))) as Element of NAT by A40, A39, INT_1:3;
[/c\] >= c by INT_1:def 7;
then A46: N0 >= c by A38, XXREAL_0:2;
N0 >= 1 by A44, XXREAL_0:2;
then N0 + N0 >= N0 + 1 by XREAL_1:6;
then A47: N0 to_power (2 * N0) >= N0 to_power (N0 + 1) by A45, PRE_FF:8;
N0 to_power (N0 + 1) = (N0 to_power N0) * (N0 to_power 1) by A40, A42, POWER:27
.= (N0 to_power N0) * N0 by POWER:25 ;
then A48: N0 to_power (N0 + 1) >= c * (N0 to_power N0) by A46, XREAL_1:64;
(g taken_every 2) . N0 = g . (2 * N0) by ASYMPT_0:def 15
.= (2 * N0) to_power (2 * N0) by A2, A43 ;
then (g taken_every 2) . N0 > N0 to_power (2 * N0) by A40, A42, A43, POWER:37;
then (g taken_every 2) . N0 > N0 to_power (N0 + 1) by A47, XXREAL_0:2;
then (g taken_every 2) . N0 > c * (N0 to_power N0) by A48, XXREAL_0:2;
then (g taken_every 2) . N0 > c * (g . N0) by A2, A40, A42;
hence contradiction by A35, A37, A41; :: thesis: verum

end;

A49: now :: thesis: for n being Nat st n >= 2 holds
f . n <= f . (n + 1)

let n be Nat; :: thesis: ( n >= 2 implies f . n <= f . (n + 1) )
A50: n in NAT by ORDINAL1:def 12;
A51: f . (n + 1) = (n + 1) to_power (2 to_power [\(log (2,(n + 1)))/]) by A1;
assume A52: n >= 2 ; :: thesis: f . n <= f . (n + 1)
then A53: f . n = n to_power (2 to_power [\(log (2,n))/]) by A1, A50;
A54: n + 1 > n + 0 by XREAL_1:8;
then log (2,n) <= log (2,(n + 1)) by A52, POWER:57;
then [\(log (2,n))/] <= [\(log (2,(n + 1)))/] by PRE_FF:9;
then A55: 2 to_power [\(log (2,n))/] <= 2 to_power [\(log (2,(n + 1)))/] by PRE_FF:8;
n + 1 > 0 + 1 by A52, XREAL_1:8;
then A56: (n + 1) to_power (2 to_power [\(log (2,n))/]) <= (n + 1) to_power (2 to_power [\(log (2,(n + 1)))/]) by A55, PRE_FF:8;
log (2,n) >= log (2,2) by A52, PRE_FF:10;
then log (2,n) >= 1 by POWER:52;
then [\(log (2,n))/] >= [\1/] by PRE_FF:9;
then [\(log (2,n))/] >= 1 ;
then 2 to_power [\(log (2,n))/] > 2 to_power 0 by POWER:39;
then n to_power (2 to_power [\(log (2,n))/]) <= (n + 1) to_power (2 to_power [\(log (2,n))/]) by A52, A54, POWER:37;
hence f . n <= f . (n + 1) by A53, A51, A56, XXREAL_0:2; :: thesis: verum

end;

A57: now :: thesis: for n being Nat st n >= 1 holds
g . n <= g . (n + 1)

let n be Nat; :: thesis: ( n >= 1 implies g . n <= g . (n + 1) )
A58: n in NAT by ORDINAL1:def 12;
assume A59: n >= 1 ; :: thesis: g . n <= g . (n + 1)
A60: n + 1 > n + 0 by XREAL_1:8;
then A61: n to_power n < (n + 1) to_power n by A59, POWER:37;
n + 1 >= 1 + 1 by A59, XREAL_1:6;
then n + 1 > 1 by XXREAL_0:2;
then A62: (n + 1) to_power n < (n + 1) to_power (n + 1) by A60, POWER:39;
A63: g . (n + 1) = (n + 1) to_power (n + 1) by A2;
g . n = n to_power n by A2, A59, A58;
hence g . n <= g . (n + 1) by A63, A62, A61, XXREAL_0:2; :: thesis: verum

end;

take g ; :: thesis: ( g = g & f in Big_Theta (g,POWEROF2SET) & not f in Big_Theta g & f is eventually-nondecreasing & g is eventually-nondecreasing & not g is_smooth_wrt 2 )
f is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence ( g = g & f in Big_Theta (g,POWEROF2SET) & not f in Big_Theta g & f is eventually-nondecreasing & g is eventually-nondecreasing & not g is_smooth_wrt 2 ) by A6, A13, A49, A57, A34; :: thesis: verum