Error bounds for executable binary floats

These bounds relate operations on Model fmt to exact real arithmetic. The function toReal interprets finite values in ℝ, and the format parameter selects the corresponding Flocq-style grid. This real-valued grid has no upper exponent bound, so the executable operation theorems apply when the result is finite.

The operation theorems require finite inputs and outputs because infinities and NaNs have no real value. Signed zeros both have real value zero.

@[reducible, inline]

noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.ulpAt (fmt : FloatFormat) (x : ℝ) : ℝ

One unit in the last place at x for the precision and gradual-underflow grid of fmt.

@[reducible, inline]

noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt (fmt : FloatFormat) (x : ℝ) : ℝ

Half an ULP at x for the precision and gradual-underflow grid of fmt.

@[reducible, inline]

noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.minNormalAt (fmt : FloatFormat) : ℝ

The least positive normal magnitude of fmt.

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instMonotoneExpFexpOf (fmt : FloatFormat) : Flocq.MonotoneExp (fexpOf fmt)

The exponent-selection function of every executable format is monotone.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_roundAt_sub_le (fmt : FloatFormat) (x : ℝ) : |roundAt fmt x - x| ≤ epsilonAt fmt x

Nearest-even rounding to fmt has at most half an ULP of absolute error.

The format-specific epsilonAt follows the subnormal grid near zero, so this bound is useful even where a uniform relative-error bound is impossible.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_mem_Icc (fmt : FloatFormat) (x : ℝ) : x ∈ Set.Icc (roundAt fmt x - epsilonAt fmt x) (roundAt fmt x + epsilonAt fmt x)

The exact real input lies in the half-ULP enclosure around its rounded value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.relativeError_roundAt_le_of_normal (fmt : FloatFormat) (x : ℝ) (hx : x ≠ 0) (hnormal : minNormalAt fmt ≤ |x|) : Flocq.ErrorBounds.relativeError x (roundAt fmt x) hx ≤ Flocq.bpow Numerics.binaryRadix (1 - Int.ofNat (fmt.fracWidth + 1)) / 2

Normal-range nearest-even rounding has the standard relative error bound 2^(1-precision) / 2.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_add_sub_le {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : isFinite (x.add y) = true) : |toReal (x.add y) - (x.toReal + y.toReal)| ≤ epsilonAt fmt (x.toReal + y.toReal)

Absolute error of one finite executable addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_sub_sub_le {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : isFinite (x.sub y) = true) : |toReal (x.sub y) - (x.toReal - y.toReal)| ≤ epsilonAt fmt (x.toReal - y.toReal)

Absolute error of one finite executable subtraction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_mul_sub_le {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : isFinite (x.mul y) = true) : |toReal (x.mul y) - x.toReal * y.toReal| ≤ epsilonAt fmt (x.toReal * y.toReal)

Absolute error of one finite executable multiplication.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_div_sub_le {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) (hout : isFinite (x.div y) = true) : |toReal (x.div y) - x.toReal / y.toReal| ≤ epsilonAt fmt (x.toReal / y.toReal)

Absolute error of one finite executable division by a nonzero divisor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_sqrt_sub_le {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hdomain : x.isZero = true ∨ x.signBit = false) : |toReal x.sqrt - √x.toReal| ≤ epsilonAt fmt √x.toReal

Absolute error of one finite executable square root on a nonnegative input, including either signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_fma_sub_le {fmt : FloatFormat} (x y z : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hz : z.isFinite = true) (hout : isFinite (x.fma y z) = true) : |toReal (x.fma y z) - (x.toReal * y.toReal + z.toReal)| ≤ epsilonAt fmt (x.toReal * y.toReal + z.toReal)

Absolute error of one finite executable fused multiply-add.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_cast_of_abs_toReal_le_posMaxFinite {src dst : FloatFormat} (x : Model src) (hdst : dst.isIEEE = true) (hx : x.isFinite = true) (hbound : |x.toReal| ≤ (posMaxFinite dst).toReal) : isFinite (cast src dst x) = true

