Infinite endpoints of decimal adjacency

An infinite neighbor of a finite datum is justified by a bound on every finite datum in the format. Moving inward from infinity selects the extreme finite value. The status theorem remains unchanged at each endpoint.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_infinity_value (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hx : Datum.Valid f (Datum.finite s c q)) (hout : (nextUp f (Datum.finite s c q)).value = Datum.infinity false) : Datum.finiteValue s c q = ↑(f.coefficientBound - 1) * 10 ^ f.maxQuantum

A finite input can have positive infinity as successor only at the finite maximum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_infinite_bound (f : Format) (x : Datum) (hx : Datum.Valid f x) (a : ℚ) (ha : x.toRat? = some a) (hout : (nextUp f x).value = Datum.infinity false) (y : Datum) (v : ℚ) (hy : Datum.Valid f y) (hv : y.toRat? = some v) : v ≤ a

There is no larger finite datum when nextUp reaches positive infinity.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown_infinite_bound (f : Format) (x : Datum) (hx : Datum.Valid f x) (a : ℚ) (ha : x.toRat? = some a) (hout : (nextDown f x).value = Datum.infinity true) (y : Datum) (v : ℚ) (hy : Datum.Valid f y) (hv : y.toRat? = some v) : a ≤ v

There is no smaller finite datum when nextDown reaches negative infinity.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_positive_infinity (f : Format) : nextUp f (Datum.infinity false) = { value := Datum.infinity false }

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_negative_infinity (f : Format) : nextUp f (Datum.infinity true) = { value := f.maxFinite true }

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown_negative_infinity (f : Format) : nextDown f (Datum.infinity true) = { value := Datum.infinity true }

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown_positive_infinity (f : Format) : nextDown f (Datum.infinity false) = { value := f.maxFinite false }

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp_negative_infinity_le (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hx : Datum.Valid f (Datum.finite s c q)) : -(↑(f.coefficientBound - 1) * 10 ^ f.maxQuantum) ≤ Datum.finiteValue s c q

Moving inward from negative infinity returns the smallest finite value.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown_positive_infinity_ge (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (hx : Datum.Valid f (Datum.finite s c q)) : Datum.finiteValue s c q ≤ ↑(f.coefficientBound - 1) * 10 ^ f.maxQuantum

Moving inward from positive infinity returns the largest finite value.