2.3. Unnormed topological vector spaces🔗

Mathlib also provides support for Landau notation for functions taking values in topological vector spaces that do not carry norms. We may place ourselves in this situation as follows:

variable {𝕜 E : Type*} [NontriviallyNormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
  [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  (f g : α → E)

Without a norm, it is necessary to use the scalar action and so an alternative notation with room to specify the scalars is required. The key definitions and notation are as follows:

IsBigOTVS with notation f =O[𝕜; l] g
IsLittleOTVS with notation f =o[𝕜; l] g

Critically, Mathlib knows that if one does have a norm, then IsBigOTVS and IsBigO are equivalent:

example {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    (f g : α → E) :
    f =O[𝕜; l] g ↔ f =O[l] g :=
  isBigOTVS_iff_isBigO

Likewise Mathlib knows the corresponding little-o result isLittleOTVS_iff_isLittleO.