TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Flocq.Calculation.Operations

Exact Operations on Mantissa/Exponent Values #

These operations manipulate FloatRep representations without rounding. Addition aligns both operands to their smaller exponent; multiplication adds exponents. Their correctness theorems are radix-parametric counterparts of Flocq's Calc.Operations results.

source
theorem FloatLib.Floats.Formats.Flocq.intPower_cast_eq_bpow (β : Numerics.Radix) {e : ℤ} (he : 0 ≤ e) :
↑(intPower β e) = bpow β e

Integer radix powers agree with real radix powers at nonnegative exponents.

source
structure FloatLib.Floats.Formats.Flocq.FloatAlignment :
Type

Two integer mantissas expressed on a common exponent grid.

  • leftMantissa : ℤ

    First aligned mantissa.

  • rightMantissa : ℤ

    Second aligned mantissa.

  • exponent : ℤ

    Common exponent, equal to the smaller input exponent.

Instances For
    source
    def FloatLib.Floats.Formats.Flocq.FloatRep.align {β : Numerics.Radix} (f g : FloatRep β) :
    FloatAlignment

    Align two representations to the smaller exponent without changing their real values.

    Instances For
      source
      theorem FloatLib.Floats.Formats.Flocq.FloatRep.align_toReal {β : Numerics.Radix} (f g : FloatRep β) :
      toReal f = toReal { mantissa := (f.align g).leftMantissa, exponent := (f.align g).exponent } ∧ toReal g = toReal { mantissa := (f.align g).rightMantissa, exponent := (f.align g).exponent }

      Alignment preserves both represented real values.

      source
      theorem FloatLib.Floats.Formats.Flocq.FloatRep.align_exponent {β : Numerics.Radix} (f g : FloatRep β) :
      (f.align g).exponent = min f.exponent g.exponent

      Alignment selects the minimum input exponent.

      source
      @[inline]
      def FloatLib.Floats.Formats.Flocq.FloatRep.negExact {β : Numerics.Radix} (f : FloatRep β) :
      FloatRep β

      Exact negation of a mantissa/exponent representation.

      Instances For
        source
        def FloatLib.Floats.Formats.Flocq.FloatRep.absExact {β : Numerics.Radix} (f : FloatRep β) :
        FloatRep β

        Exact absolute value of a mantissa/exponent representation.

        Instances For
          source
          def FloatLib.Floats.Formats.Flocq.FloatRep.addExact {β : Numerics.Radix} (f g : FloatRep β) :
          FloatRep β

          Exact addition after exponent alignment.

          Instances For
            source
            def FloatLib.Floats.Formats.Flocq.FloatRep.subExact {β : Numerics.Radix} (f g : FloatRep β) :
            FloatRep β

            Exact subtraction after exponent alignment.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.Flocq.FloatRep.mulExact {β : Numerics.Radix} (f g : FloatRep β) :
              FloatRep β

              Exact multiplication of mantissas with exponent addition.

              Instances For
                source
                @[simp]
                theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_negExact {β : Numerics.Radix} (f : FloatRep β) :
                toReal f.negExact = -toReal f

                Exact representation negation denotes real negation.

                source
                @[simp]
                theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_absExact {β : Numerics.Radix} (f : FloatRep β) :
                toReal f.absExact = |toReal f|

                Exact representation absolute value denotes real absolute value.

                source
                @[simp]
                theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_addExact {β : Numerics.Radix} (f g : FloatRep β) :
                toReal (f.addExact g) = toReal f + toReal g

                Exact aligned addition denotes real addition.

                source
                @[simp]
                theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_subExact {β : Numerics.Radix} (f g : FloatRep β) :
                toReal (f.subExact g) = toReal f - toReal g

                Exact aligned subtraction denotes real subtraction.

                source
                @[simp]
                theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_mulExact {β : Numerics.Radix} (f g : FloatRep β) :
                toReal (f.mulExact g) = toReal f * toReal g

                Exact mantissa/exponent multiplication denotes real multiplication.