爲浮點乘法

Question

假設嚴格不等式一個，X，和ÿ是正IEEE浮點數與 X < ÿ。證明一個 × X < 一個 × ý其中× 表示浮點乘法舍入到最接近的。

天真，你可能認爲對於一些一個和X接近Ÿ， 你會得到一個 × X = 一個 × ÿ。事實證明，這個 不可能發生（只要非規格化的數字，infinities和NaN排除在 之外）。

我對一個優雅的證明感興趣，如果可能的話，還有一本書或紙 這裏給出。

TAKE 2：正如Pascal Cuoq的回覆所示，以上聲明爲 false。 和 = 1的限制版本如何？這裏是 聲明予以證明：

假設一個和X是積極的IEEE浮點數與 X < 1.證明一個 × X < 一個其中× 表示浮點乘法舍入到最近。

Answer 1

爲了把一個正式證明你的修訂問題（以稍微改變語言）：

假設a和x與x < 1積極IEEE浮點數。證明[ax] < a其中[]表示默認的浮點舍入。

WLOG，讓a在[1, 2)。如果a是1，那麼聲明是非常正確的，所以我們實際上只需要在(1,2)中考慮a。 x < 1意味着x <= 1 - u/2，其中u = ulp(1) = ulp(a)。我們有：

ax <= a - au/2 

我們也有a > 1，所以au/2 > u/2，所以：

ax <= a - au/2 < a - u/2 

因爲ax一半以上低於a的ULP，[ax] < a。

Answer 2

的屬性是假的，如由下面的C99程序當與編譯器爲double和FLT_EVAL_METHOD = 0提供IEEE binary64編譯：

#include <stdio.h> 
#include <math.h> 
#include <float.h> 

int main(void) { 
    double z = 1.0; 
    double y = nextafter(z, 0.0); 
    double x = nextafter(y, 0.0); 
    double a = 1.0 + 2 * DBL_EPSILON; 

    printf("%a %a\n", a*x, a*y); 
} 

結果：

0x1.0000000000001p+0 0x1.0000000000001p+0 

這y的前身1.0,x的前身y和a的繼任者1.0。 x和y的值在他們的binade的頂部，其中相對精度最好，並且a*x和a*y的值在他們的底部，其中相對精度最差。這是如何a*x和a*y四捨五入到相同的值。

在有關財產，因爲一個反例只能x和y由單一的ULP和a乘法把他們的目的地binade相比相對較低，他們在原籍binade分離發生看起來如此。