:: ASYMPT_1 semantic presentation

E1: for b1 being Nat holds
not ( b1 >= 2 & not 2 to_power b1 > b1 + 1 )
proof
defpred S1[ Nat] means 2 to_power a1 > a1 + 1;
2 to_power 2 = 2 ^2 by POWER:53
.= 2 * 2 by SQUARE_1:def 3
.= 4 ;
then E2: S1[2] ;
E3: for b1 being Nat holds
( ( b1 >= 2 & S1[b1] ) implies ( S1[b1 + 1] ) )
proof
let c1 be Nat;
assume that c1 >= 2
and E4: 2 to_power c1 > c1 + 1 ;
2 to_power (c1 + 1) = (2 to_power c1) * (2 to_power 1) by POWER:32
.= (2 to_power c1) * 2 by POWER:30
.= (2 to_power c1) + (2 to_power c1) ;
then E5: 2 to_power (c1 + 1) > (c1 + 1) + (2 to_power c1) by E4, XREAL_1:8;
2 to_power c1 > 0 by POWER:39;
then 2 to_power c1 >= 0 + 1 by INT_1:20;
then (c1 + 1) + (2 to_power c1) >= (c1 + 1) + 1 by XREAL_1:8;
hence 2 to_power (c1 + 1) > (c1 + 1) + 1 by E5, XREAL_1:2;
end;
for b1 being Nat holds
( b1 >= 2 implies S1[b1] ) from INT_2:sch 1(E2, E3);
 hence for b1 being Nat holds
not ( b1 >= 2 & not 2 to_power b1 > b1 + 1 ) ;
end;

theorem :: ASYMPT_1:1
for b1, b2 being Real_Sequence holds
not ( b1 . 0 = 0 & for b3 being Nat holds
( b3 > 0 implies b1 . b3 = ((((12 * (b3 to_power 3)) * (log 2,b3)) - (5 * (b3 ^2 ))) + ((log 2,b3) ^2 )) + 36 ) & b2 . 0 = 0 & for b3 being Nat holds
( b3 > 0 implies b2 . b3 = (b3 to_power 3) * (log 2,b3) ) & for b3, b4 being eventually-positive Real_Sequence holds
not ( b3 = b1 & b4 = b2 & b3 in Big_Oh b4 ) )
proof
let c1, c2 be Real_Sequence;
assume that E2: ( c1 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies c1 . b1 = ((((12 * (b1 to_power 3)) * (log 2,b1)) - (5 * (b1 ^2 ))) + ((log 2,b1) ^2 )) + 36 ) )
and E3: ( c2 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies c2 . b1 = (b1 to_power 3) * (log 2,b1) ) ) ;
c1 is eventually-positive
proof
take 3 ; :: uses ASYMPT_0:def 6
let c3 be Nat;
assume E4: c3 >= 3 ;
then c3 > 1 by XREAL_1:2;
then E5: c3 to_power 3 > c3 to_power 2 by POWER:44;
E6: c3 to_power 2 > 0 by E4, POWER:39;
E7: log 2,c3 >= log 2,3 by E4, PRE_FF:12;
log 2,3 > log 2,2 by POWER:65;
then log 2,3 > 1 by POWER:60;
then log 2,c3 > 1 by E7, XREAL_1:2;
then (c3 to_power 3) * (log 2,c3) > (c3 to_power 2) * 1 by E5, E6, REAL_2:199;
then 12 * ((c3 to_power 3) * (log 2,c3)) > 5 * (c3 to_power 2) by E6, REAL_2:199;
then (12 * (c3 to_power 3)) * (log 2,c3) > (5 * (c3 ^2 )) + 0 by POWER:53;
then E8: ((12 * (c3 to_power 3)) * (log 2,c3)) - (5 * (c3 ^2 )) > 0 by XREAL_1:22;
(log 2,c3) ^2 >= 0 by SQUARE_1:72;
then (((12 * (c3 to_power 3)) * (log 2,c3)) - (5 * (c3 ^2 ))) + ((log 2,c3) ^2 ) > 0 + 0 by E8, XREAL_1:10;
then ((((12 * (c3 to_power 3)) * (log 2,c3)) - (5 * (c3 ^2 ))) + ((log 2,c3) ^2 )) + 36 > 0 + 0 by XREAL_1:10;
hence c1 . c3 > 0 by E2, E4;
end;
then reconsider c3 = c1 as eventually-positive Real_Sequence ;
c2 is eventually-positive
proof
take 2 ; :: uses ASYMPT_0:def 6
let c4 be Nat;
assume E4: c4 >= 2 ;
then log 2,c4 >= log 2,2 by PRE_FF:12;
then E5: log 2,c4 >= 1 by POWER:60;
c4 to_power 3 > 0 by E4, POWER:39;
then (c4 to_power 3) * (log 2,c4) > (c4 to_power 3) * 0 by E5, XREAL_1:70;
hence c2 . c4 > 0 by E3, E4;
end;
then reconsider c4 = c2 as eventually-positive Real_Sequence ;
take c3 ;
take c4 ;
ex b1 being Real_Sequence st
( b1 . 0 = 0 & for b2 being Nat holds
( b2 > 0 implies b1 . b2 = ((12 * (b2 to_power 3)) * (log 2,b2)) - (5 * (b2 ^2 )) ) )
proof
defpred S1[ Nat, Real] means ( ( a1 = 0 implies a2 = 0 ) & ( a1 > 0 implies a2 = ((12 * (a1 to_power 3)) * (log 2,a1)) - (5 * (a1 ^2 )) ) );
E4: for b1 being Element of NAT holds
ex b2 being Element of REAL st
S1[b1,b2]
proof
let c5 be Nat;
not ( not c5 = 0 & not c5 > 0 ) ;
hence ex b1 being Element of REAL st
S1[c5,b1] ;
end;
consider c5 being Function of NAT , REAL such that
E5: for b1 being Element of NAT holds
S1[b1,c5 . b1] from FUNCT_2:sch 3(E4);
 take c5 ;
