TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Logarithmic.Exact.Proof

Real semantics and correctness of exact logarithmic numbers #

The exact codes from Exact.Runtime denote zero or signed integral powers of the radix. This module defines their real interpretation and numerical system, then connects the executable rational decoder to that interpretation and proves multiplication refinement.

The proof views add only erased propositions to the existing code. The configured family uses these results to expose exact logarithmic multiplication through ExecFloat.

source
noncomputable def FloatLib.Floats.Formats.Logarithmic.Code.toReal {radix : Numerics.Radix} :
Code radix → ℝ

Real value of a logarithmic code.

Instances For
    source
    noncomputable def FloatLib.Floats.Formats.Logarithmic.numericalSystem (radix : Numerics.Radix) :
    Numerics.NumericalSystem

    Real semantics of exact logarithmic codes.

    Instances For
      source
      @[reducible, inline]
      abbrev FloatLib.Floats.Formats.Logarithmic.At (radix : Numerics.Radix) (value : Numerics.NumericalValue ℝ) :
      Type

      A logarithmic code with an erased proof of its complete denotation.

      Instances For
        source
        @[reducible, inline]
        abbrev FloatLib.Floats.Formats.Logarithmic.AtFinite (radix : Numerics.Radix) (value : ℝ) :
        Type

        A logarithmic code with an erased proof of its real value.

        Instances For

          Arithmetic refinement #

          source
          @[simp]
          theorem FloatLib.Floats.Formats.Logarithmic.Code.toReal_zero (radix : Numerics.Radix) :
          zero.toReal = 0

          The distinguished logarithmic zero code decodes to real zero.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.Logarithmic.Code.toRat_zero (radix : Numerics.Radix) :
          zero.toRat = 0

          The distinguished logarithmic zero code decodes to rational zero.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.Logarithmic.Code.cast_toRat {radix : Numerics.Radix} (value : Code radix) :
          ↑value.toRat = value.toReal

          The executable rational decoder agrees with the exact real semantics.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.Logarithmic.Code.toReal_mul {radix : Numerics.Radix} (left right : Code radix) :
          (left.mul right).toReal = left.toReal * right.toReal

          Decoding logarithmic multiplication gives exact real multiplication.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.Logarithmic.Code.toRat_mul {radix : Numerics.Radix} (left right : Code radix) :
          (left.mul right).toRat = left.toRat * right.toRat

          Logarithmic multiplication is exact in the executable rational domain as well.

          source
          @[simp]
          theorem FloatLib.Floats.Formats.Logarithmic.numericalSystem_represents_iff {radix : Numerics.Radix} (code : Code radix) (value : ℝ) :
          (numericalSystem radix).Represents code value ↔ code.toReal = value

          Representation in the logarithmic system is equality of decoded real values.

          source
          theorem FloatLib.Floats.Formats.Logarithmic.mul_refines {radix : Numerics.Radix} :
          Numerics.Operation.Finite2 (numericalSystem radix) (numericalSystem radix) (numericalSystem radix) Code.mul fun (left right : ℝ) => left * right

          Logarithmic multiplication exactly refines multiplication over the reals.