Affine Quantization

This module gives one affine quantizer for real scalars. For a positive scale $s$, zero point $z$, and integer code interval $[q_{\min},q_{\max}]$, quantization and reconstruction are

$$ Q(x)=\operatorname{clamp}\!\left(\operatorname{round}(x/s)+z,q_{\min},q_{\max}\right), \qquad D(k)=s(k-z). $$

Theorems below cover code-range safety, monotonicity, in-range code round trips, and the half-step reconstruction bound when saturation is inactive. The shape-polymorphic tensor lift belongs to the TorchLean specification adapter NN.Spec.Quantization.

The equations follow the integer-arithmetic quantization scheme used by common neural-network runtimes. See Jacob et al., "Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference," CVPR 2018, doi:10.1109/CVPR.2018.00286.

structure TorchLean.Floats.Quantization.AffineQuantizer : Type

Parameters of a bounded affine quantizer.

• scale : ℝ

  Distance between adjacent reconstructed real values.

• zeroPoint : ℤ

  Integer code representing real zero when it lies in the code range.

• qmin : ℤ

  Smallest stored code.

• qmax : ℤ

  Largest stored code.

• scale_pos : 0 < self.scale

  A quantization scale is strictly positive.

• codeRange : self.qmin ≤ self.qmax

  The code interval is nonempty.

def TorchLean.Floats.Quantization.AffineQuantizer.clampCode (q : AffineQuantizer) (code : ℤ) : ℤ

Saturate an integer to the quantizer's code interval.

noncomputable def TorchLean.Floats.Quantization.AffineQuantizer.rawCode (q : AffineQuantizer) (rnd : ℝ → ℤ) (x : ℝ) : ℤ

Integer code before saturation.

noncomputable def TorchLean.Floats.Quantization.AffineQuantizer.quantize (q : AffineQuantizer) (rnd : ℝ → ℤ) (x : ℝ) : ℤ

Quantize a real value using the supplied integer rounding rule and saturate it to the code set.

noncomputable def TorchLean.Floats.Quantization.AffineQuantizer.dequantize (q : AffineQuantizer) (code : ℤ) : ℝ

Reconstruct a real value from an integer code.

theorem TorchLean.Floats.Quantization.AffineQuantizer.clampCode_mem (q : AffineQuantizer) (code : ℤ) : q.qmin ≤ q.clampCode code ∧ q.clampCode code ≤ q.qmax

Saturation always returns a valid code.

@[simp]

theorem TorchLean.Floats.Quantization.AffineQuantizer.clampCode_eq_self (q : AffineQuantizer) {code : ℤ} (hlo : q.qmin ≤ code) (hhi : code ≤ q.qmax) : q.clampCode code = code

Saturation fixes a code already inside the representable interval.

theorem TorchLean.Floats.Quantization.AffineQuantizer.quantize_mem (q : AffineQuantizer) (rnd : ℝ → ℤ) (x : ℝ) : q.qmin ≤ q.quantize rnd x ∧ q.quantize rnd x ≤ q.qmax

Every quantized scalar lies in the declared code interval.

@[simp]

theorem TorchLean.Floats.Quantization.AffineQuantizer.dequantize_zeroPoint (q : AffineQuantizer) : q.dequantize q.zeroPoint = 0

Dequantizing the zero point gives real zero.

theorem TorchLean.Floats.Quantization.AffineQuantizer.quantize_mono (q : AffineQuantizer) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x y : ℝ} (hxy : x ≤ y) : q.quantize rnd x ≤ q.quantize rnd y

Quantization is monotone for every valid integer rounding rule.

@[simp]

theorem TorchLean.Floats.Quantization.AffineQuantizer.quantize_dequantize (q : AffineQuantizer) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {code : ℤ} (hlo : q.qmin ≤ code) (hhi : code ≤ q.qmax) : q.quantize rnd (q.dequantize code) = code

Every in-range integer code survives a dequantize/quantize round trip.

theorem TorchLean.Floats.Quantization.AffineQuantizer.dequantize_rawCode_error_le (q : AffineQuantizer) (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) : |q.dequantize (q.rawCode rnd x) - x| ≤ q.scale / 2

Without saturation, nearest affine quantization has error at most half a quantization step.

theorem TorchLean.Floats.Quantization.AffineQuantizer.dequantize_quantize_error_le (q : AffineQuantizer) (rnd : ℝ → ℤ) [NeuralValidRndToNearest rnd] (x : ℝ) (hlo : q.qmin ≤ q.rawCode rnd x) (hhi : q.rawCode rnd x ≤ q.qmax) : |q.dequantize (q.quantize rnd x) - x| ≤ q.scale / 2

The half-step bound survives saturation whenever clipping is inactive.