thus c5 . 0 = 0 by E5;
let c6 be Nat;
thus ( c6 > 0 implies c5 . c6 = ((12 * (c6 to_power 3)) * (log 2,c6)) - (5 * (c6 ^2 )) ) by E5;
end;
then consider c5 being Real_Sequence such that
E4: ( c5 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies c5 . b1 = ((12 * (b1 to_power 3)) * (log 2,b1)) - (5 * (b1 ^2 )) ) ) ;
c5 is eventually-positive
proof
take 3 ; :: uses ASYMPT_0:def 6
let c6 be Nat;
assume E5: c6 >= 3 ;
then c6 > 1 by XREAL_1:2;
then E6: c6 to_power 3 > c6 to_power 2 by POWER:44;
E7: c6 to_power 2 > 0 by E5, POWER:39;
E8: log 2,c6 >= log 2,3 by E5, PRE_FF:12;
log 2,3 > log 2,2 by POWER:65;
then log 2,3 > 1 by POWER:60;
then log 2,c6 > 1 by E8, XREAL_1:2;
then (c6 to_power 3) * (log 2,c6) > (c6 to_power 2) * 1 by E6, E7, REAL_2:199;
then 12 * ((c6 to_power 3) * (log 2,c6)) > 5 * (c6 to_power 2) by E7, REAL_2:199;
then (12 * (c6 to_power 3)) * (log 2,c6) > (5 * (c6 ^2 )) + 0 by POWER:53;
then ((12 * (c6 to_power 3)) * (log 2,c6)) - (5 * (c6 ^2 )) > 0 by XREAL_1:22;
hence c5 . c6 > 0 by E4, E5;
end;
then reconsider c6 = c5 as eventually-positive Real_Sequence ;
ex b1 being Real_Sequence st
( b1 . 0 = 0 & for b2 being Nat holds
( b2 > 0 implies b1 . b2 = ((log 2,b2) ^2 ) + 36 ) )
proof
defpred S1[ Nat, Real] means ( ( a1 = 0 implies a2 = 0 ) & ( a1 > 0 implies a2 = ((log 2,a1) ^2 ) + 36 ) );
E5: for b1 being Element of NAT holds
ex b2 being Element of REAL st
S1[b1,b2]
proof
let c7 be Nat;
per cases not ( not c7 = 0 & not c7 > 0 ) ;
suppose c7 = 0 ;
hence ex b1 being Element of REAL st
S1[c7,b1] ;
end;
suppose c7 > 0 ;
hence ex b1 being Element of REAL st
S1[c7,b1] ;
end;
end;
end;
consider c7 being Function of NAT , REAL such that
E6: for b1 being Element of NAT holds
S1[b1,c7 . b1] from FUNCT_2:sch 3(E5);
 take c7 ;
