Theorems · Definition · approximation theory

Asymptotics.IsBigOWith

{α : Type u_18} → {E : Type u_19} → {F : Type u_20} → [Norm E] → [Norm F] → ℝ → Filter α → (α → E) → (α → F) → Prop

This version of the Landau notation IsBigOWith C l f g where f and g are two functions on a type α and l is a filter on α, means that eventually for l, ‖f‖ is bounded by C * ‖g‖. In other words, ‖f‖ / ‖g‖ is eventually bounded by C, modulo division by zero issues that are avoided by this definition. Probably you want to use IsBigO instead of this relation.

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

187 results in Mathlib

Foundations

Depth 98 from the axioms, rests on 1,960 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NormNorm