Finite-prefix extension of a big O bound (source code)

= Finite-prefix extension of a big O bound
{title2=$f=O(g),\ g(n)\ne0\ \Longrightarrow\ \sup_n|f(n)/g(n)|<\infty$}

Let $f,g:\mathbb N\to\mathbb R$, with $g(n)\ne0$ everywhere. An eventual bound $|f(n)|\leq C|g(n)|$ can be made valid for all natural numbers by enlarging $C$ to the maximum of itself and the finitely many ratios $|f(n)|/|g(n)|$ before its cutoff. Conversely, a global bound is an eventual bound. Nonvanishing on the finite prefix is essential: $g(0)=0$, $f(0)=1$, and $f(n)=g(n)=1$ for $n\geq1$ give an eventual bound but no global one. The useful principle is that finitely many finite ratios cannot destroy a <big O notation>.