thus ( c7 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies c7 . b1 = ((log 2,b1) ^2 ) + 36 ) ) by E6;
end;
then consider c7 being Real_Sequence such that
E5: ( c7 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies c7 . b1 = ((log 2,b1) ^2 ) + 36 ) ) ;
c7 is eventually-positive
proof
take 1 ; :: uses ASYMPT_0:def 6
let c8 be Nat;
assume E6: c8 >= 1 ;
(log 2,c8) ^2 >= 0 by SQUARE_1:72;
then ((log 2,c8) ^2 ) + 36 > 0 + 0 by XREAL_1:10;
hence c7 . c8 > 0 by E5, E6;
end;
then reconsider c8 = c7 as eventually-positive Real_Sequence ;
set c9 = max c6,c8;
for b1 being Nat holds c3 . b1 = (c6 . b1) + (c8 . b1)
proof
let c10 be Nat;
thus c3 . c10 = (c6 . c10) + (c8 . c10)
proof
per cases not ( not c10 = 0 & not c10 > 0 ) ;
suppose c10 = 0 ;
hence c3 . c10 = (c6 . c10) + (c8 . c10) by E2, E4, E5;
end;
suppose E6: c10 > 0 ;
then c6 . c10 = ((12 * (c10 to_power 3)) * (log 2,c10)) - (5 * (c10 ^2 )) by E4;
then (c6 . c10) + (c8 . c10) = (((12 * (c10 to_power 3)) * (log 2,c10)) - (5 * (c10 ^2 ))) + (((log 2,c10) ^2 ) + 36) by E5, E6
.= ((((12 * (c10 to_power 3)) * (log 2,c10)) - (5 * (c10 ^2 ))) + ((log 2,c10) ^2 )) + 36 ;
hence c3 . c10 = (c6 . c10) + (c8 . c10) by E2, E6;
end;
end;
end;
end;
then E6: Big_Oh c3 = Big_Oh (c6 + c8) by SEQ_1:11
.= Big_Oh (max c6,c8) by ASYMPT_0:9 ;
4 = 2 * 2
.= 2 ^2 by SQUARE_1:def 3
.= 2 to_power 2 by POWER:53 ;
then E7: log 2,4 = 2 * (log 2,2) by POWER:63
.= 2 * 1 by POWER:60
.= 2 ;
E8: for b1 being Nat holds
not ( b1 >= 4 & not 7 * (b1 ^2 ) > c8 . b1 )
proof
defpred S1[ Nat] means 7 * (a1 ^2 ) > c8 . a1;
E9: S1[4]
proof
E10: 7 * (4 ^2 ) = 7 * (4 * 4) by SQUARE_1:def 3
.= 112 ;
c8 . 4 = (2 ^2 ) + 36 by E5, E7
.= (2 * 2) + 36 by SQUARE_1:def 3
.= 40 ;
hence S1[4] by E10;
end;
E10: for b1 being Nat holds
( ( b1 >= 4 & S1[b1] ) implies ( S1[b1 + 1] ) )
proof
let c10 be Nat;
assume that E11: c10 >= 4
and E12: 7 * (c10 ^2 ) > c8 . c10 ;
E13: c8 . c10 = ((log 2,c10) ^2 ) + 36 by E5, E11;
7 * ((c10 + 1) ^2 ) = 7 * (((c10 ^2 ) + (2 * c10)) + 1) by SQUARE_1:65
.= (7 * (c10 ^2 )) + ((7 * (2 * c10)) + (7 * 1)) ;
then E14: 7 * ((c10 + 1) ^2 ) > (c8 . c10) + ((7 * (2 * c10)) + (7 * 1)) by E12, XREAL_1:8;
E15: c8 . (c10 + 1) = ((log 2,(c10 + 1)) ^2 ) + 36 by E5;
c10 >= 1 by E11, XREAL_1:2;
then c10 + c10 >= c10 + 1 by XREAL_1:8;
then E16: log 2,(c10 + c10) >= log 2,(c10 + 1) by PRE_FF:12;
c10 + 1 >= 4 + 0 by E11, XREAL_1:10;
then log 2,(c10 + 1) >= 2 by E7, PRE_FF:12;
then (log 2,(c10 + c10)) ^2 >= (log 2,(c10 + 1)) ^2 by E16, SQUARE_1:77;
then E17: c8 . (c10 + 1) <= ((log 2,(c10 + c10)) ^2 ) + 36 by E15, XREAL_1:8;
log 2,(c10 + c10) = log 2,(2 * c10) ;
then log 2,(c10 + c10) = (log 2,c10) + (log 2,2) by E11, POWER:61;
then E18: (log 2,(c10 + c10)) ^2 = ((log 2,c10) + 1) ^2 by POWER:60
.= (((log 2,c10) ^2 ) + (2 * (log 2,c10))) + 1 by SQUARE_1:65 ;
c10 >= 2 by E11, XREAL_1:2;
then E19: 2 to_power c10 > c10 + 1 by E1;
E20: log 2,c10 >= 2 by E7, E11, PRE_FF:12;
c10 + 1 > c10 + 0 by XREAL_1:10;
then 2 to_power c10 > c10 by E19, XREAL_1:2;
then log 2,(2 to_power c10) > log 2,c10 by E11, POWER:65;
then c10 * (log 2,2) > log 2,c10 by POWER:63;
then c10 * 1 > log 2,c10 by POWER:60;
then 14 * c10 > 2 * (log 2,c10) by E20, REAL_2:199;
then ((7 * 2) * c10) + 7 > (2 * (log 2,c10)) + 1 by XREAL_1:10;
then ((log 2,c10) ^2 ) + ((2 * (log 2,c10)) + 1) < ((log 2,c10) ^2 ) + ((7 * (2 * c10)) + 7) by XREAL_1:8;
then ((log 2,(c10 + c10)) ^2 ) + 36 < (((log 2,c10) ^2 ) + ((7 * (2 * c10)) + 7)) + 36 by E18, XREAL_1:8;
then (c8 . c10) + ((7 * (2 * c10)) + (7 * 1)) > c8 . (c10 + 1) by E13, E17, XREAL_1:2;
hence S1[c10 + 1] by E14, XREAL_1:2;
end;
for b1 being Nat holds
( b1 >= 4 implies S1[b1] ) from INT_2:sch 1(E9, E10);
 hence for b1 being Nat holds
