Logarithm of a polynomially bounded positive count is sublinear
ProvedOAI.PiExponent.DeterminantContradiction.log_nat_div_tendsto_zero_of_polynomial_boundnumber-theoryopenai-pi-exponent-017
Any eventually positive natural-valued function with an eventual polynomial upper bound has logarithm divided by its argument tending to zero.
Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.SpecificLimits.Basic open Filter open scoped Topology
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.log_nat_div_tendsto_zero_of_polynomial_bound
(f : ℝ → ℕ) (N : ℕ) (C : ℝ) (hC : 0 < C)
(hpos : ∀ᶠ H : ℝ in atTop, 1 ≤ (f H : ℝ))
(hbound : ∀ᶠ H : ℝ in atTop, (f H : ℝ) ≤ C * (H + 1) ^ N) :
Tendsto (fun H : ℝ => Real.log (f H : ℝ) / H) atTop (𝓝 0) := by sorrySource