Semiring of order classes
I’ve always disliked the common abuse of the big-O notation, and preferred to regard $\Order f$ — where $f \in \Nat \to {\mathbb Q^+}$, in which $\mathbb Q^+$ is the set of nonnegative rationals — as denoting a class/set of functions, namely $$ \Order f \defeq \braces{ \phi \in \Nat \to {\mathbb Q^+} \mid \exists N, C \in \Nat.\ \forall n \geq N.\ \phi\ n \leq C \cdot f\ n } $$ (And yes, I’m omitting unnecessary parentheses and function arguments.) This way we can simply interpret statements like \begin{align} \Order f + \Order g &= \Order(f + g) \label{eq:addition} \\ \Order f \cdot \Order g &= \Order(f \cdot g) \label{eq:multiplication} \end{align} as real equations about sets and their operations (pairwise element addition and multiplication on the left-hand sides for the two equations above), and even nicer, we can start talking about structures of these ‘order classes’. One potentially useful fact is that the order classes form a semiring, and the purpose of this post is to do the (not very exciting) verification. Some questions I asked myself while I thought it through are listed and answered in the end.
With Equations \ref{eq:addition} and \ref{eq:multiplication} (which we will verify later), the verification is straightforward and essentially proceeds by applying the equations to the semiring laws. We can work slightly more abstractly with the following lemma.
Lemma. Let $(R, +, \cdot, 0, 1)$ be a semiring and $(S, +, \cdot, 0, 1)$ a set with similarly typed operations (whose names are overloaded) with no specified laws. If there is a surjective mapping $m \in R \to S$ that preserves all the four operations, then $S$ is a semiring as well.
The proof of the lemma is routine; for example, letting $n \in S \to R$ be a right inverse of $m$, associativity of addition is proved by (for all $x, y, z \in S$) \begin{align*} & (x + y) + z \\ ={}& \reason{$n$ is a right inverse of $m$} \\ & (m\ (n\ x) + m\ (n\ y)) + m\ (n\ z) \\ ={}& \reason{$m$ preserves addition (twice)} \\ & m\ ((n\ x + n\ y) + n\ z) \\ ={}& \reason{associativity of addition on $R$} \\ & m\ (n\ x + (n\ y + n\ z)) \\ ={}& \reason{$m$ preserves addition (twice)} \\ & m\ (n\ x) + (m\ (n\ y) + m\ (n\ z)) \\ ={}& \reason{$n$ is a right inverse of $m$} \\ & x + (y + z) \end{align*} Then all it takes is instantiating the lemma with $R \defeq \Nat \to {\mathbb Q^+}$ (with pointwise addition and multiplication and everywhere $0$ and $1$), $m \defeq \Order$, and $S \defeq \braces{ \Order f \mid f \in \Nat \to {\mathbb Q^+} }$.
The real work is the verification of Equations \ref{eq:addition} and \ref{eq:multiplication}. For Equation \ref{eq:addition}, after expanding the definitions we see that, for all $h \in \Nat \to {\mathbb Q^+}$, we have to show the equivalence of the two statements \begin{align} \exists \phi, \psi \in \Nat \to {\mathbb Q^+}.\ & h = \phi + \psi \label{eq:lhs0} \\ \and{}& \exists \awa{N_\psi}{N_\phi}, \awa{C_\psi}{C_\phi} \in \Nat.\ \forall n \geq \awa{N_\psi}{N_\phi}.\ \phi\ n \leq \awa{C_\psi}{C_\phi} \cdot f\ n \label{eq:lhs1} \\ \and{}& \exists N_\psi, C_\psi \in \Nat.\ \forall n \geq N_\psi.\ \psi\ n \leq C_\psi \cdot g\ n \label{eq:lhs2} \end{align} and $$ \exists N_h, C_h \in \Nat.\ \forall n \geq N_h.\ h\ n \leq C_h \cdot (f\ n + g\ n) $$ In the forward direction, choose $N_h \defeq \max(N_\phi, N_\psi)$ and $C_h \defeq \max(C_\phi, C_\psi)$. Then for all $n \geq N_h$, \begin{align} & h\ n \notag \\ ={} & \reason{(\ref{eq:lhs0})} \notag \\ & \phi\ n + \psi\ n \notag \\ \leq{}& \reason{(\ref{eq:lhs1}) and (\ref{eq:lhs2})} \notag \\ & C_\phi \cdot f\ n + C_\psi \cdot g\ n \notag \\ \leq{}& \reason{choice of $C_h$; arithmetic} \label{step:monotonicity} \\ & C_h \cdot (f\ n + g\ n) \notag \end{align} As for the backward direction, since for all $x, y, z \in {\mathbb Q^+}$ we have \begin{equation} x \leq y + z \quad\Rightarrow\quad \exists y', z' \in {\mathbb Q^+}.\ x = y' + z' \and y' \leq y \and z' \leq z \label{eq:decomposition} \end{equation} we can find $\phi$ and $\psi$ such that for all $n \geq N_h$ we have $h\ n = \phi\ n + \psi\ n$, $\phi\ n \leq C_h \cdot f\ n$, and $\psi\ n \leq C_h \cdot g\ n $; additionally, for $n < N_h$ we can make $\phi\ n \defeq h\ n$ and $\psi\ n \defeq 0$ to fully establish (\ref{eq:lhs0}). And (\ref{eq:lhs1}) and (\ref{eq:lhs2}) immediately follow if we choose both $N_\phi$ and $N_\psi$ to be $N_h$ and both $C_\phi$ and $C_\psi$ to be $C_h$. Equation \ref{eq:multiplication} can be proved similarly.
Q&A
Why don’t the order classes form a ring?
Because additive inverses don’t exist for the order classes in general. The obvious candidate $\Order(-f)$ doesn’t work (even if we expand the codomain to $\mathbb Q$) because $\Order f + \Order(-f) \neq \Order(0)$. Note that this breaks Equation \ref{eq:addition}.
How is Equation \ref{eq:addition} broken when functions can take negative values?
The inequality (\ref{step:monotonicity}) depends on the fact $C_\phi \leq C_h \Rightarrow C_\phi \cdot f\ n \leq C_h \cdot f\ n$ (and an analogous one for $C_\psi$ and $g$), which doesn’t hold if $f\ n$ is negative.
Can’t the codomain of the functions be just $\Nat$?
In this case the analogous property to (\ref{eq:decomposition}) for multiplication doesn’t hold — consider a function $h$ whose values are (increasingly large) primes and thus cannot be decomposed, but which can still be bounded by the product of two smaller-valued functions.
Is there a well-definedness problem for operations on the order classes?
It may seem that when we compute the order classes using Equations \ref{eq:addition} and \ref{eq:multiplication} we are doing something similar to the typical computation on equivalence classes, namely choosing representatives and performing computation on the representatives, in which case the result might crucially depend on the choice of representatives and become ill-defined. This is not the case for the order classes though, since order class addition/multiplication is not defined in terms of representatives — it’s just set addition/multiplication. Therefore the equations actually affirm that the result of order class addition/multiplication (which is defined independently from representatives) coincides with the result of adding/multiplying any representatives, and thus the choice of representatives is not crucial because all choices necessarily lead to the same independently defined result. In symbols: if $\Order f = \Order f'$ and $\Order g = \Order g'$, then $\Order(f + g) = \Order f + \Order g = \Order f' + \Order g' = \Order(f' + g')$.
