let f be eventually-nonnegative Real_Sequence; :: thesis: for t being eventually-nonnegative eventually-nondecreasing Real_Sequence
for b being Element of NAT st f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) holds
t in Big_Omega f
let t be eventually-nonnegative eventually-nondecreasing Real_Sequence; :: thesis: for b being Element of NAT st f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) holds
t in Big_Omega f
let b be Element of NAT ; :: thesis: ( f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) implies t in Big_Omega f )
assume that
A1: f is smooth and
A2: b >= 2 and
A3: t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) ; :: thesis: t in Big_Omega f
consider N2 being Nat such that
A4: for m being Nat st m >= N2 holds
t . m <= t . (m + 1) by Def6;
A5: f is_smooth_wrt b by A1, A2;
then f taken_every b in Big_Oh f ;
then consider s being Element of Funcs (NAT,REAL) such that
A6: f taken_every b = s and
A7: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( s . n <= c * (f . n) & s . n >= 0 ) ) ) ;
consider c being Real, N3 being Element of NAT such that
A8: c > 0 and
A9: for n being Element of NAT st n >= N3 holds
( s . n <= c * (f . n) & s . n >= 0 ) by A7;
f is eventually-nondecreasing by A5;
then consider N1 being Nat such that
A10: for m being Nat st m >= N1 holds
f . m <= f . (m + 1) ;
consider N5 being Nat such that
A11: for n being Nat st n >= N5 holds
t . n >= 0 by Def2;
set X = { (b |^ n) where n is Element of NAT : verum } ;
consider r being Element of Funcs (NAT,REAL) such that
A12: r = t and
A13: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N & n in { (b |^ n) where n is Element of NAT : verum } holds
( d * (f . n) <= r . n & r . n >= 0 ) ) ) by A3;
consider a being Real, N4 being Element of NAT such that
A14: a > 0 and
A15: for n being Element of NAT st n >= N4 & n in { (b |^ n) where n is Element of NAT : verum } holds
( a * (f . n) <= r . n & r . n >= 0 ) by A13;
A16: b > 1 by A2, XXREAL_0:2;
reconsider N0 = max ((max (N1,N2)),(max (N3,N4))) as Element of NAT by ORDINAL1:def 12;
A17: N0 >= max (N1,N2) by XXREAL_0:25;
max (N1,N2) >= N2 by XXREAL_0:25;
then A18: N0 >= N2 by A17, XXREAL_0:2;
max (N1,N2) >= N1 by XXREAL_0:25;
then A19: N0 >= N1 by A17, XXREAL_0:2;
A20: N0 >= max (N3,N4) by XXREAL_0:25;
max (N3,N4) >= N4 by XXREAL_0:25;
then A21: N0 >= N4 by A20, XXREAL_0:2;
max (N3,N4) >= N3 by XXREAL_0:25;
then A22: N0 >= N3 by A20, XXREAL_0:2;
reconsider N = max (N5,(max (1,(b * N0)))) as Element of NAT by ORDINAL1:def 12;
A23: N >= max (1,(b * N0)) by XXREAL_0:25;
max (1,(b * N0)) >= b * N0 by XXREAL_0:25;
then A24: N >= b * N0 by A23, XXREAL_0:2;
b >= 1 by A2, XXREAL_0:2;
then b * N0 >= 1 * N0 by XREAL_1:64;
then A25: N >= N0 by A24, XXREAL_0:2;
A26: N >= N5 by XXREAL_0:25;
A27: max (1,(b * N0)) >= 1 by XXREAL_0:25;
then A28: N >= 1 by A23, XXREAL_0:2;

