The rounding of the doubles of the model

Ratpoints.Double.ofRatio and Ratpoints.Double.ofDyadic, the doubles nearest to ±n / d and to ±m 2 ^ e, which strtod and the conversions of the model compute, are never a NaN (Ratpoints.Double.isNaN_ofRatio, Ratpoints.Double.isNaN_ofDyadic), and a finite result is a faithful rounding: the number lies strictly between the neighbours nextDown x and nextUp x of the result x (Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofRatio, Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofDyadic), so that no double other than x lies between x and the number. This is what the program needs of strtod: the end of a search interval that it moves outward to a double from the double that strtod reads lands on the nearest double on its side. The successor of the double of a height bound 1 ≤ H < 2 ^ 63 is finite and above H (Ratpoints.Double.isFinite_ofInt64_and_lt_toRat_nextUp), which gives the bound h of the default search interval [-h, h] (Ratpoints.Double.isFinite_and_le_toRat_ofInt64_nextUp).

The proof goes through the significand M and the exponent q of its last place that both functions round to, M 2 ^ q within half a unit 2 ^ (q - 1) of the number (Ratpoints.Double.ofRatio_rounding, Ratpoints.Double.ofDyadic_rounding), and the last step that both take, the carry at 2 ^ 53 and the bits of the double (Ratpoints.Double.ofSignificand and Ratpoints.Double.assemble of the model, the fields of the result by Ratpoints.Double.fields_assemble), whose neighbours have the values of the magnitudes next to that of the result, in units of 2 ^ (-1074) (Ratpoints.Double.magnitudeUnits_fields_succ, Ratpoints.Double.lt_nextUp_and_nextDown_lt).

Main definitions

• Ratpoints.Double.roundDiv, Ratpoints.Double.ratioExponent, Ratpoints.Double.ratioPair, Ratpoints.Double.ratioLast: the rounding of a quotient and the exponents of Ratpoints.Double.ofRatio.

Main statements

• Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofRatio, Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofDyadic: the faithful rounding.
• Ratpoints.Double.isNaN_ofRatio, Ratpoints.Double.isNaN_ofDyadic: no NaN.
• Ratpoints.Double.isFinite_and_le_toRat_ofInt64_nextUp: the double of 1 ≤ H < 2 ^ 63, moved up to the next double when it is below 2 ^ 63 and its conversion to a long below H, is finite and at least H.

The neighbours of a finite double

theorem Ratpoints.Double.magnitudeUnits_fields_succ {E F : ℕ} (hF : F < 2 ^ 52) : magnitudeUnits (E * 2 ^ 52 + F + 1) = magnitudeUnits (E * 2 ^ 52 + F) + 2 ^ (max E 1 - 1)

The units of 2 ^ (-1074) between the values of the consecutive magnitudes with the exponent field E and the fraction F and the next: 2 ^ (E - 1) for E ≥ 1, and 1 for E = 0, also where the fraction carries into the exponent.

theorem Ratpoints.Double.valueOfOrderValue_maxOrderValue : valueOfOrderValue ↑maxOrderValue = ⊤

theorem Ratpoints.Double.valueOfOrderValue_neg_maxOrderValue : valueOfOrderValue (-↑maxOrderValue) = ⊥

theorem Ratpoints.Double.expField_mul_add_fracField_lt {x : Double} (hf : x.isFinite = true) : x.expField * 2 ^ 52 + x.fracField < maxOrderValue

theorem Ratpoints.Double.ne_huge_of_isFinite {x : Double} (hf : x.isFinite = true) : x.bits ≠ huge.bits ∧ x.bits ≠ huge.neg.bits

theorem Ratpoints.Double.lt_valueOfOrderValue_add_one {k : ℕ} {v : ℚ} (hk : k < maxOrderValue) (h : v < ↑(magnitudeUnits (k + 1)) * 2 ^ (-1074)) : WithBotTop.coe v < valueOfOrderValue (↑k + 1)

