Intervals with arbitrary endpoint representations

The endpoint pair does not impose an order, radix, infinity representation, or rounding policy. Contains interprets finite endpoints through an explicit partial decoder. Failed decoding excludes NaNs, NaRs, and other values outside the chosen scalar interpretation.

structure FloatLib.Numerics.Interval (α : Type u_1) : Type u_1

An endpoint pair; construction alone does not assert that the bounds are ordered.

• lo : α

  Lower endpoint.

• hi : α

  Upper endpoint.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqInterval {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Interval α✝)

def FloatLib.Numerics.instDecidableEqInterval.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Interval α✝) : Decidable (x✝ = x✝¹)

def FloatLib.Numerics.instReprInterval.repr {α✝ : Type u_1} [Repr α✝] : Interval α✝ → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.instReprInterval {α✝ : Type u_1} [Repr α✝] : Repr (Interval α✝)

def FloatLib.Numerics.Interval.point {α : Type u_1} (x : α) : Interval α

A point interval preserves its endpoint representation exactly.

def FloatLib.Numerics.Interval.map {α : Type u_1} {β : Type u_2} (f : α → β) (I : Interval α) : Interval β

Change both endpoint representations by the same function.

def FloatLib.Numerics.Interval.decode? {α : Type u_1} {β : Type u_2} (decode : α → Option β) (I : Interval α) : Option (Interval β)

Decode both finite endpoints, failing if either endpoint has no scalar interpretation.

def FloatLib.Numerics.Interval.Contains {α : Type u_1} {β : Type u_2} [LE β] (decode : α → Option β) (I : Interval α) (x : β) : Prop

Scalar membership requires successful decoding and both endpoint inequalities.

def FloatLib.Numerics.Interval.ofBounds? {α : Type u_1} {β : Type u_2} [LinearOrder β] (decode : α → Option β) (lo hi : α) : Option (Interval α)

Keep finite ordered bounds; special values and reversed bounds return none.

structure FloatLib.Numerics.OutwardRounding (α : Type u_1) (β : Type u_2) [LE β] : Type (max u_1 u_2)

Partial outward rounding for any endpoint carrier and ordered scalar interpretation.

Success certifies finite decoded bounds; failure can report overflow or an unavailable enclosure. In particular, this interface does not require bounded formats to represent infinities.

• decode : α → Option β

  Finite scalar interpretation of an encoded endpoint.

• enclose? : β → Option (Interval α)

  Try to bracket an exact scalar by representable endpoints.

• sound {x : β} {I : Interval α} : self.enclose? x = some I → Interval.Contains self.decode I x

  Every successful result encloses the exact scalar.