A29: now :: thesis: for n being Element of NAT st n >= N holds
( (a * (c ")) * (f . n) <= t . n & t . n >= 0 )

N * (b ") >= (b ") * (b * N0) by A24, XREAL_1:64;
then N * (b ") >= ((b ") * b) * N0 ;
then A30: N * (b ") >= 1 * N0 by A2, XCMPLX_0:def 7;
let n be Element of NAT ; :: thesis: ( n >= N implies ( (a * (c ")) * (f . n) <= t . n & t . n >= 0 ) )
set n1 = b to_power [\(log (b,n))/];
A31: log (b,n) <= [\(log (b,n))/] + 1 by INT_1:29;
assume A32: n >= N ; :: thesis: ( (a * (c ")) * (f . n) <= t . n & t . n >= 0 )
then A33: n = b to_power (log (b,n)) by A23, A27, A16, POWER:def 3;
n >= 1 by A28, A32, XXREAL_0:2;
then A34: log (b,n) >= log (b,1) by A16, PRE_FF:10;
[\(log (b,n))/] >= 0

proof

(log (b,n)) - 1 < [\(log (b,n))/] by INT_1:def 6;
then 1 + ((log (b,n)) - 1) < [\(log (b,n))/] + 1 by XREAL_1:6;
then A35: (1 + (- 1)) + (log (b,n)) < [\(log (b,n))/] + 1 ;
assume [\(log (b,n))/] < 0 ; :: thesis: contradiction
then [\(log (b,n))/] <= - 1 by INT_1:8;
then log (b,n) < 0 by A35, XREAL_1:6;
hence contradiction by A16, A34, POWER:51; :: thesis: verum

end;

then reconsider i = [\(log (b,n))/] as Element of NAT by INT_1:3;
A36: b to_power [\(log (b,n))/] = b |^ i by POWER:41;
n * (b ") >= N * (b ") by A32, XREAL_1:64;
then n * (b ") >= N0 by A30, XXREAL_0:2;
then A37: n / b >= N0 by XCMPLX_0:def 9;
reconsider n1 = b to_power [\(log (b,n))/] as Element of NAT by A36;
A38: n1 in { (b |^ n) where n is Element of NAT : verum } by A36;
set n2 = b * n1;
b * n1 = (b to_power 1) * (b to_power [\(log (b,n))/])
.= b to_power ([\(log (b,n))/] + 1) by A2, POWER:27 ;
then A39: n <= b * n1 by A16, A33, A31, PRE_FF:8;
then n * (b ") <= (b ") * (b * (b to_power [\(log (b,n))/])) by XREAL_1:64;
then n * (b ") <= ((b ") * b) * (b to_power [\(log (b,n))/]) ;
then n * (b ") <= 1 * (b to_power [\(log (b,n))/]) by A2, XCMPLX_0:def 7;
then n / b <= n1 by XCMPLX_0:def 9;
then A40: n1 >= N0 by A37, XXREAL_0:2;
then n1 >= N4 by A21, XXREAL_0:2;
then A41: a * (f . n1) <= t . n1 by A12, A15, A38;
n1 >= N3 by A22, A40, XXREAL_0:2;
then s . n1 <= c * (f . n1) by A9;
then (c ") * (s . n1) <= (c ") * (c * (f . n1)) by A8, XREAL_1:64;
then (c ") * (s . n1) <= ((c ") * c) * (f . n1) ;
then (c ") * (s . n1) <= 1 * (f . n1) by A8, XCMPLX_0:def 7;
then (c ") * (f . (b * n1)) <= f . n1 by A6, Def15;
then A42: a * ((c ") * (f . (b * n1))) <= a * (f . n1) by A14, XREAL_1:64;
[\(log (b,n))/] <= log (b,n) by INT_1:def 6;
then A43: b to_power [\(log (b,n))/] <= b to_power (log (b,n)) by A16, PRE_FF:8;
n >= N0 by A25, A32, XXREAL_0:2;
then n >= N1 by A19, XXREAL_0:2;
then f . n <= f . (b * n1) by A10, A39, Th1;
then A44: (a * (c ")) * (f . n) <= (a * (c ")) * (f . (b * n1)) by A8, A14, XREAL_1:64;
n1 >= N2 by A18, A40, XXREAL_0:2;
then t . n1 <= t . n by A4, A33, A43, Th1;
then a * (f . n1) <= t . n by A41, XXREAL_0:2;
then (a * (c ")) * (f . (b * n1)) <= t . n by A42, XXREAL_0:2;
hence (a * (c ")) * (f . n) <= t . n by A44, XXREAL_0:2; :: thesis: t . n >= 0
n >= N5 by A26, A32, XXREAL_0:2;
hence t . n >= 0 by A11; :: thesis: verum

end;

A45: t is Element of Funcs (NAT,REAL) by FUNCT_2:8;
a * (c ") > (c ") * 0 by A8, A14, XREAL_1:68;
hence t in Big_Omega f by A45, A29; :: thesis: verum