Real stochastic rounding thresholds

The report's floor and nearest-even formulas can be tested by comparing the exact real fraction with one rational threshold. These identities apply to irrational fractions as well. They justify the integer square comparisons used when rounding a square root.

Reference: P3109 unapproved interim report 4.0.3, revision 34f5964, §4.7.4.

noncomputable def FloatLib.Floats.Formats.P3109.RealRounding.nearestEven (value : ℝ) : ℕ

Nearest integer to a nonnegative real, with ties sent to the even integer.

@[simp]

theorem FloatLib.Floats.Formats.P3109.RealRounding.nearestEven_natCast (n : ℕ) : nearestEven ↑n = n

The real RNITE formula preserves natural numbers.

theorem FloatLib.Floats.Formats.P3109.RealRounding.le_nearestEven_iff (value : ℝ) (boundary : ℕ) (_hb : 0 < boundary) (hv : 0 ≤ value) : boundary ≤ nearestEven value ↔ ↑boundary - 1 / 2 < value ∨ value = ↑boundary - 1 / 2 ∧ boundary % 2 = 0

Reaching a positive integer by nearest-even rounding is decided at its lower halfway point. At that point it is the parity of the upper integer that decides the tie.

theorem FloatLib.Floats.Formats.P3109.RealRounding.floor_selection_iff (root : ℝ) (lower scale random : ℕ) (hscale : 0 < scale) (hrandom : random < scale) (hroot : ↑lower ≤ root) : scale ≤ ⌊(root - ↑lower) * ↑scale⌋₊ + random ↔ ↑(lower * scale + (scale - random)) / ↑scale ≤ root

Floor-based stochastic selection is a comparison against an exact rational threshold.

theorem FloatLib.Floats.Formats.P3109.RealRounding.nearestEven_selection_iff (root : ℝ) (lower scale random : ℕ) (hscale : 0 < scale) (hrandom : random < scale) (hroot : ↑lower ≤ root) : scale ≤ nearestEven ((root - ↑lower) * ↑scale) + random ↔ ↑(lower * (2 * scale) + (2 * (scale - random) - 1)) / (2 * ↑scale) < root ∨ root = ↑(lower * (2 * scale) + (2 * (scale - random) - 1)) / (2 * ↑scale) ∧ (scale - random) % 2 = 0

Nearest-even stochastic selection includes its halfway point exactly for an even boundary.