Miscellaneous operators

The following operators are underspecified and therefore not suitable for formal proofs.

Functions with relative error

This set of functions is defined with related theorems on relative error. They can be used to express properties that cannot be directly expressed through unary rounding operators.

{add|sub|mul}_rel< precision [, minimum_exponent] >(..., ...)

If the minimum exponent is not provided, the bound on the relative error is assumed to be valid on the entire domain. Otherwise the interval [math] is excluded from the domain.

Talking about the expression add_rel<20,-60>(a,b) is like talking about a fresh expression c such that not |a + b| <= 1b-60 -> |c -/ (a + b)| <= 1b-20.

Rounding operators with homogen properties

To be written.