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 )
set f = seq_n^ 1;
set h = g taken_every 2;
set X = POWEROF2SET ;
g is eventually-positive
proof
take 1 ; :: according to ASYMPT_0:def 6 :: thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not g . b1 <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not g . n <= 0 )
assume A2: n >= 1 ; :: thesis: not g . n <= 0
thus g . n > 0 :: thesis: verum
proof
end;
end;
then reconsider g = g as eventually-positive Real_Sequence ;
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 )
A3: 3 = 4 - 1 ;
A4: seq_n^ 1 is Element of Funcs NAT ,REAL by FUNCT_2:11;
A5: 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
A6: n >= 1 and
A7: n in POWEROF2SET ; :: thesis: ( 1 * (g . n) <= (seq_n^ 1) . n & (seq_n^ 1) . n <= 1 * (g . n) )
A8: (seq_n^ 1) . n = n to_power 1 by A6, Def3
.= n by POWER:30 ;
hence 1 * (g . n) <= (seq_n^ 1) . n by A1, A7; :: thesis: (seq_n^ 1) . n <= 1 * (g . n)
thus (seq_n^ 1) . n <= 1 * (g . n) by A1, A7, A8; :: thesis: verum
end;
A9: 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;
A10: now
assume seq_n^ 1 in Big_Theta g ; :: thesis: contradiction
then consider t being Element of Funcs NAT ,REAL such that
A11: t = seq_n^ 1 and
A12: 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 A9;
consider c, d being Real, N being Element of NAT such that
c > 0 and
A13: d > 0 and
A14: for n being Element of NAT st n >= N holds
( d * (g . n) <= t . n & t . n <= c * (g . n) ) by A12;
set N0 = max (max N,2),[/(1 / d)\];
A15: ( max (max N,2),[/(1 / d)\] >= max N,2 & max (max N,2),[/(1 / d)\] >= [/(1 / d)\] ) by XXREAL_0:25;
A16: ( max N,2 >= N & max N,2 >= 2 ) by XXREAL_0:25;
then A17: ( max (max N,2),[/(1 / d)\] >= N & max (max N,2),[/(1 / d)\] >= 2 ) by A15, 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 A15, 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;
2 to_power N0 > N0 + 1 by A17, Lm1;
then A18: N1 > N0 by XREAL_1:22;
then A19: N1 >= N by A17, XXREAL_0:2;
A20: N1 > [/(1 / d)\] by A15, A18, XXREAL_0:2;
[/(1 / d)\] >= 1 / d by INT_1:def 5;
then N1 > 1 / d by A20, XXREAL_0:2;
then N1 * N1 > N1 * (1 / d) by A18, XREAL_1:70;
then d * (N1 ^2 ) > (N1 * (1 / d)) * d by A13, XREAL_1:70;
then d * (N1 ^2 ) > N1 * ((1 / d) * d) ;
then A21: d * (N1 ^2 ) > N1 * 1 by A13, XCMPLX_1:88;
not N1 in POWEROF2SET by A15, A16, Lm57, XXREAL_0:2;
then A22: g . N1 = N1 to_power 2 by A1
.= N1 ^2 by POWER:53 ;
t . N1 = N1 to_power 1 by A11, A18, Def3
.= N1 by POWER:30 ;
hence contradiction by A14, A19, A21, A22; :: thesis: verum
end;
A23: g taken_every 2 is Element of Funcs NAT ,REAL by FUNCT_2:11;
A24: 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 )
A25: (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 A26: n in POWEROF2SET ; :: thesis: (g taken_every 2) . n <= 4 * (g . n)
then consider m being Element of NAT such that
A27: n = 2 to_power m ;
2 * n = (2 to_power 1) * (2 to_power m) by A27, POWER:30
.= 2 to_power (m + 1) by POWER:32 ;
then 2 * n in POWEROF2SET ;
then A28: g . (2 * n) = 2 * n by A1;
g . n = n by A1, A26;
hence (g taken_every 2) . n <= 4 * (g . n) by A25, A28, XREAL_1:66; :: thesis: verum
end;
suppose A29: 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
A30: 2 * n = 2 to_power m ;
thus contradiction :: thesis: verum
proof
per cases ( m = 0 or m > 0 ) ;
suppose m = 0 ; :: thesis: contradiction
then A31: (n * 2) * (2 " ) = 1 * (2 " ) by A30, POWER:29;
now
assume 1 / 2 is Element of NAT ; :: thesis: contradiction
then 0 + 1 <= 1 / 2 by NAT_1:13;
hence contradiction ; :: thesis: verum
end;
hence contradiction by A31; :: thesis: verum
end;
suppose m > 0 ; :: thesis: contradiction
then m >= 0 + 1 by NAT_1:13;
then A32: m - 1 >= 0 by XREAL_1:21;
A33: 2 * n = 2 to_power ((m + (- 1)) + 1) by A30
.= (2 to_power (m - 1)) * (2 to_power 1) by POWER:32
.= (2 to_power (m - 1)) * 2 by POWER:30 ;
m - 1 is Element of NAT by A32, INT_1:16;
hence contradiction by A29, A33; :: thesis: verum
end;
end;
end;
end;
then A34: 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, A29
.= n ^2 by POWER:53 ;
hence (g taken_every 2) . n <= 4 * (g . n) by A34, ASYMPT_0:def 18; :: thesis: verum
end;
end;
end;
thus (g taken_every 2) . n >= 0 :: thesis: verum
proof
end;
end;
A35: 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)
A36: (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;
A37: (seq_n^ 1) . (n + 1) = (n + 1) to_power 1 by Def3
.= n + 1 by POWER:30 ;
n + 0 <= n + 1 by XREAL_1:8;
hence (seq_n^ 1) . n <= (seq_n^ 1) . (n + 1) by A36, A37; :: thesis: verum
end;
now
assume g is eventually-nondecreasing ; :: thesis: contradiction
then consider N being Element of NAT such that
A38: 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;
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 A39: (2 to_power (2 * (max N,1))) - 1 >= 1 - 1 by XREAL_1:11;
A40: 2 * (max N,1) >= 2 * 1 by XREAL_1:66, XXREAL_0:25;
reconsider N1 = (2 to_power (2 * (max N,1))) - 1 as Element of NAT by A39, INT_1:16;
not N1 in POWEROF2SET by A40, Lm57;
then A41: g . N1 = N1 to_power 2 by A1;
N1 + 1 in POWEROF2SET ;
then A42: g . (N1 + 1) = N1 + 1 by A1;
A43: 2 * (max N,1) >= 2 * 1 by XREAL_1:66, XXREAL_0:25;
then 2 to_power (2 * (max N,1)) >= 2 to_power 2 by PRE_FF:10;
then 2 to_power (2 * (max N,1)) >= 2 ^2 by POWER:53;
then N1 >= 3 by A3, XREAL_1:11;
then N1 >= 2 by XXREAL_0:2;
then N1 ^2 > N1 + 1 by Lm55;
then A44: g . N1 > g . (N1 + 1) by A41, A42, POWER:53;
A45: max N,1 >= N by XXREAL_0:25;
2 to_power (2 * (max N,1)) > (2 * (max N,1)) + 1 by A43, Lm1;
then A46: N1 > 2 * (max N,1) by XREAL_1:22;
2 * (max N,1) >= 1 * (max N,1) by XREAL_1:66;
then N1 >= max N,1 by A46, XXREAL_0:2;
then N1 >= N by A45, XXREAL_0:2;
hence contradiction by A38, A44; :: thesis: verum
end;
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 A4, A5, A10, A23, A24, A35, ASYMPT_0:def 8; :: thesis: verum