Theorems · Theorem · real analysis

Asymptotics.IsBigO.rpow

∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
  0 ≤ r → 0 ≤ᶠ[l] g → f =O[l] g → (fun x => f x ^ r) =O[l] fun x => g x ^ r

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Cited by

3 results in Mathlib

Foundations

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