theorem :: ASYMPT_0:40

for f being eventually-nonnegative Real_Sequence

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Element of NAT st f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Theta f

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Element of NAT st f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Theta f