Nearest Rounding with a Tie Choice

nearestChoice chooseUp rounds to a nearest integer. At an exact midpoint, chooseUp f decides whether the lower integer f or the upper integer f + 1 is selected. This is the native Lean counterpart of Flocq's Znearest choice. nearestAwayChoice is the tie rule of IEEE 754-2019 roundTiesToAway.

noncomputable def FloatLib.Floats.Formats.Flocq.nearestChoice (chooseUp : ℤ → Bool) (x : ℝ) : ℤ

Round to a nearest integer, resolving a midpoint according to its lower integer.

theorem FloatLib.Floats.Formats.Flocq.nearestChoice_eq_floor_or_ceil (chooseUp : ℤ → Bool) (x : ℝ) : nearestChoice chooseUp x = ⌊x⌋ ∨ nearestChoice chooseUp x = ⌈x⌉

Choice-based nearest rounding always selects floor or ceiling.

theorem FloatLib.Floats.Formats.Flocq.nearestChoice_bounds (chooseUp : ℤ → Bool) (x : ℝ) : ⌊x⌋ ≤ nearestChoice chooseUp x ∧ nearestChoice chooseUp x ≤ ⌊x⌋ + 1

Choice-based nearest rounding lies between floor and floor plus one.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.nearestChoice_intCast (chooseUp : ℤ → Bool) (n : ℤ) : nearestChoice chooseUp ↑n = n

Choice-based nearest rounding fixes integers.

theorem FloatLib.Floats.Formats.Flocq.nearestChoice_abs_sub_le_half (chooseUp : ℤ → Bool) (x : ℝ) : |↑(nearestChoice chooseUp x) - x| ≤ 1 / 2

Every tie choice has absolute error at most one half.

theorem FloatLib.Floats.Formats.Flocq.nearestChoice_mono (chooseUp : ℤ → Bool) {x y : ℝ} (hxy : x ≤ y) : nearestChoice chooseUp x ≤ nearestChoice chooseUp y

Choice-based nearest rounding is monotone.

instance FloatLib.Floats.Formats.Flocq.nearestChoiceValid (chooseUp : ℤ → Bool) : ValidRndToNearest (nearestChoice chooseUp)

Every tie-choice nearest mode is a valid nearest rounding mode.

def FloatLib.Floats.Formats.Flocq.nearestAwayChoice (f : ℤ) : Bool

Tie choice of rounding to nearest with ties away from zero.

A midpoint f + 1/2 above a nonnegative integer f is positive and goes up to f + 1. A midpoint above a negative integer is negative and stays at f. Either way the tie goes to the neighbor of larger magnitude.