Proving that $a\le \text{fl}\left(\frac{a+b}{2}\right)\le b$

Question

Suppose that $a$ and $b$ are some floating point numbers such that $a\lt b$. How can I show that $$a\le \text{fl}\left(\frac{a+b}{2}\right)\le b$$ specifically in IEEE standard floating point arithmetic? In this, for example $\text{fl}(a)$ refers to the floating point number closest so some value $a$.

Answer 1

This problem does not require us to carry out or exploit properties of floating point arithmetic, as it defines $fl((a+b)/2)$ simply as that floating-point representable number closest to $(a+b)/2$. Note that this is a slight misstatement, in that "closest" may not uniquely determine $fl((a+b)/2)$, but this will not affect our reasoning to the conclusion below.

Now the floating-point representable numbers are a finite subset of the real numbers, so given that $a,b$ are (exactly) floating point numbers, with:

$$ a \lt b $$

there are only three possibilities:

$$ fl\left( \frac{a+b}{2} \right) \lt a \lt b $$

$$ a \le fl\left( \frac{a+b}{2} \right) \le b $$

$$ a \lt b \lt fl\left( \frac{a+b}{2} \right) $$

So we ask ourselves which of these are sensible. Is it possible that the closest floating-point representable number to the actual value of $(a+b)/2$ is less than $a$ or greater than $b$? Clearly the actual value is strictly between $a$ and $b$.

Therefore any floating-point number less than $a$ cannot be as close as $a$ is to $(a+b)/2$, nor can any floating-point number greater than $b$ be as close as $b$ is to $(a+b)/2$.

Hence only the middle possibility is viable.

Answer 2

In general, we have $x < y$ implies that $\text{fl}(x) \leq \text{fl}(y)$, see Floating point arithmetic in IEEE standard floating point arithmetic This property also solves the problem.

It is interesting to note that the computed average need not fall in the interval between $a$ and $b$, at least not in base 10. Here $a=6.377$ and $b=6.379$ provides a counterexample when the calculations are done with four significant figures. The true sum is $s=12.756$ which rounds to $\hat{s} = 12.76$. Division by $2$ then yields the computed average of $\hat{\mu} = 6.380$ which is larger than either of $a$ and $b$!