Logarithm of polynomially bounded natural-valued functions is sublinear
ProvedOAI.PiExponent.log_nat_function_div_tendsto_zero_of_eventual_polynomial_boundnumber-theoryopenai-pi-exponent-017
If an integer-valued function is eventually at least one and bounded above by a fixed polynomial in H+1, then its logarithm divided by H tends to zero.
Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.SpecificLimits.Basic open Filter Topology
Formal statement
theorem OAI.PiExponent.log_nat_function_div_tendsto_zero_of_eventual_polynomial_bound (f : ℝ → ℕ) (C : ℝ) (p : ℕ) (hC : 0 < C) (hbound : ∀ᶠ H : ℝ in atTop, 1 ≤ f H ∧ (f H : ℝ) ≤ C * (H + 1) ^ p) : Tendsto (fun H : ℝ => Real.log (f H : ℝ) / H) atTop (𝓝 0) := by sorry
Source