not ( b1 >= 4 & not 7 * (b1 ^2 ) > c8 . b1 ) ;
end;
E9: for b1 being Nat holds
not ( b1 >= 4 & not c6 . b1 > 7 * (b1 ^2 ) )
proof
let c10 be Nat;
assume E10: c10 >= 4 ;
then E11: c6 . c10 = ((12 * (c10 to_power 3)) * (log 2,c10)) - (5 * (c10 ^2 )) by E4;
c10 > 1 by E10, XREAL_1:2;
then E12: c10 to_power 3 > c10 to_power 2 by POWER:44;
E13: c10 to_power 2 > 0 by E10, POWER:39;
log 2,c10 >= log 2,4 by E10, PRE_FF:12;
then log 2,c10 > 1 by E7, XREAL_1:2;
then (c10 to_power 3) * (log 2,c10) > (c10 to_power 2) * 1 by E12, E13, REAL_2:199;
then 12 * ((c10 to_power 3) * (log 2,c10)) > 12 * (c10 to_power 2) by XREAL_1:70;
then (12 * (c10 to_power 3)) * (log 2,c10) > 12 * (c10 ^2 ) by POWER:53;
then c6 . c10 > (12 * (c10 ^2 )) - (5 * (c10 ^2 )) by E11, XREAL_1:11;
hence c6 . c10 > 7 * (c10 ^2 ) ;
end;
E10: for b1 being Nat holds
not ( b1 >= 4 & not c6 . b1 > c8 . b1 )
proof
let c10 be Nat;
assume E11: c10 >= 4 ;
then E12: c6 . c10 > 7 * (c10 ^2 ) by E9;
7 * (c10 ^2 ) > c8 . c10 by E8, E11;
hence c6 . c10 > c8 . c10 by E12, XREAL_1:2;
end;
E11: for b1 being Nat holds
( b1 >= 4 implies (max c6,c8) . b1 = c6 . b1 )
proof
let c10 be Nat;
assume c10 >= 4 ;
then E12: c6 . c10 > c8 . c10 by E10;
thus (max c6,c8) . c10 = max (c6 . c10),(c8 . c10) by ASYMPT_0:def 10
.= c6 . c10 by E12, SQUARE_1:def 2 ;
end;
E12: max c6,c8 is Element of Funcs NAT ,REAL by FUNCT_2:11;
consider c10 being Nat such that
E13: for b1 being Nat holds
not ( b1 >= c10 & not (max c6,c8) . b1 > 0 ) by ASYMPT_0:def 6;
now
let c11 be Nat;
assume E14: c11 >= max 4,c10 ;
E15: ( max 4,c10 >= 4 & max 4,c10 >= c10 ) by SQUARE_1:46;
then E16: ( c11 >= 4 & c11 >= c10 ) by E14, XREAL_1:2;
then E17: (max c6,c8) . c11 = c6 . c11 by E11
.= ((12 * (c11 to_power 3)) * (log 2,c11)) - (5 * (c11 ^2 )) by E4, E14, E15 ;
c11 to_power 2 > 0 by E14, E15, POWER:39;
then c11 ^2 > 0 by POWER:53;
then 5 * (c11 ^2 ) > 5 * 0 by XREAL_1:70;
then (max c6,c8) . c11 <= ((12 * (c11 to_power 3)) * (log 2,c11)) - 0 by E17, REAL_1:92;
then (max c6,c8) . c11 <= 12 * ((c11 to_power 3) * (log 2,c11)) ;
hence (max c6,c8) . c11 <= 12 * (c4 . c11) by E3, E14, E15;
thus (max c6,c8) . c11 >= 0 by E13, E16;
end;
then E14: max c6,c8 in Big_Oh c4 by E12;
c3 in Big_Oh c3 by ASYMPT_0:10;
hence ( c3 = c1 & c4 = c2 & c3 in Big_Oh c4 ) by E6, E14, ASYMPT_0:12;
end;

