Theorems · Theorem · approximation theory

Asymptotics.IsBigOWith.mul

∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S} {c₁ c₂ : ℝ},
  Asymptotics.IsBigOWith c₁ l f₁ g₁ →
    Asymptotics.IsBigOWith c₂ l f₂ g₂ → Asymptotics.IsBigOWith (c₁ * c₂) l (fun x => f₁ x * f₂ x) fun x => g₁ x * g₂ x

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

SeminormedRingNormedRingNormMulClass