TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Floats.NeuralFloat.Analysis.StandardUlp

ULP Conditions for Standard Formats #

FIX, positive-precision FLX, and positive-precision FLT do not flush the selected ULP to zero. These witnesses make the generic ULP representability theorem available for each standard family.

source
@[reducible, inline]
abbrev TorchLean.Floats.fixNotFlushToZero (emin : ℤ) :
NeuralExpNotFlushToZero (FIXExp emin)

Fixed-point exponent selection preserves ULP representability.

Instances For
    source
    @[reducible, inline]
    abbrev TorchLean.Floats.flxNotFlushToZero (prec : ℤ) (hprec : 0 < prec) :
    NeuralExpNotFlushToZero (FLXExp prec)

    Positive-precision unbounded floats preserve ULP representability.

    Instances For
      source
      @[reducible, inline]
      abbrev TorchLean.Floats.fltNotFlushToZero (emin prec : ℤ) (hprec : 0 < prec) :
      NeuralExpNotFlushToZero (FLTExp emin prec)

      Positive-precision lower-bounded floats preserve ULP representability.

      Instances For