TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Flocq.Theory.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 FloatLib.Floats.Formats.Flocq.fixNotFlushToZero (emin : ℤ) :
ExpNotFlushToZero (fixExp emin)

Fixed-point exponent selection preserves ULP representability.

Instances For
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.Formats.Flocq.flxNotFlushToZero (prec : ℤ) (hprec : 0 < prec) :
    ExpNotFlushToZero (flxExp prec)

    Positive-precision unbounded floats preserve ULP representability.

    Instances For
      source
      @[reducible, inline]
      abbrev FloatLib.Floats.Formats.Flocq.fltNotFlushToZero (emin prec : ℤ) (hprec : 0 < prec) :
      ExpNotFlushToZero (fltExp emin prec)

      Positive-precision lower-bounded floats preserve ULP representability.

      Instances For