TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Arithmetic.Square

Once-projected P3109 squares #

Squaring reuses exact multiplication and projects once into the requested destination. The source and destination may have different widths, precisions, signedness, and domains.

source
@[inline]
def FloatLib.Floats.ExecFloat.P3109.square {format : Formats.P3109.Format} (value : P3109 format) (target : Formats.P3109.Format := format) (mode : Formats.P3109.RoundingMode := Formats.P3109.RoundingMode.nearest) (saturation : Formats.P3109.SaturationMode := Formats.P3109.SaturationMode.none) :
P3109 target

Square the exact decoded operand and project once into target, by default the operand's format, with multiplication's NaN and infinity behavior.

Instances For
    source
    theorem FloatLib.Floats.ExecFloat.P3109.square_eq_mul {format : Formats.P3109.Format} (value : P3109 format) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) :
    value.square target mode saturation = value.mul value target mode saturation

    Squaring is multiplication of the operand by itself, for every projection option.

    source
    theorem FloatLib.Floats.ExecFloat.P3109.decode_square_finite {format : Formats.P3109.Format} (value : P3109 format) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) (q : ℚ) (hvalue : value.toClosedRat = Numerics.NumericalValue.finite q) :
    Formats.P3109.Format.SameDatum (value.square target mode saturation).decode (target.projectRatValue { rounding := mode, saturation := saturation } (Numerics.NumericalValue.finite (q * q)))

    A finite square is projected from the exact rational square with no intermediate rounding.