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;
A6:
now 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 ;
( 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
;
( 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, INT_1:25;
hence
1
* (g . n) <= f . n
by A2, A7;
f . n <= 1 * (g . n)thus
f . n <= 1
* (g . n)
by A2, A7, A11;
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 not f in Big_Theta gassume
f in Big_Theta g
;
contradictionthen 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;
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
by INT_1:25;
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;
verum end;
A34:
now not g is_smooth_wrt 2assume
g is_smooth_wrt 2
;
contradictionthen 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;
verum end;
A49:
now for n being Nat st n >= 2 holds
f . n <= f . (n + 1)let n be
Nat;
( 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
;
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
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 A52, A54, POWER:37;
hence
f . n <= f . (n + 1)
by A53, A51, A56, XXREAL_0:2;
verum end;
A57:
now for n being Nat st n >= 1 holds
g . n <= g . (n + 1)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 A6, A13, A49, A57, A34; verum