Quantize: range, fixed quantum, and numerical error

The successful result has exactly the requested quantum, including signed zero. The coefficient is obtained by a single exact rational rounding on that grid. The range test is necessary and sufficient for a finite result.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantizeMagnitude_valid (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (q : ℤ) : Datum.Valid f (quantizeMagnitude f mode s x q).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantize_valid (f : Format) (mode : RoundingMode) (x y : Datum) : Datum.Valid f (quantize f mode x y).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantizeMagnitude_invalid_iff (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (q : ℤ) : (quantizeMagnitude f mode s x q).status.invalid = true ↔ ¬(f.minQuantum ≤ q ∧ q ≤ f.maxQuantum ∧ mode.roundAt s x q < f.coefficientBound)

Invalid is raised precisely when the requested rounded representation does not fit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantizeMagnitude_of_not_invalid (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (q : ℤ) (h : (quantizeMagnitude f mode s x q).status.invalid = false) : quantizeMagnitude f mode s x q = { value := Datum.finite s (mode.roundAt s x q) q, status := { inexact := decide (↑(mode.roundAt s x q) * 10 ^ q ≠ x) } }

A successful quantization has the specified sign, grid, and rounded coefficient.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantize_range_flags (f : Format) (mode : RoundingMode) (x y : Datum) : (quantize f mode x y).status.underflow = false ∧ (quantize f mode x y).status.overflow = false ∧ (quantize f mode x y).status.divideByZero = false

Quantize raises neither underflow nor overflow, even for inexact subnormal results.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantize_same_quantum (f : Format) (mode : RoundingMode) (s t : Bool) (c d : ℕ) (q : ℤ) (hv : Datum.Valid f (Datum.finite s c q)) : quantize f mode (Datum.finite s c q) (Datum.finite t d q) = { value := Datum.finite s c q }

Quantization to an already represented quantum preserves the entire finite datum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantize_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (s t : Bool) (c d : ℕ) (q r : ℤ) (h : (quantize f mode (Datum.finite s c q) (Datum.finite t d r)).status.invalid = false) : ∃ (value : ℚ), (quantize f mode (Datum.finite s c q) (Datum.finite t d r)).value.toRat? = some value ∧ |value - Datum.finiteValue s c q| ≤ 10 ^ r / 2

The nearest-mode error uses the requested quantum, not a normalized precision grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantize_inexact_iff (f : Format) (mode : RoundingMode) (s t : Bool) (c d : ℕ) (q r : ℤ) (v : ℚ) (hv : (quantize f mode (Datum.finite s c q) (Datum.finite t d r)).value.toRat? = some v) : (quantize f mode (Datum.finite s c q) (Datum.finite t d r)).status.inexact = true ↔ v ≠ Datum.finiteValue s c q

On success the inexact flag records a numerical change, independently of the sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantize_error_lt_one (f : Format) (mode : RoundingMode) (s t : Bool) (c d : ℕ) (q r : ℤ) (h : (quantize f mode (Datum.finite s c q) (Datum.finite t d r)).status.invalid = false) : ∃ (value : ℚ), (quantize f mode (Datum.finite s c q) (Datum.finite t d r)).value.toRat? = some value ∧ |value - Datum.finiteValue s c q| < 10 ^ r

Every rounding direction changes the value by less than one requested grid unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.le_quantize_towardPositive (f : Format) (s t : Bool) (c d : ℕ) (q r : ℤ) (h : (quantize f RoundingMode.towardPositive (Datum.finite s c q) (Datum.finite t d r)).status.invalid = false) : ∃ (value : ℚ), (quantize f RoundingMode.towardPositive (Datum.finite s c q) (Datum.finite t d r)).value.toRat? = some value ∧ Datum.finiteValue s c q ≤ value

Upward quantization is an upper bound on the exact input value, for either sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.quantize_towardNegative_le (f : Format) (s t : Bool) (c d : ℕ) (q r : ℤ) (h : (quantize f RoundingMode.towardNegative (Datum.finite s c q) (Datum.finite t d r)).status.invalid = false) : ∃ (value : ℚ), (quantize f RoundingMode.towardNegative (Datum.finite s c q) (Datum.finite t d r)).value.toRat? = some value ∧ value ≤ Datum.finiteValue s c q

Downward quantization is a lower bound on the exact input value, for either sign.