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