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 ) & g . 0 = 0 & ( 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
A1: ( 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 ) ) and
A2: ( g . 0 = 0 & ( 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 )
f is eventually-positive
proof
take 3 ; :: according to ASYMPT_0:def 6 :: thesis: for b1 being Element of NAT holds
( not 3 <= b1 or not f . b1 <= 0 )
let n be Element of NAT ; :: thesis: ( not 3 <= n or not f . n <= 0 )
assume A3: n >= 3 ; :: thesis: not f . n <= 0
then n > 1 by XXREAL_0:2;
then A4: n to_power 3 > n to_power 2 by POWER:44;
A5: n to_power 2 > 0 by A3, POWER:39;
A6: log 2,n >= log 2,3 by A3, PRE_FF:12;
log 2,3 > log 2,2 by POWER:65;
then log 2,3 > 1 by POWER:60;
then log 2,n > 1 by A6, XXREAL_0:2;
then (n to_power 3) * (log 2,n) > (n to_power 2) * 1 by A4, A5, XREAL_1:100;
then 12 * ((n to_power 3) * (log 2,n)) > 5 * (n to_power 2) by A5, XREAL_1:100;
then (12 * (n to_power 3)) * (log 2,n) > (5 * (n ^2 )) + 0 by POWER:53;
then ((12 * (n to_power 3)) * (log 2,n)) - (5 * (n ^2 )) > 0 by XREAL_1:22;
then (((12 * (n to_power 3)) * (log 2,n)) - (5 * (n ^2 ))) + ((log 2,n) ^2 ) > 0 + 0 by XREAL_1:10, XREAL_1:65;
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 A1, A3; :: thesis: verum
end;
then reconsider f = f as eventually-positive Real_Sequence ;
g is eventually-positive
proof
take 2 ; :: according to ASYMPT_0:def 6 :: thesis: for b1 being Element of NAT holds
( not 2 <= b1 or not g . b1 <= 0 )
let n be Element of NAT ; :: thesis: ( not 2 <= n or not g . n <= 0 )
assume A7: n >= 2 ; :: thesis: not g . n <= 0
then log 2,n >= log 2,2 by PRE_FF:12;
then A8: log 2,n >= 1 by POWER:60;
n to_power 3 > 0 by A7, POWER:39;
then (n to_power 3) * (log 2,n) > (n to_power 3) * 0 by A8, XREAL_1:70;
hence not g . n <= 0 by A2, A7; :: thesis: verum
end;
then reconsider g = g 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 )) ) );
A9: 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]
( n = 0 or n > 0 ) ;
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
consider h being Function of NAT ,REAL such that
A10: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A9);
 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 A10; :: 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 A10; :: thesis: verum
end;
then consider p being Real_Sequence such that
A11: ( p . 0 = 0 & ( 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
take 3 ; :: according to ASYMPT_0:def 6 :: thesis: for b1 being Element of NAT holds
( not 3 <= b1 or not p . b1 <= 0 )
let n be Element of NAT ; :: thesis: ( not 3 <= n or not p . n <= 0 )
assume A12: n >= 3 ; :: thesis: not p . n <= 0
then n > 1 by XXREAL_0:2;
then A13: n to_power 3 > n to_power 2 by POWER:44;
A14: n to_power 2 > 0 by A12, POWER:39;
A15: log 2,n >= log 2,3 by A12, PRE_FF:12;
log 2,3 > log 2,2 by POWER:65;
then log 2,3 > 1 by POWER:60;
then log 2,n > 1 by A15, XXREAL_0:2;
then (n to_power 3) * (log 2,n) > (n to_power 2) * 1 by A13, A14, XREAL_1:100;
then 12 * ((n to_power 3) * (log 2,n)) > 5 * (n to_power 2) by A14, XREAL_1:100;
then (12 * (n to_power 3)) * (log 2,n) > (5 * (n ^2 )) + 0 by POWER:53;
then ((12 * (n to_power 3)) * (log 2,n)) - (5 * (n ^2 )) > 0 by XREAL_1:22;
hence not p . n <= 0 by A11, A12; :: thesis: verum
end;
then reconsider p = p as eventually-positive Real_Sequence ;
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 ) );
A16: 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]
( n = 0 or n > 0 ) ;
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
consider h being Function of NAT ,REAL such that
A17: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A16);
 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 A17; :: thesis: verum
