Floating-point rounding

25 fully proved

Rounding to an integer

DefinitionNearest-integer rounding with ties to even#✓fully proved

For \(m\) in a linearly ordered field \(K\) with a floor function, \(\operatorname{rne}(m)\) is the integer \(\lfloor m \rfloor\) if \(m - \lfloor m \rfloor < 1/2\), the integer \(\lfloor m \rfloor + 1\) if \(m - \lfloor m \rfloor > 1/2\), and, when \(m - \lfloor m \rfloor = 1/2\), whichever of \(\lfloor m \rfloor\) and \(\lfloor m \rfloor + 1\) is even.

def rne (m : K) : ℤ :=
  if m - ⌊m⌋ < 1 / 2 then ⌊m⌋
  else if 1 / 2 < m - ⌊m⌋ then ⌊m⌋ + 1
  else if Even ⌊m⌋ then ⌊m⌋ else ⌊m⌋ + 1

Used by 14

Used byThe relative error bound · Round to nearest for floating-point numbers · Bound on the rounded significand · Round to nearest integer · Rounding to the nearest integer is within one half · Rounding error bounded by the distances to neighbouring integers · Ties to even for floating-point rounding · Ties to even for the nearest integer · Round to nearest, ties to even · The rounding error at the scale of the last place · Rounding gives a floating-point number · In the normal range, rounding stays in the format · Rounding to nearest preserves integer lower bounds · Rounding to nearest preserves integer upper bounds

TheoremRounding error bounded by the distances to neighbouring integers#✓fully proved

Let \(K\) be a linearly ordered field with a floor function. For every \(m \in K\), the integer \(\operatorname{rne}(m)\) obtained by rounding \(m\) to the nearest integer, ties to even, satisfies \(|\operatorname{rne}(m) - m| \le m - \lfloor m \rfloor\) and \(|\operatorname{rne}(m) - m| \le \lfloor m \rfloor + 1 - m\).

theorem abs_rne_sub_le_min (m : K) :
    |(rne m : K) - m| ≤ m - ⌊m⌋ ∧ |(rne m : K) - m| ≤ ⌊m⌋ + 1 - m

Uses 1 · Used by 2

Statement usesNearest-integer rounding with ties to even

Used byRound to nearest integer · Rounding to the nearest integer is within one half

TheoremRound to nearest integer#✓fully proved

Let \(K\) be a linearly ordered field with a floor function. For every \(m \in K\) and every integer \(k\), the integer \(\operatorname{rne}(m)\) obtained by rounding \(m\) to the nearest integer, ties to even, satisfies \(|\operatorname{rne}(m) - m| \le |k - m|\): no integer is closer to \(m\) than \(\operatorname{rne}(m)\).

theorem abs_rne_sub_le (m : K) (k : ℤ) : |(rne m : K) - m| ≤ |(k : K) - m|

Uses 2 · Used by 5

Statement usesNearest-integer rounding with ties to even

Proof usesRounding error bounded by the distances to neighbouring integers

Used byThe relative error bound · Round to nearest for floating-point numbers · Rounding gives a floating-point number · Rounding to nearest preserves integer lower bounds · Rounding to nearest preserves integer upper bounds

TheoremRounding to the nearest integer is within one half#✓fully proved

Let \(K\) be a linearly ordered field with a floor function. For every \(m \in K\), the integer \(\operatorname{rne}(m)\) obtained by rounding \(m\) to the nearest integer, ties to even, satisfies \(|\operatorname{rne}(m) - m| \le 1/2\).

theorem abs_rne_sub_le_half (m : K) : |(rne m : K) - m| ≤ 1 / 2

Uses 2 · Used by 1

Statement usesNearest-integer rounding with ties to even

Proof usesRounding error bounded by the distances to neighbouring integers

Used byThe relative error bound

TheoremTies to even for the nearest integer#✓fully proved

