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:8;
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
Nat such that A12:
for
m being
Nat st
m >= N0 holds
|.(((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 7;
reconsider N2 =
max (
(max (N0,N)),
(max ([/c\],2))) as
Element of
NAT by A17, A18, INT_1:3;
set N3 =
(2 to_power N2) - 1;
2
to_power N2 > 0
by POWER:34;
then
2
to_power N2 >= 0 + 1
by NAT_1:13;
then reconsider N3 =
(2 to_power N2) - 1 as
Element of
NAT by INT_1:3;
A26:
2
to_power N3 > 0
by POWER:34;
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:20;
then A29:
(seq_n^ 1) . N3 =
N3 to_power 1
by Def3
.=
N3
by POWER:25
;
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:10;
then
N3 * (log (2,2)) <= log (2,
(c * N3))
by POWER:55;
then
N3 * 1
<= log (2,
(c * N3))
by POWER:52;
then A30:
N3 <= (log (2,c)) + (log (2,N3))
by A15, A28, POWER:53;
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:10;
then
(log (2,N3)) + (log (2,N3)) >= (log (2,c)) + (log (2,N3))
by XREAL_1:6;
then
N3 <= 2
* (log (2,N3))
by A30, XXREAL_0:2;
then
N3 / 2
<= log (2,
N3)
by XREAL_1:79;
then
(N3 ") * (N3 * (1 / 2)) <= (log (2,N3)) * (N3 ")
by XREAL_1:64;
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:
|.(((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:25
;
hence
contradiction
by A31, A32, ABSVALUE:def 1;
verum
end;
then A36:
seq_n^ 1 is eventually-nondecreasing
;
(seq_n^ 1) taken_every 2 is Element of Funcs (NAT,REAL)
by FUNCT_2:8;
then
seq_n^ 1 is_smooth_wrt 2
by A36, A1;
hence
seq_n^ 1 is smooth
by ASYMPT_0:37; not f is eventually-nondecreasing
A37:
3 = 4 - 1
;