Asymptotic bounds on natural numbers

For any natural base greater than one, exponentials eventually dominate fixed multiples of powers, and fixed multiples of logarithms are eventually at most the input. The inequalities are stated in ℕ; the polynomial bound specializes Mathlib's isLittleO_pow_const_const_pow_of_one_lt.

theorem Nat.eventually_mul_pow_le_pow (c k : ℕ) {b : ℕ} (hb : 1 < b) : ∀ᶠ (n : ℕ) in Filter.atTop, c * n ^ k ≤ b ^ n

Every fixed multiple of a power is eventually at most an exponential of base greater than one.

theorem Nat.eventually_mul_log_le (c : ℕ) {b : ℕ} (hb : 1 < b) : ∀ᶠ (n : ℕ) in Filter.atTop, c * log b n ≤ n

Every fixed multiple of the logarithm in a base greater than one is eventually at most the input.

theorem Nat.eventually_mul_log2_le (c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c * n.log2 ≤ n

Every fixed multiple of the binary logarithm is eventually at most the input.