TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Real

Real values of configured binary values #

toReal? reads a configured binary value as the real number it denotes, through its proof model, and returns none for NaNs and infinities, which have no real value. toReal is the total version, which maps them to zero as Model.toReal does.

The theorems toReal_add through toReal_sqrt state the IEEE rounding contract on the configured carrier: a finite result of x + y, x - y, x * y, x / y, or sqrt x is the nearest-even rounding Model.roundAt of the exact real result. abs_toReal_add_sub_le and its siblings turn that into an absolute error of at most half an ulp, Model.epsilonAt format. They need an IEEE descriptor, finite operands, a finite result (square root always has one), a nonzero divisor for division, a nonnegative operand for square root, and, like toModel_hAdd, the instance argument that the selected capability computes the configured model operation. Instance search proves that argument for every capability the library declares.

source
noncomputable def FloatLib.Floats.ExecFloat.Binary.toReal? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) :
Option ℝ

Exact real value of a finite configured binary value, or none for a NaN or an infinity.

Instances For
    source
    noncomputable def FloatLib.Floats.ExecFloat.Binary.toReal {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) :
    ℝ

    Real value of a configured binary value. A NaN or an infinity, which has no real value, gives zero. Theorems about it carry finiteness hypotheses, and toReal? is the partial version.

    Instances For
      source
      @[simp]
      theorem FloatLib.Floats.ExecFloat.Binary.toReal?_eq_none_iff {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) :
      value.toReal? = none ↔ value.isFinite = false

      The optional real value is absent exactly for the values that are not finite.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.toReal_of_toRat?_eq_some {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} {q : ℚ} (hvalue : value.toRat? = some q) :
      value.toReal = ↑q

      A value whose exact rational value is q has real value q.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.toReal?_eq_some_toReal {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] {value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} (hvalue : value.isFinite = true) :
      value.toReal? = some value.toReal

      A finite value's optional real value is its real value.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.toReal_add {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Add (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.add] (hformat : format.isIEEE = true) (hleft : left.isFinite = true) (hright : right.isFinite = true) (hresult : (left + right).isFinite = true) :
      (left + right).toReal = Formats.BinaryInterchange.Model.roundAt format (left.toReal + right.toReal)

      A finite configured sum is the nearest-even rounding of the exact real sum.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.toReal_sub {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Sub (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sub] (hformat : format.isIEEE = true) (hleft : left.isFinite = true) (hright : right.isFinite = true) (hresult : (left - right).isFinite = true) :
      (left - right).toReal = Formats.BinaryInterchange.Model.roundAt format (left.toReal - right.toReal)

      A finite configured difference is the nearest-even rounding of the exact real difference.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.toReal_mul {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Mul (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.mul] (hformat : format.isIEEE = true) (hleft : left.isFinite = true) (hright : right.isFinite = true) (hresult : (left * right).isFinite = true) :
      (left * right).toReal = Formats.BinaryInterchange.Model.roundAt format (left.toReal * right.toReal)

      A finite configured product is the nearest-even rounding of the exact real product.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.toReal_div {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Div (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.div] (hformat : format.isIEEE = true) (hleft : left.isFinite = true) (hright : right.isFinite = true) (hzero : right.isZero = false) (hresult : (left / right).isFinite = true) :
      (left / right).toReal = Formats.BinaryInterchange.Model.roundAt format (left.toReal / right.toReal)

      A finite configured quotient by a nonzero divisor is the nearest-even rounding of the exact real quotient.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.toReal_sqrt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Sqrt (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sqrt] (hformat : format.isIEEE = true) (hvalue : value.isFinite = true) (hdomain : value.isZero = true ∨ value.signBit = false) :
      toReal value.sqrt = Formats.BinaryInterchange.Model.roundAt format √value.toReal

      The configured square root of a finite zero or positive value is the nearest-even rounding of the exact real square root. The result is always finite.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.abs_toReal_add_sub_le {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Add (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.add] (hformat : format.isIEEE = true) (hleft : left.isFinite = true) (hright : right.isFinite = true) (hresult : (left + right).isFinite = true) :
      |(left + right).toReal - (left.toReal + right.toReal)| ≤ Formats.BinaryInterchange.Model.epsilonAt format (left.toReal + right.toReal)

      A finite configured sum is within half an ulp of the exact real sum.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.abs_toReal_sub_sub_le {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Sub (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sub] (hformat : format.isIEEE = true) (hleft : left.isFinite = true) (hright : right.isFinite = true) (hresult : (left - right).isFinite = true) :
      |(left - right).toReal - (left.toReal - right.toReal)| ≤ Formats.BinaryInterchange.Model.epsilonAt format (left.toReal - right.toReal)

      A finite configured difference is within half an ulp of the exact real difference.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.abs_toReal_mul_sub_le {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Mul (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.mul] (hformat : format.isIEEE = true) (hleft : left.isFinite = true) (hright : right.isFinite = true) (hresult : (left * right).isFinite = true) :
      |(left * right).toReal - left.toReal * right.toReal| ≤ Formats.BinaryInterchange.Model.epsilonAt format (left.toReal * right.toReal)

      A finite configured product is within half an ulp of the exact real product.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.abs_toReal_div_sub_le {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Div (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.div] (hformat : format.isIEEE = true) (hleft : left.isFinite = true) (hright : right.isFinite = true) (hzero : right.isZero = false) (hresult : (left / right).isFinite = true) :
      |(left / right).toReal - left.toReal / right.toReal| ≤ Formats.BinaryInterchange.Model.epsilonAt format (left.toReal / right.toReal)

      A finite configured quotient by a nonzero divisor is within half an ulp of the exact real quotient.

      source
      theorem FloatLib.Floats.ExecFloat.Binary.abs_toReal_sqrt_sub_le {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] [Backend.PolicyFor (Formats.BinaryInterchange.Configured.Family format code plan)] {value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code} [cap : Sqrt (Formats.BinaryInterchange.Configured.Family format code plan)] [Capability.HasSpec cap Formats.BinaryInterchange.Configured.Spec.sqrt] (hformat : format.isIEEE = true) (hvalue : value.isFinite = true) (hdomain : value.isZero = true ∨ value.signBit = false) :
      |toReal value.sqrt - √value.toReal| ≤ Formats.BinaryInterchange.Model.epsilonAt format √value.toReal

      The configured square root of a finite zero or positive value is within half an ulp of the exact real square root.