2.2. General case and further notation🔗

The definition underlying the notation introduced above is IsBigO. This definition applies to functions whose domain carries a filter and whose codomains carry a norm. For simplicity here we will assume the functions take values in the same codomain and this this is actually a normed group.

variable {α E : Type*}
  (l : Filter α) [NormedAddCommGroup E]
  (f g : α → E)

In this setting, we can witness Mathlib's support for further Landau notation as follows:

f =O[l] g notation for IsBigO
f =Θ[l] g notation for IsTheta
f =o[l] g notation for IsLittleO
f ~[l] g notation for IsEquivalent

We note some familiar properties:

example : f =Θ[l] g ↔ f =O[l] g ∧ g =O[l] f := Iff.rfl

example : f ~[l] g ↔ (f - g) =o[l] g := Iff.rfl

We also note that there exists a more quantiative variant of IsBigO which allows control over the constant, this is IsBigOWith.