TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Arithmetic.Constants

Correctness of finite constants #

The format-generic encodings of positive and negative one are finite normal values and decode to the corresponding real constants. These facts are useful for powers, reciprocals, and executable interval constructors.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_posOne (fmt : FloatFormat) :
(posOne fmt).isFinite = true

Positive one is finite in every supported format.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_negOne (fmt : FloatFormat) :
(negOne fmt).isFinite = true

Negative one is finite in every supported format.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_posOne (fmt : FloatFormat) :
(posOne fmt).toReal = 1

Positive one denotes the real number 1 in every supported format.

source
@[simp]
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_negOne (fmt : FloatFormat) :
(negOne fmt).toReal = -1

Negative one denotes the real number -1 in every supported format.