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 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 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 set holds
( not 2 <= b1 or not g . b1 <= 0 )
let n be Nat; :: thesis: ( not 2 <= n or not g . n <= 0 )
A3: n in NAT by ORDINAL1:def 12;
assume A4: 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 A4, XREAL_1:68;
hence not g . n <= 0 by A1, A4, A3; :: thesis: verum
end;
then reconsider g = g as eventually-positive Real_Sequence ;
A5: now :: thesis: for n being Element of NAT st n >= 4 holds
( (1 / 4) * (g . n) <= f . n & f . n <= 1 * (g . n) )
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 A6: n >= 4 ; :: thesis: ( (1 / 4) * (g . n) <= f . n & f . n <= 1 * (g . n) )
then A7: (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)) ) );
A8: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of REAL st S1[x,y]
per cases ( x = zz or x > 0 ) ;
suppose x = zz ; :: thesis: ex y being Element of REAL st S1[x,y]
hence ex y being Element of REAL st S1[x,y] ; :: thesis: verum
end;
suppose A9: x > 0 ; :: thesis: ex y being Element of REAL st S1[x,y]
log (2,(n / 2)) in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S1[x,y] by A9; :: thesis: verum
end;
end;
end;
consider h being sequence of REAL such that
A10: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A8);
 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 A10; :: 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 A10; :: thesis: verum
end;
then consider p being Real_Sequence such that
A11: p . 0 = 0 and
A12: for m being Element of NAT st m > 0 holds
p . m = log (2,(n / 2)) ;
A13: [/(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;
A14: n * (2 ") > 0 * (2 ") by A6, XREAL_1:68;
A15: now :: thesis: not n1 - 1 < 0
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 A14, INT_1:def 7; :: thesis: verum
end;
(n * (log (2,n))) * (4 ") >= (2 * n) * (4 ") by A6, 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 A16: ((n * (log (2,n))) / 2) - (n / 2) >= (n * (log (2,n))) / 4 by XREAL_1:19;
2 * 2 <= n by A6;
then 2 <= n / 2 by XREAL_1:77;
then log (2,2) <= log (2,(n / 2)) by PRE_FF:10;
then A17: 1 <= log (2,(n / 2)) by POWER:52;
reconsider n2 = n1 - 1 as Element of NAT by A15, INT_1:3;
A18: 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
A19: n2 + 1 <= k and
k <= n ; :: thesis: p . k <= seq_logn . k
n / 2 <= k by A13, A19, XXREAL_0:2;
then log (2,(n / 2)) <= log (2,k) by A14, PRE_FF:10;
then p . k <= log (2,k) by A12, A19;
hence p . k <= seq_logn . k by A19, Def2; :: thesis: verum
end;
n >= n1 by Lm17;
then A20: Sum (seq_logn,n,n2) >= Sum (p,n,n2) by A18, Lm16;
A21: now :: thesis: not n - n2 < n / 2
[/(n / 2)\] < (n / 2) + 1 by INT_1:def 7;
then n2 < n / 2 by XREAL_1:19;
then A22: (n / 2) + n2 < (n / 2) + (n / 2) by XREAL_1:6;
assume n - n2 < n / 2 ; :: thesis: contradiction
hence contradiction by A22, 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 A24: 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 A11, A12, Lm18;
then A25: Sum (p,n,n2) >= (n / 2) * (log (2,(n / 2))) by A21, A17, XREAL_1:64;
(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 A25, A7, A16, XXREAL_0:2;
then Sum (seq_logn,n,n2) >= (1 / 4) * (g . n) by A20, XXREAL_0:2;
then Sum (seq_logn,n) >= (1 / 4) * (g . n) by A24, 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) ) );
A26: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of REAL st S1[x,y]
per cases ( x = zz or x > 0 ) ;
suppose x = zz ; :: thesis: ex y being Element of REAL st S1[x,y]
hence ex y being Element of REAL st S1[x,y] ; :: thesis: verum
end;
suppose A27: x > 0 ; :: thesis: ex y being Element of REAL st S1[x,y]
log (2,n) in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S1[x,y] by A27; :: thesis: verum
end;
end;
end;
consider h being sequence of REAL such that
A28: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A26);
 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 A28; :: 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 A28; :: thesis: verum
end;
then consider q being Real_Sequence such that
A29: q . 0 = 0 and
A30: for m being Element of NAT st m > 0 holds
q . m = log (2,n) ;
A31: Sum (q,n) = n * (log (2,n)) by A29, A30, 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 A32: k <= n ; :: thesis: seq_logn . k <= q . k
per cases ( k = 0 or k > 0 ) ;
suppose A33: k > 0 ; :: thesis: seq_logn . k <= q . k
then log (2,k) <= log (2,n) by A32, PRE_FF:10;
then seq_logn . k <= log (2,n) by A33, Def2;
hence seq_logn . k <= q . k by A30, A33; :: thesis: verum
end;
end;
end;
then A34: 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, A6, A34, A31;
hence f . n <= 1 * (g . n) by A2; :: thesis: verum
end;
take g ; :: thesis: ( g = g & f in Big_Theta g )
A35: 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 A35, A5; :: thesis: verum