E2: for b1 being logbase Real
for b2 being Real_Sequence holds
( ( b2 . 0 = 0 & for b3 being Nat holds
( b3 > 0 implies b2 . b3 = log b1,b3 ) ) implies ( not b1 > 1 or b2 is eventually-positive ) )
proof
let c1 be logbase Real;
let c2 be Real_Sequence;
assume that E3: c1 > 1
and E4: ( c2 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies c2 . b1 = log c1,b1 ) ) ;
E5: ( c1 > 0 & c1 <> 1 ) by ASYMPT_0:def 3;
set c3 = [/c1\];
E6: [/c1\] >= c1 by INT_1:def 5;
E7: [/c1\] > 0 by E5, INT_1:def 5;
then reconsider c4 = [/c1\] as Nat by INT_1:16;
now
let c5 be Nat;
assume E8: c5 >= c4 + 1 ;
c4 + 1 > c4 + 0 by XREAL_1:10;
then c5 > c4 by E8, XREAL_1:2;
then E9: log c1,c5 > log c1,c4 by E3, E7, POWER:65;
log c1,c4 >= log c1,c1 by E3, E6, PRE_FF:12;
then log c1,c5 > log c1,c1 by E9, XREAL_1:2;
then log c1,c5 > 0 by E5, POWER:60;
hence c2 . c5 > 0 by E4, E8;
end;
hence c2 is eventually-positive by ASYMPT_0:def 6;
end;

