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 4 :: 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:10;
then log (2,n) >= 1 by POWER:52;
then n * (log (2,n)) > n * 0 by A3, XREAL_1:68;
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:54
.= (n / 2) * ((log (2,n)) - 1) by POWER:52
.= ((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 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 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 7;
then reconsider n1 = [/(n / 2)\] as Element of NAT by INT_1:3;
set n2 = n1 - 1;
A12: n * (2 ") > 0 * (2 ") by A5, XREAL_1:68;
A13: now
assume n1 - 1 < 0 ; :: thesis: contradiction
then n1 - 1 <= - 1 by INT_1:8;
then (n1 - 1) + 1 <= (- 1) + 1 by XREAL_1:6;
hence contradiction by A12, INT_1:def 7; :: thesis: verum
end;
(n * (log (2,n))) * (4 ") >= (2 * n) * (4 ") by A5, Lm45, XREAL_1:64;
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:19;
then A14: ((n * (log (2,n))) / 2) - (n / 2) >= (n * (log (2,n))) / 4 by XREAL_1:19;
2 * 2 <= n by A5;
then 2 <= n / 2 by XREAL_1:77;
then log (2,2) <= log (2,(n / 2)) by PRE_FF:10;
then A15: 1 <= log (2,(n / 2)) by POWER:52;
reconsider n2 = n1 - 1 as Element of NAT by A13, INT_1:3;
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:10;
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 7;
then n2 < n / 2 by XREAL_1:19;
then A20: (n / 2) + n2 < (n / 2) + (n / 2) by XREAL_1:6;
assume n - n2 < n / 2 ; :: thesis: contradiction
hence contradiction by A20, XREAL_1:19; :: 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
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:6;
then Sum (seq_logn,n) >= (Sum (seq_logn,n)) - (Sum (seq_logn,n2)) by XREAL_1:20;
then A22: Sum (seq_logn,n) >= Sum (seq_logn,n,n2) by SERIES_1:def 6;
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:64;
(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 S1[ 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 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
A25: for x being Element of NAT holds S1[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 A30: k > 0 ; :: thesis: seq_logn . k <= q . k
then log (2,k) <= log (2,n) by A29, PRE_FF:10;
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:8;
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