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 4 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not g . b₁ <= 0 )
let n be Nat; :: thesis: ( not 1 <= n or not g . n <= 0 )
A3: n in NAT by ORDINAL1:def 12;
assume A4: 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, A4; :: thesis: verum

end;

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

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

end;

end;

end;

end;

set h = g taken_every 2;
reconsider s = g as eventually-positive Real_Sequence by A2;
take s ; :: thesis: ( 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 )
thus s = g ; :: thesis: ( 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 )
set X = POWEROF2SET ;
set f = seq_n^ 1;
A5: g taken_every 2 is Element of Funcs (NAT,REAL) by FUNCT_2:8;

A6: now :: thesis: for n being Element of NAT st n >= 0 holds
( (g taken_every 2) . n <= 4 * (g . n) & (g taken_every 2) . n >= 0 )

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 )
A7: (g taken_every 2) . n = g . (2 * n) by ASYMPT_0:def 15;
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 A8: n in POWEROF2SET ; :: thesis: (g taken_every 2) . n <= 4 * (g . n)

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

end;

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

now :: thesis: not 2 * n in POWEROF2SET

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

proof

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

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

A14: now :: thesis: 1 / 2 is not Element of NAT

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 A12, A13, POWER:24;
hence contradiction by A14; :: thesis: verum

end;

suppose m > 0 ; :: thesis: contradiction

then m >= 0 + 1 by NAT_1:13;
then A15: m - 1 is Element of NAT by INT_1:3;
2 * n = 2 to_power ((m + (- 1)) + 1) by A12
.= (2 to_power (m - 1)) * (2 to_power 1) by POWER:27
.= (2 to_power (m - 1)) * 2 by POWER:25 ;
hence contradiction by A11, A15; :: thesis: verum

end;

end;

end;

end;

then A16: g . (2 * n) = (2 * n) to_power 2 by A1
.= (2 * n) ^2 by POWER:46
.= 4 * (n ^2) ;
g . n = n to_power 2 by A1, A11
.= n ^2 by POWER:46 ;
hence (g taken_every 2) . n <= 4 * (g . n) by A16, ASYMPT_0:def 15; :: 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, A7; :: 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 15; :: thesis: verum

end;

end;

end;

end;

