let g be Real_Sequence; :: thesis: ( ( 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 ) ) ; :: thesis: 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

proof

take 1 ; :: according to ASYMPT_0:def 6 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not g . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not g . n <= 0 )
assume A3: n >= 1 ; :: thesis: not g . n <= 0
thus g . n > 0 :: thesis: verum

proof

per cases ( n in POWEROF2SET or not n in POWEROF2SET ) ;

suppose n in POWEROF2SET ; :: thesis: g . n > 0

hence g . n > 0 by A1, A3; :: thesis: verum

end;

suppose not n in POWEROF2SET ; :: thesis: g . n > 0

then g . n = n to_power 2 by A1;
hence g . n > 0 by A3, POWER:39; :: thesis: verum

end;

end;

end;

end;

set h = g taken_every 2;
reconsider g = g as eventually-positive Real_Sequence by A2;
take g ; :: thesis: ( 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:11;

A5: now

let n be Element of NAT ; :: thesis: ( n >= 0 implies ( (g taken_every 2) . n <= 4 * (g . n) & (g taken_every 2) . n >= 0 ) )
assume n >= 0 ; :: thesis: ( (g taken_every 2) . n <= 4 * (g . n) & (g taken_every 2) . n >= 0 )
A6: (g taken_every 2) . n = g . (2 * n) by ASYMPT_0:def 18;
thus (g taken_every 2) . n <= 4 * (g . n) :: thesis: (g taken_every 2) . n >= 0

proof

per cases ( n in POWEROF2SET or not n in POWEROF2SET ) ;

suppose A7: n in POWEROF2SET ; :: thesis: (g taken_every 2) . n <= 4 * (g . n)

then consider m being Element of NAT such that
A8: n = 2 to_power m ;
2 * n = (2 to_power 1) * (2 to_power m) by A8, POWER:30
.= 2 to_power (m + 1) by POWER:32 ;
then 2 * n in POWEROF2SET ;
then A9: g . (2 * n) = 2 * n by A1;
g . n = n by A1, A7;
hence (g taken_every 2) . n <= 4 * (g . n) by A6, A9, XREAL_1:66; :: thesis: verum

end;

suppose A10: not n in POWEROF2SET ; :: thesis: (g taken_every 2) . n <= 4 * (g . n)

now

assume 2 * n in POWEROF2SET ; :: thesis: contradiction
then consider m being Element of NAT such that
A11: 2 * n = 2 to_power m ;
thus contradiction :: thesis: verum

proof

per cases ( m = 0 or m > 0 ) ;

suppose A12: m = 0 ; :: thesis: contradiction

A13: now

assume 1 / 2 is Element of NAT ; :: thesis: contradiction
then 0 + 1 <= 1 / 2 by NAT_1:13;
hence contradiction ; :: thesis: verum

end;

(n * 2) * (2 " ) = 1 * (2 " ) by A11, A12, POWER:29;
hence contradiction by A13; :: thesis: verum

end;

suppose m > 0 ; :: thesis: contradiction

then m >= 0 + 1 by NAT_1:13;
then m - 1 >= 0 by XREAL_1:21;
then A14: m - 1 is Element of NAT by INT_1:16;
2 * n = 2 to_power ((m + (- 1)) + 1) by A11
.= (2 to_power (m - 1)) * (2 to_power 1) by POWER:32
.= (2 to_power (m - 1)) * 2 by POWER:30 ;
hence contradiction by A10, A14; :: thesis: verum

end;

end;

end;

end;

then A15: g . (2 * n) = (2 * n) to_power 2 by A1
.= (2 * n) ^2 by POWER:53
.= 4 * (n ^2 ) ;
g . n = n to_power 2 by A1, A10
.= n ^2 by POWER:53 ;
hence (g taken_every 2) . n <= 4 * (g . n) by A15, ASYMPT_0:def 18; :: thesis: verum

end;

end;

end;

thus (g taken_every 2) . n >= 0 :: thesis: verum

proof

per cases ( 2 * n in POWEROF2SET or not 2 * n in POWEROF2SET ) ;

suppose 2 * n in POWEROF2SET ; :: thesis: (g taken_every 2) . n >= 0

hence (g taken_every 2) . n >= 0 by A1, A6; :: thesis: verum

end;

suppose not 2 * n in POWEROF2SET ; :: thesis: (g taken_every 2) . n >= 0

then g . (2 * n) = (2 * n) to_power 2 by A1;
hence (g taken_every 2) . n >= 0 by ASYMPT_0:def 18; :: thesis: verum

end;

end;

end;

end;

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 ; :: thesis: contradiction
then 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:16;
set N1 = (2 to_power N0) - 1;
2 to_power N0 > 0 by POWER:39;
then 2 to_power N0 >= 0 + 1 by NAT_1:13;
then (2 to_power N0) - 1 >= 0 by XREAL_1:21;
then reconsider N1 = (2 to_power N0) - 1 as Element of NAT by INT_1:16;
A27: [/(1 / d)\] >= 1 / d by INT_1:def 5;
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:53 ;
2 to_power N0 > N0 + 1 by A26, Lm1;
then A29: N1 > N0 by XREAL_1:22;
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:70;
then d * (N1 ^2 ) > (N1 * (1 / d)) * d by A20, XREAL_1:70;
then d * (N1 ^2 ) > N1 * ((1 / d) * d) ;
then A31: d * (N1 ^2 ) > N1 * 1 by A20, XCMPLX_1:88;
t . N1 = N1 to_power 1 by A18, A29, Def3
.= N1 by POWER:30 ;
hence contradiction by A21, A30, A31, A28; :: thesis: verum

end;

A32: 3 = 4 - 1 ;

A33: now

assume g is eventually-nondecreasing ; :: thesis: contradiction
then 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 8;
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:10;
then 2 to_power (2 * (max N,1)) >= 1 by POWER:29;
then (2 to_power (2 * (max N,1))) - 1 >= 1 - 1 by XREAL_1:11;
then reconsider N1 = (2 to_power (2 * (max N,1))) - 1 as Element of NAT by INT_1:16;
A36: 2 * (max N,1) >= 2 * 1 by XREAL_1:66, 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:22;
2 to_power (2 * (max N,1)) >= 2 to_power 2 by A36, PRE_FF:10;
then 2 to_power (2 * (max N,1)) >= 2 ^2 by POWER:53;
then N1 >= 3 by A32, XREAL_1:11;
then N1 >= 2 by XXREAL_0:2;
then A38: N1 ^2 > N1 + 1 by Lm47;
2 * (max N,1) >= 2 * 1 by XREAL_1:66, 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:66;
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:53;
hence contradiction by A34, A40; :: thesis: verum

end;

A41: now

let n be Element of NAT ; :: thesis: ( n >= 0 implies (seq_n^ 1) . n <= (seq_n^ 1) . (n + 1) )
assume n >= 0 ; :: thesis: (seq_n^ 1) . n <= (seq_n^ 1) . (n + 1)
A42: n + 0 <= n + 1 by XREAL_1:8;
A43: (seq_n^ 1) . n = n

proof

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: (seq_n^ 1) . n = n

hence (seq_n^ 1) . n = n by Def3; :: thesis: verum

end;

suppose n > 0 ; :: thesis: (seq_n^ 1) . n = n

hence (seq_n^ 1) . n = n to_power 1 by Def3
.= n by POWER:30 ;
:: thesis: verum

end;

end;

end;

(seq_n^ 1) . (n + 1) = (n + 1) to_power 1 by Def3
.= n + 1 by POWER:30 ;
hence (seq_n^ 1) . n <= (seq_n^ 1) . (n + 1) by A43, A42; :: thesis: verum

end;

A44: now

let n be Element of NAT ; :: thesis: ( n >= 1 & n in POWEROF2SET implies ( 1 * (g . n) <= (seq_n^ 1) . n & (seq_n^ 1) . n <= 1 * (g . n) ) )
assume that
A45: n >= 1 and
A46: n in POWEROF2SET ; :: thesis: ( 1 * (g . n) <= (seq_n^ 1) . n & (seq_n^ 1) . n <= 1 * (g . n) )
A47: (seq_n^ 1) . n = n to_power 1 by A45, Def3
.= n by POWER:30 ;
hence 1 * (g . n) <= (seq_n^ 1) . n by A1, A46; :: thesis: (seq_n^ 1) . n <= 1 * (g . n)
thus (seq_n^ 1) . n <= 1 * (g . n) by A1, A46, A47; :: thesis: verum

end;

seq_n^ 1 is Element of Funcs NAT ,REAL by FUNCT_2:11;
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 8; :: thesis: verum