A decision procedure for linear "big O" equations

Jeremy Avigad, Kevin Donnelly

Let $F$ be the set of functions from an infinite set, $S$, to an ordered ring, $R$. For $f$, $g$, and $h$ in $F$, the assertion $f=g+O(h)$ means that for some constant $C$, $|f…