set h = seq_logn ;
let f, g be Real_Sequence; :: thesis: ( ( 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: 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 b₁ being Element of NAT holds
( not 2 <= b₁ or not g . b₁ <= 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 ;

A4: now

let n be Element of NAT ; :: thesis: ( n >= 4 implies ( (1 / 4) * (g . n) <= f . n & f . n <= 1 * (g . n) ) )
set n1 = [/(n / 2)\];
assume A5: n >= 4 ; :: thesis: ( (1 / 4) * (g . n) <= f . n & f . n <= 1 * (g . n) )
then A6: (n / 2) * (log 2,(n / 2)) = (n / 2) * ((log 2,n) - (log 2,2)) by POWER:62
.= (n / 2) * ((log 2,n) - 1) by POWER:60
.= ((n * (log 2,n)) / 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 / 2) ) )

proof

defpred S₁[ 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 S₁[x,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[n,y]

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: ex y being Element of REAL st S₁[n,y]

hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex y being Element of REAL st S₁[n,y]

hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

end;

end;

consider h being Function of NAT ,REAL such that
A8: for x being Element of NAT holds S₁[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 and
A10: for m being Element of NAT st m > 0 holds
p . m = log 2,(n / 2) ;
A11: [/(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;
A12: n * (2 " ) > 0 * (2 " ) by A5, XREAL_1:70;

A13: 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 A12, INT_1:def 5; :: thesis: verum

end;

(n * (log 2,n)) * (4 " ) >= (2 * n) * (4 " ) by A5, Lm45, 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 A14: ((n * (log 2,n)) / 2) - (n / 2) >= (n * (log 2,n)) / 4 by XREAL_1:21;
2 * 2 <= n by A5;
then 2 <= n / 2 by XREAL_1:79;
then log 2,2 <= log 2,(n / 2) by PRE_FF:12;
then A15: 1 <= log 2,(n / 2) by POWER:60;
reconsider n2 = n1 - 1 as Element of NAT by A13, INT_1:16;
A16: 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
A17: n2 + 1 <= k and
k <= n ; :: thesis: p . k <= seq_logn . k
n / 2 <= k by A11, A17, XXREAL_0:2;
then log 2,(n / 2) <= log 2,k by A12, PRE_FF:12;
then p . k <= log 2,k by A10, A17;
hence p . k <= seq_logn . k by A17, Def2; :: thesis: verum

end;

n >= n1 by Lm17;
then A18: Sum seq_logn ,n,n2 >= Sum p,n,n2 by A16, Lm16;

A19: now

[/(n / 2)\] < (n / 2) + 1 by INT_1:def 5;
then n2 < n / 2 by XREAL_1:21;
then A20: (n / 2) + n2 < (n / 2) + (n / 2) by XREAL_1:8;
assume n - n2 < n / 2 ; :: thesis: contradiction
hence contradiction by A20, XREAL_1:21; :: thesis: verum

end;

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

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: seq_logn . k >= 0

hence seq_logn . k >= 0 by Def2; :: thesis: verum

end;

suppose A21: k > 0 ; :: thesis: seq_logn . k >= 0

then k >= 0 + 1 by NAT_1:13;
then log 2,k >= log 2,1 by PRE_FF:12;
then log 2,k >= 0 by POWER:59;
hence seq_logn . k >= 0 by A21, Def2; :: thesis: verum

end;

end;

end;

then Sum seq_logn ,n2 >= 0 by Lm12;
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 A22: Sum seq_logn ,n >= Sum seq_logn ,n,n2 by SERIES_1:def 7;
Sum p,n,n2 = (n - n2) * (log 2,(n / 2)) by A9, A10, Lm18;
then A23: Sum p,n,n2 >= (n / 2) * (log 2,(n / 2)) by A19, A15, XREAL_1:66;
(n * (log 2,n)) / 4 = (g . n) / 4 by A1, A5
.= (1 / 4) * (g . n) ;
then Sum p,n,n2 >= (1 / 4) * (g . n) by A23, A6, A14, XXREAL_0:2;
then Sum seq_logn ,n,n2 >= (1 / 4) * (g . n) by A18, XXREAL_0:2;
then Sum seq_logn ,n >= (1 / 4) * (g . n) by A22, XXREAL_0:2;
hence (1 / 4) * (g . n) <= f . n by A2, Lm44; :: thesis: 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 ) )

proof

defpred S₁[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = log 2,n ) );
A24: for x being Element of NAT ex y being Element of REAL st S₁[x,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[n,y]

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: ex y being Element of REAL st S₁[n,y]

hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex y being Element of REAL st S₁[n,y]

hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

end;

end;

consider h being Function of NAT ,REAL such that
A25: for x being Element of NAT holds S₁[x,h . x] from FUNCT_2:sch 3(A24);
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 A25; :: 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 A25; :: thesis: verum

end;

then consider q being Real_Sequence such that
A26: q . 0 = 0 and
A27: for m being Element of NAT st m > 0 holds
q . m = log 2,n ;
A28: Sum q,n = n * (log 2,n) by A26, A27, Lm14;
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 A29: k <= n ; :: thesis: seq_logn . k <= q . k

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: seq_logn . k <= q . k

hence seq_logn . k <= q . k by A26, Def2; :: thesis: verum

end;

suppose A30: k > 0 ; :: thesis: seq_logn . k <= q . k

then log 2,k <= log 2,n by A29, PRE_FF:12;
then seq_logn . k <= log 2,n by A30, Def2;
hence seq_logn . k <= q . k by A27, A30; :: thesis: verum

end;

end;

end;

then A31: Sum seq_logn ,n <= Sum q,n by Lm13;
log 2,(n ! ) = f . n by A2
.= Sum seq_logn ,n by A2, Lm44 ;
then log 2,(n ! ) <= 1 * (g . n) by A1, A5, A31, A28;
hence f . n <= 1 * (g . n) by A2; :: thesis: verum

end;

take g ; :: thesis: ( g = g & f in Big_Theta g )
A32: f is Element of Funcs NAT ,REAL by FUNCT_2:11;
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;
hence ( g = g & f in Big_Theta g ) by A32, A4; :: thesis: verum