Order of interval endpoints

Boolean endpoint comparisons agree with real order for finite values and with extended-real order for non-NaN values, including infinities. The non-NaN hypotheses are needed because NaNs are unordered.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.le_iff_leB_eq_true {fmt : FloatFormat} (x y : Model fmt) : x.le y ↔ leB x y = true

The proposition-valued and Boolean executable non-strict orders agree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.le_iff_toEReal_le_of_isNaN_eq_false {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) : x.le y ↔ x.toEReal ≤ y.toEReal

On non-NaN values, executable comparison agrees exactly with extended-real ≤.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.leB_eq_true_iff_toEReal_le_of_isNaN_eq_false {fmt : FloatFormat} (x y : Model fmt) (hx : x.isNaN = false) (hy : y.isNaN = false) : leB x y = true ↔ x.toEReal ≤ y.toEReal

Boolean endpoint comparison agrees with extended-real order on non-NaN values.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.leB_eq_true_iff_toReal_le_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hx : x.isFinite = true) (hy : y.isFinite = true) : leB x y = true ↔ x.toReal ≤ y.toReal

On finite values, executable boolean comparison agrees exactly with real ≤.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.le_iff_toReal_le_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hx : x.isFinite = true) (hy : y.isFinite = true) : x.le y ↔ x.toReal ≤ y.toReal

On finite values, the proposition-valued executable order agrees exactly with real ≤.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.validExtended_of_toEReal_le {fmt : FloatFormat} {I : Interval fmt} (hlo : I.lo.isNaN = false) (hhi : I.hi.isNaN = false) (hordered : I.lo.toEReal ≤ I.hi.toEReal) : I.ValidExtended

Ordered, non-NaN extended-real endpoints define a valid interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.Valid.toReal_ordered {fmt : FloatFormat} {I : Interval fmt} (hI : I.Valid) : I.lo.toReal ≤ I.hi.toReal

A valid interval's decoded lower endpoint does not exceed its decoded upper endpoint.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ValidExtended.toEReal_ordered {fmt : FloatFormat} {I : Interval fmt} (hI : I.ValidExtended) : I.lo.toEReal ≤ I.hi.toEReal

An extended-valid interval has ordered extended-real endpoints.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.valid_point_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) : (point x).Valid

A finite executable value defines a valid degenerate interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.validExtended_point_of_isNaN_eq_false {fmt : FloatFormat} (x : Model fmt) (hx : x.isNaN = false) : (point x).ValidExtended

Every non-NaN value defines an extended-valid degenerate interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.validExtended_whole (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : (whole fmt).ValidExtended

The full IEEE range, including infinities, is extended-valid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.eRealMem_whole (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (x : EReal) : (whole fmt).ERealMem x

Every extended-real value belongs to the full IEEE range.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ofBounds_lower_le {fmt : FloatFormat} (lo hi : Model fmt) (hfmt : fmt.isIEEE = true) : (ofBounds lo hi).lo.toEReal ≤ lo.toEReal

Checking candidate endpoints can only lower the lower bound of an IEEE enclosure.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.le_ofBounds_upper {fmt : FloatFormat} (lo hi : Model fmt) (hfmt : fmt.isIEEE = true) : hi.toEReal ≤ (ofBounds lo hi).hi.toEReal

Checking candidate endpoints can only raise the upper bound of an IEEE enclosure.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.ofBounds_eq_of_isFinite {fmt : FloatFormat} (lo hi : Model fmt) (hlo : lo.isFinite = true) (hhi : hi.isFinite = true) (hordered : lo.toReal ≤ hi.toReal) : ofBounds lo hi = { lo := lo, hi := hi }

Ordered finite bounds survive the enclosure check exactly.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.realMem_ofBounds {fmt : FloatFormat} {lo hi : Model fmt} {x : ℝ} (hlo : lo.isFinite = true) (hhi : hi.isFinite = true) (hx : { lo := lo, hi := hi }.RealMem x) : (ofBounds lo hi).RealMem x

A real enclosure with finite candidate endpoints survives the bounds check.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.validExtended_ofBounds {fmt : FloatFormat} (lo hi : Model fmt) (hfmt : fmt.isIEEE = true) : (ofBounds lo hi).ValidExtended

Checked IEEE bounds always define an ordered interval without NaN endpoints.