Bfloat16 consequences of the generic theory

The general format-rounding theorem specializes to two useful bfloat16 facts. Widening to binary32 is exact because both formats have the same normal exponent range and binary32 adds fraction bits. Addition performs exact dyadic addition followed by one bfloat16 nearest-even rounding step.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_cast_bfloat16_binary32 {x : Model FloatFormat.bfloat16} (hx : x.isFinite = true) : (cast FloatFormat.bfloat16 FloatFormat.binary32 x).toReal = x.toReal

Widening a finite bfloat16 value to binary32 preserves its exact real value.

@[reducible, inline]

noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.bf16Round (x : ℝ) : ℝ

Bfloat16 rounding viewed as a real function.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bfloat16_add_eq_bf16Round {x y : Model FloatFormat.bfloat16} (hx : x.isFinite = true) (hy : y.isFinite = true) (hfin : (x.add y).isFinite = true) : (x.add y).toReal = bf16Round (x.toReal + y.toReal)

Finite bfloat16 addition is exact real addition followed by one nearest-even rounding step.