theorem :: ASYMPT_1:2
for b1, b2 being logbase Real
for b3, b4 being Real_Sequence holds
not ( b1 > 1 & b2 > 1 & b3 . 0 = 0 & for b5 being Nat holds
( b5 > 0 implies b3 . b5 = log b1,b5 ) & b4 . 0 = 0 & for b5 being Nat holds
( b5 > 0 implies b4 . b5 = log b2,b5 ) & for b5, b6 being eventually-positive Real_Sequence holds
not ( b5 = b3 & b6 = b4 & Big_Oh b5 = Big_Oh b6 ) )
proof
let c1, c2 be logbase Real;
let c3, c4 be Real_Sequence;
assume that E3: c1 > 1
and E4: c2 > 1
and E5: ( c3 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies c3 . b1 = log c1,b1 ) )
and E6: ( c4 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies c4 . b1 = log c2,b1 ) ) ;
reconsider c5 = c3 as eventually-positive Real_Sequence by E3, E5, E2;
reconsider c6 = c4 as eventually-positive Real_Sequence by E4, E6, E2;
take c5 ;
take c6 ;
E7: ( c1 > 0 & c1 <> 1 ) by ASYMPT_0:def 3;
E8: ( c2 > 0 & c2 <> 1 ) by ASYMPT_0:def 3;
now
let c7 be set ;
hereby
assume c7 in Big_Oh c5 ;
then consider c8 being Element of Funcs NAT ,REAL such that
E9: c7 = c8
and E10: ex b1 being Realex b2 being Nat st
( b1 > 0 & for b3 being Nat holds
( b3 >= b2 implies ( c8 . b3 <= b1 * (c5 . b3) & c8 . b3 >= 0 ) ) ) ;
consider c9 being Real, c10 being Nat such that
E11: c9 > 0
and E12: for b1 being Nat holds
( b1 >= c10 implies ( c8 . b1 <= c9 * (c5 . b1) & c8 . b1 >= 0 ) ) by E10;
log c1,c2 > log c1,1 by E3, E4, POWER:65;
then log c1,c2 > 0 by E7, POWER:59;
then E13: c9 * (log c1,c2) > c9 * 0 by E11, XREAL_1:70;
now
take c11 = c10 + 1;
let c12 be Nat;
assume E14: c12 >= c11 ;
c10 + 1 > c10 + 0 by XREAL_1:10;
then E15: c12 > c10 by E14, XREAL_1:2;
then E16: c8 . c12 <= c9 * (c5 . c12) by E12;
c5 . c12 = log c1,c12 by E5, E14
.= (log c1,c2) * (log c2,c12) by E7, E8, E14, POWER:64 ;
then c8 . c12 <= (c9 * (log c1,c2)) * (log c2,c12) by E16;
hence c8 . c12 <= (c9 * (log c1,c2)) * (c6 . c12) by E6, E14;
thus c8 . c12 >= 0 by E12, E15;
end;
hence c7 in Big_Oh c6 by E9, E13;
end;assume c7 in Big_Oh c6 ;
then consider c8 being Element of Funcs NAT ,REAL such that
E9: c7 = c8
and E10: ex b1 being Realex b2 being Nat st
( b1 > 0 & for b3 being Nat holds
( b3 >= b2 implies ( c8 . b3 <= b1 * (c6 . b3) & c8 . b3 >= 0 ) ) ) ;
consider c9 being Real, c10 being Nat such that
E11: c9 > 0
and E12: for b1 being Nat holds
( b1 >= c10 implies ( c8 . b1 <= c9 * (c6 . b1) & c8 . b1 >= 0 ) ) by E10;
log c2,c1 > log c2,1 by E3, E4, POWER:65;
then log c2,c1 > 0 by E8, POWER:59;
then E13: c9 * (log c2,c1) > c9 * 0 by E11, XREAL_1:70;
now
take c11 = c10 + 1;
let c12 be Nat;
assume E14: c12 >= c11 ;
c10 + 1 > c10 + 0 by XREAL_1:10;
then E15: c12 > c10 by E14, XREAL_1:2;
then E16: c8 . c12 <= c9 * (c6 . c12) by E12;
c6 . c12 = log c2,c12 by E6, E14
.= (log c2,c1) * (log c1,c12) by E7, E8, E14, POWER:64 ;
then c8 . c12 <= (c9 * (log c2,c1)) * (log c1,c12) by E16;
hence c8 . c12 <= (c9 * (log c2,c1)) * (c5 . c12) by E5, E14;
thus c8 . c12 >= 0 by E12, E15;
end;
hence c7 in Big_Oh c5 by E9, E13;
end;
hence ( c5 = c3 & c6 = c4 & Big_Oh c5 = Big_Oh c6 ) by TARSKI:2;
end;