theorem Ratpoints.Double.valueOfOrderValue_neg_sub_one_lt {k : ℕ} {v : ℚ} (hk : k < maxOrderValue) (h : v < ↑(magnitudeUnits (k + 1)) * 2 ^ (-1074)) : valueOfOrderValue (-↑k - 1) < WithBotTop.coe (-v)

theorem Ratpoints.Double.valueOfOrderValue_sub_one_lt {k : ℕ} {v : ℚ} (hk : k < maxOrderValue) (hv : 0 < v) (h : k ≠ 0 → ↑(magnitudeUnits (k - 1)) * 2 ^ (-1074) < v) : valueOfOrderValue (↑k - 1) < WithBotTop.coe v

theorem Ratpoints.Double.lt_valueOfOrderValue_neg_add_one {k : ℕ} {v : ℚ} (hk : k < maxOrderValue) (hv : 0 < v) (h : k ≠ 0 → ↑(magnitudeUnits (k - 1)) * 2 ^ (-1074) < v) : WithBotTop.coe (-v) < valueOfOrderValue (-↑k + 1)

theorem Ratpoints.Double.lt_nextUp_and_nextDown_lt {x : Double} {k : ℕ} {v : ℚ} (hf : x.isFinite = true) (hkx : x.expField * 2 ^ 52 + x.fracField = k) (hv : 0 < v) (hup : v < ↑(magnitudeUnits (k + 1)) * 2 ^ (-1074)) (hdown : k ≠ 0 → ↑(magnitudeUnits (k - 1)) * 2 ^ (-1074) < v) : WithBotTop.coe (if x.signBit = true then -v else v) < doubleValue x.nextUp.bits ∧ doubleValue x.nextDown.bits < WithBotTop.coe (if x.signBit = true then -v else v)

A positive rational number v strictly between the values of the magnitudes k - 1 and k + 1 next to the magnitude k of a finite double x, in units of 2 ^ (-1074), lies, with the sign of x, strictly between the values of nextDown x and nextUp x.

Finite, infinite and neighbouring doubles

theorem Ratpoints.Double.isFinite_iff_natAbs_orderValue_lt {x : Double} (hx : x.isNaN = false) : x.isFinite = true ↔ x.orderValue.natAbs < maxOrderValue

theorem Ratpoints.Double.isFinite_nextUp_of_expField_lt {x : Double} (hf : x.isFinite = true) (hE : x.expField < 2046) : x.nextUp.isFinite = true

theorem Ratpoints.Double.isFinite_nextDown_or_doubleValue_eq_bot {x : Double} (hf : x.isFinite = true) : x.nextDown.isFinite = true ∨ doubleValue x.nextDown.bits = ⊥

theorem Ratpoints.Double.isFinite_nextUp_or_doubleValue_eq_top {x : Double} (hf : x.isFinite = true) : x.nextUp.isFinite = true ∨ doubleValue x.nextUp.bits = ⊤

theorem Ratpoints.Double.le_of_lt_nextUp {x y : Double} (hx : x.isNaN = false) (hy : y.isNaN = false) (hi : x.bits ≠ huge.bits) (h : doubleValue y.bits < doubleValue x.nextUp.bits) : doubleValue y.bits ≤ doubleValue x.bits

theorem Ratpoints.Double.le_nextDown_of_doubleValue_lt {x y : Double} (hx : x.isNaN = false) (hy : y.isNaN = false) (hi : x.bits ≠ huge.neg.bits) (h : doubleValue y.bits < doubleValue x.bits) : doubleValue y.bits ≤ doubleValue x.nextDown.bits

theorem Ratpoints.Double.doubleValue_of_isInf {x : Double} (hi : x.isInf = true) : doubleValue x.bits = if x.signBit = true then ⊥ else ⊤

theorem Ratpoints.Double.zero_lt_of_isInf {x : Double} (hi : x.isInf = true) : zero.lt x = !x.signBit

