floating-point - “0.00x <= 0.001 * x”是否始终保持两倍？

Question

例：

0.008 == 0.001 * 8
0.009  < 0.001 * 9
0.035 == 0.001 * 35
0.036  < 0.001 * 36

我还测试了以下模式：

0.0x   <= 0.01   * x
0.000x <= 0.0001 * x

我已经在MATLAB和C中测试了数千个。
我的问题：

如果一直存在，为什么？如果没有，有什么反例吗？

如果始终成立，以下所有模式是否正确？
0.0000000000000x <= 0.0000000000001 * x ; for arbitrary zeros

Answer 1

.000005 <= .000001 * 5评估为false。
Matlab specifies double to be IEEE-754 binary64，但是C标准没有，尽管许多实现使用它。通常，以2和10为基数的浮点数。在底数为10的情况下，构成关系成立，实际上，两个表达式在格式的范围内相等。 （当x太大以至于将其转换为double时，无穷大，相等性就不成立。）在其他基础上，可以找到类似于此答案中所示的反例。1对于此答案的其余部分，IEEE-在数字格式和操作行为方面均假定为754 binary64。
我们应该了解如何评估诸如.000…000x <= .000…0001 * x的表达式：

首先，源文本中的每个数字都转换为double。在此转换过程中，数字将四舍五入为可表示的值。此舍入通常通过舍入到最接近的可表示值，并与具有偶数低位（位）的值相关联。
然后执行乘法，结果就好像实数结果舍入为可表示的值。同样，四舍五入是最常见的。
然后评估比较<=。这没有错误；当且仅当右操作数大于或等于左操作数时，它才会生成true。

我认为x是非负数。否定的x，请参阅第一个附录。
首先，考虑使用最近舍入法。
将.000001转换为double会产生0.0000009999999999999999999948148111825886258685613938723690807819366455078125。在使用printf(".99f\n", .000001);的良好C实现中可以看到这一点。 （由于C标准既没有完全指定编译时十进制数字到浮点数的转换，也没有完全通过printf指定浮点数到十进制的转换，因此在不使用正确的四舍五入的实现中可能会有一些变化。 ）如我们所见，它小于.000001。可以通过打印.1，.01，.001等轻松找到它，直到找到恰好四舍五入的数字。然后，我们测试各种x，直到找到恰好针对它的.00000x取整。将.000005转换为double产生0.0000050000000000000004090152695701565477293115691281855106353759765625。接下来，对于小整数x，x在double中可以精确表示，因此将该操作数转换为double不会产生舍入错误。我们几乎满意.00000x <= .000001 * x，因为左侧包含四舍五入，而右侧包含四舍五入。但是，乘法也可能会舍入，从而使我们无法做好准备。再次，测试几个x可能会发现一个没有发生这种情况的示例-如果乘法不精确，那么它是向上舍入还是向下舍入基本上取决于x中的某个位，因此很少有试验足以找到一个可行的例子。
回到原始比例，用.001代替.000001，我们可以说.00x <= .001 * x对于小于253的所有x成立。这是因为所有此类整数x在double中都可以精确表示，并且.001到double取整，产生0.001000000000000000020816681711721685132943093776702880859375。因此，即使左侧.00x向下舍入，右侧也包含向上舍入，只能通过乘法中的向下舍入来补偿，因为x到<的转换中没有舍入cc>。由于每次舍入只能移至下一个可表示的值，而不能跳过任何下一个值，因此乘法中的舍入不能使右侧偏左。因此，double对于所有小于253的.00x <= .001 * x成立。
高于此值，将x转换为x可能会导致舍入错误，并且搜索很容易找到反例（在253以上的第四个奇数中）：double，将9007199254741.001 <= .001 * 9007199254741001转换为9007199254741.001会产生 ，将 double转换为 9007199254741.001953125会产生 9007199254741001，而右侧的值将计算为 double。
如果考虑其他舍入模式：

朝-∞（向下舍入）或向0舍入时，右侧将向下遭受多达三个舍入误差，因此我们可以预期在很多情况下该关系失败。
向+∞取整（向上取整）时，右侧必须至少经历一个向上取整误差，因为 9007199254741000永远无法在基数为2的浮点数中精确表示，并且向上取整规则永远不允许右侧取整。消除了此错误，并且左侧只能有一个舍入错误，它永远不会超过右侧的错误，因此该关系必须始终成立。

附加物
9007199254741可以为负吗？该问题的语法建议否，因为对于 .000…0001 = -3， x将变为 x，这不会形成正确的数字。如果我们将其设置为 .00x，则当 .00-3的大小太大以至于将其转换为 -.003会产生-∞时， .00x <= .001 * x会失败，但不会太大，从而将 x转换为 double会产生- ∞。在这种情况下，我们将有限值与-∞进行比较，并且比较结果为false。在 .00x格式的范围内（值保持有限），比较会遇到上述问题，但需要对舍入规则进行一些修改。
请注意，如果 double足够小，则将其转换为 double可能会产生零（在除向+∞以外的任何标准舍入模式下），并且 .000…0001可能足够大以使其产生∞，在这种情况下将它们相乘会产生一个NaN（或陷阱），并且该关系不成立，因为NaN与数字没有关系。
脚注
1在以10为倍数的底数中，可能会有一些不寻常的相互作用，而这个答案并未探讨。