Let \(K\) be a linearly ordered field with a floor function, let \(m \in K\), and let \(\operatorname{rne}(m)\) be the integer obtained by rounding \(m\) to the nearest integer, ties to even. If \(|\operatorname{rne}(m) - m| = 1/2\), that is, \(m\) is halfway between two consecutive integers, then \(\operatorname{rne}(m)\) is even.

theorem even_rne_of_abs_sub_eq_half {m : K} (h : |(rne m : K) - m| = 1 / 2) : Even (rne m)

Uses 1 · Used by 1

Statement usesNearest-integer rounding with ties to even

Used byTies to even for floating-point rounding

TheoremRounding to nearest preserves integer upper bounds#✓fully proved

Let \(K\) be a linearly ordered field with a floor function, let \(m \in K\) and let \(k\) be an integer. If \(m \le k\), then \(\operatorname{rne}(m) \le k\), where \(\operatorname{rne}(m)\) is \(m\) rounded to the nearest integer with ties to even.

theorem rne_le_of_le {m : K} {k : ℤ} (h : m ≤ k) : rne m ≤ k

Uses 2 · Used by 2

Statement usesNearest-integer rounding with ties to even

Proof usesRound to nearest integer

Used byBound on the rounded significand · In the normal range, rounding stays in the format

TheoremRounding to nearest preserves integer lower bounds#✓fully proved

Let \(K\) be a linearly ordered field with a floor function, let \(m \in K\) and let \(k\) be an integer. If \(k \le m\), then \(k \le \operatorname{rne}(m)\), where \(\operatorname{rne}(m)\) is \(m\) rounded to the nearest integer with ties to even.

theorem le_rne_of_le {m : K} {k : ℤ} (h : (k : K) ≤ m) : k ≤ rne m

Uses 2 · Used by 2

Statement usesNearest-integer rounding with ties to even

Proof usesRound to nearest integer

Used byBound on the rounded significand · In the normal range, rounding stays in the format

Floating-point numbers and rounding

DefinitionBinary floating-point numbers#✓fully proved

For a natural number \(p\), an element \(x\) of a linearly ordered field with a floor function is a binary floating-point number with a \(p\)-bit significand and unbounded exponent when \(x = m \cdot 2^e\) for some integers \(m\) and \(e\) with \(|m| < 2^p\).

def IsFloat (x : K) : Prop := ∃ m e : ℤ, |m| < 2 ^ p ∧ x = m * 2 ^ e

Used by 6

Used byRound to nearest for floating-point numbers · Round to nearest in a bounded format · Floating-point numbers round to themselves · Floating-point subtraction is exact under Sterbenz's condition · Rounding gives a floating-point number · Sterbenz's lemma

DefinitionFloating-point numbers of a bounded format#✓fully proved

For a natural number \(p\) and integers \(q_{\min}\) and \(q_{\max}\), an element \(x\) of a linearly ordered field with a floor function is a number of the binary format with \(p\)-bit significands and last-place exponents in \([q_{\min}, q_{\max}]\) when \(x = m \cdot 2^e\) for some integers \(m\) and \(e\) with \(|m| < 2^p\) and \(q_{\min} \le e \le q_{\max}\). These are zero, the subnormal numbers and the normal numbers of the format.

In IEEE 754 terms, \(q_{\min} = e_{\min} - p + 1\) and \(q_{\max} = e_{\max} - p + 1\).

def IsFloatIn (qmin qmax : ℤ) (x : K) : Prop :=
  ∃ m e : ℤ, |m| < 2 ^ p ∧ qmin ≤ e ∧ e ≤ qmax ∧ x = m * 2 ^ e

Used by 3

Used byRound to nearest in a bounded format · In the normal range, rounding stays in the format · Sterbenz's lemma in a bounded format

DefinitionExponent of the last place#✓fully proved