theorem Ratpoints.Double.isFinite_of_isInf_eq_false {x : Double} (hx : x.isNaN = false) (hi : x.isInf = false) : x.isFinite = true

theorem Ratpoints.Double.isNaN_huge : huge.isNaN = false

theorem Ratpoints.Double.isNaN_huge_neg : huge.neg.isNaN = false

theorem Ratpoints.Double.doubleValue_huge : doubleValue huge.bits = ⊤

theorem Ratpoints.Double.doubleValue_huge_neg : doubleValue huge.neg.bits = ⊥

The last step of ofRatio and ofDyadic

theorem Ratpoints.Double.isNaN_assemble (neg : Bool) {M : ℕ} (q : ℤ) (hM : M < 2 ^ 53) : (assemble neg M q).isNaN = false

theorem Ratpoints.Double.isNaN_ofSignificand (neg : Bool) {M : ℕ} (q : ℤ) (hM : M ≤ 2 ^ 53) : (ofSignificand neg M q).isNaN = false

theorem Ratpoints.Double.isFinite_ofSignificand {neg : Bool} {M : ℕ} {q : ℤ} (hM : M ≤ 2 ^ 53) (hq : q + 1076 < 2046) : (ofSignificand neg M q).isFinite = true ∧ (ofSignificand neg M q).signBit = neg ∧ (ofSignificand neg M q).expField < 2046

The magnitudes next to an assembled double

theorem Ratpoints.Double.magnitudeUnits_of_lt {M : ℕ} (h : M < 2 ^ 52) : magnitudeUnits M = M ∧ magnitudeUnits (M + 1) = M + 1 ∧ magnitudeUnits (M - 1) = M - 1

theorem Ratpoints.Double.magnitudeUnits_normal_mul {M : ℕ} {q : ℤ} (h1 : 2 ^ 52 ≤ M) (h2 : M < 2 ^ 53) (hq : -1074 ≤ q) : ↑(magnitudeUnits ((q + 1075).toNat * 2 ^ 52 + (M - 2 ^ 52))) * 2 ^ (-1074) = ↑M * 2 ^ q

theorem Ratpoints.Double.magnitudeUnits_normal_succ_mul {M : ℕ} {q : ℤ} (h1 : 2 ^ 52 ≤ M) (h2 : M < 2 ^ 53) (hq : -1074 ≤ q) : ↑(magnitudeUnits ((q + 1075).toNat * 2 ^ 52 + (M - 2 ^ 52) + 1)) * 2 ^ (-1074) = (↑M + 1) * 2 ^ q

theorem Ratpoints.Double.magnitudeUnits_mul_of_succ_eq {E F k : ℕ} (hF : F < 2 ^ 52) (hk : E * 2 ^ 52 + F + 1 = k) : ↑(magnitudeUnits (E * 2 ^ 52 + F)) * 2 ^ (-1074) = ↑(magnitudeUnits k) * 2 ^ (-1074) - 2 ^ (↑(max E 1 - 1) - 1074)

theorem Ratpoints.Double.magnitudeUnits_normal_pred_mul {M : ℕ} {q : ℤ} (h1 : 2 ^ 52 ≤ M) (h2 : M < 2 ^ 53) (hq : -1074 ≤ q) : ↑(magnitudeUnits ((q + 1075).toNat * 2 ^ 52 + (M - 2 ^ 52) - 1)) * 2 ^ (-1074) = ↑M * 2 ^ q - if M = 2 ^ 52 ∧ -1074 < q then 2 ^ (q - 1) else 2 ^ q

The value of the magnitude below that of a normal double M 2 ^ q: half a unit 2 ^ q lower at the bottom of a binade (M = 2 ^ 52, above the least exponent), a unit lower otherwise.

