TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Complex.NumericalSystem

Executable complex values as numerical systems #

A complex code denotes a value in ℂ when both scalar components are finite. Its denotation is undefined if either component is NaN or infinite.

source
noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.numericalSystem (fmt : FloatFormat) :
Numerics.NumericalSystem

Complex semantics over an arbitrary component format.

Instances For
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.AtValue (fmt : FloatFormat) (value : Numerics.NumericalValue ℂ) :
    Type

    An executable complex value with an erased proof of its complete denotation.

    Instances For
      source
      @[reducible, inline]
      abbrev FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.At (fmt : FloatFormat) (value : ℂ) :
      Type

      An executable complex value with an erased proof of its finite complex value.

      Instances For
        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.numericalSystem_represents_of_isFinite {fmt : FloatFormat} (z : ExecComplex fmt) (hz : z.isFinite = true) :
        (numericalSystem fmt).Represents z z.toComplex

        Finite executable components denote their assembled mathematical complex value.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.represents_iff {fmt : FloatFormat} (z : ExecComplex fmt) (value : ℂ) :
        (numericalSystem fmt).Represents z value ↔ z.isFinite = true ∧ z.toComplex = value

        A complex code represents a value exactly when both components are finite and decode to it.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.neg_refines (fmt : FloatFormat) :
        Numerics.Operation.Finite1 (numericalSystem fmt) (numericalSystem fmt) neg fun (value : ℂ) => -value

        Componentwise sign negation refines exact complex negation.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.conj_refines (fmt : FloatFormat) :
        Numerics.Operation.Finite1 (numericalSystem fmt) (numericalSystem fmt) conj ⇑(starRingEnd ℂ)

        Conjugation refines exact mathematical complex conjugation.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.add_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) :
        Numerics.Operation.Finite2If (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) add (roundedAdd fmt) fun (x x_1 result : (numericalSystem fmt).Code) => isFinite result = true

        Complex addition refines its explicit componentwise rounded semantics.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.sub_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) :
        Numerics.Operation.Finite2If (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) sub (roundedSub fmt) fun (x x_1 result : (numericalSystem fmt).Code) => isFinite result = true

        Complex subtraction refines its explicit componentwise rounded semantics.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.mul_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) :
        Numerics.Operation.Finite2If (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) mul (roundedMul fmt) fun (x y x_1 : (numericalSystem fmt).Code) => MulFinite x y

        Complex multiplication refines all six scalar rounding sites in roundedMul.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.div_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) :
        Numerics.Operation.Finite2If (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) div (roundedDiv fmt) fun (x y x_1 : (numericalSystem fmt).Code) => DivFinite x y

        Ratio division refines its selected rounded expression under all scalar domain obligations.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.normSq_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) :
        Numerics.Operation.Finite1If (numericalSystem fmt) (Model.numericalSystem fmt) normSq (roundedNormSq fmt) fun (z : (numericalSystem fmt).Code) (x : (Model.numericalSystem fmt).Code) => NormSqFinite z

        Squared magnitude refines a real-valued rounded expression in the scalar numerical system.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.magnitude_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) :
        Numerics.Operation.Finite1If (numericalSystem fmt) (Model.numericalSystem fmt) magnitude (roundedMagnitude fmt) fun (z : (numericalSystem fmt).Code) (x : (Model.numericalSystem fmt).Code) => MagnitudeFinite z

        Scaled magnitude refines its real-valued expression, retaining the scalar domain conditions.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toReal_normSq_of_represents {fmt : FloatFormat} {z : ExecComplex fmt} {value : ℂ} (hfmt : fmt.isIEEE = true) (hz : (numericalSystem fmt).Represents z value) (hfinite : z.NormSqFinite) :
        z.normSq.toReal = roundedNormSq fmt value

        Decode squared magnitude directly when the complex input represents a specified value.

        source
        theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toReal_magnitude_of_represents {fmt : FloatFormat} {z : ExecComplex fmt} {value : ℂ} (hfmt : fmt.isIEEE = true) (hz : (numericalSystem fmt).Represents z value) (hfinite : z.MagnitudeFinite) :
        z.magnitude.toReal = roundedMagnitude fmt value

        Decode magnitude directly when the complex input represents a specified value.