theorem MathlibNt.Analysis.eventually_const_mul_log_rpow_le_rpow (C b : ℝ) {a : ℝ} (ha : 0 < a) : ∀ᶠ (x : ℝ) in Filter.atTop, C * Real.log x ^ b ≤ x ^ a

A fixed scalar multiple of any real log power is eventually below any positive power, with the threshold selected before the varying real input.