TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.NeuralFloat.Analysis.Ulp

Unit in the Last Place #

Format-generic properties of neuralUlp, including the lower-exponent witness used to define ulp 0. The definitions and hypotheses follow Flocq's Core/Ulp.v.

source
theorem TorchLean.Floats.neuralNegligibleExp_value_unique {fexp : ℤ → ℤ} [NeuralValidExp fexp] {n m : ℤ} (hn : IsNeuralNegligibleExp fexp n) (hm : IsNeuralNegligibleExp fexp m) :
fexp n = fexp m

Two negligible-exponent witnesses select the same format exponent.

source
theorem TorchLean.Floats.neuralNegligibleExp_none_iff_forall_lt {fexp : ℤ → ℤ} :
neuralNegligibleExp fexp = none ↔ ∀ (n : ℤ), fexp n < n

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

source
@[simp]
theorem TorchLean.Floats.neuralUlp_neg {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) :
neuralUlp β fexp (-x) = neuralUlp β fexp x

ULP is invariant under negation.

source
@[simp]
theorem TorchLean.Floats.neuralUlp_abs {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) :
neuralUlp β fexp |x| = neuralUlp β fexp x

ULP is invariant under absolute value.

source
theorem TorchLean.Floats.neuralUlp_bpow {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (e : ℤ) :
neuralUlp β fexp (neuralBpow β e) = neuralBpow β (fexp (e + 1))

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

source
class TorchLean.Floats.NeuralExpNotFlushToZero (fexp : ℤ → ℤ) :
Prop

Exponent functions for which ULP values themselves remain representable.

  • ulpExponent (e : ℤ) : fexp (fexp e + 1) ≤ fexp e
Instances
    source
    theorem TorchLean.Floats.neural_generic_format_ulp_zero {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] :
    neuralGenericFormat β fexp (neuralUlp β fexp 0)

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

    source
    theorem TorchLean.Floats.neural_generic_format_ulp {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] [NeuralExpNotFlushToZero fexp] (x : ℝ) :
    neuralGenericFormat β fexp (neuralUlp β fexp x)

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

    source
    theorem TorchLean.Floats.neuralRound_ceil_eq_floor_add_ulp {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] {x : ℝ} (hx : ¬neuralGenericFormat β fexp x) :
    neuralRound neuralCeilRound x = neuralRound neuralFloorRound x + neuralUlp β fexp x

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

    source
    theorem TorchLean.Floats.neuralUlp_le_abs_of_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] {x : ℝ} (hx0 : x ≠ 0) (hx : neuralGenericFormat β fexp x) :
    neuralUlp β fexp x ≤ |x|

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

    source
    theorem TorchLean.Floats.neuralUlp_mono_pos {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] [NeuralMonotoneExp fexp] {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) :
    neuralUlp β fexp x ≤ neuralUlp β fexp y

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