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).

theorem TorchLean.Floats.neuralUlp_div_abs_le_FLX {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : x ≠ 0) : neuralUlp β (FLXExp prec) x / |x| ≤ neuralBpow β (1 - prec)

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

theorem TorchLean.Floats.relative_error_round_FLX {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) : ErrorBounds.relativeError x (neuralRound rnd x) hx ≤ neuralBpow β (1 - prec) / 2

Nearest FLX rounding has the standard uniform relative-error bound.

theorem TorchLean.Floats.neural_round_relative_error_FLX {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) : ∃ (δ : ℝ), |δ| ≤ neuralBpow β (1 - prec) / 2 ∧ neuralRound rnd x = x * (1 + δ)

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

theorem TorchLean.Floats.neuralUlp_div_abs_le_FLT_normal {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : x ≠ 0) (hnormal : neuralBpow β (emin + prec - 1) ≤ |x|) : neuralUlp β (FLTExp emin prec) x / |x| ≤ neuralBpow β (1 - prec)

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

theorem TorchLean.Floats.relative_error_round_FLT_normal {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) (hx : x ≠ 0) (hnormal : neuralBpow β (emin + prec - 1) ≤ |x|) : ErrorBounds.relativeError x (neuralRound rnd x) hx ≤ neuralBpow β (1 - prec) / 2

Nearest FLT rounding has the FLX relative bound throughout the normal range.