let g be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds g . n = (((n ^2) - n) + 1) to_power 4 ) implies ex s being eventually-positive Real_Sequence st
( s = g & Big_Oh (seq_n^ 8) = Big_Oh s ) )
assume A1: for n being Element of NAT holds g . n = (((n ^2) - n) + 1) to_power 4 ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = g & Big_Oh (seq_n^ 8) = Big_Oh s )
g is eventually-positive
proof
take 0 ; :: according to ASYMPT_0:def 4 :: thesis: for b1 being set holds
( not 0 <= b1 or not g . b1 <= 0 )
let n be Nat; :: thesis: ( not 0 <= n or not g . n <= 0 )
A2: n in NAT by ORDINAL1:def 12;
assume n >= 0 ; :: thesis: not g . n <= 0
g . n = (((n ^2) - n) + 1) to_power 4 by A1, A2;
hence not g . n <= 0 by Lm21, POWER:34, A2; :: thesis: verum
end;
then reconsider g = g as eventually-positive Real_Sequence ;
take g ; :: thesis: ( g = g & Big_Oh (seq_n^ 8) = Big_Oh g )
set f = seq_n^ 8;
A3: now :: thesis: for n being Element of NAT st n >= 1 holds
( g . n <= 1 * ((seq_n^ 8) . n) & g . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= 1 implies ( g . n <= 1 * ((seq_n^ 8) . n) & g . n >= 0 ) )
A4: g . n = (((n ^2) - n) + 1) to_power 4 by A1;
assume A5: n >= 1 ; :: thesis: ( g . n <= 1 * ((seq_n^ 8) . n) & g . n >= 0 )
then A6: ((n ^2) - n) + 1 <= n ^2 by Lm23;
(seq_n^ 8) . n = n to_power (2 * 4) by A5, Def3
.= (n to_power 2) to_power 4 by A5, POWER:33
.= (n ^2) to_power 4 by POWER:46 ;
hence g . n <= 1 * ((seq_n^ 8) . n) by A4, A6, Lm6, Lm21; :: thesis: g . n >= 0
thus g . n >= 0 by A4, Lm21, POWER:34; :: thesis: verum
end;
A7: now :: thesis: for n being Element of NAT st n >= 1 holds
( (seq_n^ 8) . n <= 16 * (g . n) & (seq_n^ 8) . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= 1 implies ( (seq_n^ 8) . n <= 16 * (g . n) & (seq_n^ 8) . n >= 0 ) )
A8: g . n = (((n ^2) - n) + 1) to_power 4 by A1;
A9: ((n ^2) - n) + 1 > 0 by Lm21;
assume A10: n >= 1 ; :: thesis: ( (seq_n^ 8) . n <= 16 * (g . n) & (seq_n^ 8) . n >= 0 )
then A11: (seq_n^ 8) . n = n to_power (2 * 4) by Def3
.= (n to_power 2) to_power 4 by A10, POWER:33
.= (n ^2) to_power 4 by POWER:46 ;
A12: n * n > n * 0 by A10, XREAL_1:68;
n ^2 <= 2 * (((n ^2) - n) + 1) by A10, Lm24;
then (seq_n^ 8) . n <= (2 * (((n ^2) - n) + 1)) to_power 4 by A11, A12, Lm6;
hence (seq_n^ 8) . n <= 16 * (g . n) by A8, A9, POWER:30, POWER:62; :: thesis: (seq_n^ 8) . n >= 0
thus (seq_n^ 8) . n >= 0 by A11, A12, POWER:34; :: thesis: verum
end;
seq_n^ 8 is Element of Funcs (NAT,REAL) by FUNCT_2:8;
then A13: seq_n^ 8 in Big_Oh g by A7;
g is Element of Funcs (NAT,REAL) by FUNCT_2:8;
then g in Big_Oh (seq_n^ 8) by A3;
hence ( g = g & Big_Oh (seq_n^ 8) = Big_Oh g ) by A13, Lm5; :: thesis: verum