Rounded Arithmetic on Mantissa/Exponent Values

Rounded arithmetic on FloatRep values uses exact representation operations where finite radix expansions suffice. Addition, subtraction, and multiplication first use their exact FloatRep operations. Division and square root need not have finite radix expansions, so they are formed over the reals and rounded directly into the selected format.

These definitions model finite rounded arithmetic. IEEE exceptional behavior for zero divisors, negative square roots, infinities, and NaNs belongs to FloatLib.Floats.ExecFloat.

noncomputable def FloatLib.Floats.Formats.Flocq.FloatRep.addRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f g : FloatRep β) : FloatRep β

Exact addition followed by rounding into the selected format.

noncomputable def FloatLib.Floats.Formats.Flocq.FloatRep.subRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f g : FloatRep β) : FloatRep β

Exact subtraction followed by rounding into the selected format.

noncomputable def FloatLib.Floats.Formats.Flocq.FloatRep.mulRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f g : FloatRep β) : FloatRep β

Exact multiplication followed by rounding into the selected format.

noncomputable def FloatLib.Floats.Formats.Flocq.FloatRep.divRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f g : FloatRep β) : FloatRep β

Exact real division followed by rounding into the selected format.

noncomputable def FloatLib.Floats.Formats.Flocq.FloatRep.sqrtRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f : FloatRep β) : FloatRep β

Exact real square root followed by rounding into the selected format.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_addRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f g : FloatRep β) : toReal (addRounded rnd f g) = round rnd (toReal f + toReal g)

Rounded addition denotes real addition followed by the selected format rounding.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_subRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f g : FloatRep β) : toReal (subRounded rnd f g) = round rnd (toReal f - toReal g)

Rounded subtraction denotes real subtraction followed by the selected format rounding.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_mulRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f g : FloatRep β) : toReal (mulRounded rnd f g) = round rnd (toReal f * toReal g)

Rounded multiplication denotes real multiplication followed by the selected format rounding.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_divRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f g : FloatRep β) : toReal (divRounded rnd f g) = round rnd (toReal f / toReal g)

Rounded division denotes real division followed by the selected format rounding.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.FloatRep.toReal_sqrtRounded {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (f : FloatRep β) : toReal (sqrtRounded rnd f) = round rnd √(toReal f)

Rounded square root denotes real square root followed by the selected format rounding.