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 Element of NAT such that
A4: for m being Element of NAT st m >= N2 holds
t . m <= t . (m + 1) by Def8;
A5: f is_smooth_wrt b by A1, A2, Def20;
then f taken_every b in Big_Oh f by Def19;
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, Def19;
then consider N1 being Element of NAT such that
A10: for m being Element of NAT st m >= N1 holds
f . m <= f . (m + 1) by Def8;
consider N5 being Element of NAT such that
A11: for n being Element of NAT st n >= N5 holds
t . n >= 0 by Def4;
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;
set N0 = max (max N1,N2),(max N3,N4);
A17: max (max N1,N2),(max N3,N4) >= max N1,N2 by XXREAL_0:25;
max N1,N2 >= N2 by XXREAL_0:25;
then A18: max (max N1,N2),(max N3,N4) >= N2 by A17, XXREAL_0:2;
max N1,N2 >= N1 by XXREAL_0:25;
then A19: max (max N1,N2),(max N3,N4) >= N1 by A17, XXREAL_0:2;
A20: max (max N1,N2),(max N3,N4) >= max N3,N4 by XXREAL_0:25;
max N3,N4 >= N4 by XXREAL_0:25;
then A21: max (max N1,N2),(max N3,N4) >= N4 by A20, XXREAL_0:2;
max N3,N4 >= N3 by XXREAL_0:25;
then A22: max (max N1,N2),(max N3,N4) >= N3 by A20, XXREAL_0:2;
set N = max N5,(max 1,(b * (max (max N1,N2),(max N3,N4))));
A23: max N5,(max 1,(b * (max (max N1,N2),(max N3,N4)))) >= max 1,(b * (max (max N1,N2),(max N3,N4))) by XXREAL_0:25;
max 1,(b * (max (max N1,N2),(max N3,N4))) >= b * (max (max N1,N2),(max N3,N4)) by XXREAL_0:25;
then A24: max N5,(max 1,(b * (max (max N1,N2),(max N3,N4)))) >= b * (max (max N1,N2),(max N3,N4)) by A23, XXREAL_0:2;
b >= 1 by A2, XXREAL_0:2;
then b * (max (max N1,N2),(max N3,N4)) >= 1 * (max (max N1,N2),(max N3,N4)) by XREAL_1:66;
then A25: max N5,(max 1,(b * (max (max N1,N2),(max N3,N4)))) >= max (max N1,N2),(max N3,N4) by A24, XXREAL_0:2;
A26: max N5,(max 1,(b * (max (max N1,N2),(max N3,N4)))) >= N5 by XXREAL_0:25;
A27: max 1,(b * (max (max N1,N2),(max N3,N4))) >= 1 by XXREAL_0:25;
then A28: max N5,(max 1,(b * (max (max N1,N2),(max N3,N4)))) >= 1 by A23, XXREAL_0:2;

A29: now

(max N5,(max 1,(b * (max (max N1,N2),(max N3,N4))))) * (b " ) >= (b " ) * (b * (max (max N1,N2),(max N3,N4))) by A24, XREAL_1:66;
then (max N5,(max 1,(b * (max (max N1,N2),(max N3,N4))))) * (b " ) >= ((b " ) * b) * (max (max N1,N2),(max N3,N4)) ;
then A30: (max N5,(max 1,(b * (max (max N1,N2),(max N3,N4))))) * (b " ) >= 1 * (max (max N1,N2),(max N3,N4)) by A2, XCMPLX_0:def 7;
let n be Element of NAT ; :: thesis: ( n >= max N5,(max 1,(b * (max (max N1,N2),(max N3,N4)))) 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:52;
assume A32: n >= max N5,(max 1,(b * (max (max N1,N2),(max N3,N4)))) ; :: 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:12;
[\(log b,n)/] >= 0

proof

(log b,n) - 1 < [\(log b,n)/] by INT_1:def 4;
then 1 + ((log b,n) - 1) < [\(log b,n)/] + 1 by XREAL_1:8;
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:21;
then log b,n < 0 by A35, XREAL_1:8;
hence contradiction by A16, A34, POWER:59; :: thesis: verum

end;

then reconsider i = [\(log b,n)/] as Element of NAT by INT_1:16;
A36: b to_power [\(log b,n)/] = b |^ i by POWER:46;
n * (b " ) >= (max N5,(max 1,(b * (max (max N1,N2),(max N3,N4))))) * (b " ) by A32, XREAL_1:66;
then n * (b " ) >= max (max N1,N2),(max N3,N4) by A30, XXREAL_0:2;
then A37: n / b >= max (max N1,N2),(max N3,N4) 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)/]) by POWER:30
.= b to_power ([\(log b,n)/] + 1) by A2, POWER:32 ;
then A39: n <= b * n1 by A16, A33, A31, PRE_FF:10;
then n * (b " ) <= (b " ) * (b * (b to_power [\(log b,n)/])) by XREAL_1:66;
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 >= max (max N1,N2),(max N3,N4) 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:66;
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, Def18;
then A42: a * ((c " ) * (f . (b * n1))) <= a * (f . n1) by A14, XREAL_1:66;
[\(log b,n)/] <= log b,n by INT_1:def 4;
then A43: b to_power [\(log b,n)/] <= b to_power (log b,n) by A16, PRE_FF:10;
n >= max (max N1,N2),(max N3,N4) 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:66;
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:11;
a * (c " ) > (c " ) * 0 by A8, A14, XREAL_1:70;
hence t in Big_Omega f by A45, A29; :: thesis: verum