let f be eventually-nonnegative Real_Sequence; :: thesis: for t being eventually-nonnegative eventually-nondecreasing Real_Sequence
for b being 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 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 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
reconsider b = b as Element of NAT by ORDINAL1:def 12;
A4: 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
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;
then consider N1 being Nat such that
A10: for m being Nat st m >= N1 holds
f . m <= f . (m + 1) ;
consider N2 being Nat such that
A11: for m being Nat st m >= N2 holds
t . m <= t . (m + 1) by Def6;
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;
reconsider N0 = max ((max (N1,N2)),(max (N3,N4))) as Element of NAT by ORDINAL1:def 12;
A16: N0 >= max (N1,N2) by XXREAL_0:25;
max (N1,N2) >= N2 by XXREAL_0:25;
then A17: N0 >= N2 by A16, XXREAL_0:2;
max (N1,N2) >= N1 by XXREAL_0:25;
then A18: N0 >= N1 by A16, XXREAL_0:2;
A19: N0 >= max (N3,N4) by XXREAL_0:25;
max (N3,N4) >= N4 by XXREAL_0:25;
then A20: N0 >= N4 by A19, XXREAL_0:2;
max (N3,N4) >= N3 by XXREAL_0:25;
then A21: N0 >= N3 by A19, XXREAL_0:2;
consider N5 being Nat such that
A22: for n being Nat st n >= N5 holds
t . n >= 0 by Def2;
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
( t . n <= (a * c) * (f . 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 ( t . n <= (a * c) * (f . n) & t . n >= 0 ) )
set n1 = b to_power [\(log (b,n))/];
assume A31: n >= N ; :: 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 :: thesis: not [\(log (b,n))/] < 0

(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))/])
.= 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 ") >= N * (b ") by A31, XREAL_1:64;
then n * (b ") >= N0 by A30, XXREAL_0:2;
then A38: n / b >= N0 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 >= N0 by A38, XXREAL_0:2;
then A41: n1 >= N3 by A21, XXREAL_0:2;
A42: n >= N0 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, Def15;
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