Generalizing Big O notation to arbitrary vector spaces

Question

I'm constructing a Coq library for Big-O notation. Naturally, I'd like it to be as general as possible. The Wikipedia page on Big-O notation says

The generalization to functions taking values in any normed vector space is straightforward (replacing absolute values by norms)

Of course, there's no inline citation. My attempt at doing this yielded the following:

Definition big_O (f g : V -> V) : Prop :=
    ∃ k : K, 0 < k ∧ exists n0 : K, 0 < n0 ∧ ∀ n : V, n0 ≤ ∥n∥ -> ∥f n∥ ≤ k * ∥g n∥.

Which translates to the following in informal language:

Definition 1. Given a vector space $V$ with (semi)norm $\lVert-\rVert$ over a totally ordered field $(K,\leq)$ and functions $f,g:V\to V$, we say that $f\in O(g)$ iff there exists some positive $k$ and $n_0$ in $K$ such that for all vectors $n\in V$ with $n_0 \leq \lVert n\rVert$, $\rVert f(n)\rVert\leq k\cdot\lVert g(n)\rVert$.

However, I feel like the following definition is somewhat more elegant and general:

Definition big_O (f g : V -> V) : Prop :=
    ∃ k : K, k ≠ 0 ∧ ∃ n0 : V, ∀ n : V, ∥n0∥ ≤ ∥n∥ -> ∥f n∥ ≤ ∥k · g n∥.

Which translates to the following:

Definition 2. Given a vector space $V$ with (semi)norm $\lVert-\rVert$ over a totally ordered field $(K,\leq)$ and functions $f,g:V\to V$, we say that $f\in O(g)$ iff there exists some nonzero $k$ and some $n_0$ in $V$ such that for all vectors $n\in V$ with $\lVert n_0\rVert \leq \lVert n\rVert$, $\lVert f(n)\rVert\leq \lVert k\cdot g(n)\rVert$.

So I guess I have a few questions:

1. Does anyone have a good reference for the generalization to vector spaces?
2. Do you think these definitions are equivalent? Any proofs or counterexamples?
3. This is somewhat opinion-based, but any arguments for using one or the other?

Answer 1

Here is a straightforward generalization of the asymptotic notation to functions taking values in normed vector spaces:

Let $X$ be a topological space, $\overline X\supseteq X$ a superspace in which $X$ is dense, and $a\in\overline X$. Let $Y$ be a normed vector space, and $f,g\colon X\to Y$. Then we say

• $f(x)=O(g(x))$ as $x\to a$ if there is a neighbourhood $U\ni a$ and $q>0$ such that $\|f(x)\|\le q\left\|g(x)\right\|$ for all $x\in U\cap X$;

• $f(x)=o(g(x))$ as $x\to a$ if for every $q>0$, there is a neighbourhood $U\ni a$ such that $\|f(x)\|\le q\left\|g(x)\right\|$ for all $x\in U\cap X$.

This is for standard, real-valued norms. You seem to be interested also in norms valued in nonarchimedean ordered fields $K$. In this case, there are at least two useful possibilities how to cast the definition, namely (1) by taking $q\in\mathbb Q$, or (2) by taking $q\in K$. Which one is more suitable depends on the intended use case.

Further generalizations are possible, seeing as we didn’t actually use most of the structure of $Y$.

You are apparently trying to define only the special case with $a=\infty$. Thus, you need to decide what are appropriate neighbourhoods of infinity in your spaces (complements of bounded sets? complements of compact sets?).