definition
let c1, c2, c3 be Real;
func seq_a^ a1,a2,a3 -> Real_Sequence means :E3: :: ASYMPT_1:def 1
for b1 being Nat holds a4 . b1 = a1 to_power ((a2 * b1) + a3);
existence
ex b1 being Real_Sequence st
for b2 being Nat holds b1 . b2 = c1 to_power ((c2 * b2) + c3)
proof
deffunc H1( Nat) -> Element of REAL = c1 to_power ((c2 * a1) + c3);
consider c4 being Function of NAT , REAL such that
E3: for b1 being Nat holds c4 . b1 = H1(b1) from FUNCT_2:sch 4();
 take c4 ;
let c5 be Nat;
thus c4 . c5 = c1 to_power ((c2 * c5) + c3) by E3;
end;
uniqueness
for b1, b2 being Real_Sequence holds
( ( for b3 being Nat holds b1 . b3 = c1 to_power ((c2 * b3) + c3) & for b3 being Nat holds b2 . b3 = c1 to_power ((c2 * b3) + c3) ) implies ( b1 = b2 ) )
proof
let c4, c5 be Real_Sequence;
assume that E3: for b1 being Nat holds c4 . b1 = c1 to_power ((c2 * b1) + c3)
and E4: for b1 being Nat holds c5 . b1 = c1 to_power ((c2 * b1) + c3) ;
now
let c6 be Nat;
thus c4 . c6 = c1 to_power ((c2 * c6) + c3) by E3
.= c5 . c6 by E4 ;
end;
hence c4 = c5 by FUNCT_2:113;
end;
end;

:: deftheorem E3 defines seq_a^ ASYMPT_1:def 1 :
for b1, b2, b3 being Real
for b4 being Real_Sequence holds
( b4 = seq_a^ b1,b2,b3 iff for b5 being Nat holds b4 . b5 = b1 to_power ((b2 * b5) + b3) );

registration
let c1 be positive Real;
let c2, c3 be Real;
cluster seq_a^ a1,a2,a3 -> eventually-positive ;
coherence
seq_a^ c1,c2,c3 is eventually-positive
proof
set c4 = seq_a^ c1,c2,c3;
take 0 ; :: uses ASYMPT_0:def 6
let c5 be Nat;
assume c5 >= 0 ;
(seq_a^ c1,c2,c3) . c5 = c1 to_power ((c2 * c5) + c3) by E3;
hence (seq_a^ c1,c2,c3) . c5 > 0 by POWER:39;
end;
end;

E4: for b1, b2, b3 being Real holds
( ( ) implies ( not b1 > 0 or not b3 > 0 or not b3 <> 1 or b1 to_power b2 = b3 to_power (b2 * (log b3,b1)) ) )
proof
let c1, c2, c3 be Real;
assume that E5: c1 > 0
and E6: c3 > 0
and E7: c3 <> 1 ;
E8: c1 to_power c2 > 0 by E5, POWER:39;
log c3,(c1 to_power c2) = c2 * (log c3,c1) by E5, E6, E7, POWER:63;
hence c1 to_power c2 = c3 to_power (c2 * (log c3,c1)) by E6, E7, E8, POWER:def 3;
end;

