let f, g be Real_Sequence; :: thesis: ( g . 0 = 0 & ( for n being Element of NAT st n > 0 holds
g . n = n * (log 2,n) ) & ( for n being Element of NAT holds f . n = log 2,(n ! ) ) implies ex s being eventually-nonnegative Real_Sequence st
( s = g & f in Big_Theta s ) )
assume that
A1: ( g . 0 = 0 & ( for n being Element of NAT st n > 0 holds
g . n = n * (log 2,n) ) ) and
A2: for n being Element of NAT holds f . n = log 2,(n ! ) ; :: thesis: ex s being eventually-nonnegative Real_Sequence st
( s = g & f in Big_Theta s )
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 A3: n >= 2 ; :: thesis: not g . n <= 0
then log 2,n >= log 2,2 by PRE_FF:12;
then log 2,n >= 1 by POWER:60;
then n * (log 2,n) > n * 0 by A3, XREAL_1:70;
hence not g . n <= 0 by A1, A3; :: thesis: verum
end;
then reconsider g = g as eventually-positive Real_Sequence ;
take g ; :: thesis: ( g = g & f in Big_Theta g )
set h = seq_logn ;
A4: Big_Theta g = { s where s is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (g . n) <= s . n & s . n <= c * (g . n) ) ) ) } by ASYMPT_0:27;
A5: f is Element of Funcs NAT ,REAL by FUNCT_2:11;
now
let n be Element of NAT ; :: thesis: ( n >= 4 implies ( (1 / 4) * (g . n) <= f . n & f . n <= 1 * (g . n) ) )
assume A6: n >= 4 ; :: thesis: ( (1 / 4) * (g . n) <= f . n & f . n <= 1 * (g . n) )
ex s being Real_Sequence st
( s . 0 = 0 & ( for m being Element of NAT st m > 0 holds
s . m = log 2,(n / 2) ) )
proof
defpred S1[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = log 2,(n / 2) ) );
A7: 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 = 0 or n > 0 ) ;
suppose n = 0 ; :: 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 n > 0 ; :: 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;
end;
end;
consider h being Function of NAT ,REAL such that
A8: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A7);
 take h ; :: thesis: ( h . 0 = 0 & ( for m being Element of NAT st m > 0 holds
h . m = log 2,(n / 2) ) )
thus h . 0 = 0 by A8; :: thesis: for m being Element of NAT st m > 0 holds
h . m = log 2,(n / 2)
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = log 2,(n / 2) )
thus ( n > 0 implies h . n = log 2,(n / 2) ) by A8; :: thesis: verum
end;
then consider p being Real_Sequence such that
A9: ( p . 0 = 0 & ( for m being Element of NAT st m > 0 holds
p . m = log 2,(n / 2) ) ) ;
ex s being Real_Sequence st
( s . 0 = 0 & ( for m being Element of NAT st m > 0 holds
s . m = log 2,n ) )
proof
defpred S1[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = log 2,n ) );
A10: 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 = 0 or n > 0 ) ;
suppose n = 0 ; :: 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 n > 0 ; :: 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;
end;
end;
consider h being Function of NAT ,REAL such that
A11: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A10);
 take h ; :: thesis: ( h . 0 = 0 & ( for m being Element of NAT st m > 0 holds
h . m = log 2,n ) )
thus h . 0 = 0 by A11; :: thesis: for m being Element of NAT st m > 0 holds
h . m = log 2,n
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = log 2,n )
thus ( n > 0 implies h . n = log 2,n ) by A11; :: thesis: verum
end;
then consider q being Real_Sequence such that
A12: ( q . 0 = 0 & ( for m being Element of NAT st m > 0 holds
q . m = log 2,n ) ) ;
set n1 = [/(n / 2)\];
A13: n * (2 " ) > 0 * (2 " ) by A6, XREAL_1:70;
A14: [/(n / 2)\] >= n / 2 by INT_1:def 5;
then reconsider n1 = [/(n / 2)\] as Element of NAT by INT_1:16;
set n2 = n1 - 1;
now
assume n1 - 1 < 0 ; :: thesis: contradiction
then n1 - 1 <= - 1 by INT_1:21;
then (n1 - 1) + 1 <= (- 1) + 1 by XREAL_1:8;
hence contradiction by A13, INT_1:def 5; :: thesis: verum
end;
then reconsider n2 = n1 - 1 as Element of NAT by INT_1:16;
for k being Element of NAT st k <= n2 holds
seq_logn . k >= 0
proof
let k be Element of NAT ; :: thesis: ( k <= n2 implies seq_logn . k >= 0 )
assume k <= n2 ; :: thesis: seq_logn . k >= 0
end;
then Sum seq_logn ,n2 >= 0 by Lm17;
then (Sum seq_logn ,n) + (Sum seq_logn ,n2) >= (Sum seq_logn ,n) + 0 by XREAL_1:8;
then Sum seq_logn ,n >= (Sum seq_logn ,n) - (Sum seq_logn ,n2) by XREAL_1:22;
then A16: Sum seq_logn ,n >= Sum seq_logn ,n,n2 by SERIES_1:def 7;
n >= n1 by Lm22;
then n + (- 1) >= n1 + (- 1) by XREAL_1:8;
then n - 1 >= n1 + (- 1) ;
then A17: n >= n2 + 1 by XREAL_1:21;
for k being Element of NAT st n2 + 1 <= k & k <= n holds
p . k <= seq_logn . k
proof
let k be Element of NAT ; :: thesis: ( n2 + 1 <= k & k <= n implies p . k <= seq_logn . k )
assume that
A18: n2 + 1 <= k and
k <= n ; :: thesis: p . k <= seq_logn . k
n / 2 <= k by A14, A18, XXREAL_0:2;
then log 2,(n / 2) <= log 2,k by A13, PRE_FF:12;
then p . k <= log 2,k by A9, A18;
hence p . k <= seq_logn . k by A18, Def2; :: thesis: verum
end;
then A19: Sum seq_logn ,n,n2 >= Sum p,n,n2 by A17, Lm21;
A20: now
assume A21: n - n2 < n / 2 ; :: thesis: contradiction
[/(n / 2)\] < (n / 2) + 1 by INT_1:def 5;
then n2 < n / 2 by XREAL_1:21;
then (n / 2) + n2 < (n / 2) + (n / 2) by XREAL_1:8;
hence contradiction by A21, XREAL_1:21; :: thesis: verum
end;
A22: Sum p,n,n2 = (n - n2) * (log 2,(n / 2)) by A9, Lm23;
2 * 2 <= n by A6;
then 2 <= n / 2 by XREAL_1:79;
then log 2,2 <= log 2,(n / 2) by PRE_FF:12;
then 1 <= log 2,(n / 2) by POWER:60;
then A23: Sum p,n,n2 >= (n / 2) * (log 2,(n / 2)) by A20, A22, XREAL_1:66;
A24: (n / 2) * (log 2,(n / 2)) = (n / 2) * ((log 2,n) - (log 2,2)) by A6, POWER:62
.= (n / 2) * ((log 2,n) - 1) by POWER:60
.= ((n * (log 2,n)) / 2) - (n / 2) ;
(n * (log 2,n)) * (4 " ) >= (2 * n) * (4 " ) by A6, Lm51, XREAL_1:66;
then ((n * (log 2,n)) / 2) - ((n * (log 2,n)) / 4) >= n / 2 ;
then (n * (log 2,n)) / 2 >= (n / 2) + ((n * (log 2,n)) / 4) by XREAL_1:21;
then A25: ((n * (log 2,n)) / 2) - (n / 2) >= (n * (log 2,n)) / 4 by XREAL_1:21;
(n * (log 2,n)) / 4 = (g . n) / 4 by A1, A6
.= (1 / 4) * (g . n) ;
then Sum p,n,n2 >= (1 / 4) * (g . n) by A23, A24, A25, XXREAL_0:2;
then Sum seq_logn ,n,n2 >= (1 / 4) * (g . n) by A19, XXREAL_0:2;
then Sum seq_logn ,n >= (1 / 4) * (g . n) by A16, XXREAL_0:2;
hence (1 / 4) * (g . n) <= f . n by A2, Lm50; :: thesis: f . n <= 1 * (g . n)
A26: log 2,(n ! ) = f . n by A2
.= Sum seq_logn ,n by A2, Lm50 ;
for k being Element of NAT st k <= n holds
seq_logn . k <= q . k
proof
let k be Element of NAT ; :: thesis: ( k <= n implies seq_logn . k <= q . k )
assume A27: k <= n ; :: thesis: seq_logn . k <= q . k
end;
then A29: Sum seq_logn ,n <= Sum q,n by Lm18;
Sum q,n = n * (log 2,n) by A12, Lm19;
then log 2,(n ! ) <= 1 * (g . n) by A1, A6, A26, A29;
hence f . n <= 1 * (g . n) by A2; :: thesis: verum
end;
hence ( g = g & f in Big_Theta g ) by A4, A5; :: thesis: verum