ex s being Real_Sequence st
( s . 0 = 0 & ( for n being Element of NAT st n > 0 holds
s . n = ((log (2,n)) ^2) + 36 ) )
then consider q being Real_Sequence such that
A4:
q . 0 = 0
and
A5:
for n being Element of NAT st n > 0 holds
q . n = ((log (2,n)) ^2) + 36
;
q is eventually-positive
then reconsider q = q as eventually-positive Real_Sequence ;
let f, g be Real_Sequence; ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 ) & ( for n being Element of NAT st n > 0 holds
g . n = (n to_power 3) * (log (2,n)) ) implies ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = g & s in Big_Oh s1 ) )
assume that
A8:
f . 0 = 0
and
A9:
for n being Element of NAT st n > 0 holds
f . n = ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36
and
A10:
for n being Element of NAT st n > 0 holds
g . n = (n to_power 3) * (log (2,n))
; ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = g & s in Big_Oh s1 )
A11:
g is eventually-positive
4 =
2 ^2
.=
2 to_power 2
by POWER:46
;
then A15: log (2,4) =
2 * (log (2,2))
by POWER:55
.=
2 * 1
by POWER:52
.=
2
;
A16:
for n being Element of NAT st n >= 4 holds
7 * (n ^2) > q . n
proof
defpred S1[
Nat]
means 7
* ($1 ^2) > q . $1;
A17:
for
k being
Nat st
k >= 4 &
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( k >= 4 & S1[k] implies S1[k + 1] )
assume that A18:
k >= 4
and A19:
7
* (k ^2) > q . k
;
S1[k + 1]
A20:
q . (k + 1) = ((log (2,(k + 1))) ^2) + 36
by A5;
k >= 2
by A18, XXREAL_0:2;
then A21:
2
to_power k > k + 1
by Lm1;
k + 1
> k + 0
by XREAL_1:8;
then
2
to_power k > k
by A21, XXREAL_0:2;
then
log (2,
(2 to_power k))
> log (2,
k)
by A18, POWER:57;
then
k * (log (2,2)) > log (2,
k)
by POWER:55;
then A22:
k * 1
> log (2,
k)
by POWER:52;
log (2,
k)
>= 2
by A15, A18, PRE_FF:10;
then
14
* k > 2
* (log (2,k))
by A22, XREAL_1:98;
then
((7 * 2) * k) + 7
> (2 * (log (2,k))) + 1
by XREAL_1:8;
then A23:
((log (2,k)) ^2) + ((2 * (log (2,k))) + 1) < ((log (2,k)) ^2) + ((7 * (2 * k)) + 7)
by XREAL_1:6;
log (2,
(k + k))
= log (2,
(2 * k))
;
then
log (2,
(k + k))
= (log (2,k)) + (log (2,2))
by A18, POWER:53;
then (log (2,(k + k))) ^2 =
((log (2,k)) + 1) ^2
by POWER:52
.=
(((log (2,k)) ^2) + (2 * (log (2,k)))) + 1
;
then A24:
((log (2,(k + k))) ^2) + 36
< (((log (2,k)) ^2) + ((7 * (2 * k)) + 7)) + 36
by A23, XREAL_1:6;
k >= 1
by A18, XXREAL_0:2;
then
k + k >= k + 1
by XREAL_1:6;
then A25:
log (2,
(k + k))
>= log (2,
(k + 1))
by PRE_FF:10;
k + 1
>= 4
+ 0
by A18, XREAL_1:8;
then
log (2,
(k + 1))
>= 2
by A15, PRE_FF:10;
then
(log (2,(k + k))) ^2 >= (log (2,(k + 1))) ^2
by A25, SQUARE_1:15;
then A26:
q . (k + 1) <= ((log (2,(k + k))) ^2) + 36
by A20, XREAL_1:6;
7
* ((k + 1) ^2) = (7 * (k ^2)) + ((7 * (2 * k)) + (7 * 1))
;
then A27:
7
* ((k + 1) ^2) > (q . k) + ((7 * (2 * k)) + (7 * 1))
by A19, XREAL_1:6;
k in NAT
by ORDINAL1:def 12;
then
q . k = ((log (2,k)) ^2) + 36
by A5, A18;
then
(q . k) + ((7 * (2 * k)) + (7 * 1)) > q . (k + 1)
by A26, A24, XXREAL_0:2;
hence
S1[
k + 1]
by A27, XXREAL_0:2;
verum
end;
q . 4 =
(2 ^2) + 36
by A5, A15
.=
40
;
then A28:
S1[4]
;
for
n being
Nat st
n >= 4 holds
S1[
n]
from NAT_1:sch 8(A28, A17);
hence
for
n being
Element of
NAT st
n >= 4 holds
7
* (n ^2) > q . n
;
verum
end;
reconsider g = g as eventually-positive Real_Sequence by A11;
f is eventually-positive
proof
log (2,3)
> log (2,2)
by POWER:57;
then A29:
log (2,3)
> 1
by POWER:52;
take
3
;
ASYMPT_0:def 4 for b1 being set holds
( not 3 <= b1 or not f . b1 <= 0 )
let n be
Nat;
( not 3 <= n or not f . n <= 0 )
assume A30:
n >= 3
;
not f . n <= 0
then A31:
n to_power 2
> 0
by POWER:34;
n > 1
by A30, XXREAL_0:2;
then A32:
n to_power 3
> n to_power 2
by POWER:39;
A33:
n in NAT
by ORDINAL1:def 12;
log (2,
n)
>= log (2,3)
by A30, PRE_FF:10;
then
log (2,
n)
> 1
by A29, XXREAL_0:2;
then
(n to_power 3) * (log (2,n)) > (n to_power 2) * 1
by A32, A31, XREAL_1:98;
then
12
* ((n to_power 3) * (log (2,n))) > 5
* (n to_power 2)
by A31, XREAL_1:98;
then
(12 * (n to_power 3)) * (log (2,n)) > (5 * (n ^2)) + 0
by POWER:46;
then
((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) > 0
by XREAL_1:20;
then
(((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2) > 0 + 0
by XREAL_1:8, XREAL_1:63;
then
((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36
> 0 + 0
;
hence
not
f . n <= 0
by A9, A30, A33;
verum
end;
then reconsider f = f as eventually-positive Real_Sequence ;
take
f
; ex s1 being eventually-positive Real_Sequence st
( f = f & s1 = g & f in Big_Oh s1 )
take
g
; ( f = f & g = g & f in Big_Oh g )
ex s being Real_Sequence st
( s . 0 = 0 & ( for n being Element of NAT st n > 0 holds
s . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) ) )
then consider p being Real_Sequence such that
A37:
p . 0 = 0
and
A38:
for n being Element of NAT st n > 0 holds
p . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))
;
p is eventually-positive
proof
log (2,3)
> log (2,2)
by POWER:57;
then A39:
log (2,3)
> 1
by POWER:52;
take
3
;
ASYMPT_0:def 4 for b1 being set holds
( not 3 <= b1 or not p . b1 <= 0 )
let n be
Nat;
( not 3 <= n or not p . n <= 0 )
assume A40:
n >= 3
;
not p . n <= 0
then A41:
n to_power 2
> 0
by POWER:34;
n > 1
by A40, XXREAL_0:2;
then A42:
n to_power 3
> n to_power 2
by POWER:39;
A43:
n in NAT
by ORDINAL1:def 12;
log (2,
n)
>= log (2,3)
by A40, PRE_FF:10;
then
log (2,
n)
> 1
by A39, XXREAL_0:2;
then
(n to_power 3) * (log (2,n)) > (n to_power 2) * 1
by A42, A41, XREAL_1:98;
then
12
* ((n to_power 3) * (log (2,n))) > 5
* (n to_power 2)
by A41, XREAL_1:98;
then
(12 * (n to_power 3)) * (log (2,n)) > (5 * (n ^2)) + 0
by POWER:46;
then
((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) > 0
by XREAL_1:20;
hence
not
p . n <= 0
by A38, A40, A43;
verum
end;
then reconsider p = p as eventually-positive Real_Sequence ;
set t = max (p,q);
consider N being Nat such that
A44:
for n being Nat st n >= N holds
(max (p,q)) . n > 0
by ASYMPT_0:def 4;
A45:
for n being Element of NAT st n >= 4 holds
p . n > 7 * (n ^2)
proof
let n be
Element of
NAT ;
( n >= 4 implies p . n > 7 * (n ^2) )
assume A46:
n >= 4
;
p . n > 7 * (n ^2)
then
n > 1
by XXREAL_0:2;
then A47:
n to_power 3
> n to_power 2
by POWER:39;
log (2,
n)
>= log (2,4)
by A46, PRE_FF:10;
then A48:
log (2,
n)
> 1
by A15, XXREAL_0:2;
n to_power 2
> 0
by A46, POWER:34;
then
(n to_power 3) * (log (2,n)) > (n to_power 2) * 1
by A47, A48, XREAL_1:98;
then
12
* ((n to_power 3) * (log (2,n))) > 12
* (n to_power 2)
by XREAL_1:68;
then A49:
(12 * (n to_power 3)) * (log (2,n)) > 12
* (n ^2)
by POWER:46;
p . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))
by A38, A46;
then
p . n > (12 * (n ^2)) - (5 * (n ^2))
by A49, XREAL_1:9;
hence
p . n > 7
* (n ^2)
;
verum
end;
A50:
for n being Element of NAT st n >= 4 holds
p . n > q . n
A53:
for n being Element of NAT st n >= 4 holds
(max (p,q)) . n = p . n
reconsider mN = max (4,N) as Element of NAT by ORDINAL1:def 12;
A55:
now for n being Element of NAT st n >= mN holds
( (max (p,q)) . n <= 12 * (g . n) & (max (p,q)) . n >= 0 )let n be
Element of
NAT ;
( n >= mN implies ( (max (p,q)) . n <= 12 * (g . n) & (max (p,q)) . n >= 0 ) )assume A56:
n >= mN
;
( (max (p,q)) . n <= 12 * (g . n) & (max (p,q)) . n >= 0 )A57:
max (4,
N)
>= 4
by XXREAL_0:25;
then (max (p,q)) . n =
p . n
by A53, A56, XXREAL_0:2
.=
((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))
by A38, A56, A57
;
then
(max (p,q)) . n <= ((12 * (n to_power 3)) * (log (2,n))) - 0
by XREAL_1:13;
then
(max (p,q)) . n <= 12
* ((n to_power 3) * (log (2,n)))
;
hence
(max (p,q)) . n <= 12
* (g . n)
by A10, A56, A57;
(max (p,q)) . n >= 0
max (4,
N)
>= N
by XXREAL_0:25;
then
n >= N
by A56, XXREAL_0:2;
hence
(max (p,q)) . n >= 0
by A44;
verum end;
max (p,q) is Element of Funcs (NAT,REAL)
by FUNCT_2:8;
then A58:
max (p,q) in Big_Oh g
by A55;
for n being Nat holds f . n = (p . n) + (q . n)
proof
let n be
Nat;
f . n = (p . n) + (q . n)
A59:
n in NAT
by ORDINAL1:def 12;
thus
f . n = (p . n) + (q . n)
verumproof
per cases
( n = 0 or n > 0 )
;
suppose A60:
n > 0
;
f . n = (p . n) + (q . n)then
p . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))
by A38, A59;
then (p . n) + (q . n) =
(((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + (((log (2,n)) ^2) + 36)
by A5, A60, A59
.=
((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36
;
hence
f . n = (p . n) + (q . n)
by A9, A60, A59;
verum end; end;
end;
end;
then A61: Big_Oh f =
Big_Oh (p + q)
by SEQ_1:7
.=
Big_Oh (max (p,q))
by ASYMPT_0:9
;
f in Big_Oh f
by ASYMPT_0:10;
hence
( f = f & g = g & f in Big_Oh g )
by A61, A58, ASYMPT_0:12; verum