TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Model.ERealSemantics

Extended-real interpretation of binary models #

Every non-NaN Model fmt has an extended-real interpretation. Finite values use their exact real decoding, while the two infinities map to ⊥ and ⊤. The partial interpretation maps NaNs to none; toEReal is a convenient totalization that maps that single unordered case to zero.

The definitions and proofs are uniform in fmt.

source
noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal? {fmt : FloatFormat} (x : Model fmt) :
Option EReal

Extended-real interpretation of Model; none is reserved exactly for NaNs.

Instances For
    source
    noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal {fmt : FloatFormat} (x : Model fmt) :
    EReal

    Total extended-real interpretation, with the unordered NaN case mapped to zero.

    Instances For
      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal?_eq_none_iff_isNaN_eq_true {fmt : FloatFormat} (x : Model fmt) :
      x.toEReal? = none ↔ x.isNaN = true

      The partial extended-real interpretation is undefined exactly on NaNs.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_eq_false_of_isInf_eq_true {fmt : FloatFormat} (x : Model fmt) (hx : x.isInf = true) :
      x.isNaN = false

      A value classified as infinity is not classified as NaN.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isZero_eq_false_of_isInf_eq_true {fmt : FloatFormat} (x : Model fmt) (hx : x.isInf = true) :
      x.isZero = false

      A value classified as infinity is not classified as zero.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isInf_eq_false_of_isFinite_eq_true {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) :
      x.isInf = false

      Finite values are not infinities.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal?_eq_some_toReal_of_isFinite_eq_true {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) :
      x.toEReal? = some ↑x.toReal

      Finite values enter EReal through their exact real interpretation.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_of_toEReal? {fmt : FloatFormat} {x : Model fmt} {r : EReal} (hx : x.toEReal? = some r) :
      x.toEReal = r

      Totalization agrees with every successful partial interpretation.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_of_toEReal?_none {fmt : FloatFormat} {x : Model fmt} (hx : x.toEReal? = none) :
      x.toEReal = 0

      Totalization maps the partial NaN case to zero.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_eq_ite {fmt : FloatFormat} (x : Model fmt) :
      x.toEReal = if x.isNaN = true then 0 else if x.isInf = true then if x.signBit = true then ⊥ else ⊤ else ↑x.toReal

      Direct case expansion of the total extended-real interpretation.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_eq_coe_toReal_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) :
      x.toEReal = ↑x.toReal

      On finite values, the total interpretation is the coercion of toReal.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_zero (fmt : FloatFormat) (sign : Bool) :
      (zero fmt sign).toEReal = 0

      The policy-aware zero constructor denotes zero in the extended reals.

      Special values #

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal?_ofModel_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) :
      (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).toEReal? = some 0

      The partial interpretation maps an IEEE model-packed signed zero to zero.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_ofModel_zero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) :
      (ofModel fmt (Float.Model.UnpackedFloat.zero sign)).toEReal = 0

      The total interpretation maps an IEEE model-packed signed zero to zero.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal?_ofModel_infinity (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) :
      (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).toEReal? = some (if modelSignBit sign = true then ⊥ else ⊤)

      The partial interpretation maps a model-packed infinity to the endpoint selected by its sign.

      source
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_ofModel_infinity (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Float.Model.UnpackedFloat.Sign) :
      (ofModel fmt (Float.Model.UnpackedFloat.infinity sign)).toEReal = if modelSignBit sign = true then ⊥ else ⊤

      The total interpretation maps a model-packed infinity to the endpoint selected by its sign.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_signedZero (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (negative : Bool) :
      (if negative = true then negZero fmt else posZero fmt).toEReal = 0

      Either IEEE signed zero denotes zero in the extended reals.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_posInf (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) :
      (posInf fmt).toEReal = ⊤

      Positive executable infinity denotes ⊤ in a conventional IEEE format.

      source
      @[simp]
      theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_negInf (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) :
      (negInf fmt).toEReal = ⊥

      Negative executable infinity denotes ⊥ in a conventional IEEE format.