I'm constructing [a Coq library for Big-O notation](https://github.com/siddharthist/coq-big-o). Naturally, I'd like it to be as general as possible. The Wikipedia page on Big-O notation [says](https://en.wikipedia.org/wiki/Big_O_notation#Generalizations_and_related_usages) 



> 
> 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?



Generalizing Big O notation to arbitrary vector spaces
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?).