For a natural number \(p\) (the significand length) and \(x\) in a linearly ordered field \(K\) with a floor function, the exponent of the last place of \(x\) is the integer \(\lfloor \log_2 |x| \rfloor - (p - 1)\). Here \(\lfloor \log_2 |x| \rfloor\) is the integer logarithm: the largest integer \(n\) with \(2^n \le |x|\) when \(x \ne 0\), and \(0\) when \(x = 0\).

def ulpExp (x : K) : ℤ := Int.log 2 |x| - ((p : ℤ) - 1)

Used by 9

Used byThe relative error bound · Round to nearest for floating-point numbers · Bound on the rounded significand · Ties to even for floating-point rounding · Round to nearest, ties to even · The rounding error at the scale of the last place · Rounding gives a floating-point number · In the normal range, rounding stays in the format · Bounds on the scaled significand

DefinitionRound to nearest, ties to even#✓fully proved

For a natural number \(p\) and an element \(x\) of a linearly ordered field with a floor function, let \(e\) be the exponent of the last place of \(x\) at precision \(p\), and let \(\operatorname{rne}\) round to the nearest integer with ties to the even one. The rounding of \(x\) to nearest, ties to even, is \(\mathrm{fl}_p(x) = \operatorname{rne}(x / 2^e) \cdot 2^e\): scale \(x\) so that its last place is the units digit, round to the nearest integer with ties to even, and scale back.

def fl (x : K) : K := rne (x / 2 ^ ulpExp p x) * 2 ^ ulpExp p x

Uses 2 · Used by 9

Statement usesNearest-integer rounding with ties to even · Exponent of the last place

Used byThe relative error bound · Round to nearest for floating-point numbers · Round to nearest in a bounded format · Ties to even for floating-point rounding · Floating-point numbers round to themselves · The rounding error at the scale of the last place · Floating-point subtraction is exact under Sterbenz's condition · Rounding gives a floating-point number · In the normal range, rounding stays in the format

TheoremBounds on the scaled significand#✓fully proved

Let \(K\) be a linearly ordered field with a floor function, let \(p \ge 1\) be a natural number and let \(x \in K\) be nonzero. Let \(e = \lfloor \log_2 |x| \rfloor - (p - 1)\) be the exponent of the last place of \(x\) for \(p\)-bit significands. Then \(2^{p-1} \le |x / 2^e|\) and \(|x / 2^e| < 2^p\).

theorem scaled_bounds (hp : 1 ≤ p) {x : K} (hx : x ≠ 0) :
    (2 : K) ^ (p - 1) ≤ |x / 2 ^ ulpExp p x| ∧ |x / 2 ^ ulpExp p x| < 2 ^ p

Uses 1 · Used by 2

Statement usesExponent of the last place

Used byRound to nearest for floating-point numbers · Bound on the rounded significand

TheoremThe rounding error at the scale of the last place#✓fully proved

Let \(x\) be an element of a linearly ordered field with a floor function, let \(p\) be a natural number, and let \(e\) be the exponent of the last place of \(x\) at precision \(p\). Writing \(\operatorname{rne}\) for rounding to the nearest integer with ties to even, the rounding \(\mathrm{fl}_p(x)\) of \(x\) to nearest, ties to even, at precision \(p\) has the error \(\mathrm{fl}_p(x) - x = (\operatorname{rne}(x / 2^e) - x / 2^e) \cdot 2^e\).

theorem fl_sub_eq (x : K) :
    fl p x - x = ((rne (x / 2 ^ ulpExp p x) : K) - x / 2 ^ ulpExp p x) * 2 ^ ulpExp p x

Uses 3 · Used by 3

Statement usesRound to nearest, ties to even · Nearest-integer rounding with ties to even · Exponent of the last place

Used byThe relative error bound · Round to nearest for floating-point numbers · Ties to even for floating-point rounding

TheoremThe relative error bound#✓fully proved

