Tensor Quantization

This module lifts FloatLib's RealAffineQuantizer pointwise over TorchLean's shape-indexed tensors. The real-domain specification retains arbitrary valid rounding rules. The rational tensor API imports FloatLib's executable affine quantizer directly.

FloatLib's RealAffineQuantizer supplies a real-valued scale, bounded integer codes, and a caller-chosen rounding rule. Its AffineQuantizer supplies executable rational nearest-even quantization, and the Flocq adapter proves agreement with the real specification. Scalar definitions and rounding proofs stay in FloatLib so tensor clients use the same grids and error bounds.

The equations follow Jacob et al., "Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference," CVPR 2018, doi:10.1109/CVPR.2018.00286.

noncomputable def FloatLib.Numerics.Quantization.RealAffineQuantizer.quantizeTensor (q : RealAffineQuantizer) (rnd : ℝ → ℤ) {s : Spec.Shape} (x : TorchLean.Tensor ℝ s) : TorchLean.Tensor ℤ s

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

noncomputable def FloatLib.Numerics.Quantization.RealAffineQuantizer.dequantizeTensor (q : RealAffineQuantizer) {s : Spec.Shape} (codes : TorchLean.Tensor ℤ s) : TorchLean.Tensor ℝ s

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

def FloatLib.Numerics.Quantization.RealAffineQuantizer.SaturationInactive (q : RealAffineQuantizer) (rnd : ℝ → ℤ) {s : Spec.Shape} (x : TorchLean.Tensor ℝ s) : Prop

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

def FloatLib.Numerics.Quantization.RealAffineQuantizer.CodesInRange (q : RealAffineQuantizer) {s : Spec.Shape} (codes : TorchLean.Tensor ℤ s) : Prop

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

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.quantizeTensor_inRange (q : RealAffineQuantizer) (rnd : ℝ → ℤ) {s : Spec.Shape} (x : TorchLean.Tensor ℝ s) : q.CodesInRange (q.quantizeTensor rnd x)

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

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.quantizeTensor_mono (q : RealAffineQuantizer) (rnd : ℝ → ℤ) [Floats.Formats.Flocq.ValidRnd rnd] {s : Spec.Shape} {x y : TorchLean.Tensor ℝ s} (hxy : TorchLean.Tensor.Forall₂ (fun (x1 x2 : ℝ) => x1 ≤ x2) x y) : TorchLean.Tensor.Forall₂ (fun (x1 x2 : ℤ) => x1 ≤ x2) (q.quantizeTensor rnd x) (q.quantizeTensor rnd y)

Pointwise order is preserved by tensor quantization.

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.quantizeTensor_dequantizeTensor (q : RealAffineQuantizer) (rnd : ℝ → ℤ) [Floats.Formats.Flocq.ValidRnd rnd] {s : Spec.Shape} {codes : TorchLean.Tensor ℤ s} (hcodes : q.CodesInRange codes) : q.quantizeTensor rnd (q.dequantizeTensor codes) = codes

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

theorem FloatLib.Numerics.Quantization.RealAffineQuantizer.dequantizeTensor_quantizeTensor_error_le (q : RealAffineQuantizer) (rnd : ℝ → ℤ) [Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {x : TorchLean.Tensor ℝ s} (hinactive : q.SaturationInactive rnd x) : TorchLean.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.