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 ) )
proof
defpred S1[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = ((log (2,$1)) ^2) + 36 ) );
A1: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of REAL st S1[n,y]
per cases ( n = zz or n > 0 ) ;
suppose n = zz ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
suppose A2: n > 0 ; :: thesis: ex y being Element of REAL st S1[n,y]
((log (2,n)) ^2) + 36 in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S1[n,y] by A2; :: thesis: verum
end;
end;
end;
consider h being sequence of REAL such that
A3: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A1);
 take h ; :: thesis: ( h . 0 = 0 & ( for n being Element of NAT st n > 0 holds
h . n = ((log (2,n)) ^2) + 36 ) )
thus ( h . 0 = 0 & ( for n being Element of NAT st n > 0 holds
h . n = ((log (2,n)) ^2) + 36 ) ) by A3; :: thesis: verum
end;
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
proof
take 1 ; :: according to ASYMPT_0:def 4 :: thesis: for b1 being set holds
( not 1 <= b1 or not q . b1 <= 0 )
let n be Nat; :: thesis: ( not 1 <= n or not q . n <= 0 )
A6: n in NAT by ORDINAL1:def 12;
A7: ((log (2,n)) ^2) + 36 > 0 + 0 by XREAL_1:8, XREAL_1:63;
assume n >= 1 ; :: thesis: not q . n <= 0
hence not q . n <= 0 by A5, A7, A6; :: thesis: verum
end;
then reconsider q = q as eventually-positive Real_Sequence ;
let f, g be Real_Sequence; :: thesis: ( 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)) ; :: thesis: ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = g & s in Big_Oh s1 )
A11: g is eventually-positive
proof
take 2 ; :: according to ASYMPT_0:def 4 :: thesis: for b1 being set holds
( not 2 <= b1 or not g . b1 <= 0 )
let n be Nat; :: thesis: ( not 2 <= n or not g . n <= 0 )
assume A12: n >= 2 ; :: thesis: not g . n <= 0
then log (2,n) >= log (2,2) by PRE_FF:10;
then A13: log (2,n) >= 1 by POWER:52;
A14: n in NAT by ORDINAL1:def 12;
n to_power 3 > 0 by A12, POWER:34;
then (n to_power 3) * (log (2,n)) > (n to_power 3) * 0 by A13, XREAL_1:68;
hence not g . n <= 0 by A10, A12, A14; :: thesis: verum
end;
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; :: thesis: ( k >= 4 & S1[k] implies S1[k + 1] )
assume that
A18: k >= 4 and
A19: 7 * (k ^2) > q . k ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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 ; :: according to ASYMPT_0:def 4 :: thesis: for b1 being set holds
( not 3 <= b1 or not f . b1 <= 0 )
let n be Nat; :: thesis: ( not 3 <= n or not f . n <= 0 )
assume A30: n >= 3 ; :: thesis: 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; :: thesis: verum
end;
then reconsider f = f as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = f & s1 = g & f in Big_Oh s1 )
take g ; :: thesis: ( 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)) ) )
proof
defpred S1[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = ((12 * ($1 to_power 3)) * (log (2,$1))) - (5 * ($1 ^2)) ) );
A34: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of REAL st S1[n,y]
A35: ( n = zz or n > 0 ) ;
((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S1[n,y] by A35; :: thesis: verum
end;
consider h being sequence of REAL such that
A36: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A34);
 take h ; :: thesis: ( h . 0 = 0 & ( for n being Element of NAT st n > 0 holds
h . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) ) )
thus h . 0 = 0 by A36; :: thesis: for n being Element of NAT st n > 0 holds
h . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) )
thus ( n > 0 implies h . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) ) by A36; :: thesis: verum
end;
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 ; :: according to ASYMPT_0:def 4 :: thesis: for b1 being set holds
( not 3 <= b1 or not p . b1 <= 0 )
let n be Nat; :: thesis: ( not 3 <= n or not p . n <= 0 )
assume A40: n >= 3 ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( n >= 4 implies p . n > 7 * (n ^2) )
assume A46: n >= 4 ; :: thesis: 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) ; :: thesis: verum
end;
A50: for n being Element of NAT st n >= 4 holds
p . n > q . n
proof
let n be Element of NAT ; :: thesis: ( n >= 4 implies p . n > q . n )
assume A51: n >= 4 ; :: thesis: p . n > q . n
then A52: 7 * (n ^2) > q . n by A16;
p . n > 7 * (n ^2) by A45, A51;
hence p . n > q . n by A52, XXREAL_0:2; :: thesis: verum
end;
A53: for n being Element of NAT st n >= 4 holds
(max (p,q)) . n = p . n
proof
let n be Element of NAT ; :: thesis: ( n >= 4 implies (max (p,q)) . n = p . n )
assume n >= 4 ; :: thesis: (max (p,q)) . n = p . n
then A54: p . n > q . n by A50;
thus (max (p,q)) . n = max ((p . n),(q . n)) by ASYMPT_0:def 7
.= p . n by A54, XXREAL_0:def 10 ; :: thesis: verum
end;
reconsider mN = max (4,N) as Element of NAT by ORDINAL1:def 12;
A55: now :: thesis: 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 ; :: thesis: ( n >= mN implies ( (max (p,q)) . n <= 12 * (g . n) & (max (p,q)) . n >= 0 ) )
assume A56: n >= mN ; :: thesis: ( (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; :: thesis: (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; :: thesis: 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; :: thesis: f . n = (p . n) + (q . n)
A59: n in NAT by ORDINAL1:def 12;
thus f . n = (p . n) + (q . n) :: thesis: verum
proof
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: f . n = (p . n) + (q . n)
hence f . n = (p . n) + (q . n) by A8, A37, A4; :: thesis: verum
end;
suppose A60: n > 0 ; :: thesis: 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; :: thesis: 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; :: thesis: verum