theorem Ratpoints.Double.lt_nextUp_and_nextDown_lt_assemble_of_lt {neg : Bool} {M : ℕ} {v : ℚ} (h : M < 2 ^ 52) (hv : 0 < v) (hup : v < (↑M + 1) * 2 ^ (-1074)) (hdown : M ≠ 0 → (↑M - 1) * 2 ^ (-1074) < v) : WithBotTop.coe (if neg = true then -v else v) < doubleValue (assemble neg M (-1074)).nextUp.bits ∧ doubleValue (assemble neg M (-1074)).nextDown.bits < WithBotTop.coe (if neg = true then -v else v)

A subnormal or zero x = ±M 2 ^ (-1074) (M < 2 ^ 52) and a positive v within less than 2 ^ (-1074) of M 2 ^ (-1074): the neighbours of x lie on either side of ±v.

theorem Ratpoints.Double.lt_nextUp_and_nextDown_lt_assemble_of_two_pow_le {neg : Bool} {M : ℕ} {q : ℤ} {v : ℚ} (h1 : 2 ^ 52 ≤ M) (h2 : M < 2 ^ 53) (hq : -1074 ≤ q) (hq' : q + 1075 < 2047) (hv : 0 < v) (hup : v < (↑M + 1) * 2 ^ q) (hdown : (↑M * 2 ^ q - if M = 2 ^ 52 ∧ -1074 < q then 2 ^ (q - 1) else 2 ^ q) < v) : WithBotTop.coe (if neg = true then -v else v) < doubleValue (assemble neg M q).nextUp.bits ∧ doubleValue (assemble neg M q).nextDown.bits < WithBotTop.coe (if neg = true then -v else v)

A normal x = ±M 2 ^ q (2 ^ 52 ≤ M < 2 ^ 53) and a positive v below (M + 1) 2 ^ q and above the value of the magnitude below that of x: the neighbours of x lie on either side of ±v.

Faithful rounding of a significand

theorem Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofSignificand_two_pow {neg : Bool} {q : ℤ} {v : ℚ} (hv : 0 < v) (hq : -1074 ≤ q) (hlo : ↑(2 ^ 53) * 2 ^ q - 2 ^ (q - 1) ≤ v) (hhi : v ≤ ↑(2 ^ 53) * 2 ^ q + 2 ^ (q - 1)) (hf : (ofSignificand neg (2 ^ 53) q).isFinite = true) : WithBotTop.coe (if neg = true then -v else v) < doubleValue (ofSignificand neg (2 ^ 53) q).nextUp.bits ∧ doubleValue (ofSignificand neg (2 ^ 53) q).nextDown.bits < WithBotTop.coe (if neg = true then -v else v)

theorem Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofSignificand_of_ne {neg : Bool} {M : ℕ} {q : ℤ} {v : ℚ} (hv : 0 < v) (hM : M < 2 ^ 53) (hq : -1074 ≤ q) (hlo : ↑M * 2 ^ q - 2 ^ (q - 1) ≤ v) (hhi : v ≤ ↑M * 2 ^ q + 2 ^ (q - 1)) (hnorm : -1074 < q → 2 ^ (q + 52) ≤ v) (hf : (ofSignificand neg M q).isFinite = true) : WithBotTop.coe (if neg = true then -v else v) < doubleValue (ofSignificand neg M q).nextUp.bits ∧ doubleValue (ofSignificand neg M q).nextDown.bits < WithBotTop.coe (if neg = true then -v else v)

theorem Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofSignificand {neg : Bool} {M : ℕ} {q : ℤ} {v : ℚ} (hv : 0 < v) (hM : M ≤ 2 ^ 53) (hq : -1074 ≤ q) (hlo : ↑M * 2 ^ q - 2 ^ (q - 1) ≤ v) (hhi : v ≤ ↑M * 2 ^ q + 2 ^ (q - 1)) (hnorm : -1074 < q → 2 ^ (q + 52) ≤ v) (hf : (ofSignificand neg M q).isFinite = true) : WithBotTop.coe (if neg = true then -v else v) < doubleValue (ofSignificand neg M q).nextUp.bits ∧ doubleValue (ofSignificand neg M q).nextDown.bits < WithBotTop.coe (if neg = true then -v else v)

The double of a significand M ≤ 2 ^ 53 rounded from a positive v to within half a unit of the exponent q ≥ -1074 of its last place, with v ≥ 2 ^ (q + 52) when q is not the least exponent, is a faithful rounding of ±v when it is finite.

Rounding to the nearest integer

def Ratpoints.Double.roundDiv (a b : ℕ) : ℕ

a / b rounded to the nearest integer, ties to even, as Ratpoints.Double.ofRatio rounds the quotient of a and b ≠ 0: the remainder r decides, rounding up when 2 r > b and when 2 r = b and the quotient is odd.

Equations

• Ratpoints.Double.roundDiv a b = if b < 2 * (a % b) ∨ 2 * (a % b) = b ∧ a / b % 2 = 1 then a / b + 1 else a / b

theorem Ratpoints.Double.roundDiv_bounds_nat (a : ℕ) {b : ℕ} (hb : 0 < b) : 2 * roundDiv a b * b ≤ 2 * a + b ∧ 2 * a ≤ (2 * roundDiv a b + 1) * b

theorem Ratpoints.Double.roundDiv_bounds (a : ℕ) {b : ℕ} (hb : 0 < b) : ↑(roundDiv a b) - 1 / 2 ≤ ↑a / ↑b ∧ ↑a / ↑b ≤ ↑(roundDiv a b) + 1 / 2

theorem Ratpoints.Double.roundShift_eq_roundDiv (m : ℕ) {k : ℤ} (hk : 0 < k) : roundShift m k = roundDiv m (2 ^ k.toNat)

theorem Ratpoints.Double.roundShift_bounds (m : ℕ) (k : ℤ) : ↑(roundShift m k) - 1 / 2 ≤ ↑m / 2 ^ k ∧ ↑m / 2 ^ k ≤ ↑(roundShift m k) + 1 / 2

ofRatio

def Ratpoints.Double.ratioExponent (n d : ℕ) : ℤ

The exponent E with 2 ^ E ≤ n / d < 2 ^ (E + 1) that Ratpoints.Double.ofRatio finds from the lengths of n and d in bits and one comparison (Ratpoints.Double.ratioExponent_bounds).

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Double.ratioLast (n d : ℕ) : ℤ

The exponent of the last place of the double that Ratpoints.Double.ofRatio rounds n / d to: Ratpoints.Double.ratioExponent n d - 52, and -1074 for the subnormals.

Equations

• Ratpoints.Double.ratioLast n d = max (Ratpoints.Double.ratioExponent n d - 52) (-1074)

def Ratpoints.Double.ratioPair (n d : ℕ) (q : ℤ) : ℕ × ℕ

The numerator and the denominator of n / (d 2 ^ q) that Ratpoints.Double.ofRatio divides.

Equations

• Ratpoints.Double.ratioPair n d q = if 0 ≤ q then (n, d * 2 ^ q.toNat) else (n * 2 ^ (-q).toNat, d)

theorem Ratpoints.Double.ofRatio_eq {neg : Bool} {n : ℕ} (d : ℕ) (hn : n ≠ 0) : ofRatio neg n d = ofSignificand neg (roundDiv (ratioPair n d (ratioLast n d)).1 (ratioPair n d (ratioLast n d)).2) (ratioLast n d)

theorem Ratpoints.Double.two_zpow_le_div_iff {n d : ℕ} (hd : d ≠ 0) (e : ℤ) : (if 0 ≤ e then decide (d * 2 ^ e.toNat ≤ n) else decide (d ≤ n * 2 ^ (-e).toNat)) = true ↔ 2 ^ e ≤ ↑n / ↑d

theorem Ratpoints.Double.two_zpow_log2_div_bounds {n d : ℕ} (hn : n ≠ 0) (hd : d ≠ 0) : 2 ^ (↑n.log2 - ↑d.log2 - 1) < ↑n / ↑d ∧ ↑n / ↑d < 2 ^ (↑n.log2 - ↑d.log2 + 1)

theorem Ratpoints.Double.ratioExponent_bounds {n d : ℕ} (hn : n ≠ 0) (hd : d ≠ 0) : 2 ^ ratioExponent n d ≤ ↑n / ↑d ∧ ↑n / ↑d < 2 ^ (ratioExponent n d + 1)

theorem Ratpoints.Double.ratioPair_snd_pos {n d : ℕ} (hd : d ≠ 0) (q : ℤ) : 0 < (ratioPair n d q).2

theorem Ratpoints.Double.ratioPair_div (n d : ℕ) (q : ℤ) : ↑(ratioPair n d q).1 / ↑(ratioPair n d q).2 = ↑n / ↑d / 2 ^ q

theorem Ratpoints.Double.ofRatio_rounding {n d : ℕ} (hn : n ≠ 0) (hd : d ≠ 0) : roundDiv (ratioPair n d (ratioLast n d)).1 (ratioPair n d (ratioLast n d)).2 ≤ 2 ^ 53 ∧ -1074 ≤ ratioLast n d ∧ ↑(roundDiv (ratioPair n d (ratioLast n d)).1 (ratioPair n d (ratioLast n d)).2) * 2 ^ ratioLast n d - 2 ^ (ratioLast n d - 1) ≤ ↑n / ↑d ∧ ↑n / ↑d ≤ ↑(roundDiv (ratioPair n d (ratioLast n d)).1 (ratioPair n d (ratioLast n d)).2) * 2 ^ ratioLast n d + 2 ^ (ratioLast n d - 1) ∧ (-1074 < ratioLast n d → 2 ^ (ratioLast n d + 52) ≤ ↑n / ↑d)

The significand M and the exponent q of its last place that Ratpoints.Double.ofRatio rounds n / d to: M ≤ 2 ^ 53, q ≥ -1074, M 2 ^ q within half a unit 2 ^ (q - 1) of n / d, and n / d ≥ 2 ^ (q + 52) when q is not the least exponent.

theorem Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofRatio {neg : Bool} {n d : ℕ} (hn : n ≠ 0) (hd : d ≠ 0) (hf : (ofRatio neg n d).isFinite = true) : WithBotTop.coe (if neg = true then -(↑n / ↑d) else ↑n / ↑d) < doubleValue (ofRatio neg n d).nextUp.bits ∧ doubleValue (ofRatio neg n d).nextDown.bits < WithBotTop.coe (if neg = true then -(↑n / ↑d) else ↑n / ↑d)

Ratpoints.Double.ofRatio rounds faithfully: when it is finite, ±n / d lies strictly between the neighbours of the result.

theorem Ratpoints.Double.isNaN_ofRatio (neg : Bool) (n : ℕ) {d : ℕ} (hd : d ≠ 0) : (ofRatio neg n d).isNaN = false

ofDyadic

theorem Ratpoints.Double.ofDyadic_eq {neg : Bool} {m : ℕ} (e : ℤ) (hm : m ≠ 0) : ofDyadic neg m e = ofSignificand neg (roundShift m (max (↑m.log2 + e - 52) (-1074) - e)) (max (↑m.log2 + e - 52) (-1074))

theorem Ratpoints.Double.ofDyadic_rounding {m : ℕ} (hm : m ≠ 0) (e : ℤ) : roundShift m (max (↑m.log2 + e - 52) (-1074) - e) ≤ 2 ^ 53 ∧ -1074 ≤ max (↑m.log2 + e - 52) (-1074) ∧ ↑(roundShift m (max (↑m.log2 + e - 52) (-1074) - e)) * 2 ^ max (↑m.log2 + e - 52) (-1074) - 2 ^ (max (↑m.log2 + e - 52) (-1074) - 1) ≤ ↑m * 2 ^ e ∧ ↑m * 2 ^ e ≤ ↑(roundShift m (max (↑m.log2 + e - 52) (-1074) - e)) * 2 ^ max (↑m.log2 + e - 52) (-1074) + 2 ^ (max (↑m.log2 + e - 52) (-1074) - 1) ∧ (-1074 < max (↑m.log2 + e - 52) (-1074) → 2 ^ (max (↑m.log2 + e - 52) (-1074) + 52) ≤ ↑m * 2 ^ e)

The significand M and the exponent q of its last place that Ratpoints.Double.ofDyadic rounds m 2 ^ e to: M ≤ 2 ^ 53, q ≥ -1074, M 2 ^ q within half a unit 2 ^ (q - 1) of m 2 ^ e, and m 2 ^ e ≥ 2 ^ (q + 52) when q is not the least exponent.

theorem Ratpoints.Double.lt_nextUp_and_nextDown_lt_ofDyadic {neg : Bool} {m : ℕ} {e : ℤ} (hm : m ≠ 0) (hf : (ofDyadic neg m e).isFinite = true) : WithBotTop.coe (if neg = true then -(↑m * 2 ^ e) else ↑m * 2 ^ e) < doubleValue (ofDyadic neg m e).nextUp.bits ∧ doubleValue (ofDyadic neg m e).nextDown.bits < WithBotTop.coe (if neg = true then -(↑m * 2 ^ e) else ↑m * 2 ^ e)

Ratpoints.Double.ofDyadic rounds faithfully: when it is finite, ±m 2 ^ e lies strictly between the neighbours of the result.

theorem Ratpoints.Double.isNaN_ofDyadic (neg : Bool) (m : ℕ) (e : ℤ) : (ofDyadic neg m e).isNaN = false

The double of the height bound

theorem Ratpoints.Double.isFinite_ofInt64_and_lt_toRat_nextUp {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) : (ofInt64 H.toInt64).isFinite = true ∧ (ofInt64 H.toInt64).signBit = false ∧ (ofInt64 H.toInt64).nextUp.isFinite = true ∧ ↑H < (ofInt64 H.toInt64).nextUp.toRat

The double of 1 ≤ H < 2 ^ 63 is finite, with the sign bit clear, and the next double is finite and above H.

theorem Ratpoints.Double.isFinite_and_le_toRat_ofInt64_nextUp {H : ℕ} (hH : 1 ≤ H) (hH63 : H < 2 ^ 63) : have h := ofInt64 H.toInt64; have h := if (h.lt twoPow63 && decide (h.toInt64 < H.toInt64)) = true then h.nextUp else h; h.isFinite = true ∧ ↑H ≤ h.toRat

The double of 1 ≤ H < 2 ^ 63, moved up to the next double when it is below 2 ^ 63 and its conversion to a long is below H, is finite and at least H: the bound h of the default search interval [-h, h] of Ratpoints.searchIntervals, and Ratpoints.Cli.heightEnd.

Zeros and infinities

theorem Ratpoints.Double.beq_zero_ofRatio_zero (neg : Bool) (d : ℕ) : (ofRatio neg 0 d).beq zero = true

theorem Ratpoints.Double.isFinite_ite_huge (neg : Bool) : (if neg = true then huge.neg else huge).isFinite = false

theorem Ratpoints.Double.nextUp_of_beq_zero {x : Double} (hz : x.beq zero = true) : x.nextUp = { bits := 1 }

theorem Ratpoints.Double.toRat_zero_nextUp : zero.nextUp.toRat = 2 ^ (-1074)

theorem Ratpoints.Double.doubleValue_one : doubleValue 1 = WithBotTop.coe (2 ^ (-1074))