The multiplication and division of Cauchy reals.
WARNING: this file is experimental and likely to change in future releases.
Note on the convergence modulus for x when computing 1/x:
Thinking in terms of absolute and relative errors and scales we get:
- 2^n is absolute error of 1/x (the requested error)
- 2^k is a lower bound of x -> 2^-k is an upper bound of 1/x
For simplicity lets’ say 2^k is the scale of x and 2^-k is the scale of 1/x.
With this we get:
- relative error of 1/x = absolute error of 1/x / scale of 1/x = 2^n / 2^-k = 2^(n+k)
- 1/x maintains relative error
- relative error of x = relative error 1/x = 2^(n+k)
- absolute error of x = relative error x * scale of x = 2^(n+k) * 2^k
- absolute error of x = 2^(n+2*k)