Relative Error in the FLX Format

The unbounded-exponent flxExp prec format has a uniform relative-error bound. For a nonzero input, its ULP is β^(magnitude x - prec), while the magnitude lower bound gives β^(magnitude x - 1) ≤ |x|. Their ratio is therefore at most β^(1 - prec).

Combining the ULP ratio with nearest rounding gives the unit-roundoff bound u = β^(1 - prec) / 2. The same bound holds for FLT inputs in the normal range. The sharper classical bound u / (1 + u) for nearest rounding is not proved here.

theorem FloatLib.Floats.Formats.Flocq.ulp_div_abs_le_FLX {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : x ≠ 0) : ulp β (flxExp prec) x / |x| ≤ bpow β (1 - prec)

The relative size of one FLX ULP is at most β^(1-prec).

theorem FloatLib.Floats.Formats.Flocq.relative_error_round_FLX {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) : ErrorBounds.relativeError x (round rnd x) hx ≤ bpow β (1 - prec) / 2

Nearest FLX rounding has relative error at most the unit roundoff u = β^(1 - prec) / 2.

theorem FloatLib.Floats.Formats.Flocq.round_relative_error_FLX {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) : ∃ (δ : ℝ), |δ| ≤ bpow β (1 - prec) / 2 ∧ round rnd x = x * (1 + δ)

Nearest FLX rounding admits the usual multiplicative model round x = x * (1 + δ) with |δ| ≤ u, where u = β^(1 - prec) / 2 is the unit roundoff.

theorem FloatLib.Floats.Formats.Flocq.ulp_div_abs_le_FLT_normal {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : x ≠ 0) (hnormal : bpow β (emin + prec - 1) ≤ |x|) : ulp β (fltExp emin prec) x / |x| ≤ bpow β (1 - prec)

In the normal range, one FLT ULP has relative size at most β^(1-prec).

theorem FloatLib.Floats.Formats.Flocq.relative_error_round_FLT_normal {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) (hnormal : bpow β (emin + prec - 1) ≤ |x|) : ErrorBounds.relativeError x (round rnd x) hx ≤ bpow β (1 - prec) / 2

Nearest FLT rounding has relative error at most u = β^(1 - prec) / 2 in the normal range.