Let \(K\) be a linearly ordered field with a floor function and let \(p\) be a natural number. For every \(x \in K\), the rounding \(\mathrm{fl}(x)\) of \(x\) to nearest, ties to even, with \(p\)-bit significands satisfies \(|\mathrm{fl}(x) - x| \le u\,|x|\), where \(u = 2^{-p}\) is the unit roundoff.

The exponent is unbounded, so the bound holds for every \(x\), with no underflow or overflow.

theorem abs_fl_sub_le (x : K) : |fl p x - x| ≤ 2 ^ (-(p : ℤ)) * |x|

Uses 6

Statement usesRound to nearest, ties to even

Proof usesRound to nearest integer · Rounding to the nearest integer is within one half · The rounding error at the scale of the last place · Nearest-integer rounding with ties to even · Exponent of the last place

TheoremRound to nearest for floating-point numbers#✓fully proved

Let \(K\) be a linearly ordered field with a floor function and let \(p \ge 1\). For every \(x \in K\) and every binary floating-point number \(f \in K\) with a \(p\)-bit significand (and unbounded exponent), the rounding \(\mathrm{fl}(x)\) of \(x\) to nearest, ties to even, with \(p\)-bit significands satisfies \(|\mathrm{fl}(x) - x| \le |f - x|\): no floating-point number is closer to \(x\) than \(\mathrm{fl}(x)\).

theorem abs_fl_sub_le_of_isFloat (hp : 1 ≤ p) (x : K) {f : K} (hf : IsFloat p f) :
    |fl p x - x| ≤ |f - x|

Uses 7 · Used by 2

Statement usesBinary floating-point numbers · Round to nearest, ties to even

Proof usesRound to nearest integer · The rounding error at the scale of the last place · Nearest-integer rounding with ties to even · Bounds on the scaled significand · Exponent of the last place

Used byRound to nearest in a bounded format · Floating-point numbers round to themselves

TheoremFloating-point numbers round to themselves#✓fully proved

Let \(p \ge 1\) and let \(x\) be an element of a linearly ordered field with a floor function. If \(x\) is a binary floating-point number with a \(p\)-bit significand, that is, \(x = m \cdot 2^e\) for some integers \(m\) and \(e\) with \(|m| < 2^p\), then rounding \(x\) to nearest, ties to even, at precision \(p\) returns \(x\): \(\mathrm{fl}_p(x) = x\).

theorem fl_eq_self (hp : 1 ≤ p) {x : K} (hx : IsFloat p x) : fl p x = x

Uses 3 · Used by 1

Statement usesBinary floating-point numbers · Round to nearest, ties to even

Proof usesRound to nearest for floating-point numbers

Used byFloating-point subtraction is exact under Sterbenz's condition

TheoremTies to even for floating-point rounding#✓fully proved

Let \(K\) be a linearly ordered field with a floor function, let \(p\) be a natural number, let \(x \in K\), and let \(e\) be the exponent of the last place of \(x\), which is \(\lfloor \log_2 |x| \rfloor - (p - 1)\) for \(x \ne 0\). If the rounding \(\mathrm{fl}(x)\) of \(x\) to nearest, ties to even, with \(p\)-bit significands satisfies \(|\mathrm{fl}(x) - x| = 2^e / 2\), then the integer \(\operatorname{rne}(x / 2^e)\), the significand of \(\mathrm{fl}(x)\) at the last place of \(x\), is even.

theorem even_of_abs_fl_sub_eq {x : K} (h : |fl p x - x| = 2 ^ ulpExp p x / 2) :
    Even (rne (x / 2 ^ ulpExp p x))

Uses 5

Statement usesRound to nearest, ties to even · Nearest-integer rounding with ties to even · Exponent of the last place

Proof usesTies to even for the nearest integer · The rounding error at the scale of the last place

TheoremBound on the rounded significand#✓fully proved

Let \(K\) be a linearly ordered field with a floor function, let \(p \ge 1\), let \(x \in K\) be nonzero, and let \(e = \lfloor \log_2 |x| \rfloor - (p - 1)\) be the exponent of the last place of \(x\). Then \(|\operatorname{rne}(x / 2^e)| \le 2^p\), where \(\operatorname{rne}\) rounds to the nearest integer, ties to even.

