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 6 :: thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not g . b1 <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not g . n <= 0 )
assume A4: n >= 1 ; :: thesis: not g . n <= 0
then g . n = n to_power n by A2;
hence not g . n <= 0 by A4, POWER:39; :: thesis: verum
end;
set h = g taken_every 2;
reconsider g = g as eventually-positive Real_Sequence by A3;
A5: now
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
A6: n >= 1 and
A7: n in POWEROF2SET ; :: thesis: ( 1 * (g . n) <= f . n & f . n <= 1 * (g . n) )
consider n1 being Element of NAT such that
A8: n = 2 to_power n1 by A7;
A9: f . n = n to_power (2 to_power [\(log 2,n)/]) by A1, A6;
log 2,n = n1 * (log 2,2) by A8, POWER:63
.= n1 * 1 by POWER:60 ;
then A10: f . n = n to_power n by A9, A8, INT_1:47;
hence 1 * (g . n) <= f . n by A2, A6; :: thesis: f . n <= 1 * (g . n)
thus f . n <= 1 * (g . n) by A2, A6, A10; :: thesis: verum
end;
A11: 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;
A12: now
assume f in Big_Theta g ; :: thesis: contradiction
then consider t being Element of Funcs NAT ,REAL such that
A13: t = f and
A14: 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 A11;
consider c, d being Real, N being Element of NAT such that
c > 0 and
A15: d > 0 and
A16: for n being Element of NAT st n >= N holds
( d * (g . n) <= t . n & t . n <= c * (g . n) ) by A14;
set N1 = max [/(1 / d)\],(max N,2);
A17: max [/(1 / d)\],(max N,2) >= [/(1 / d)\] by XXREAL_0:25;
A18: max [/(1 / d)\],(max N,2) is Integer by XXREAL_0:16;
A19: max [/(1 / d)\],(max N,2) >= max N,2 by XXREAL_0:25;
max N,2 >= N by XXREAL_0:25;
then A20: max [/(1 / d)\],(max N,2) >= N by A19, XXREAL_0:2;
max N,2 >= 2 by XXREAL_0:25;
then A21: max [/(1 / d)\],(max N,2) >= 2 by A19, XXREAL_0:2;
reconsider N1 = max [/(1 / d)\],(max N,2) as Element of NAT by A19, A18, INT_1:16;
reconsider N2 = 2 to_power N1 as Element of NAT ;
A22: N2 > N1 + 1 by A21, Lm1;
N1 > 1 by A21, 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:22;
then log 2,(2 to_power (N1 + 1)) > log 2,(N2 + 1) by POWER:65;
then (N1 + 1) * (log 2,2) > log 2,(N2 + 1) by POWER:63;
then A23: (N1 + 1) * 1 > log 2,(N2 + 1) by POWER:60;
A24: now
assume [\(log 2,(N2 + 1))/] > N1 ; :: thesis: contradiction
then A25: [\(log 2,(N2 + 1))/] >= N1 + 1 by INT_1:20;
log 2,(N2 + 1) >= [\(log 2,(N2 + 1))/] by INT_1:def 4;
hence contradiction by A23, A25, XXREAL_0:2; :: thesis: verum
end;
A26: g . (N2 + 1) = (N2 + 1) to_power (N2 + 1) by A2;
then A27: g . (N2 + 1) > 0 by POWER:39;
N1 + 1 > N1 + 0 by XREAL_1:10;
then A28: N2 > N1 by A22, XXREAL_0:2;
A29: N2 + 1 > N2 + 0 by XREAL_1:10;
then N2 + 1 > N1 by A28, XXREAL_0:2;
then N2 + 1 > N by A20, XXREAL_0:2;
then A30: d * (g . (N2 + 1)) <= t . (N2 + 1) by A16;
[/(1 / d)\] >= 1 / d by INT_1:def 5;
then N1 >= 1 / d by A17, XXREAL_0:2;
then N2 >= 1 / d by A28, XXREAL_0:2;
then A31: N2 + 1 > (1 / d) + 0 by XREAL_1:10;
log 2,N2 = N1 * (log 2,2) by POWER:63
.= N1 * 1 by POWER:60 ;
then log 2,(N2 + 1) > N1 by A22, A29, POWER:65;
then [\(log 2,(N2 + 1))/] >= [\N1/] by PRE_FF:11;
then A32: [\(log 2,(N2 + 1))/] >= N1 by INT_1:47;
t . (N2 + 1) = (N2 + 1) to_power (2 to_power [\(log 2,(N2 + 1))/]) by A1, A13;
then (g . (N2 + 1)) / (t . (N2 + 1)) = ((N2 + 1) to_power (N2 + 1)) / ((N2 + 1) to_power N2) by A26, A32, A24, XXREAL_0:1
.= (N2 + 1) to_power ((N2 + 1) - N2) by POWER:34
.= N2 + 1 by POWER:30 ;
then 1 / ((g . (N2 + 1)) / (t . (N2 + 1))) < 1 / (1 / d) by A15, A31, XREAL_1:90;
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 A27, XREAL_1:70;
hence contradiction by A30, A27, XCMPLX_1:88; :: thesis: verum
end;
A33: now
assume g is_smooth_wrt 2 ; :: thesis: contradiction
then g taken_every 2 in Big_Oh g by ASYMPT_0:def 19;
then consider t being Element of Funcs NAT ,REAL such that
A34: t = g taken_every 2 and
A35: 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
A36: for n being Element of NAT st n >= N holds
( t . n <= c * (g . n) & t . n >= 0 ) by A35;
set N0 = max [/c\],(max N,2);
A37: max [/c\],(max N,2) >= [/c\] by XXREAL_0:25;
A38: max [/c\],(max N,2) is Integer by XXREAL_0:16;
A39: max [/c\],(max N,2) >= max N,2 by XXREAL_0:25;
max N,2 >= N by XXREAL_0:25;
then A40: max [/c\],(max N,2) >= N by A39, XXREAL_0:2;
A41: max N,2 >= 2 by XXREAL_0:25;
then A42: 2 * (max [/c\],(max N,2)) > 1 * (max [/c\],(max N,2)) by A39, XREAL_1:70;
A43: max [/c\],(max N,2) >= 2 by A39, A41, XXREAL_0:2;
then A44: max [/c\],(max N,2) > 1 by XXREAL_0:2;
reconsider N0 = max [/c\],(max N,2) as Element of NAT by A39, A38, INT_1:16;
[/c\] >= c by INT_1:def 5;
then A45: N0 >= c by A37, XXREAL_0:2;
N0 >= 1 by A43, XXREAL_0:2;
then N0 + N0 >= N0 + 1 by XREAL_1:8;
then A46: N0 to_power (2 * N0) >= N0 to_power (N0 + 1) by A44, PRE_FF:10;
N0 to_power (N0 + 1) = (N0 to_power N0) * (N0 to_power 1) by A39, A41, POWER:32
.= (N0 to_power N0) * N0 by POWER:30 ;
then A47: N0 to_power (N0 + 1) >= c * (N0 to_power N0) by A45, XREAL_1:66;
(g taken_every 2) . N0 = g . (2 * N0) by ASYMPT_0:def 18
.= (2 * N0) to_power (2 * N0) by A2, A42 ;
then (g taken_every 2) . N0 > N0 to_power (2 * N0) by A39, A41, A42, POWER:42;
then (g taken_every 2) . N0 > N0 to_power (N0 + 1) by A46, XXREAL_0:2;
then (g taken_every 2) . N0 > c * (N0 to_power N0) by A47, XXREAL_0:2;
then (g taken_every 2) . N0 > c * (g . N0) by A2, A39, A41;
hence contradiction by A34, A36, A40; :: thesis: verum
end;
A48: now
let n be Element of NAT ; :: thesis: ( n >= 2 implies f . n <= f . (n + 1) )
A49: f . (n + 1) = (n + 1) to_power (2 to_power [\(log 2,(n + 1))/]) by A1;
assume A50: n >= 2 ; :: thesis: f . n <= f . (n + 1)
then A51: f . n = n to_power (2 to_power [\(log 2,n)/]) by A1;
A52: n + 1 > n + 0 by XREAL_1:10;
then log 2,n <= log 2,(n + 1) by A50, POWER:65;
then [\(log 2,n)/] <= [\(log 2,(n + 1))/] by PRE_FF:11;
then A53: 2 to_power [\(log 2,n)/] <= 2 to_power [\(log 2,(n + 1))/] by PRE_FF:10;
n + 1 > 0 + 1 by A50, XREAL_1:10;
then A54: (n + 1) to_power (2 to_power [\(log 2,n)/]) <= (n + 1) to_power (2 to_power [\(log 2,(n + 1))/]) by A53, PRE_FF:10;
log 2,n >= log 2,2 by A50, PRE_FF:12;
then log 2,n >= 1 by POWER:60;
then [\(log 2,n)/] >= [\1/] by PRE_FF:11;
then [\(log 2,n)/] >= 1 by INT_1:47;
then 2 to_power [\(log 2,n)/] > 2 to_power 0 by POWER:44;
then n to_power (2 to_power [\(log 2,n)/]) <= (n + 1) to_power (2 to_power [\(log 2,n)/]) by A50, A52, POWER:42;
hence f . n <= f . (n + 1) by A51, A49, A54, XXREAL_0:2; :: thesis: verum
end;
A55: now
let n be Element of NAT ; :: thesis: ( n >= 1 implies g . n <= g . (n + 1) )
assume A56: n >= 1 ; :: thesis: g . n <= g . (n + 1)
A57: n + 1 > n + 0 by XREAL_1:10;
then A58: n to_power n < (n + 1) to_power n by A56, POWER:42;
n + 1 >= 1 + 1 by A56, XREAL_1:8;
then n + 1 > 1 by XXREAL_0:2;
then A59: (n + 1) to_power n < (n + 1) to_power (n + 1) by A57, POWER:44;
A60: g . (n + 1) = (n + 1) to_power (n + 1) by A2;
g . n = n to_power n by A2, A56;
hence g . n <= g . (n + 1) by A60, A59, A58, 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:11;
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 A5, A12, A48, A55, A33, ASYMPT_0:def 8; :: thesis: verum