Theorems · Theorem · approximation theory

Asymptotics.IsBigO.smul

∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {R : Type u_13} {𝕜' : Type u_16} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedRing R] [inst_3 : NormedDivisionRing 𝕜'] {f' : α → E'}
  {g' : α → F'} {l : Filter α} [inst_4 : Module R E'] [IsBoundedSMul R E'] [inst_6 : Module 𝕜' F'] [NormSMulClass 𝕜' F']
  {k₁ : α → R} {k₂ : α → 𝕜'}, k₁ =O[l] k₂ → f' =O[l] g' → (fun x => k₁ x • f' x) =O[l] fun x => k₂ x • g' x

Defined in

Mathlib.Analysis.Asymptotics.Lemmas

Cited by

4 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupSeminormedRingNormedDivisionRingModuleIsBoundedSMulModuleNormSMulClass