RFR: 8077587: BigInteger Roots [v52]
fabioromano1
duke at openjdk.org
Tue Jul 29 12:28:01 UTC 2025
On Tue, 29 Jul 2025 12:06:37 GMT, fabioromano1 <duke at openjdk.org> wrote:
>> To the above, we can also add
>>
>> *
>> * Noting that x ≥ 2^(bl-1) and ex ≥ 0, similarly to the above we further get
>> * x 2^(-sh') ≥ 2^(ex+P-1) ≥ 2^(P-1)
>> * which shows that ⌊x / 2^sh'⌋ has at least P bits of precision.
>
> @rgiulietti Yes, but why that complication, it is not more natural to prove it in the following way?
>
> recalling x < 2^bl:
> x / 2^sh' = x / 2^(sh-ex) ≤ 2^bl / 2^(sh-ex) = 2^(bl - (sh-ex)) ≤ 2^ME < Double.MAX_VALUE
> ```
> relying on the fact that `bl - (sh-ex)` is the length of the shifted value?
> To the above, we can also add
>
> ```
> *
> * Noting that x ≥ 2^(bl-1) and ex ≥ 0, similarly to the above we further get
> * x 2^(-sh') ≥ 2^(ex+P-1) ≥ 2^(P-1)
> * which shows that ⌊x / 2^sh'⌋ has at least P bits of precision.
> ```
And this should follow by the fact that `bl - (sh-ex) ≥ bl - sh = bl - (bl - P) = P`, since `ex ≥ 0`.
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/24898#discussion_r2239646258
More information about the core-libs-dev
mailing list