Real values of exact dyadics

A dyadic denotes its signed integer significand times an integral power of two. Its rational and real interpretations agree, so exact arithmetic identities can be transported by casting. These definitions do not depend on any floating-point format.

noncomputable def FloatLib.Numerics.Dyadic.toReal (d : Dyadic) : ℝ

Interpret an exact dyadic (-1)^sign * significand * 2^exponent as a real.

@[simp]

theorem FloatLib.Numerics.Dyadic.cast_toRat (d : Dyadic) : ↑d.toRat = d.toReal

The exact rational and real interpretations of a dyadic agree.

@[simp]

theorem FloatLib.Numerics.Dyadic.cast_signedSignificand (d : Dyadic) : ↑d.signedSignificand = (if d.negative = true then -1 else 1) * ↑d.significand

Casting the signed significand separates its sign from its natural magnitude.

@[simp]

theorem FloatLib.Numerics.Dyadic.toReal_mk_false (significand : ℕ) (exponent : ℤ) : { negative := false, significand := significand, exponent := exponent }.toReal = ↑significand * 2 ^ exponent

A nonnegative dyadic constructor has the expected unsigned real denotation.