Standard Format Theorems

Connections between the generic format predicate and the concrete FIX, FLX, and FLT families. The fixed-point equivalence is the first instance of the generic pattern used by the floating-point families.

theorem FloatLib.Floats.Formats.Flocq.fixFormat_of_generic {β : Numerics.Radix} (emin : ℤ) (x : ℝ) (hx : genericFormat β (fixExp emin) x) : FIXFormat emin x

The generic format generated by fixExp emin is contained in FIXFormat emin.

theorem FloatLib.Floats.Formats.Flocq.generic_of_fixFormat {β : Numerics.Radix} (emin : ℤ) (x : ℝ) (hx : FIXFormat emin x) : genericFormat β (fixExp emin) x

Every fixed-point value belongs to the generic format generated by fixExp emin.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FIX_iff {β : Numerics.Radix} (emin : ℤ) (x : ℝ) : genericFormat β (fixExp emin) x ↔ FIXFormat emin x

FIXFormat and the corresponding generic format describe the same real values.

theorem FloatLib.Floats.Formats.Flocq.bpow_eq_natPow {β : Numerics.Radix} (p : ℤ) (hp : 0 ≤ p) : bpow β p = ↑(β.base ^ p.toNat)

A radix power with nonnegative exponent agrees with the corresponding natural-number power.

theorem FloatLib.Floats.Formats.Flocq.flxFormat_of_generic {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : genericFormat β (flxExp prec) x) : FLXFormat prec x

The generic flxExp format satisfies the explicit FLX mantissa bound.

theorem FloatLib.Floats.Formats.Flocq.generic_of_flxFormat {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : FLXFormat prec x) : genericFormat β (flxExp prec) x

Every explicit bounded-mantissa FLX value belongs to the corresponding generic format.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLX_iff {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) (x : ℝ) : genericFormat β (flxExp prec) x ↔ FLXFormat prec x

FLXFormat is exactly the generic format generated by flxExp.

theorem FloatLib.Floats.Formats.Flocq.fltFormat_of_generic {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : genericFormat β (fltExp emin prec) x) : FLTFormat emin prec x

The generic fltExp format satisfies the explicit FLT mantissa and exponent bounds.

theorem FloatLib.Floats.Formats.Flocq.generic_of_fltFormat {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : FLTFormat emin prec x) : genericFormat β (fltExp emin prec) x

Every explicit bounded-mantissa FLT value belongs to the corresponding generic format.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLT_iff {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) : genericFormat β (fltExp emin prec) x ↔ FLTFormat emin prec x

FLTFormat is exactly the generic format generated by fltExp.