Theorems · Theorem · real analysis

isLittleO_exp_neg_mul_rpow_atTop

∀ {a : ℝ}, 0 < a → ∀ (b : ℝ), (fun x => Real.exp (-a * x)) =o[Filter.atTop] fun x => x ^ b

exp (-a * x) = o(x ^ s) as x → ∞, for any positive a and real s.

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Cited by

4 results in Mathlib

Foundations

Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound