Theorems · Theorem · real analysis

Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le_of_imp

∀ {a b : ℝ}, a ≤ b → (b = 0 → a = 0) → (fun x => x ^ b) =O[nhdsWithin 0 (Set.Ici 0)] fun x => x ^ a

If a ≤ b, then x^b = O(x^a) as x → 0, x ≥ 0, unless b = 0 and a ≠ 0.

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Cited by

2 results in Mathlib

Foundations

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