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_Oh f,{ (b |^ n) where n is Element of NAT : verum } holds
t in Big_Oh 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_Oh f,{ (b |^ n) where n is Element of NAT : verum } holds
t in Big_Oh f
let b be Element of NAT ; :: thesis: ( f is smooth & b >= 2 & t in Big_Oh f,{ (b |^ n) where n is Element of NAT : verum } implies t in Big_Oh f )
assume that
A1: f is smooth and
A2: b >= 2 and
A3: t in Big_Oh f,{ (b |^ n) where n is Element of NAT : verum } ; :: thesis: t in Big_Oh f
A4: 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
A5: f taken_every b = s and
A6: 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
A7: c > 0 and
A8: for n being Element of NAT st n >= N3 holds
( s . n <= c * (f . n) & s . n >= 0 ) by A6;
A9: b > 1 by A2, XXREAL_0:2;
f is eventually-nondecreasing by A4, 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 N2 being Element of NAT such that
A11: for m being Element of NAT st m >= N2 holds
t . m <= t . (m + 1) by Def8;
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 c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N & n in { (b |^ n) where n is Element of NAT : verum } holds
( r . n <= c * (f . 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
( r . n <= a * (f . n) & r . n >= 0 ) by A13;
set N0 = max (max N1,N2),(max N3,N4);
A16: max (max N1,N2),(max N3,N4) >= max N1,N2 by XXREAL_0:25;
max N1,N2 >= N2 by XXREAL_0:25;
then A17: max (max N1,N2),(max N3,N4) >= N2 by A16, XXREAL_0:2;
max N1,N2 >= N1 by XXREAL_0:25;
then A18: max (max N1,N2),(max N3,N4) >= N1 by A16, XXREAL_0:2;
A19: max (max N1,N2),(max N3,N4) >= max N3,N4 by XXREAL_0:25;
max N3,N4 >= N4 by XXREAL_0:25;
then A20: max (max N1,N2),(max N3,N4) >= N4 by A19, XXREAL_0:2;
max N3,N4 >= N3 by XXREAL_0:25;
then A21: max (max N1,N2),(max N3,N4) >= N3 by A19, XXREAL_0:2;
consider N5 being Element of NAT such that
A22: for n being Element of NAT st n >= N5 holds
t . n >= 0 by Def4;
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 ( t . n <= (a * c) * (f . n) & t . n >= 0 ) )
set n1 = b to_power [\(log b,n)/];
assume A31: n >= max N5,(max 1,(b * (max (max N1,N2),(max N3,N4)))) ; :: thesis: ( t . n <= (a * c) * (f . n) & t . n >= 0 )
then A32: n = b to_power (log b,n) by A23, A27, A9, POWER:def 3;
n >= 1 by A28, A31, XXREAL_0:2;
then log b,n >= log b,1 by A9, PRE_FF:12;
then A33: log b,n >= 0 by A9, POWER:59;

A34: now

(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;
hence contradiction by A33, A35, XREAL_1:8; :: thesis: verum

end;

then reconsider i = [\(log b,n)/] as Element of NAT by INT_1:16;
reconsider n3 = [\(log b,n)/] + 1 as Element of NAT by A34, INT_1:16;
b to_power [\(log b,n)/] = b |^ i by POWER:46;
then reconsider n1 = b to_power [\(log b,n)/] as Element of NAT ;
set n2 = b * n1;
A36: 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 b * n1 = b |^ n3 by POWER:46;
then A37: b * n1 in { (b |^ n) where n is Element of NAT : verum } ;
n * (b " ) >= (max N5,(max 1,(b * (max (max N1,N2),(max N3,N4))))) * (b " ) by A31, XREAL_1:66;
then n * (b " ) >= max (max N1,N2),(max N3,N4) by A30, XXREAL_0:2;
then A38: n / b >= max (max N1,N2),(max N3,N4) by XCMPLX_0:def 9;
log b,n <= [\(log b,n)/] + 1 by INT_1:52;
then A39: n <= b * n1 by A9, A32, A36, 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 A38, XXREAL_0:2;
then A41: n1 >= N3 by A21, XXREAL_0:2;
A42: n >= max (max N1,N2),(max N3,N4) by A25, A31, XXREAL_0:2;
then n >= N4 by A20, XXREAL_0:2;
then b * n1 >= N4 by A39, XXREAL_0:2;
then A43: t . (b * n1) <= a * (f . (b * n1)) by A12, A15, A37;
f . (b * n1) = s . n1 by A5, Def18;
then f . (b * n1) <= c * (f . n1) by A8, A41;
then A44: a * (f . (b * n1)) <= a * (c * (f . n1)) by A14, XREAL_1:66;
n >= N2 by A17, A42, XXREAL_0:2;
then t . n <= t . (b * n1) by A11, A39, Th1;
then t . n <= a * (f . (b * n1)) by A43, XXREAL_0:2;
then A45: t . n <= (a * c) * (f . n1) by A44, XXREAL_0:2;
A46: n1 >= N1 by A18, A40, XXREAL_0:2;
[\(log b,n)/] <= log b,n by INT_1:def 4;
then n1 <= n by A9, A32, PRE_FF:10;
then (a * c) * (f . n1) <= (a * c) * (f . n) by A10, A7, A14, A46, Th1, XREAL_1:66;
hence t . n <= (a * c) * (f . n) by A45, XXREAL_0:2; :: thesis: t . n >= 0
n >= N5 by A26, A31, XXREAL_0:2;
hence t . n >= 0 by A22; :: thesis: verum

end;

A47: t is Element of Funcs NAT ,REAL by FUNCT_2:11;
a * c > c * 0 by A7, A14, XREAL_1:70;
hence t in Big_Oh f by A47, A29; :: thesis: verum