end;
then consider q being Real_Sequence such that
A18: ( q . 0 = 0 & ( 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 6 :: thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not q . b1 <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not q . n <= 0 )
assume A19: n >= 1 ; :: thesis: not q . n <= 0
((log 2,n) ^2 ) + 36 > 0 + 0 by XREAL_1:10, XREAL_1:65;
hence not q . n <= 0 by A18, A19; :: thesis: verum
end;
then reconsider q = q as eventually-positive Real_Sequence ;
set t = max p,q;
for n being Element of NAT holds f . n = (p . n) + (q . n)
proof
let n be Element of NAT ; :: thesis: f . n = (p . n) + (q . n)
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 A1, A11, A18; :: thesis: verum
end;
suppose A20: n > 0 ; :: thesis: f . n = (p . n) + (q . n)
then p . n = ((12 * (n to_power 3)) * (log 2,n)) - (5 * (n ^2 )) by A11;
then (p . n) + (q . n) = (((12 * (n to_power 3)) * (log 2,n)) - (5 * (n ^2 ))) + (((log 2,n) ^2 ) + 36) by A18, A20
.= ((((12 * (n to_power 3)) * (log 2,n)) - (5 * (n ^2 ))) + ((log 2,n) ^2 )) + 36 ;
hence f . n = (p . n) + (q . n) by A1, A20; :: thesis: verum
end;
end;
end;
end;
then A21: Big_Oh f = Big_Oh (p + q) by SEQ_1:11
.= Big_Oh (max p,q) by ASYMPT_0:9 ;
4 = 2 ^2
.= 2 to_power 2 by POWER:53 ;
then A22: log 2,4 = 2 * (log 2,2) by POWER:63
.= 2 * 1 by POWER:60
.= 2 ;
A23: 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;
A24: S1[4]
proof
q . 4 = (2 ^2 ) + 36 by A18, A22
.= 40 ;
hence S1[4] ; :: thesis: verum
end;
A25: 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
A26: k >= 4 and
A27: 7 * (k ^2 ) > q . k ; :: thesis: S1[k + 1]
k in NAT by ORDINAL1:def 13;
then A28: q . k = ((log 2,k) ^2 ) + 36 by A18, A26;
7 * ((k + 1) ^2 ) = (7 * (k ^2 )) + ((7 * (2 * k)) + (7 * 1)) ;
then A29: 7 * ((k + 1) ^2 ) > (q . k) + ((7 * (2 * k)) + (7 * 1)) by A27, XREAL_1:8;
A30: q . (k + 1) = ((log 2,(k + 1)) ^2 ) + 36 by A18;
k >= 1 by A26, XXREAL_0:2;
then k + k >= k + 1 by XREAL_1:8;
then A31: log 2,(k + k) >= log 2,(k + 1) by PRE_FF:12;
k + 1 >= 4 + 0 by A26, XREAL_1:10;
then log 2,(k + 1) >= 2 by A22, PRE_FF:12;
then (log 2,(k + k)) ^2 >= (log 2,(k + 1)) ^2 by A31, SQUARE_1:77;
then A32: q . (k + 1) <= ((log 2,(k + k)) ^2 ) + 36 by A30, XREAL_1:8;
log 2,(k + k) = log 2,(2 * k) ;
then log 2,(k + k) = (log 2,k) + (log 2,2) by A26, POWER:61;
then A33: (log 2,(k + k)) ^2 = ((log 2,k) + 1) ^2 by POWER:60
.= (((log 2,k) ^2 ) + (2 * (log 2,k))) + 1 ;
k >= 2 by A26, XXREAL_0:2;
then A34: 2 to_power k > k + 1 by Lm1;
A35: log 2,k >= 2 by A22, A26, PRE_FF:12;
k + 1 > k + 0 by XREAL_1:10;
then 2 to_power k > k by A34, XXREAL_0:2;
then log 2,(2 to_power k) > log 2,k by A26, POWER:65;
then k * (log 2,2) > log 2,k by POWER:63;
then k * 1 > log 2,k by POWER:60;
then 14 * k > 2 * (log 2,k) by A35, XREAL_1:100;
then ((7 * 2) * k) + 7 > (2 * (log 2,k)) + 1 by XREAL_1:10;
then ((log 2,k) ^2 ) + ((2 * (log 2,k)) + 1) < ((log 2,k) ^2 ) + ((7 * (2 * k)) + 7) by XREAL_1:8;
then ((log 2,(k + k)) ^2 ) + 36 < (((log 2,k) ^2 ) + ((7 * (2 * k)) + 7)) + 36 by A33, XREAL_1:8;
then (q . k) + ((7 * (2 * k)) + (7 * 1)) > q . (k + 1) by A28, A32, XXREAL_0:2;
hence S1[k + 1] by A29, XXREAL_0:2; :: thesis: verum
end;
for n being Nat st n >= 4 holds
S1[n] from NAT_1:sch 8(A24, A25);
 hence for n being Element of NAT st n >= 4 holds
7 * (n ^2 ) > q . n ; :: thesis: verum
end;
A36: 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 A37: n >= 4 ; :: thesis: p . n > 7 * (n ^2 )
then A38: p . n = ((12 * (n to_power 3)) * (log 2,n)) - (5 * (n ^2 )) by A11;
n > 1 by A37, XXREAL_0:2;
then A39: n to_power 3 > n to_power 2 by POWER:44;
A40: n to_power 2 > 0 by A37, POWER:39;
log 2,n >= log 2,4 by A37, PRE_FF:12;
then log 2,n > 1 by A22, XXREAL_0:2;
then (n to_power 3) * (log 2,n) > (n to_power 2) * 1 by A39, A40, XREAL_1:100;
then 12 * ((n to_power 3) * (log 2,n)) > 12 * (n to_power 2) by XREAL_1:70;
then (12 * (n to_power 3)) * (log 2,n) > 12 * (n ^2 ) by POWER:53;
then p . n > (12 * (n ^2 )) - (5 * (n ^2 )) by A38, XREAL_1:11;
hence p . n > 7 * (n ^2 ) ; :: thesis: verum
end;
A41: 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 A42: n >= 4 ; :: thesis: p . n > q . n
then A43: p . n > 7 * (n ^2 ) by A36;
7 * (n ^2 ) > q . n by A23, A42;
hence p . n > q . n by A43, XXREAL_0:2; :: thesis: verum
end;
A44: 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 A45: p . n > q . n by A41;
thus (max p,q) . n = max (p . n),(q . n) by ASYMPT_0:def 10
.= p . n by A45, XXREAL_0:def 10 ; :: thesis: verum
end;
A46: max p,q is Element of Funcs NAT ,REAL by FUNCT_2:11;
consider N being Element of NAT such that
A47: for n being Element of NAT st n >= N holds
(max p,q) . n > 0 by ASYMPT_0:def 6;
now
let n be Element of NAT ; :: thesis: ( n >= max 4,N implies ( (max p,q) . n <= 12 * (g . n) & (max p,q) . n >= 0 ) )
assume A48: n >= max 4,N ; :: thesis: ( (max p,q) . n <= 12 * (g . n) & (max p,q) . n >= 0 )
A49: ( max 4,N >= 4 & max 4,N >= N ) by XXREAL_0:25;
then A50: ( n >= 4 & n >= N ) by A48, XXREAL_0:2;
A51: (max p,q) . n = p . n by A44, A48, A49, XXREAL_0:2
.= ((12 * (n to_power 3)) * (log 2,n)) - (5 * (n ^2 )) by A11, A48, A49 ;
(max p,q) . n <= ((12 * (n to_power 3)) * (log 2,n)) - 0 by A51, XREAL_1:15;
then (max p,q) . n <= 12 * ((n to_power 3) * (log 2,n)) ;
hence (max p,q) . n <= 12 * (g . n) by A2, A48, A49; :: thesis: (max p,q) . n >= 0
thus (max p,q) . n >= 0 by A47, A50; :: thesis: verum
end;
then A52: max p,q in Big_Oh g by A46;
f in Big_Oh f by ASYMPT_0:10;
hence ( f = f & g = g & f in Big_Oh g ) by A21, A52, ASYMPT_0:12; :: thesis: verum