Polynomial powers of the logarithm are bounded by every positive power

Proved

WordRAM.APSPBridge.real_log_pow_le_rpow

by wurtle · Nov 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptoticsfine-grained-complexitylogarithm

For every natural number $m$ and every positive real $\varepsilon$ , there is a positive constant $K$ such that for every real $x\ge2$ ,

(\log x)^m\le K\,x^{\varepsilon}.

Thus every fixed polynomial power of the logarithm grows more slowly than every positive power of $x$ . This is the analytic estimate behind absorbing polylogarithmic overhead in runtime-transfer arguments.

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

set_option autoImplicit false

Formal statement

theorem WordRAM.APSPBridge.real_log_pow_le_rpow (m : Nat) {ε : ℝ} (hε : 0 < ε) : ∃ K : ℝ, 0 < K ∧ ∀ x : ℝ, 2 ≤ x → (Real.log x) ^ m ≤ K * x ^ ε := by sorry

Source

Standard asymptotic estimate

\log^m x=o(x^\varepsilon)

; used in the mission 'Two WordRAM models: equivalence with polylogarithmic overhead' for the fine-grained transfer step.

View graph