A17: Big_Theta s = { 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;

A18: now :: thesis: not seq_n^ 1 in Big_Theta s

assume seq_n^ 1 in Big_Theta s ; :: thesis: contradiction
then consider t being Element of Funcs (NAT,REAL) such that
A19: t = seq_n^ 1 and
A20: 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 A17;
consider c, d being Real, N being Element of NAT such that
c > 0 and
A21: d > 0 and
A22: for n being Element of NAT st n >= N holds
( d * (g . n) <= t . n & t . n <= c * (g . n) ) by A20;
set N0 = max ((max (N,2)),[/(1 / d)\]);
A23: max ((max (N,2)),[/(1 / d)\]) >= max (N,2) by XXREAL_0:25;
max (N,2) >= N by XXREAL_0:25;
then A24: max ((max (N,2)),[/(1 / d)\]) >= N by A23, XXREAL_0:2;
A25: max ((max (N,2)),[/(1 / d)\]) >= [/(1 / d)\] by XXREAL_0:25;
A26: max (N,2) >= 2 by XXREAL_0:25;
then A27: max ((max (N,2)),[/(1 / d)\]) >= 2 by A23, 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 A23, 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 reconsider N1 = (2 to_power N0) - 1 as Element of NAT by INT_1:3;
A28: [/(1 / d)\] >= 1 / d by INT_1:def 7;
not N1 in POWEROF2SET by A23, A26, Lm49, XXREAL_0:2;
then A29: g . N1 = N1 to_power 2 by A1
.= N1 ^2 by POWER:46 ;
2 to_power N0 > N0 + 1 by A27, Lm1;
then A30: N1 > N0 by XREAL_1:20;
then A31: N1 >= N by A24, XXREAL_0:2;
N1 > [/(1 / d)\] by A25, A30, XXREAL_0:2;
then N1 > 1 / d by A28, XXREAL_0:2;
then N1 * N1 > N1 * (1 / d) by A30, XREAL_1:68;
then d * (N1 ^2) > (N1 * (1 / d)) * d by A21, XREAL_1:68;
then d * (N1 ^2) > N1 * ((1 / d) * d) ;
then A32: d * (N1 ^2) > N1 * 1 by A21, XCMPLX_1:87;
t . N1 = N1 to_power 1 by A19, A30, Def3
.= N1 by POWER:25 ;
hence contradiction by A22, A31, A32, A29; :: thesis: verum

end;

A33: 3 = 4 - 1 ;

A34: now :: thesis: not g is eventually-nondecreasing

assume g is eventually-nondecreasing ; :: thesis: contradiction
then consider N being Nat such that
A35: for n being Nat st n >= N holds
g . n <= g . (n + 1) ;
set N0 = max (N,1);
set N1 = (2 to_power (2 * (max (N,1)))) - 1;
A36: 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;
A37: 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 A38: N1 > 2 * (max (N,1)) by XREAL_1:20;
2 to_power (2 * (max (N,1))) >= 2 to_power 2 by A37, PRE_FF:8;
then 2 to_power (2 * (max (N,1))) >= 2 ^2 by POWER:46;
then N1 >= 3 by A33, XREAL_1:9;
then N1 >= 2 by XXREAL_0:2;
then A39: N1 ^2 > N1 + 1 by Lm47;
A40: 2 * (max (N,1)) in NAT by ORDINAL1:def 12;
2 * (max (N,1)) >= 2 * 1 by XREAL_1:64, XXREAL_0:25;
then not N1 in POWEROF2SET by Lm49;
then A41: 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 A38, XXREAL_0:2;
then A42: N1 >= N by A36, XXREAL_0:2;
N1 + 1 in POWEROF2SET by A40;
then g . (N1 + 1) = N1 + 1 by A1;
then g . N1 > g . (N1 + 1) by A41, A39, POWER:46;
hence contradiction by A35, A42; :: thesis: verum

end;

A43: now :: thesis: for n being Nat st n >= 0 holds
(seq_n^ 1) . n <= (seq_n^ 1) . (n + 1)

let n be Nat; :: thesis: ( n >= 0 implies (seq_n^ 1) . n <= (seq_n^ 1) . (n + 1) )
A44: n in NAT by ORDINAL1:def 12;
assume n >= 0 ; :: thesis: (seq_n^ 1) . n <= (seq_n^ 1) . (n + 1)
A45: n + 0 <= n + 1 by XREAL_1:6;
A46: (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, A44
.= n by POWER:25 ;
:: thesis: verum

end;

end;

end;

(seq_n^ 1) . (n + 1) = (n + 1) to_power 1 by Def3
.= n + 1 by POWER:25 ;
hence (seq_n^ 1) . n <= (seq_n^ 1) . (n + 1) by A46, A45; :: thesis: verum

end;

reconsider jj = 1 as Real ;
reconsider j = 1 as Element of NAT ;

A47: now :: thesis: for n being Element of NAT st n >= j & n in POWEROF2SET holds
( jj * (s . n) <= (seq_n^ 1) . n & (seq_n^ 1) . n <= jj * (s . n) )

let n be Element of NAT ; :: thesis: ( n >= j & n in POWEROF2SET implies ( jj * (s . n) <= (seq_n^ 1) . n & (seq_n^ 1) . n <= jj * (s . n) ) )
assume that
A48: n >= j and
A49: n in POWEROF2SET ; :: thesis: ( jj * (s . n) <= (seq_n^ 1) . n & (seq_n^ 1) . n <= jj * (s . n) )
A50: (seq_n^ 1) . n = n to_power 1 by A48, Def3
.= n by POWER:25 ;
hence jj * (s . n) <= (seq_n^ 1) . n by A1, A49; :: thesis: (seq_n^ 1) . n <= jj * (s . n)
thus (seq_n^ 1) . n <= jj * (s . n) by A1, A49, A50; :: thesis: verum

end;

seq_n^ 1 is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence seq_n^ 1 in Big_Theta (s,POWEROF2SET) by A47; :: thesis: ( 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 )
thus ( 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 ) by A18, A5, A6, A43, A34; :: thesis: verum