theorem Real.tendsto_pow_log_div_pow_atTop (a b : ℝ) (ha : 0 < a) : Filter.Tendsto (fun (x : ℝ) => log x ^ b / x ^ a) Filter.atTop (nhds 0)

log^b x / x^a goes to zero at infinity if a is positive.