Theorems · Definition · approximation theory

Asymptotics.IsLittleO

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

The Landau notation f =o[l] 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 an arbitrarily small constant multiple of ‖g‖. In other words, ‖f‖ / ‖g‖ tends to 0 along l, modulo division by zero issues that are avoided by this definition.

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

375 results in Mathlib

Foundations

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

Assumes

NormNorm