Since \(|x / 2^e| < 2^p\), the value \(2^p\) occurs only when rounding carries into the next binade.

theorem abs_rne_le (hp : 1 ≤ p) {x : K} (hx : x ≠ 0) :
    |rne (x / 2 ^ ulpExp p x)| ≤ 2 ^ p

Uses 5 · Used by 2

Statement usesNearest-integer rounding with ties to even · Exponent of the last place

Proof usesRounding to nearest preserves integer lower bounds · Rounding to nearest preserves integer upper bounds · Bounds on the scaled significand

Used byRounding gives a floating-point number · In the normal range, rounding stays in the format

TheoremRounding gives a floating-point number#✓fully proved

Let \(p \ge 1\). For every element \(x\) of a linearly ordered field with a floor function, the rounding \(\mathrm{fl}_p(x)\) of \(x\) to nearest, ties to even, is a binary floating-point number with a \(p\)-bit significand: \(\mathrm{fl}_p(x) = m \cdot 2^e\) for some integers \(m\) and \(e\) with \(|m| < 2^p\).

theorem isFloat_fl (hp : 1 ≤ p) (x : K) : IsFloat p (fl p x)

Uses 6

Statement usesBinary floating-point numbers · Round to nearest, ties to even

Proof usesBound on the rounded significand · Round to nearest integer · Nearest-integer rounding with ties to even · Exponent of the last place

The normal range of a bounded format

TheoremIn the normal range, rounding stays in the format#✓fully proved

Let \(p \ge 1\), let \(q_{\min}\) and \(q_{\max}\) be integers, and let \(x\) be an element of a linearly ordered field with a floor function. If \(2^{q_{\min} + p - 1} \le |x|\) (\(x\) is at least the smallest normal number) and \(|x| \le (2^p - 1) \cdot 2^{q_{\max}}\) (\(x\) is at most the largest finite number), then the rounding \(\mathrm{fl}_p(x)\) of \(x\) to nearest, ties to even, is a number of the binary format with \(p\)-bit significands whose last place has exponent in \([q_{\min}, q_{\max}]\).

Since \(\mathrm{fl}_p(x)\) is also a nearest number of the format to \(x\), with relative error at most \(2^{-p}\), rounding in the format in the normal range is the nearest-even rounding.

theorem isFloatIn_fl (hp : 1 ≤ p) {qmin qmax : ℤ} {x : K}
    (hlo : (2 : K) ^ (qmin + ((p : ℤ) - 1)) ≤ |x|) (hhi : |x| ≤ (2 ^ p - 1) * 2 ^ qmax) :
    IsFloatIn p qmin qmax (fl p x)

Uses 7

Statement usesFloating-point numbers of a bounded format · Round to nearest, ties to even

Proof usesBound on the rounded significand · Rounding to nearest preserves integer lower bounds · Nearest-integer rounding with ties to even · Rounding to nearest preserves integer upper bounds · Exponent of the last place

TheoremRound to nearest in a bounded format#✓fully proved

Let \(K\) be a linearly ordered field with a floor function, let \(p \ge 1\), and let \(q_{\min}\) and \(q_{\max}\) be integers. For every \(x \in K\) and every number \(f\) of the binary format with \(p\)-bit significands and last-place exponents in \([q_{\min}, q_{\max}]\), the rounding \(\mathrm{fl}(x)\) of \(x\) to nearest, ties to even, with \(p\)-bit significands satisfies \(|\mathrm{fl}(x) - x| \le |f - x|\).

theorem abs_fl_sub_le_of_isFloatIn (hp : 1 ≤ p) (x : K) {qmin qmax : ℤ} {f : K}
    (hf : IsFloatIn p qmin qmax f) : |fl p x - x| ≤ |f - x|

Uses 4

