let g be Real_Sequence; ( ( for n being Element of NAT holds
( ( n in POWEROF2SET implies g . n = n ) & ( not n in POWEROF2SET implies g . n = n to_power 2 ) ) ) implies ex s being eventually-positive Real_Sequence st
( s = g & seq_n^ 1 in Big_Theta (s,POWEROF2SET) & not seq_n^ 1 in Big_Theta s & s taken_every 2 in Big_Oh s & seq_n^ 1 is eventually-nondecreasing & not s is eventually-nondecreasing ) )
assume A1:
for n being Element of NAT holds
( ( n in POWEROF2SET implies g . n = n ) & ( not n in POWEROF2SET implies g . n = n to_power 2 ) )
; ex s being eventually-positive Real_Sequence st
( s = g & seq_n^ 1 in Big_Theta (s,POWEROF2SET) & not seq_n^ 1 in Big_Theta s & s taken_every 2 in Big_Oh s & seq_n^ 1 is eventually-nondecreasing & not s is eventually-nondecreasing )
A2:
g is eventually-positive
set h = g taken_every 2;
reconsider g = g as eventually-positive Real_Sequence by A2;
take
g
; ( g = g & seq_n^ 1 in Big_Theta (g,POWEROF2SET) & not seq_n^ 1 in Big_Theta g & g taken_every 2 in Big_Oh g & seq_n^ 1 is eventually-nondecreasing & not g is eventually-nondecreasing )
set X = POWEROF2SET ;
set f = seq_n^ 1;
A4:
g taken_every 2 is Element of Funcs (NAT,REAL)
by FUNCT_2:8;
A16:
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;
A17:
now assume
seq_n^ 1
in Big_Theta g
;
contradictionthen consider t being
Element of
Funcs (
NAT,
REAL)
such that A18:
t = seq_n^ 1
and A19:
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 A16;
consider c,
d being
Real,
N being
Element of
NAT such that
c > 0
and A20:
d > 0
and A21:
for
n being
Element of
NAT st
n >= N holds
(
d * (g . n) <= t . n &
t . n <= c * (g . n) )
by A19;
set N0 =
max (
(max (N,2)),
[/(1 / d)\]);
A22:
max (
(max (N,2)),
[/(1 / d)\])
>= max (
N,2)
by XXREAL_0:25;
max (
N,2)
>= N
by XXREAL_0:25;
then A23:
max (
(max (N,2)),
[/(1 / d)\])
>= N
by A22, XXREAL_0:2;
A24:
max (
(max (N,2)),
[/(1 / d)\])
>= [/(1 / d)\]
by XXREAL_0:25;
A25:
max (
N,2)
>= 2
by XXREAL_0:25;
then A26:
max (
(max (N,2)),
[/(1 / d)\])
>= 2
by A22, XXREAL_0:2;
max (
(max (N,2)),
[/(1 / d)\]) is
Integer
by XXREAL_0:16;
then reconsider N0 =
max (
(max (N,2)),
[/(1 / d)\]) as
Element of
NAT by A22, INT_1:3;
set N1 =
(2 to_power N0) - 1;
2
to_power N0 > 0
by POWER:34;
then
2
to_power N0 >= 0 + 1
by NAT_1:13;
then
(2 to_power N0) - 1
>= 0
by XREAL_1:19;
then reconsider N1 =
(2 to_power N0) - 1 as
Element of
NAT by INT_1:3;
A27:
[/(1 / d)\] >= 1
/ d
by INT_1:def 7;
not
N1 in POWEROF2SET
by A22, A25, Lm49, XXREAL_0:2;
then A28:
g . N1 =
N1 to_power 2
by A1
.=
N1 ^2
by POWER:46
;
2
to_power N0 > N0 + 1
by A26, Lm1;
then A29:
N1 > N0
by XREAL_1:20;
then A30:
N1 >= N
by A23, XXREAL_0:2;
N1 > [/(1 / d)\]
by A24, A29, XXREAL_0:2;
then
N1 > 1
/ d
by A27, XXREAL_0:2;
then
N1 * N1 > N1 * (1 / d)
by A29, XREAL_1:68;
then
d * (N1 ^2) > (N1 * (1 / d)) * d
by A20, XREAL_1:68;
then
d * (N1 ^2) > N1 * ((1 / d) * d)
;
then A31:
d * (N1 ^2) > N1 * 1
by A20, XCMPLX_1:87;
t . N1 =
N1 to_power 1
by A18, A29, Def3
.=
N1
by POWER:25
;
hence
contradiction
by A21, A30, A31, A28;
verum end;
A32:
3 = 4 - 1
;
A33:
now assume
g is
eventually-nondecreasing
;
contradictionthen consider N being
Element of
NAT such that A34:
for
n being
Element of
NAT st
n >= N holds
g . n <= g . (n + 1)
by ASYMPT_0:def 6;
set N0 =
max (
N,1);
set N1 =
(2 to_power (2 * (max (N,1)))) - 1;
A35:
max (
N,1)
>= N
by XXREAL_0:25;
2
to_power (2 * (max (N,1))) >= 2
to_power 0
by PRE_FF:8;
then
2
to_power (2 * (max (N,1))) >= 1
by POWER:24;
then
(2 to_power (2 * (max (N,1)))) - 1
>= 1
- 1
by XREAL_1:9;
then reconsider N1 =
(2 to_power (2 * (max (N,1)))) - 1 as
Element of
NAT by INT_1:3;
A36:
2
* (max (N,1)) >= 2
* 1
by XREAL_1:64, XXREAL_0:25;
then
2
to_power (2 * (max (N,1))) > (2 * (max (N,1))) + 1
by Lm1;
then A37:
N1 > 2
* (max (N,1))
by XREAL_1:20;
2
to_power (2 * (max (N,1))) >= 2
to_power 2
by A36, PRE_FF:8;
then
2
to_power (2 * (max (N,1))) >= 2
^2
by POWER:46;
then
N1 >= 3
by A32, XREAL_1:9;
then
N1 >= 2
by XXREAL_0:2;
then A38:
N1 ^2 > N1 + 1
by Lm47;
2
* (max (N,1)) >= 2
* 1
by XREAL_1:64, XXREAL_0:25;
then
not
N1 in POWEROF2SET
by Lm49;
then A39:
g . N1 = N1 to_power 2
by A1;
2
* (max (N,1)) >= 1
* (max (N,1))
by XREAL_1:64;
then
N1 >= max (
N,1)
by A37, XXREAL_0:2;
then A40:
N1 >= N
by A35, XXREAL_0:2;
N1 + 1
in POWEROF2SET
;
then
g . (N1 + 1) = N1 + 1
by A1;
then
g . N1 > g . (N1 + 1)
by A39, A38, POWER:46;
hence
contradiction
by A34, A40;
verum end;
seq_n^ 1 is Element of Funcs (NAT,REAL)
by FUNCT_2:8;
hence
( g = g & seq_n^ 1 in Big_Theta (g,POWEROF2SET) & not seq_n^ 1 in Big_Theta g & g taken_every 2 in Big_Oh g & seq_n^ 1 is eventually-nondecreasing & not g is eventually-nondecreasing )
by A44, A17, A4, A5, A41, A33, ASYMPT_0:def 6; verum