Properties For Deriving Validated Running Error Bounds

Posted by Beetle B. on Wed 15 May 2019

Theorem for FMA Let \(x,y,z\) be nonnegative floating point numbers. Assuming underflow does not occur, then \(xy+z\le o(o(xy)+z)(1+\mathbf{u}^{2})\).

Proof:

Recall from the standard model that \(o(xy)=xy(1+\epsilon),|\epsilon|\le \mathbf{u}\).

Thus, \(xy+z=o(xy)(1+\epsilon)+z,|\epsilon|\le \mathbf{u}\). It follows from the non-negativity of most of the terms that:

\begin{equation*} xy+z\le o(xy)|1+\epsilon|+z \end{equation*}
\begin{equation*} xy+z\le o(xy)(1+\mathbf{u})+z \end{equation*}
\begin{equation*} xy+z\le (o(xy)+z)(1+\mathbf{u}) \end{equation*}

Now do the same to \(o(xy)+z\):

\begin{equation*} o(xy+z)=o(o(xy)+z)|1+\epsilon'| \end{equation*}
\begin{equation*} o(xy+z)\le o(o(xy)+z)(1+\mathbf{u}) \end{equation*}

The result follows.

Theorem If \(\beta\) is even and \(p\le-e_{\min}\), and if \(k\) is a positive integer such that \(k\mathbf{u}<1\), then \(1-k\mathbf{u}\) is a normal floating point number.

Proof:

Note that \(\mathbf{u}^{-1}\) is a positive integer. We know that \(k\mathbf{u}<1\). Could it be possible that \((k+1)\mathbf{u}>1\)? The answer is no. To see this, assume it is true. Then \(k<\mathbf{u}^{-1}\) and \(\mathbf{u}^{-1}<k+1\). This implies that \(\mathbf{u}^{-1}\) is an integer strictly between the integers \(k\) and \(k+1\). Not possible.

Therefore, the strongest statement we can say is that \((k+1)\mathbf{u}\le1\). From here we get \(\mathbf{u}\le1-k\mathbf{u}<1\). Now \(\beta^{e_{\min}}\le \mathbf{u}\le1-k\mathbf{u}<1\)

Now let’s write it as:

\begin{equation*} 1-k\mathbf{u}=\mu\beta^{e-p+1} \end{equation*}

We pick the \(e\) such that \(\beta^{p-1}\le\mu<\beta^{p}\). Using the inequality above, we can show that this \(e<0\). We can write \(\mu=(\mathbf{u}^{-1}-k)\mathbf{u}\beta^{-e+p-1}\). Note that the term in parenthesis is an integer, and so is \(\mathbf{u}\beta^{e-p+1}\) (note that this is why we needed \(\beta\) to be even - to handle round to nearest). Thus \(\mu\) is an integer. The proof is complete.

Theorem Let \(k\) be a positive integer such that \(k\mathbf{u}<1\). Let \(x\) be a floating point such that \(\beta^{e_{min}}\le|x|\le\Omega\). Then:

\begin{equation*} \left(1+\mathbf{u}\right)^{k-1}|x|\le o\left(\frac{|x|}{1-k\mathbf{u}}\right) \end{equation*}

I hope such an obscure statement comes in handy some day!