Floating point powers of two

Exact powers of two

theorem Floating.valid_two_pow {n : Fixed 0} : have s := n.n.toUInt64 + 2 ^ 63; Valid (2 ^ 62) (s - 62)

two_pow is valid

@[irreducible]

def Floating.two_pow (n : Fixed 0) : Floating

Exact powers of two

Equations

• Floating.two_pow n = bif n == nan || decide (n.n.toUInt64 + 2 ^ 63 < 62) then nan else { n := 2 ^ 62, s := n.n.toUInt64 + 2 ^ 63 - 62, v := ⋯ }

theorem Floating.approx_two_pow (n : Fixed 0) : approx (two_pow n) (2 ^ n.val)

two_pow is conservative

The special case of n = 2^62

theorem Floating.valid_two_pow_special {s : UInt64} : Valid (2 ^ 62) s

two_pow_special is valid

@[irreducible]

def Floating.two_pow_special (s : UInt64) : Floating

Build 2^62 * 2^(s - 2^63)

@[simp]

theorem Floating.two_pow_special_ne_nan (s : UInt64) : two_pow_special s ≠ nan

two_pow_special never makes nan

@[simp]

theorem Floating.val_two_pow_special (s : UInt64) : (two_pow_special s).val = 2 ^ (62 + ↑s.toNat - 2 ^ 63)

two_pow_special never makes nan