reconsider q = seq_a^ (2,1,0) as eventually-positive Real_Sequence ;
set p = seq_a^ (2,2,0);
set g = seq_n^ 1;
set f = 2 (#) (seq_n^ 1);
take q ; :: thesis: ( q = seq_a^ (2,1,0) & 2 (#) (seq_n^ 1) in Big_Oh (seq_n^ 1) & not seq_a^ (2,2,0) in Big_Oh q )
thus q = seq_a^ (2,1,0) ; :: thesis: ( 2 (#) (seq_n^ 1) in Big_Oh (seq_n^ 1) & not seq_a^ (2,2,0) in Big_Oh q )
A1: now :: thesis: for n being Element of NAT st n >= 0 holds
( (2 (#) (seq_n^ 1)) . n <= 2 * ((seq_n^ 1) . n) & (2 (#) (seq_n^ 1)) . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= 0 implies ( (2 (#) (seq_n^ 1)) . n <= 2 * ((seq_n^ 1) . n) & (2 (#) (seq_n^ 1)) . n >= 0 ) )
assume n >= 0 ; :: thesis: ( (2 (#) (seq_n^ 1)) . n <= 2 * ((seq_n^ 1) . n) & (2 (#) (seq_n^ 1)) . n >= 0 )
thus (2 (#) (seq_n^ 1)) . n <= 2 * ((seq_n^ 1) . n) by SEQ_1:9; :: thesis: (2 (#) (seq_n^ 1)) . n >= 0
A2: (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:25 ;
:: thesis: verum
end;
end;
end;
2 * n >= 2 * 0 ;
hence (2 (#) (seq_n^ 1)) . n >= 0 by A2, SEQ_1:9; :: thesis: verum
end;
2 (#) (seq_n^ 1) is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence 2 (#) (seq_n^ 1) in Big_Oh (seq_n^ 1) by A1; :: thesis: not seq_a^ (2,2,0) in Big_Oh q
now :: thesis: not seq_a^ (2,2,0) in Big_Oh q
assume seq_a^ (2,2,0) in Big_Oh q ; :: thesis: contradiction
then consider t being Element of Funcs (NAT,REAL) such that
A3: t = seq_a^ (2,2,0) and
A4: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (q . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A5: c > 0 and
A6: for n being Element of NAT st n >= N holds
( t . n <= c * (q . n) & t . n >= 0 ) by A4;
ex n being Element of NAT st
( n >= N & t . n > c * (q . n) )
proof
take n = max (N,[/((log (2,c)) + 1)\]); :: thesis: ( n is set & n is Element of NAT & n >= N & t . n > c * (q . n) )
A7: n >= N by XXREAL_0:25;
n is Integer by XXREAL_0:16;
then reconsider n = n as Element of NAT by A7, INT_1:3;
A8: 2 to_power n >= 2 to_power [/((log (2,c)) + 1)\] by PRE_FF:8, XXREAL_0:25;
A9: 2 to_power (- n) > 0 by POWER:34;
[/((log (2,c)) + 1)\] >= (log (2,c)) + 1 by INT_1:def 7;
then A10: 2 to_power [/((log (2,c)) + 1)\] >= 2 to_power ((log (2,c)) + 1) by PRE_FF:8;
A11: 2 to_power ((log (2,c)) + 1) = (2 to_power (log (2,c))) * (2 to_power 1) by POWER:27
.= c * (2 to_power 1) by A5, POWER:def 3
.= c * 2 by POWER:25 ;
(c * (q . n)) * (2 to_power (- n)) = (c * (2 to_power ((1 * n) + 0))) * (2 to_power (- n)) by Def1
.= c * ((2 to_power n) * (2 to_power (- n)))
.= c * (2 to_power (n + (- n))) by POWER:27
.= c * 1 by POWER:24 ;
then 2 to_power ((log (2,c)) + 1) > (c * (q . n)) * (2 to_power (- n)) by A5, A11, XREAL_1:68;
then A12: 2 to_power [/((log (2,c)) + 1)\] > (c * (q . n)) * (2 to_power (- n)) by A10, XXREAL_0:2;
((seq_a^ (2,2,0)) . n) * (2 to_power (- n)) = (2 to_power ((2 * n) + 0)) * (2 to_power (- n)) by Def1
.= 2 to_power ((2 * n) + ((- 1) * n)) by POWER:27
.= 2 to_power (1 * n) ;
then ((seq_a^ (2,2,0)) . n) * (2 to_power (- n)) > (c * (q . n)) * (2 to_power (- n)) by A8, A12, XXREAL_0:2;
hence ( n is set & n is Element of NAT & n >= N & t . n > c * (q . n) ) by A3, A9, XREAL_1:64, XXREAL_0:25; :: thesis: verum
end;
hence contradiction by A6; :: thesis: verum
end;
hence not seq_a^ (2,2,0) in Big_Oh q ; :: thesis: verum