Rounding Into A Generic Format #

Rounding any real with a valid integer-rounding rule produces a value in the selected generic format. The proof separates inputs whose magnitude is at most the selected exponent from those above it.

source

theorem FloatLib.Floats.Formats.Flocq.validExp_small {fexp : ℤ → ℤ} [ValidExp fexp] {e : ℤ} (h : e ≤ fexp e) :

fexp (fexp e + 1) ≤ fexp e

The Valid_exp consequence used when the input magnitude is below the selected exponent.

source

theorem FloatLib.Floats.Formats.Flocq.validExp_large {fexp : ℤ → ℤ} [ValidExp fexp] {e : ℤ} (h : fexp e < e) :

fexp (e + 1) ≤ e

The Valid_exp consequence used when the selected exponent is below the input magnitude.

source

theorem FloatLib.Floats.Formats.Flocq.round_pos_small_cases {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) (hx : 0 < x) (hsmall : magnitude β x ≤ fexp (magnitude β x)) :

round rnd x = 0 ∨ round rnd x = bpow β (fexp (magnitude β x))

Positive inputs in the small-magnitude regime round either to zero or to one radix power.

source

theorem FloatLib.Floats.Formats.Flocq.generic_format_round_pos_small {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) (hx : 0 < x) (hsmall : magnitude β x ≤ fexp (magnitude β x)) :

genericFormat β fexp (round rnd x)

Rounding in the small-magnitude regime produces a generic-format value.

source

theorem FloatLib.Floats.Formats.Flocq.round_pos_large_bounds_and_generic {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) (hx : 0 < x) (hlarge : fexp (magnitude β x) < magnitude β x) :

(bpow β (magnitude β x - 1) ≤ round rnd x ∧ round rnd x ≤ bpow β (magnitude β x)) ∧ genericFormat β fexp (round rnd x)

In the large-magnitude regime, the rounded value lies between the endpoints of the input magnitude bin, including the upper endpoint, and belongs to the generic format.

source