set X = POWEROF2SET ;
let f, g be Real_Sequence; ( ( 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
; 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
set h = g taken_every 2;
reconsider g = g as eventually-positive Real_Sequence by A3;
A5:
now let n be
Element of
NAT ;
( 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
;
( 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:55
.=
n1 * 1
by POWER:52
;
then A10:
f . n = n to_power n
by A9, A8, INT_1:25;
hence
1
* (g . n) <= f . n
by A2, A6;
f . n <= 1 * (g . n)thus
f . n <= 1
* (g . n)
by A2, A6, A10;
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
;
contradictionthen 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:3;
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: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 A23:
(N1 + 1) * 1
> log (2,
(N2 + 1))
by POWER:52;
A26:
g . (N2 + 1) = (N2 + 1) to_power (N2 + 1)
by A2;
then A27:
g . (N2 + 1) > 0
by POWER:34;
N1 + 1
> N1 + 0
by XREAL_1:8;
then A28:
N2 > N1
by A22, XXREAL_0:2;
A29:
N2 + 1
> N2 + 0
by XREAL_1:8;
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 7;
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:8;
log (2,
N2) =
N1 * (log (2,2))
by POWER:55
.=
N1 * 1
by POWER:52
;
then
log (2,
(N2 + 1))
> N1
by A22, A29, POWER:57;
then
[\(log (2,(N2 + 1)))/] >= [\N1/]
by PRE_FF:9;
then A32:
[\(log (2,(N2 + 1)))/] >= N1
by INT_1:25;
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:29
.=
N2 + 1
by POWER:25
;
then
1
/ ((g . (N2 + 1)) / (t . (N2 + 1))) < 1
/ (1 / d)
by A15, A31, 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 A27, XREAL_1:68;
hence
contradiction
by A30, A27, XCMPLX_1:87;
verum end;
A33:
now assume
g is_smooth_wrt 2
;
contradictionthen
g taken_every 2
in Big_Oh g
by ASYMPT_0:def 16;
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:68;
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:3;
[/c\] >= c
by INT_1:def 7;
then A45:
N0 >= c
by A37, XXREAL_0:2;
N0 >= 1
by A43, XXREAL_0:2;
then
N0 + N0 >= N0 + 1
by XREAL_1:6;
then A46:
N0 to_power (2 * N0) >= N0 to_power (N0 + 1)
by A44, PRE_FF:8;
N0 to_power (N0 + 1) =
(N0 to_power N0) * (N0 to_power 1)
by A39, A41, POWER:27
.=
(N0 to_power N0) * N0
by POWER:25
;
then A47:
N0 to_power (N0 + 1) >= c * (N0 to_power N0)
by A45, XREAL_1:64;
(g taken_every 2) . N0 =
g . (2 * N0)
by ASYMPT_0:def 15
.=
(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:37;
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;
verum end;
A48:
now let n be
Element of
NAT ;
( 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
;
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:8;
then
log (2,
n)
<= log (2,
(n + 1))
by A50, POWER:57;
then
[\(log (2,n))/] <= [\(log (2,(n + 1)))/]
by PRE_FF:9;
then A53:
2
to_power [\(log (2,n))/] <= 2
to_power [\(log (2,(n + 1)))/]
by PRE_FF:8;
n + 1
> 0 + 1
by A50, XREAL_1:8;
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:8;
log (2,
n)
>= log (2,2)
by A50, 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
by INT_1:25;
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 A50, A52, POWER:37;
hence
f . n <= f . (n + 1)
by A51, A49, A54, XXREAL_0:2;
verum end;
take
g
; ( 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 A5, A12, A48, A55, A33, ASYMPT_0:def 6; verum