TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Flocq.Theory.Special.FTZ

Abrupt Underflow #

ftzExp emin prec is the Flocq abrupt-underflow exponent selector. Below the smallest normal magnitude it selects the normal threshold emin + prec - 1; above that threshold it agrees with the unbounded precision-prec selector. A matching rounding mode can therefore flush values below the normal range directly to zero.

source
def FloatLib.Floats.Formats.Flocq.ftzExp (emin prec e : ℤ) :
ℤ

Exponent selection with precision prec and smallest normal value β^(emin + prec - 1).

Instances For
    source
    def FloatLib.Floats.Formats.Flocq.ftzThreshold (emin prec : ℤ) :
    ℤ

    The radix exponent of the smallest normal value in the abrupt-underflow format.

    Instances For
      source
      theorem FloatLib.Floats.Formats.Flocq.ftzExp_eq_threshold {emin prec e : ℤ} (h : e ≤ ftzThreshold emin prec) :
      ftzExp emin prec e = ftzThreshold emin prec

      Below the threshold, ftzExp selects the threshold itself.

      source
      theorem FloatLib.Floats.Formats.Flocq.ftzExp_eq_sub {emin prec e : ℤ} (h : ftzThreshold emin prec < e) :
      ftzExp emin prec e = e - prec

      Above the threshold, ftzExp agrees with e - prec.

      source
      @[reducible, inline]
      abbrev FloatLib.Floats.Formats.Flocq.ftzValidExp (emin prec : ℤ) (hprec : 0 < prec) :
      ValidExp (ftzExp emin prec)

      Positive-precision abrupt-underflow exponent selection satisfies Flocq validity.

      Instances For
        source
        theorem FloatLib.Floats.Formats.Flocq.validExp_FTZ_iff (emin prec : ℤ) :
        ValidExp (ftzExp emin prec) ↔ 0 < prec

        ftzExp emin prec satisfies the exponent axioms exactly for positive precision.

        source
        def FloatLib.Floats.Formats.Flocq.FormatPrecision.ftzExp (precision : FormatPrecision) (emin : ℤ) :
        ℤ → ℤ

        The abrupt-underflow exponent selector associated with a checked precision.

        Instances For
          source
          instance FloatLib.Floats.Formats.Flocq.FormatPrecision.ftzExpValid (precision : FormatPrecision) (emin : ℤ) :
          ValidExp (precision.ftzExp emin)

          A checked precision automatically discharges the abrupt-underflow validity obligation.

          source
          theorem FloatLib.Floats.Formats.Flocq.ftzThreshold_negligible (emin prec : ℤ) :
          IsNegligibleExp (ftzExp emin prec) (ftzThreshold emin prec)

          The threshold is a negligible exponent for the abrupt-underflow format.

          source
          theorem FloatLib.Floats.Formats.Flocq.ulp_zero_FTZ {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) :
          ulp β (ftzExp emin prec) 0 = bpow β (ftzThreshold emin prec)

          The ULP at zero in the abrupt-underflow format is the smallest normal magnitude.

          source
          noncomputable def FloatLib.Floats.Formats.Flocq.fTZRound (rnd : ℝ → ℤ) (x : ℝ) :
          ℤ

          Flush an inexact scaled mantissa to zero when its magnitude is below one.

          Instances For
            source
            instance FloatLib.Floats.Formats.Flocq.fTZRoundValid (rnd : ℝ → ℤ) [ValidRnd rnd] :
            ValidRnd (fTZRound rnd)

            Flushing around (-1,1) preserves monotonicity and exact integer values.

            source
            theorem FloatLib.Floats.Formats.Flocq.round_FTZ_small {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) (x : ℝ) (hsmall : |x| < bpow β (ftzThreshold emin prec)) :
            round (fTZRound rnd) x = 0

            Values below the smallest-normal threshold flush exactly to zero.

            source
            theorem FloatLib.Floats.Formats.Flocq.round_FTZ_eq_FLX_of_normal {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) (x : ℝ) (hnormal : bpow β (ftzThreshold emin prec) ≤ |x|) :
            round (fTZRound rnd) x = round rnd x

            At normal magnitudes, abrupt-underflow rounding agrees with FLX rounding.

            source
            def FloatLib.Floats.Formats.Flocq.FTZFormat {β : Numerics.Radix} (emin prec : ℤ) (x : ℝ) :
            Prop

            Exact abrupt-underflow values are zero or normal-range FLX values.

            Instances For
              source
              theorem FloatLib.Floats.Formats.Flocq.not_ftzFormat_of_nonpos {β : Numerics.Radix} (emin prec : ℤ) (hprec : prec ≤ 0) (x : ℝ) :
              ¬FTZFormat emin prec x

              Nonpositive precision is rejected by the explicit abrupt-underflow format predicate.

              source
              theorem FloatLib.Floats.Formats.Flocq.ftzFormat_of_generic {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : genericFormat β (ftzExp emin prec) x) :
              FTZFormat emin prec x

              The generic format generated by ftzExp satisfies the explicit abrupt-underflow predicate.

              source
              theorem FloatLib.Floats.Formats.Flocq.generic_of_ftzFormat {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : FTZFormat emin prec x) :
              genericFormat β (ftzExp emin prec) x

              Every explicit abrupt-underflow value belongs to the generic ftzExp format.

              source
              theorem FloatLib.Floats.Formats.Flocq.generic_format_FTZ_iff {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) :
              genericFormat β (ftzExp emin prec) x ↔ FTZFormat emin prec x

              FTZFormat is exactly the generic format generated by ftzExp.