Theorems · Theorem · approximation theory

Asymptotics.IsBigOWith.of_pow

∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {c c' : ℝ} {l : Filter α} [NormOneClass S] {n : ℕ} {f : α → S} {g : α → R},
  Asymptotics.IsBigOWith c l (f ^ n) (g ^ n) → n ≠ 0 → c ≤ c' ^ n → 0 ≤ c' → Asymptotics.IsBigOWith c' l f g

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedRingNormedRingNormMulClassNormOneClass