set f = seq_n^ 8;
let e be Real; :: thesis: ( 0 < e & e < 1 implies ex s being eventually-positive Real_Sequence st
( s = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s ) )
assume that
A1: 0 < e and
A2: e < 1 ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s )
consider N being Element of NAT such that
A3: for n being Element of NAT st n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) by A1, A2, Lm25;
set g = seq_a^ ((1 + e),1,0);
set h = (seq_n^ 8) /" (seq_a^ ((1 + e),1,0));
reconsider g = seq_a^ ((1 + e),1,0) as eventually-positive Real_Sequence by A1;
take g ; :: thesis: ( g = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g )
thus g = seq_a^ ((1 + e),1,0) ; :: thesis: ( Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g )
A4: now :: thesis: for p being Real st p > 0 holds
ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0).| < p
let p be Real; :: thesis: ( p > 0 implies ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0).| < p )
assume A5: p > 0 ; :: thesis: ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0).| < p
reconsider p1 = p as Real ;
A6: (1 / p1) to_power (1 / 8) > 0 by A5, POWER:34;
set N1 = max (N,(max ([/((1 / p1) to_power (1 / 8))\],2)));
A7: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) >= N by XXREAL_0:25;
A8: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer
proof
per cases ( max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) = N or max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) = max ([/((1 / p) to_power (1 / 8))\],2) ) by XXREAL_0:16;
suppose max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) = N ; :: thesis: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer
hence max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer ; :: thesis: verum
end;
suppose max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) = max ([/((1 / p) to_power (1 / 8))\],2) ; :: thesis: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer
hence max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) is Integer by XXREAL_0:16; :: thesis: verum
end;
end;
end;
A9: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) >= max ([/((1 / p) to_power (1 / 8))\],2) by XXREAL_0:25;
max ([/((1 / p) to_power (1 / 8))\],2) >= [/((1 / p) to_power (1 / 8))\] by XXREAL_0:25;
then A10: max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) >= [/((1 / p) to_power (1 / 8))\] by A9, XXREAL_0:2;
max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) in NAT by A7, A8, INT_1:3;
then reconsider N1 = max (N,(max ([/((1 / p1) to_power (1 / 8))\],2))) as Nat ;
take N1 = N1; :: thesis: for n being Nat st n >= N1 holds
|.((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N1 implies |.((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0).| < p )
A11: n in NAT by ORDINAL1:def 12;
assume A12: n >= N1 ; :: thesis: |.((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0).| < p
then n >= N by A7, XXREAL_0:2;
then (n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) by A3, A11;
then A13: 2 to_power ((n * (log (2,(1 + e)))) - (8 * (log (2,n)))) > 2 to_power (8 * (log (2,n))) by POWER:39;
A14: max ([/((1 / p) to_power (1 / 8))\],2) >= 2 by XXREAL_0:25;
A15: g . n = (1 + e) to_power ((1 * n) + 0) by Def1;
((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n = ((seq_n^ 8) . n) / (g . n) by Lm4;
then A16: ((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n = (n to_power 8) / ((1 + e) to_power n) by A9, A14, A12, A15, Def3
.= (2 to_power (8 * (log (2,n)))) / ((1 + e) to_power n) by A9, A14, A12, Lm3
.= (2 to_power (8 * (log (2,n)))) / (2 to_power (n * (log (2,(1 + e))))) by A1, Lm3
.= 2 to_power ((8 * (log (2,n))) - (n * (log (2,(1 + e))))) by POWER:29
.= 2 to_power (- ((n * (log (2,(1 + e)))) - (8 * (log (2,n))))) ;
[/((1 / p) to_power (1 / 8))\] >= (1 / p) to_power (1 / 8) by INT_1:def 7;
then N1 >= (1 / p) to_power (1 / 8) by A10, XXREAL_0:2;
then n >= (1 / p) to_power (1 / 8) by A12, XXREAL_0:2;
then n to_power 8 >= ((1 / p) to_power (1 / 8)) to_power 8 by A6, Lm6;
then n to_power 8 >= (1 / p1) to_power ((1 / 8) * 8) by A5, POWER:33;
then n to_power 8 >= 1 / p1 by POWER:25;
then 1 / (n to_power 8) <= 1 / (p ") by A5, XREAL_1:85;
then 1 / (2 to_power (8 * (log (2,n)))) <= p by A9, A14, A12, Lm3;
then A17: 2 to_power (- (8 * (log (2,n)))) <= p by POWER:28;
2 to_power (8 * (log (2,n))) > 0 by POWER:34;
then 1 / (2 to_power ((n * (log (2,(1 + e)))) - (8 * (log (2,n))))) < 1 / (2 to_power (8 * (log (2,n)))) by A13, XREAL_1:88;
then 2 to_power (- ((n * (log (2,(1 + e)))) - (8 * (log (2,n))))) < 1 / (2 to_power (8 * (log (2,n)))) by POWER:28;
then ((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n < 2 to_power (- (8 * (log (2,n)))) by A16, POWER:28;
then A18: ((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n < p by A17, XXREAL_0:2;
((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n > 0 by A16, POWER:34;
hence |.((((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) . n) - 0).| < p by A18, ABSVALUE:def 1; :: thesis: verum
end;
then A19: (seq_n^ 8) /" (seq_a^ ((1 + e),1,0)) is convergent by SEQ_2:def 6;
then A20: lim ((seq_n^ 8) /" (seq_a^ ((1 + e),1,0))) = 0 by A4, SEQ_2:def 7;
then not g in Big_Oh (seq_n^ 8) by A19, ASYMPT_0:16;
then A21: not seq_n^ 8 in Big_Omega g by ASYMPT_0:19;
seq_n^ 8 in Big_Oh g by A19, A20, ASYMPT_0:16;
hence ( Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g ) by A21, Th4; :: thesis: verum