Uniform exponential growth as a positive parameter tends to zero

Extracted from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46, with shared dependency placement.

theorem Algsuperdiff.exists_rpow_inverse_threshold {b a cap C : ℝ} (hb : 1 < b) (ha : 0 < a) (hcap : 0 < cap) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ cap ∧ ∀ (gamma : ℝ), 0 < gamma → gamma ≤ gamma0 → C ≤ b ^ (a * gamma⁻¹)

Every real target lies below b^(a/γ) for all sufficiently small positive γ, with any prescribed positive upper cap on the threshold.