A finite value whose magnitude fits in the destination's finite range stays finite under conversion. With abs_toReal_cast_sub_le this discharges the output hypothesis from the input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_cast_sub_le_of_isIEEE_destination {src dst : FloatFormat} (x : Model src) (hdst : dst.isIEEE = true) (hx : x.isFinite = true) (hout : isFinite (cast src dst x) = true) : |toReal (cast src dst x) - x.toReal| ≤ epsilonAt dst x.toReal

Absolute error of one finite cross-format cast.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_toReal_cast_sub_le {src dst : FloatFormat} (x : Model src) (hsrc : src.isIEEE = true) (hdst : dst.isIEEE = true) (hx : x.isFinite = true) (hout : isFinite (cast src dst x) = true) : |toReal (cast src dst x) - x.toReal| ≤ epsilonAt dst x.toReal

IEEE-source specialization of abs_toReal_cast_sub_le_of_isIEEE_destination.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.add_exact_mem_Icc {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : isFinite (x.add y) = true) : x.toReal + y.toReal ∈ Set.Icc (toReal (x.add y) - epsilonAt fmt (x.toReal + y.toReal)) (toReal (x.add y) + epsilonAt fmt (x.toReal + y.toReal))

The exact sum lies in the half-ULP enclosure around executable addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sub_exact_mem_Icc {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : isFinite (x.sub y) = true) : x.toReal - y.toReal ∈ Set.Icc (toReal (x.sub y) - epsilonAt fmt (x.toReal - y.toReal)) (toReal (x.sub y) + epsilonAt fmt (x.toReal - y.toReal))

The exact difference lies in the half-ULP enclosure around executable subtraction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mul_exact_mem_Icc {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : isFinite (x.mul y) = true) : x.toReal * y.toReal ∈ Set.Icc (toReal (x.mul y) - epsilonAt fmt (x.toReal * y.toReal)) (toReal (x.mul y) + epsilonAt fmt (x.toReal * y.toReal))

The exact product lies in the half-ULP enclosure around executable multiplication.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.div_exact_mem_Icc {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) (hout : isFinite (x.div y) = true) : x.toReal / y.toReal ∈ Set.Icc (toReal (x.div y) - epsilonAt fmt (x.toReal / y.toReal)) (toReal (x.div y) + epsilonAt fmt (x.toReal / y.toReal))

The exact quotient lies in the half-ULP enclosure around executable division.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sqrt_exact_mem_Icc {fmt : FloatFormat} (x : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hdomain : x.isZero = true ∨ x.signBit = false) : √x.toReal ∈ Set.Icc (toReal x.sqrt - epsilonAt fmt √x.toReal) (toReal x.sqrt + epsilonAt fmt √x.toReal)

The exact square root lies in the half-ULP enclosure around executable square root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fma_exact_mem_Icc {fmt : FloatFormat} (x y z : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hz : z.isFinite = true) (hout : isFinite (x.fma y z) = true) : x.toReal * y.toReal + z.toReal ∈ Set.Icc (toReal (x.fma y z) - epsilonAt fmt (x.toReal * y.toReal + z.toReal)) (toReal (x.fma y z) + epsilonAt fmt (x.toReal * y.toReal + z.toReal))

The exact multiply-add lies in the half-ULP enclosure around executable FMA.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_exact_mem_Icc_of_isIEEE_destination {src dst : FloatFormat} (x : Model src) (hdst : dst.isIEEE = true) (hx : x.isFinite = true) (hout : isFinite (cast src dst x) = true) : x.toReal ∈ Set.Icc (toReal (cast src dst x) - epsilonAt dst x.toReal) (toReal (cast src dst x) + epsilonAt dst x.toReal)

The source real value lies in the half-ULP enclosure around a finite cast.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_exact_mem_Icc {src dst : FloatFormat} (x : Model src) (hsrc : src.isIEEE = true) (hdst : dst.isIEEE = true) (hx : x.isFinite = true) (hout : isFinite (cast src dst x) = true) : x.toReal ∈ Set.Icc (toReal (cast src dst x) - epsilonAt dst x.toReal) (toReal (cast src dst x) + epsilonAt dst x.toReal)

IEEE-source specialization of cast_exact_mem_Icc_of_isIEEE_destination.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.genericFormat_toReal_add_sub {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : isFinite (x.add y) = true) : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) (toReal (x.add y) - (x.toReal + y.toReal))

The residual of finite nearest-even addition is representable in the same format.