TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Flocq.Theory.NumericalSystem

Radix-parametric floats as numerical systems #

For any radix β ≥ 2, this module interprets FloatRep β as a numerical system with denotation m * β^e. The carrier stores a mantissa and exponent, with no bit-layout constraint.

source
noncomputable def FloatLib.Floats.Formats.Flocq.FloatRep.numericalSystem (β : Numerics.Radix) :
Numerics.NumericalSystem

Real semantics of an integer-mantissa, integer-exponent float at arbitrary radix.

Instances For
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.Formats.Flocq.FloatRep.At (β : Numerics.Radix) (value : Numerics.NumericalValue ℝ) :
    Type

    An integer-mantissa float with an erased proof of its complete real denotation.

    Instances For
      source
      @[reducible, inline]
      abbrev FloatLib.Floats.Formats.Flocq.FloatRep.AtFinite (β : Numerics.Radix) (value : ℝ) :
      Type

      An integer-mantissa float with an erased proof of its finite real value.

      Instances For
        source
        @[simp]
        theorem FloatLib.Floats.Formats.Flocq.FloatRep.numericalSystem_represents_iff {β : Numerics.Radix} (x : FloatRep β) (r : ℝ) :
        (numericalSystem β).Represents x r ↔ toReal x = r

        Representation in the generic numerical-system interface is equality of real denotations.