TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Rounding.NearestEven

Nearest-even rounding lemmas #

Format-independent integer primitives in Numerics agree with FloatLib's rounded-real nearest-even operation under the stated bounds.

Generic shift-rounding equations and floor bounds live in Numerics.Quantization.Deterministic.ShiftRight, where fixed-point and other binary quantizations can reuse them. This module adds normalized-significand bounds, oddness of nearestEven, and its agreement with executable rounding of nonnegative rationals.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundShiftRightEven_add_normalized_bounds (precision left right : ℕ) (hleft : 2 ^ precision ≤ left ∧ left < 2 ^ (precision + 1)) (hright : 2 ^ precision ≤ right ∧ right < 2 ^ (precision + 1)) :
2 ^ precision ≤ Numerics.roundShiftRightEven (left + right) 1 ∧ Numerics.roundShiftRightEven (left + right) 1 < 2 ^ (precision + 1)

Nearest-even averaging preserves the normalized interval for every significand precision.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nearestEven_neg (x : ℝ) :
Flocq.nearestEven (-x) = -Flocq.nearestEven x

Nearest-even integer rounding commutes with negation.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nearestEven_le_natCast_of_le {value : ℝ} {bound : ℕ} (hvalue : value ≤ ↑bound) :
Flocq.nearestEven value ≤ Int.ofNat bound

Nearest-even rounding never exceeds a natural upper bound of its argument.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.natCast_le_nearestEven_of_le {bound : ℕ} {value : ℝ} (hvalue : ↑bound ≤ value) :
Int.ofNat bound ≤ Flocq.nearestEven value

Nearest-even rounding never drops below a natural lower bound of its argument.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floor_real_nat_div (num den : ℕ) :
⌊↑num / ↑den⌋ = ↑(num / den)

The floor of a quotient of natural numbers in ℝ is their natural-number quotient.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nearestEven_div_eq_roundQuotientEven (num den : ℕ) (hden : den ≠ 0) :
Flocq.nearestEven (↑num / ↑den) = Int.ofNat (Numerics.roundQuotientEven num den)

Nearest-even rounding of a nonnegative rational agrees with roundQuotientEven.

source
theorem FloatLib.Floats.Formats.BinaryInterchange.Model.nearestEven_div_pow2_eq_roundShiftRightEven (num shift : ℕ) :
Flocq.nearestEven (↑num / ↑(pow2 shift)) = Int.ofNat (Numerics.roundShiftRightEven num shift)

Nearest-even rounding after division by 2^shift is executable shift rounding.