TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Flocq.Theory.Analysis.Ulp

Unit in the Last Place #

The format-generic ulp laws cover the negligible-exponent witness used to define ulp 0, invariance under sign, representability, and the relationship to adjacent rounded values. The definitions and hypotheses follow Flocq's Core/Ulp.v.

These are mathematical analysis lemmas rather than executable kernels. Keeping them in the Flocq theory namespace makes the provenance and theorem correspondence visible while allowing runtime formats to depend on smaller exact-arithmetic modules.

source
theorem FloatLib.Floats.Formats.Flocq.negligibleExp_value_unique {fexp : ℤ → ℤ} [ValidExp fexp] {n m : ℤ} (hn : IsNegligibleExp fexp n) (hm : IsNegligibleExp fexp m) :
fexp n = fexp m

Two negligible-exponent witnesses select the same format exponent.

source
theorem FloatLib.Floats.Formats.Flocq.negligibleExp_none_iff_forall_lt {fexp : ℤ → ℤ} :
negligibleExp fexp = none ↔ ∀ (n : ℤ), fexp n < n

Absence of a negligible exponent means fexp n < n at every exponent.

source
@[simp]
theorem FloatLib.Floats.Formats.Flocq.ulp_neg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) :
ulp β fexp (-x) = ulp β fexp x

ULP is invariant under negation.

source
@[simp]
theorem FloatLib.Floats.Formats.Flocq.ulp_abs {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) :
ulp β fexp |x| = ulp β fexp x

ULP is invariant under absolute value.

source
theorem FloatLib.Floats.Formats.Flocq.ulp_bpow {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (e : ℤ) :
ulp β fexp (bpow β e) = bpow β (fexp (e + 1))

The ULP of a radix power is selected at the next magnitude.

source
class FloatLib.Floats.Formats.Flocq.ExpNotFlushToZero (fexp : ℤ → ℤ) :
Prop

Exponent functions for which ULP values themselves remain representable.

  • ulpExponent (e : ℤ) : fexp (fexp e + 1) ≤ fexp e

    The radix power selected as a ULP is representable at its own magnitude.

Instances
    source
    theorem FloatLib.Floats.Formats.Flocq.generic_format_ulp_zero {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] :
    genericFormat β fexp (ulp β fexp 0)

    The zero ULP is representable, including the FLX case where it equals zero.

    source
    theorem FloatLib.Floats.Formats.Flocq.generic_format_ulp {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] [ExpNotFlushToZero fexp] (x : ℝ) :
    genericFormat β fexp (ulp β fexp x)

    Under the non-flush-to-zero condition, every ULP is representable.

    source
    theorem FloatLib.Floats.Formats.Flocq.round_ceil_eq_floor_add_ulp {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : ¬genericFormat β fexp x) :
    round ceilRound x = round floorRound x + ulp β fexp x

    For a nonrepresentable input, directed-up and directed-down rounding differ by one ULP.

    source
    theorem FloatLib.Floats.Formats.Flocq.ulp_le_abs_of_generic {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx0 : x ≠ 0) (hx : genericFormat β fexp x) :
    ulp β fexp x ≤ |x|

    One ULP is no larger than the absolute value of a nonzero representable number.

    source
    theorem FloatLib.Floats.Formats.Flocq.ulp_mono_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] [MonotoneExp fexp] {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) :
    ulp β fexp x ≤ ulp β fexp y

    ULP is monotone on positive inputs when the exponent selector is monotone.