Theorems · Theorem · approximation theory

Asymptotics.IsBigO.pow

∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} [NormOneClass S] {f : α → R} {g : α → S},
  f =O[l] g → ∀ (n : ℕ), (fun x => f x ^ n) =O[l] fun x => g x ^ n

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

8 results in Mathlib

Foundations

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

Assumes

SeminormedRingNormedRingNormMulClassNormOneClass