Theorems · Theorem · real analysis

Asymptotics.IsBigOWith.rpow

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

Defined in

Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Cited by

2 results in Mathlib

Foundations

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