theorem :: ASYMPT_1:3
for b1, b2 being positive Real holds
not ( b1 < b2 & seq_a^ b2,1,0 in Big_Oh (seq_a^ b1,1,0) )
proof
let c1, c2 be positive Real;
assume E5: c1 < c2 ;
set c3 = seq_a^ c2,1,0;
set c4 = seq_a^ c1,1,0;
hereby
assume seq_a^ c2,1,0 in Big_Oh (seq_a^ c1,1,0) ;
then consider c5 being Element of Funcs NAT ,REAL such that
E6: c5 = seq_a^ c2,1,0
and E7: ex b1 being Realex b2 being Nat st
( b1 > 0 & for b3 being Nat holds
( b3 >= b2 implies ( c5 . b3 <= b1 * ((seq_a^ c1,1,0) . b3) & c5 . b3 >= 0 ) ) ) ;
consider c6 being Real, c7 being Nat such that
E8: c6 > 0
and E9: for b1 being Nat holds
( b1 >= c7 implies ( c5 . b1 <= c6 * ((seq_a^ c1,1,0) . b1) & c5 . b1 >= 0 ) ) by E7;
set c8 = (log 2,c2) - (log 2,c1);
log 2,c2 > (log 2,c1) + 0 by E5, POWER:65;
then E10: (log 2,c2) - (log 2,c1) > 0 by XREAL_1:22;
set c9 = [/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\];
set c10 = max c7,[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\];
E11: ( max c7,[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] >= c7 & max c7,[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] >= [/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] ) by SQUARE_1:46;
( max c7,[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] = c7 or max c7,[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] = [/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] ) by SQUARE_1:49;
then reconsider c11 = max c7,[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] as Nat by E11, INT_1:16;
set c12 = c11 + 1;
set c13 = 2 to_power ((c11 + 1) * (log 2,c1));
E12: 2 to_power ((c11 + 1) * (log 2,c1)) > 0 by POWER:39;
c11 + 1 > c11 + 0 by XREAL_1:10;
then E13: ( c11 + 1 > c7 & c11 + 1 > [/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] ) by E11, XREAL_1:2;
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] >= (log 2,c6) / ((log 2,c2) - (log 2,c1)) by INT_1:def 5;
then c11 + 1 > (log 2,c6) / ((log 2,c2) - (log 2,c1)) by E13, XREAL_1:2;
then (c11 + 1) * ((log 2,c2) - (log 2,c1)) > ((log 2,c6) / ((log 2,c2) - (log 2,c1))) * ((log 2,c2) - (log 2,c1)) by E10, XREAL_1:70;
then (c11 + 1) * ((log 2,c2) - (log 2,c1)) > log 2,c6 by E10, XCMPLX_1:88;
then 2 to_power ((c11 + 1) * ((log 2,c2) - (log 2,c1))) > 2 to_power (log 2,c6) by POWER:44;
then 2 to_power (((c11 + 1) * (log 2,c2)) - ((c11 + 1) * (log 2,c1))) > c6 by E8, POWER:def 3;
then (2 to_power ((c11 + 1) * (log 2,c2))) / (2 to_power ((c11 + 1) * (log 2,c1))) > c6 by POWER:34;
then ((2 to_power ((c11 + 1) * (log 2,c2))) / (2 to_power ((c11 + 1) * (log 2,c1)))) * (2 to_power ((c11 + 1) * (log 2,c1))) > c6 * (2 to_power ((c11 + 1) * (log 2,c1))) by E12, XREAL_1:70;
then 2 to_power ((c11 + 1) * (log 2,c2)) > c6 * (2 to_power ((c11 + 1) * (log 2,c1))) by E12, XCMPLX_1:88;
then c2 to_power (c11 + 1) > c6 * (2 to_power ((c11 + 1) * (log 2,c1))) by E4;
then E14: c2 to_power (c11 + 1) > c6 * (c1 to_power (c11 + 1)) by E4;
(seq_a^ c2,1,0) . (c11 + 1) <= c6 * ((seq_a^ c1,1,0) . (c11 + 1)) by E6, E9, E13;
then c2 to_power ((1 * (c11 + 1)) + 0) <= c6 * ((seq_a^ c1,1,0) . (c11 + 1)) by E3;
hence not verum by E14, E3;
end;
end;

definition
func seq_logn -> Real_Sequence means :E5: :: ASYMPT_1:def 2
( a1 . 0 = 0 & for b1 being Nat holds
( b1 > 0 implies a1 . b1 = log 2,b1 ) );
existence
ex b1 being Real_Sequence st
( b1 . 0 = 0 & for b2 being Nat holds
( b2 > 0 implies b1 . b2 = log 2,b2 ) )
proof
defpred S1[ Nat, Real] means ( ( a1