Statement usesFloating-point numbers of a bounded format · Round to nearest, ties to even

Proof usesBinary floating-point numbers · Round to nearest for floating-point numbers

Sterbenz's lemma

TheoremThe difference of floating-point numbers within a factor of two#✓fully proved

Let \(K\) be a linearly ordered field with a floor function and let \(p\) be a natural number. Let \(x, y \in K\) and let \(m_x, m_y, e_x, e_y\) be integers with \(|m_x| < 2^p\), \(|m_y| < 2^p\), \(x = m_x 2^{e_x}\) and \(y = m_y 2^{e_y}\). If \(y / 2 \le x \le 2y\), then there is an integer \(k\) with \(|k| < 2^p\) and \(x - y = k \cdot 2^{\min(e_x, e_y)}\).

theorem exists_sub_eq_of_le {x y : K} {mx my ex ey : ℤ} (hmx : |mx| < 2 ^ p)
    (hmy : |my| < 2 ^ p) (hx : x = mx * 2 ^ ex) (hy : y = my * 2 ^ ey) (h₁ : y / 2 ≤ x)
    (h₂ : x ≤ 2 * y) : ∃ k : ℤ, |k| < 2 ^ p ∧ x - y = k * 2 ^ min ex ey

Used by 2

Used bySterbenz's lemma in a bounded format · Sterbenz's lemma

TheoremSterbenz's lemma#✓fully proved

Let \(p\) be a natural number and let \(x\) and \(y\) be binary floating-point numbers with \(p\)-bit significands (and unbounded exponent) in a linearly ordered field with a floor function. If \(y / 2 \le x \le 2y\), then \(x - y\) is also a binary floating-point number with a \(p\)-bit significand.

theorem isFloat_sub {x y : K} (hx : IsFloat p x) (hy : IsFloat p y) (h₁ : y / 2 ≤ x)
    (h₂ : x ≤ 2 * y) : IsFloat p (x - y)

Uses 2 · Used by 1

Statement usesBinary floating-point numbers

Proof usesThe difference of floating-point numbers within a factor of two

Used byFloating-point subtraction is exact under Sterbenz's condition

TheoremSterbenz's lemma in a bounded format#✓fully proved

Let \(p\) be a natural number, let \(q_{\min}\) and \(q_{\max}\) be integers, and let \(x\) and \(y\) be numbers of the binary format with \(p\)-bit significands whose last place has exponent in \([q_{\min}, q_{\max}]\) (subnormal numbers included), in a linearly ordered field with a floor function. If \(y / 2 \le x \le 2y\), then \(x - y\) is also a number of this format.

theorem isFloatIn_sub {qmin qmax : ℤ} {x y : K} (hx : IsFloatIn p qmin qmax x)
    (hy : IsFloatIn p qmin qmax y) (h₁ : y / 2 ≤ x) (h₂ : x ≤ 2 * y) :
    IsFloatIn p qmin qmax (x - y)

Uses 2

Statement usesFloating-point numbers of a bounded format

Proof usesThe difference of floating-point numbers within a factor of two

TheoremFloating-point subtraction is exact under Sterbenz's condition#✓fully proved

Let \(p \ge 1\) and let \(x\) and \(y\) be binary floating-point numbers with \(p\)-bit significands in a linearly ordered field with a floor function. If \(y / 2 \le x \le 2y\), then rounding \(x - y\) to nearest, ties to even, at precision \(p\) returns it exactly: \(\mathrm{fl}_p(x - y) = x - y\).

theorem fl_sub_eq_sub (hp : 1 ≤ p) {x y : K} (hx : IsFloat p x) (hy : IsFloat p y)
    (h₁ : y / 2 ≤ x) (h₂ : x ≤ 2 * y) : fl p (x - y) = x - y

Uses 4

Statement usesBinary floating-point numbers · Round to nearest, ties to even

Proof usesFloating-point numbers round to themselves · Sterbenz's lemma

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.