5
$\begingroup$

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?
$\endgroup$
  • 1
    $\begingroup$ Take $K = \mathbb{R}$, $V = 0$, $f=1$, $g=0$. Then $f \in O(g)$ is true according to Definition 1 (take any $n_0 > 0$ and then the conclusion is vacuously true) but false according to Definition 2. $\endgroup$ – Nate Eldredge May 13 '17 at 6:04
  • $\begingroup$ I think there is a reasonable definition for topological vector spaces $V$, $W$, and maps $f,g \colon V \to W$, but I don't remember it. I don't see why you want maps $f \colon V \to V$ on a single vector space. $\endgroup$ – Ben McKay May 13 '17 at 6:30
  • 1
    $\begingroup$ The standard notation defines what it means "$f(x)=O(g(x))$ as $x\to a$", where $a$ is an element in the completion of the original space, and while $a$ is often understood from the context and left out, it is an integral part of the concept. Now this whole thing has a straightforward generalization to maps from topological spaces to normed vector spaces, which I believe is what Wikipedia refers to. Decide what your $a$ is, and you are good to go. $\endgroup$ – Emil Jeřábek May 13 '17 at 8:41
  • $\begingroup$ @BenMcKay I'm not wedded to the idea that they are maps to and from a single space. In fact, I think they can be $f:V\to W$ and $g:V\to U$ as long as $W,U$ are over the same field. $\endgroup$ – Langston May 13 '17 at 17:01
  • $\begingroup$ @EmilJeřábek Can you expand on that as an answer or provide a reference? I'm afraid I don't see the "straightforward generalization", which is the point of asking the question. $\endgroup$ – Langston May 13 '17 at 17:02
4
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.