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:

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