Scaling accuracy and cohort independence of exponent queries

The accuracy bounds use the delivered rational value and the public overflow flag. Exact cohort selection also applies when the original shifted quantum is outside the format range but another member of its cohort is representable.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scaleB_quantum_le_of_no_overflow (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) (hfinite : (scaleB f mode (Datum.finite s c q) n).status.overflow = false) : (roundedPair f mode s (↑c * 10 ^ (q + n))).2 ≤ f.maxQuantum

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scaleB_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (s : Bool) (c : ℕ) (q n : ℤ) (hfinite : (scaleB f mode (Datum.finite s c q) n).status.overflow = false) : ∃ (v : ℚ), (scaleB f mode (Datum.finite s c q) n).value.toRat? = some v ∧ |v - Datum.finiteValue s c q * 10 ^ n| ≤ 10 ^ roundingQuantum f (↑c * 10 ^ (q + n)) / 2

Both nearest directions deliver at most half a unit of error on the selected grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scaleB_error_lt_one (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) (hfinite : (scaleB f mode (Datum.finite s c q) n).status.overflow = false) : ∃ (v : ℚ), (scaleB f mode (Datum.finite s c q) n).value.toRat? = some v ∧ |v - Datum.finiteValue s c q * 10 ^ n| < 10 ^ roundingQuantum f (↑c * 10 ^ (q + n))

Every rounding direction delivers an error smaller than one selected grid unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scaleB_towardPositive_le (f : Format) (s : Bool) (c : ℕ) (q n : ℤ) (hfinite : (scaleB f RoundingMode.towardPositive (Datum.finite s c q) n).status.overflow = false) : ∃ (v : ℚ), (scaleB f RoundingMode.towardPositive (Datum.finite s c q) n).value.toRat? = some v ∧ Datum.finiteValue s c q * 10 ^ n ≤ v

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scaleB_towardNegative_le (f : Format) (s : Bool) (c : ℕ) (q n : ℤ) (hfinite : (scaleB f RoundingMode.towardNegative (Datum.finite s c q) n).status.overflow = false) : ∃ (v : ℚ), (scaleB f RoundingMode.towardNegative (Datum.finite s c q) n).value.toRat? = some v ∧ v ≤ Datum.finiteValue s c q * 10 ^ n

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scaleB_exact_status_of_representable (f : Format) (mode : RoundingMode) (s : Bool) (c e : ℕ) (q n t : ℤ) (he : Datum.Valid f (Datum.finite s e t)) (hv : ↑c * 10 ^ (q + n) = ↑e * 10 ^ t) : (scaleB f mode (Datum.finite s c q) n).status = { }

Exactness does not require the source's shifted representation itself to be in range.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scaleB_quantum_closest_of_representable (f : Format) (mode : RoundingMode) (s : Bool) (c e : ℕ) (q n t : ℤ) (he : Datum.Valid f (Datum.finite s e t)) (hv : ↑c * 10 ^ (q + n) = ↑e * 10 ^ t) (d : ℕ) (r : ℤ) (hout : (scaleB f mode (Datum.finite s c q) n).value = Datum.finite s d r) (a : ℕ) (b : ℤ) (ha : Datum.Valid f (Datum.finite s a b)) (hab : ↑c * 10 ^ (q + n) = ↑a * 10 ^ b) : |q + n - r| ≤ |q + n - b|

Representable exact results choose the cohort member nearest the preferred shifted quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.scaleB_inexact_quantum_minimal (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q n : ℤ) (hinexact : (scaleB f mode (Datum.finite s c q) n).status.inexact = true) (d : ℕ) (r : ℤ) (hout : (scaleB f mode (Datum.finite s c q) n).value = Datum.finite s d r) (a : ℕ) (b : ℤ) (ha : Datum.Valid f (Datum.finite s a b)) (he : ↑d * 10 ^ r = ↑a * 10 ^ b) : r ≤ b

Inexact finite results, including directed overflow deliveries, use the least quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.logB_eq_of_equal_magnitude (f g : Format) (s t : Bool) (c d : ℕ) (q r : ℤ) (hc : c ≠ 0) (hd : d ≠ 0) (he : ↑c * 10 ^ q = ↑d * 10 ^ r) : (logB f (Datum.finite s c q)).value = (logB g (Datum.finite t d r)).value

Equal nonzero magnitudes have the same radix exponent, irrespective of cohort or sign.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.logB_zero (f : Format) (s : Bool) (q : ℤ) : logB f (Datum.finite s 0 q) = { value := -logBSentinel f, status := { invalid := true } }

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.logB_infinity (f : Format) (s : Bool) : logB f (Datum.infinity s) = { value := logBSentinel f, status := { invalid := true } }

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.logB_nan (f : Format) (s t : Bool) (p : ℕ) : logB f (Datum.nan s t p) = { value := logBSentinel f, status := { invalid := true } }