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.

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.