set g = seq_n^ 8;
let f be Real_Sequence; ( ( for n being Element of NAT st n > 1 holds
f . n = (n to_power 2) / (log (2,n)) ) implies ex s being eventually-positive Real_Sequence st
( s = f & Big_Oh s c= Big_Oh (seq_n^ 8) & not Big_Oh s = Big_Oh (seq_n^ 8) ) )
assume A1:
for n being Element of NAT st n > 1 holds
f . n = (n to_power 2) / (log (2,n))
; ex s being eventually-positive Real_Sequence st
( s = f & Big_Oh s c= Big_Oh (seq_n^ 8) & not Big_Oh s = Big_Oh (seq_n^ 8) )
A2:
f is eventually-positive
proof
take
2
;
ASYMPT_0:def 4 for b1 being set holds
( not 2 <= b1 or not f . b1 <= 0 )
let n be
Nat;
( not 2 <= n or not f . n <= 0 )
A3:
n in NAT
by ORDINAL1:def 12;
assume A4:
n >= 2
;
not f . n <= 0
then
log (2,
n)
>= log (2,2)
by PRE_FF:10;
then A5:
log (2,
n)
>= 1
by POWER:52;
n > 1
by A4, XXREAL_0:2;
then A6:
f . n =
(n to_power 2) / (log (2,n))
by A1, A3
.=
(n to_power 2) * ((log (2,n)) ")
;
n to_power 2
> 0
by A4, POWER:34;
then
(n to_power 2) * ((log (2,n)) ") > (n to_power 2) * 0
by A5, XREAL_1:68;
hence
not
f . n <= 0
by A6;
verum
end;
set h = f /" (seq_n^ 8);
reconsider f = f as eventually-positive Real_Sequence by A2;
A7:
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^ 8)) . n) - 0).| < pA8:
log (2,3)
> log (2,2)
by POWER:57;
let p be
Real;
( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ 8)) . n) - 0).| < p )assume A9:
p > 0
;
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ 8)) . n) - 0).| < pA10:
[/(p to_power (- (1 / 6)))\] >= p to_power (- (1 / 6))
by INT_1:def 7;
reconsider p1 =
p as
Real ;
set N =
max (3,
[/(p1 to_power (- (1 / 6)))\]);
A11:
max (3,
[/(p1 to_power (- (1 / 6)))\])
>= 3
by XXREAL_0:25;
A12:
max (3,
[/(p1 to_power (- (1 / 6)))\]) is
Integer
by XXREAL_0:16;
A13:
max (3,
[/(p1 to_power (- (1 / 6)))\])
>= [/(p to_power (- (1 / 6)))\]
by XXREAL_0:25;
max (3,
[/(p1 to_power (- (1 / 6)))\])
in NAT
by A11, A12, INT_1:3;
then reconsider N =
max (3,
[/(p1 to_power (- (1 / 6)))\]) as
Nat ;
take N =
N;
for n being Nat st n >= N holds
|.(((f /" (seq_n^ 8)) . n) - 0).| < plet n be
Nat;
( n >= N implies |.(((f /" (seq_n^ 8)) . n) - 0).| < p )A14:
n in NAT
by ORDINAL1:def 12;
assume A15:
n >= N
;
|.(((f /" (seq_n^ 8)) . n) - 0).| < pthen A16:
n >= 3
by A11, XXREAL_0:2;
then A17:
n > 1
by XXREAL_0:2;
A18:
(f /" (seq_n^ 8)) . n =
(f . n) / ((seq_n^ 8) . n)
by Lm4
.=
((n to_power 2) / (log (2,n))) / ((seq_n^ 8) . n)
by A1, A17, A14
.=
((n to_power 2) / (log (2,n))) / (n to_power 8)
by A11, A15, Def3, A14
.=
((n to_power 2) * ((log (2,n)) ")) / (n to_power 8)
.=
(((log (2,n)) ") * (n to_power 2)) * ((n to_power 8) ")
.=
((log (2,n)) ") * ((n to_power 2) * ((n to_power 8) "))
.=
((log (2,n)) ") * ((n to_power 2) / (n to_power 8))
.=
((log (2,n)) ") * (n to_power (2 - 8))
by A11, A15, POWER:29
.=
((log (2,n)) ") * (n to_power (- 6))
.=
((log (2,n)) ") * (1 / (n to_power 6))
by A11, A15, POWER:28
.=
(1 / (n to_power 6)) * (1 / (log (2,n)))
.=
1
/ ((n to_power 6) * (log (2,n)))
by XCMPLX_1:102
;
n >= [/(p to_power (- (1 / 6)))\]
by A13, A15, XXREAL_0:2;
then A19:
n >= p to_power (- (1 / 6))
by A10, XXREAL_0:2;
p1 to_power (- (1 / 6)) > 0
by A9, POWER:34;
then
n to_power 6
>= (p to_power (- (1 / 6))) to_power 6
by A19, Lm6;
then A20:
n to_power 6
>= p1 to_power ((- (1 / 6)) * 6)
by A9, POWER:33;
p1 to_power (- 1) > 0
by A9, POWER:34;
then
1
/ (n to_power 6) <= 1
/ (p to_power (- 1))
by A20, XREAL_1:85;
then
1
/ (n to_power 6) <= 1
/ (1 / (p1 to_power 1))
by A9, POWER:28;
then A21:
1
/ (n to_power 6) <= p
by POWER:25;
log (2,
n)
>= log (2,3)
by A16, PRE_FF:10;
then
log (2,
n)
> log (2,2)
by A8, XXREAL_0:2;
then A22:
log (2,
n)
> 1
by POWER:52;
A23:
n to_power 6
> 0
by A11, A15, POWER:34;
then
(n to_power 6) * 1
< (n to_power 6) * (log (2,n))
by A22, XREAL_1:68;
then
(f /" (seq_n^ 8)) . n < 1
/ (n to_power 6)
by A23, A18, XREAL_1:88;
then
(f /" (seq_n^ 8)) . n < p
by A21, XXREAL_0:2;
hence
|.(((f /" (seq_n^ 8)) . n) - 0).| < p
by A22, A18, ABSVALUE:def 1;
verum end;
then A24:
f /" (seq_n^ 8) is convergent
by SEQ_2:def 6;
then A25:
lim (f /" (seq_n^ 8)) = 0
by A7, SEQ_2:def 7;
then
not seq_n^ 8 in Big_Oh f
by A24, ASYMPT_0:16;
then A26:
not f in Big_Omega (seq_n^ 8)
by ASYMPT_0:19;
take
f
; ( f = f & Big_Oh f c= Big_Oh (seq_n^ 8) & not Big_Oh f = Big_Oh (seq_n^ 8) )
f in Big_Oh (seq_n^ 8)
by A24, A25, ASYMPT_0:16;
hence
( f = f & Big_Oh f c= Big_Oh (seq_n^ 8) & not Big_Oh f = Big_Oh (seq_n^ 8) )
by A26, Th4; verum