set X = POWEROF2SET ;
set p = seq_logn ;
set g = seq_n^ 1;
set h = (seq_n^ 1) taken_every 2;
set q = seq_logn /" (seq_n^ 1);
let f be Real_Sequence; ( ( for n being Element of NAT holds
( ( n in POWEROF2SET implies f . n = n ) & ( not n in POWEROF2SET implies f . n = 2 to_power n ) ) ) implies ( f in Big_Theta (seq_n^ 1),POWEROF2SET & not f in Big_Theta (seq_n^ 1) & seq_n^ 1 is smooth & not f is eventually-nondecreasing ) )
assume A5:
for n being Element of NAT holds
( ( n in POWEROF2SET implies f . n = n ) & ( not n in POWEROF2SET implies f . n = 2 to_power n ) )
; ( f in Big_Theta (seq_n^ 1),POWEROF2SET & not f in Big_Theta (seq_n^ 1) & seq_n^ 1 is smooth & not f is eventually-nondecreasing )
f is Element of Funcs NAT ,REAL
by FUNCT_2:11;
hence
f in Big_Theta (seq_n^ 1),POWEROF2SET
by A6; ( not f in Big_Theta (seq_n^ 1) & seq_n^ 1 is smooth & not f is eventually-nondecreasing )
A10:
Big_Theta (seq_n^ 1) = { 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 * ((seq_n^ 1) . n) <= t . n & t . n <= c * ((seq_n^ 1) . n) ) ) ) }
by ASYMPT_0:27;
hereby ( seq_n^ 1 is smooth & not f is eventually-nondecreasing )
A11:
lim (seq_logn /" (seq_n^ 1)) = 0
by Lm11;
seq_logn /" (seq_n^ 1) is
convergent
by Lm11;
then consider N0 being
Element of
NAT such that A12:
for
m being
Element of
NAT st
m >= N0 holds
abs (((seq_logn /" (seq_n^ 1)) . m) - 0 ) < 1
/ 2
by A11, SEQ_2:def 7;
assume
f in Big_Theta (seq_n^ 1)
;
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 * ((seq_n^ 1) . n) <= t . n &
t . n <= c * ((seq_n^ 1) . n) ) ) )
by A10;
consider c,
d being
Real,
N being
Element of
NAT such that A15:
c > 0
and
d > 0
and A16:
for
n being
Element of
NAT st
n >= N holds
(
d * ((seq_n^ 1) . n) <= t . n &
t . n <= c * ((seq_n^ 1) . n) )
by A14;
set N2 =
max (max N0,N),
(max [/c\],2);
A17:
max (max N0,N),
(max [/c\],2) >= max N0,
N
by XXREAL_0:25;
A18:
max (max N0,N),
(max [/c\],2) is
Integer
max N0,
N >= N0
by XXREAL_0:25;
then A19:
max (max N0,N),
(max [/c\],2) >= N0
by A17, XXREAL_0:2;
A20:
max (max N0,N),
(max [/c\],2) >= max [/c\],2
by XXREAL_0:25;
max [/c\],2
>= [/c\]
by XXREAL_0:25;
then A21:
max (max N0,N),
(max [/c\],2) >= [/c\]
by A20, XXREAL_0:2;
A22:
max [/c\],2
>= 2
by XXREAL_0:25;
then A23:
max (max N0,N),
(max [/c\],2) >= 2
by A20, XXREAL_0:2;
max N0,
N >= N
by XXREAL_0:25;
then A24:
max (max N0,N),
(max [/c\],2) >= N
by A17, XXREAL_0:2;
A25:
[/c\] >= c
by INT_1:def 5;
reconsider N2 =
max (max N0,N),
(max [/c\],2) as
Element of
NAT by A17, A18, INT_1:16;
set N3 =
(2 to_power N2) - 1;
2
to_power N2 > 0
by POWER:39;
then
2
to_power N2 >= 0 + 1
by NAT_1:13;
then
(2 to_power N2) - 1
>= 0
by XREAL_1:21;
then reconsider N3 =
(2 to_power N2) - 1 as
Element of
NAT by INT_1:16;
A26:
2
to_power N3 > 0
by POWER:39;
not
N3 in POWEROF2SET
by A20, A22, Lm49, XXREAL_0:2;
then A27:
t . N3 = 2
to_power N3
by A5, A13;
2
to_power N2 > N2 + 1
by A23, Lm1;
then A28:
N3 > N2
by XREAL_1:22;
then A29:
(seq_n^ 1) . N3 =
N3 to_power 1
by Def3
.=
N3
by POWER:30
;
N3 >= N
by A24, A28, XXREAL_0:2;
then
2
to_power N3 <= c * N3
by A16, A27, A29;
then
log 2,
(2 to_power N3) <= log 2,
(c * N3)
by A26, PRE_FF:12;
then
N3 * (log 2,2) <= log 2,
(c * N3)
by POWER:63;
then
N3 * 1
<= log 2,
(c * N3)
by POWER:60;
then A30:
N3 <= (log 2,c) + (log 2,N3)
by A15, A28, POWER:61;
N3 >= [/c\]
by A21, A28, XXREAL_0:2;
then
N3 >= c
by A25, XXREAL_0:2;
then
log 2,
N3 >= log 2,
c
by A15, PRE_FF:12;
then
(log 2,N3) + (log 2,N3) >= (log 2,c) + (log 2,N3)
by XREAL_1:8;
then
N3 <= 2
* (log 2,N3)
by A30, XXREAL_0:2;
then
N3 / 2
<= log 2,
N3
by XREAL_1:81;
then
(N3 " ) * (N3 * (1 / 2)) <= (log 2,N3) * (N3 " )
by XREAL_1:66;
then
((N3 " ) * N3) * (1 / 2) <= (log 2,N3) * (N3 " )
;
then A31:
(log 2,N3) / N3 >= 1
/ 2
by A28, XCMPLX_0:def 7;
N3 >= N0
by A19, A28, XXREAL_0:2;
then A32:
abs (((seq_logn /" (seq_n^ 1)) . N3) - 0 ) < 1
/ 2
by A12;
(seq_logn /" (seq_n^ 1)) . N3 =
(seq_logn . N3) / ((seq_n^ 1) . N3)
by Lm4
.=
(log 2,N3) / ((seq_n^ 1) . N3)
by A28, Def2
.=
(log 2,N3) / (N3 to_power 1)
by A28, Def3
.=
(log 2,N3) / N3
by POWER:30
;
hence
contradiction
by A31, A32, ABSVALUE:def 1;
verum
end;
then A35:
seq_n^ 1 is eventually-nondecreasing
by ASYMPT_0:def 8;
(seq_n^ 1) taken_every 2 is Element of Funcs NAT ,REAL
by FUNCT_2:11;
then
(seq_n^ 1) taken_every 2 in Big_Oh (seq_n^ 1)
by A1;
then
seq_n^ 1 is_smooth_wrt 2
by A35, ASYMPT_0:def 19;
hence
seq_n^ 1 is smooth
by ASYMPT_0:37; not f is eventually-nondecreasing
A36:
3 = 4 - 1
;