TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Spec.Quantization

Tensor Quantization #

This module lifts the scalar affine quantizer from NN.Floats.Quantization pointwise over TorchLean's shape-indexed tensors. The numerical definition remains usable without importing the tensor library; only this adapter depends on NN.Spec.

source
noncomputable def TorchLean.Floats.Quantization.AffineQuantizer.quantizeTensor (q : AffineQuantizer) (rnd : ℝ → ℤ) {s : Spec.Shape} (x : Spec.Tensor ℝ s) :
Spec.Tensor ℤ s

Apply the affine quantizer independently at every coordinate of an arbitrary-rank tensor.

Instances For
    source
    noncomputable def TorchLean.Floats.Quantization.AffineQuantizer.dequantizeTensor (q : AffineQuantizer) {s : Spec.Shape} (codes : Spec.Tensor ℤ s) :
    Spec.Tensor ℝ s

    Reconstruct every code in an arbitrary-rank tensor on the quantizer's real grid.

    Instances For
      source
      def TorchLean.Floats.Quantization.AffineQuantizer.SaturationInactive (q : AffineQuantizer) (rnd : ℝ → ℤ) {s : Spec.Shape} (x : Spec.Tensor ℝ s) :
      Prop

      Pointwise condition saying that quantization does not clip any coordinate of x.

      Instances For
        source
        def TorchLean.Floats.Quantization.AffineQuantizer.CodesInRange (q : AffineQuantizer) {s : Spec.Shape} (codes : Spec.Tensor ℤ s) :
        Prop

        Pointwise condition saying that every stored code belongs to the quantizer's code set.

        Instances For
          source
          theorem TorchLean.Floats.Quantization.AffineQuantizer.quantizeTensor_inRange (q : AffineQuantizer) (rnd : ℝ → ℤ) {s : Spec.Shape} (x : Spec.Tensor ℝ s) :
          q.CodesInRange (q.quantizeTensor rnd x)

          Every coordinate produced by tensor quantization lies in the declared code interval.

          source
          theorem TorchLean.Floats.Quantization.AffineQuantizer.quantizeTensor_mono (q : AffineQuantizer) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {s : Spec.Shape} {x y : Spec.Tensor ℝ s} (hxy : Spec.Tensor.Forall (fun (ab : ℝ × ℝ) => ab.1 ≤ ab.2) (Spec.zip x y)) :
          Spec.Tensor.Forall (fun (ab : ℤ × ℤ) => ab.1 ≤ ab.2) (Spec.zip (q.quantizeTensor rnd x) (q.quantizeTensor rnd y))

          Pointwise order is preserved by tensor quantization.

          source
          theorem TorchLean.Floats.Quantization.AffineQuantizer.quantizeTensor_dequantizeTensor (q : AffineQuantizer) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {s : Spec.Shape} {codes : Spec.Tensor ℤ s} (hcodes : q.CodesInRange codes) :
          q.quantizeTensor rnd (q.dequantizeTensor codes) = codes

          An in-range code tensor survives pointwise dequantization and requantization exactly.

          source
          theorem TorchLean.Floats.Quantization.AffineQuantizer.dequantizeTensor_quantizeTensor_error_le (q : AffineQuantizer) (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] {s : Spec.Shape} {x : Spec.Tensor ℝ s} (hinactive : q.SaturationInactive rnd x) :
          Spec.Tensor.Forall (fun (e : ℝ) => |e| ≤ q.scale / 2) ((q.dequantizeTensor (q.quantizeTensor rnd x)).subSpec x)

          If no coordinate clips, every tensor reconstruction error is at most half a step.