TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Quantization.Ordered

Order-theoretic representable neighbors #

Directed and stochastic quantizers need the representable values immediately below and above an exact input. These predicates use only a numerical system's denotation and the order on its finite scalar domain. They do not assume a radix, field layout, unique encoding, or executable search algorithm.

source
def FloatLib.Numerics.Quantization.Ordered.LowerNeighbor (system : NumericalSystem) [Preorder system.Scalar] (input : system.Scalar) (code : system.Code) :
Prop

code represents the greatest representable scalar not exceeding input.

Instances For
    source
    def FloatLib.Numerics.Quantization.Ordered.UpperNeighbor (system : NumericalSystem) [Preorder system.Scalar] (input : system.Scalar) (code : system.Code) :
    Prop

    code represents the least representable scalar not smaller than input.

    Instances For
      source
      theorem FloatLib.Numerics.Quantization.Ordered.lowerNeighbor_iff_isGreatest (system : NumericalSystem) [Preorder system.Scalar] (input : system.Scalar) (code : system.Code) :
      LowerNeighbor system input code ↔ ∃ (output : system.Scalar), system.Represents code output ∧ IsGreatest {y : system.Scalar | system.Representable y ∧ y ≤ input} output

      Lower neighbors are greatest elements of the representable values below the input.

      source
      theorem FloatLib.Numerics.Quantization.Ordered.upperNeighbor_iff_isLeast (system : NumericalSystem) [Preorder system.Scalar] (input : system.Scalar) (code : system.Code) :
      UpperNeighbor system input code ↔ ∃ (output : system.Scalar), system.Represents code output ∧ IsLeast {y : system.Scalar | system.Representable y ∧ input ≤ y} output

      Upper neighbors are least elements of the representable values above the input.

      source
      def FloatLib.Numerics.Quantization.Ordered.Brackets (system : NumericalSystem) [Preorder system.Scalar] (input : system.Scalar) (lower upper : system.Code) :
      Prop

      Two codes bracket an input by its lower and upper representable neighbors.

      Instances For
        source
        theorem FloatLib.Numerics.Quantization.Ordered.lowerNeighbor_isFinite {system : NumericalSystem} [Preorder system.Scalar] {input : system.Scalar} {code : system.Code} (hcode : LowerNeighbor system input code) :
        system.IsFinite code

        A lower-neighbor code has a finite denotation.

        source
        theorem FloatLib.Numerics.Quantization.Ordered.upperNeighbor_isFinite {system : NumericalSystem} [Preorder system.Scalar] {input : system.Scalar} {code : system.Code} (hcode : UpperNeighbor system input code) :
        system.IsFinite code

        An upper-neighbor code has a finite denotation.

        source
        theorem FloatLib.Numerics.Quantization.Ordered.lowerNeighbor_le {system : NumericalSystem} [Preorder system.Scalar] {input output : system.Scalar} {code : system.Code} (hcode : LowerNeighbor system input code) (houtput : system.Represents code output) :
        output ≤ input

        Every lower-neighbor value lies below its exact input.

        source
        theorem FloatLib.Numerics.Quantization.Ordered.le_upperNeighbor {system : NumericalSystem} [Preorder system.Scalar] {input output : system.Scalar} {code : system.Code} (hcode : UpperNeighbor system input code) (houtput : system.Represents code output) :
        input ≤ output

        Every upper-neighbor value lies above its exact input.