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:64;
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:64;
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:10;
then A33: log (b,n) >= 0 by A9, POWER:51;

A34: now

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

end;

then reconsider i = [\(log (b,n))/] as Element of NAT by INT_1:3;
reconsider n3 = [\(log (b,n))/] + 1 as Element of NAT by A34, INT_1:3;
b to_power [\(log (b,n))/] = b |^ i by POWER:41;
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:25
.= b to_power ([\(log (b,n))/] + 1) by A2, POWER:27 ;
then b * n1 = b |^ n3 by POWER:41;
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:64;
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:29;
then A39: n <= b * n1 by A9, A32, A36, 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 >= 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:64;
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 6;
then n1 <= n by A9, A32, PRE_FF:8;
then (a * c) * (f . n1) <= (a * c) * (f . n) by A10, A7, A14, A46, Th1, XREAL_1:64;
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:8;
a * c > c * 0 by A7, A14, XREAL_1:68;
hence t in Big_Oh f by A47, A29; :: thesis: verum