let f be Real_Sequence; :: thesis: ( ( 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 A1:
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 ) )
; :: thesis: ( 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 )
set g = seq_n^ 1;
set h = (seq_n^ 1) taken_every 2;
set p = seq_logn ;
set q = seq_logn /" (seq_n^ 1);
set X = POWEROF2SET ;
A2:
3 = 4 - 1
;
A3:
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;
A4:
f is Element of Funcs NAT ,REAL
by FUNCT_2:11;
hence
f in Big_Theta (seq_n^ 1),POWEROF2SET
by A4; :: thesis: ( not f in Big_Theta (seq_n^ 1) & seq_n^ 1 is smooth & not f is eventually-nondecreasing )
hereby :: thesis: ( seq_n^ 1 is smooth & not f is eventually-nondecreasing )
assume
f in Big_Theta (seq_n^ 1)
;
:: thesis: contradictionthen consider t being
Element of
Funcs NAT ,
REAL such that A8:
t = f
and A9:
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 A3;
consider c,
d being
Real,
N being
Element of
NAT such that A10:
(
c > 0 &
d > 0 )
and A11:
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 A9;
(
seq_logn /" (seq_n^ 1) is
convergent &
lim (seq_logn /" (seq_n^ 1)) = 0 )
by Lm16;
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 SEQ_2:def 7;
set N2 =
max (max N0,N),
(max [/c\],2);
A13:
(
max (max N0,N),
(max [/c\],2) >= max N0,
N &
max (max N0,N),
(max [/c\],2) >= max [/c\],2 )
by XXREAL_0:25;
(
max N0,
N >= N0 &
max N0,
N >= N )
by XXREAL_0:25;
then A14:
(
max (max N0,N),
(max [/c\],2) >= N0 &
max (max N0,N),
(max [/c\],2) >= N )
by A13, XXREAL_0:2;
A15:
(
max [/c\],2
>= [/c\] &
max [/c\],2
>= 2 )
by XXREAL_0:25;
then A16:
(
max (max N0,N),
(max [/c\],2) >= [/c\] &
max (max N0,N),
(max [/c\],2) >= 2 )
by A13, XXREAL_0:2;
max (max N0,N),
(max [/c\],2) is
Integer
then reconsider N2 =
max (max N0,N),
(max [/c\],2) as
Element of
NAT by A13, 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;
2
to_power N2 > N2 + 1
by A16, Lm1;
then A17:
N3 > N2
by XREAL_1:22;
then A18:
N3 >= N
by A14, XXREAL_0:2;
not
N3 in POWEROF2SET
by A13, A15, Lm57, XXREAL_0:2;
then A19:
t . N3 = 2
to_power N3
by A1, A8;
(seq_n^ 1) . N3 =
N3 to_power 1
by A17, Def3
.=
N3
by POWER:30
;
then A20:
2
to_power N3 <= c * N3
by A11, A18, A19;
2
to_power N3 > 0
by POWER:39;
then
log 2,
(2 to_power N3) <= log 2,
(c * N3)
by A20, 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 A21:
N3 <= (log 2,c) + (log 2,N3)
by A10, A17, POWER:61;
A22:
N3 >= [/c\]
by A16, A17, XXREAL_0:2;
[/c\] >= c
by INT_1:def 5;
then
N3 >= c
by A22, XXREAL_0:2;
then
log 2,
N3 >= log 2,
c
by A10, 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 A21, 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
1
* (1 / 2) <= (log 2,N3) * (N3 " )
by A17, XCMPLX_0:def 7;
then A23:
(log 2,N3) / N3 >= 1
/ 2
;
N3 >= N0
by A14, A17, XXREAL_0:2;
then A24:
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 A17, Def2
.=
(log 2,N3) / (N3 to_power 1)
by A17, Def3
.=
(log 2,N3) / N3
by POWER:30
;
hence
contradiction
by A23, A24, ABSVALUE:def 1;
:: thesis: verum
end;
then A27:
seq_n^ 1 is eventually-nondecreasing
by ASYMPT_0:def 8;
A28:
(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 A28;
then
seq_n^ 1 is_smooth_wrt 2
by A27, ASYMPT_0:def 19;
hence
seq_n^ 1 is smooth
by ASYMPT_0:37; :: thesis: not f is eventually-nondecreasing