Comparing exponential bases with polynomial factors

A fixed polynomial factor cannot compensate for a larger exponential base. This form applies directly to tensor-dimension estimates.

theorem RS.le_of_pow_le_pow_mul_polynomial (a b d : ℕ) (h : ∀ (n : ℕ), a ^ n ≤ b ^ n * (n + 1) ^ d) : a ≤ b

An exponential bounded by another exponential times a fixed polynomial has no larger base.

theorem RS.tendsto_even_root_of_polynomial_bounds (a : ℕ → ℕ) (d c : ℕ) (hlower : ∀ (n : ℕ), d ^ (2 * n) ≤ a n * (n + 1) ^ c) (hupper : ∀ (n : ℕ), a n ≤ d ^ (2 * n)) : Filter.Tendsto (fun (n : ℕ) => ↑(a n) ^ (↑(2 * n))⁻¹) Filter.atTop (nhds ↑d)

Taking even roots removes a fixed polynomial loss from an exponential sandwich, including when the exponential base is zero.