theorem MathlibNt.Analysis.eventually_nat_log_rpow_le_rpow (b d : ℝ) (hd : 0 < d) : ∀ᶠ (N : ℕ) in Filter.atTop, Real.log ↑N ^ b ≤ ↑N ^ d

Along natural numbers, every positive real power eventually dominates any fixed real power of the logarithm.