Let $\mathbb{F}$ be the set of floating point numbers in a given format, which could be either IEEE-754 binary32 (single precision) or binary64 (double precision).

Let $m(Z)$ the floating point number obtained rounding the real number $Z$.

Let $\phi(Z)$ the next floating point number greater than $Z$.

Let $\lfloor Z \rfloor$ be truncation to 64 bit unsigned integer of the positive floating point number $Z < 2^{64}$ (i.e. there are no overflow concerns).


Given three numbers $X, Y, A$, such that: $$ X, Y, A \in \mathbb{F} \\ 0<X<Y \\ A > m \left( \frac{1}{m(Y-X)} \right) \\ \lfloor m(A\cdot X) \rfloor < \lfloor m(A\cdot Y) \rfloor $$


Is it always true that? $$ \lfloor m(\phi(A)\cdot X) \rfloor < \lfloor m(\phi(A)\cdot Y) \rfloor $$

Explanation on the Question

The function $\lfloor m(z\cdot X) \rfloor$ is non-decreasing in $z$ and its behavior is stepwise constant (it looks like a ladder). Increasing $z$ by a tiny bit, the results either does not change, or it jumps to a greater unit.

I am asking if it is possible that by increasing $z$ the terms in the left hand side and right hand side always jump together, or if it is possible that only the term in left hand side jumps befor than the right one, so locally breaking the inequality.

Type of Answer Sought

Either a formal proof that it holds (or that it doesn't), or a numerical example where it does not hold (either in single or double precision) would be accepted as an answer.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.