reconsider f = seq_a^ (2,2,0) as eventually-positive Real_Sequence ;
set g = seq_n! 0;
take
f
; ( f = seq_a^ (2,2,0) & Big_Oh f c= Big_Oh (seq_n! 0) & not Big_Oh f = Big_Oh (seq_n! 0) )
thus
f = seq_a^ (2,2,0)
; ( Big_Oh f c= Big_Oh (seq_n! 0) & not Big_Oh f = Big_Oh (seq_n! 0) )
set h = f /" (seq_n! 0);
A1:
now for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n! 0)) . n) - 0).| < plet p be
Real;
( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n! 0)) . n) - 0).| < p )assume A2:
p > 0
;
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n! 0)) . n) - 0).| < pset N =
max (10,
[/(9 + (log (2,(1 / p))))\]);
A3:
max (10,
[/(9 + (log (2,(1 / p))))\])
>= 10
by XXREAL_0:25;
A4:
max (10,
[/(9 + (log (2,(1 / p))))\]) is
Integer
by XXREAL_0:16;
A5:
max (10,
[/(9 + (log (2,(1 / p))))\])
>= [/(9 + (log (2,(1 / p))))\]
by XXREAL_0:25;
max (10,
[/(9 + (log (2,(1 / p))))\])
in NAT
by A3, A4, INT_1:3;
then reconsider N =
max (10,
[/(9 + (log (2,(1 / p))))\]) as
Nat ;
take N =
N;
for n being Nat st n >= N holds
|.(((f /" (seq_n! 0)) . n) - 0).| < plet n be
Nat;
( n >= N implies |.(((f /" (seq_n! 0)) . n) - 0).| < p )A6:
n in NAT
by ORDINAL1:def 12;
A7:
[/(9 + (log (2,(1 / p))))\] >= 9
+ (log (2,(1 / p)))
by INT_1:def 7;
assume A8:
n >= N
;
|.(((f /" (seq_n! 0)) . n) - 0).| < pthen
n >= [/(9 + (log (2,(1 / p))))\]
by A5, XXREAL_0:2;
then
n >= 9
+ (log (2,(1 / p)))
by A7, XXREAL_0:2;
then
n - 9
>= log (2,
(1 / p))
by XREAL_1:19;
then
2
to_power (n - 9) >= 2
to_power (log (2,(1 / p)))
by PRE_FF:8;
then
2
to_power (n - 9) >= 1
/ p
by A2, POWER:def 3;
then A9:
1
/ (2 to_power (n - 9)) <= 1
/ (1 / p)
by A2, XREAL_1:85;
A10:
(f /" (seq_n! 0)) . n =
(f . n) / ((seq_n! 0) . n)
by Lm4
.=
(2 to_power ((2 * n) + 0)) / ((seq_n! 0) . n)
by Def1, A6
.=
(2 to_power ((2 * n) + 0)) / ((n + 0) !)
by Def4
.=
(2 to_power (2 * n)) / (n !)
;
n >= 10
by A3, A8, XXREAL_0:2;
then
(f /" (seq_n! 0)) . n < 1
/ (2 to_power (n - 9))
by A10, Lm34, A6;
then
(f /" (seq_n! 0)) . n < p
by A9, XXREAL_0:2;
hence
|.(((f /" (seq_n! 0)) . n) - 0).| < p
by A10, ABSVALUE:def 1;
verum end;
then A11:
f /" (seq_n! 0) is convergent
by SEQ_2:def 6;
then A12:
lim (f /" (seq_n! 0)) = 0
by A1, SEQ_2:def 7;
then
not seq_n! 0 in Big_Oh f
by A11, ASYMPT_0:16;
then A13:
not f in Big_Omega (seq_n! 0)
by ASYMPT_0:19;
f in Big_Oh (seq_n! 0)
by A11, A12, ASYMPT_0:16;
hence
( Big_Oh f c= Big_Oh (seq_n! 0) & not Big_Oh f = Big_Oh (seq_n! 0) )
by A13, Th4; verum