Real rounding and domains of posit hyperbolic functions

Finite inputs in the real domain round the mathematical function once, using the standard posit saturation and appended-bit tie rule. Invalid inputs and NaR are covered separately.

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.tanhRat_eq_real (format : Format) (argument : ℚ) : tanhRat format argument = RealRounding.round format (Real.tanh ↑argument)

Rational hyperbolic tangent rounds its exact real value.

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.artanhRat_eq_real (format : Format) (argument : ℚ) (hlower : -1 < argument) (hupper : argument < 1) : artanhRat format argument = RealRounding.round format (Real.artanh ↑argument)

Rational inverse hyperbolic tangent rounds its exact value on the open real domain.

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.artanhRat_eq_nar (format : Format) (argument : ℚ) (houtside : argument ≤ -1 ∨ 1 ≤ argument) : artanhRat format argument = nar format

Inverse hyperbolic tangent rejects the endpoints and exterior of its real domain.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.applyRat_nar {format : Format} (operation : ℚ → Model format) : applyRat operation (nar format) = nar format

Rational operation lifting propagates NaR independently of the operation.

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.sinhRat_eq_real (format : Format) (argument : ℚ) : sinhRat format argument = RealRounding.round format (Real.sinh ↑argument)

Rational hyperbolic sine rounds its exact real value.

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.coshRat_eq_real (format : Format) (argument : ℚ) : coshRat format argument = RealRounding.round format (Real.cosh ↑argument)

Rational hyperbolic cosine rounds its exact real value.

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.arsinhRat_eq_real (format : Format) (argument : ℚ) : arsinhRat format argument = RealRounding.round format (Real.arsinh ↑argument)

Rational inverse hyperbolic sine rounds its exact real value.

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.arcoshRat_eq_real (format : Format) (argument : ℚ) (hdomain : 1 ≤ argument) : arcoshRat format argument = RealRounding.round format (Real.arcosh ↑argument)

Rational inverse hyperbolic cosine rounds its nonnegative real branch.

theorem FloatLib.Floats.Formats.Posit.Model.Hyperbolic.arcoshRat_eq_nar (format : Format) (argument : ℚ) (houtside : argument < 1) : arcoshRat format argument = nar format

Inverse hyperbolic cosine rejects arguments below one.

theorem FloatLib.Floats.Formats.Posit.Model.tanH_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.tanH = RealRounding.round format (Real.tanh ↑q)

Every finite hyperbolic tangent has one final rounding of its exact real value.

theorem FloatLib.Floats.Formats.Posit.Model.arcTanH_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hlower : -1 < q) (hupper : q < 1) : value.arcTanH = RealRounding.round format (Real.artanh ↑q)

Inverse hyperbolic tangent rounds its exact real value for inputs strictly between -1 and 1.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.tanH_nar {format : Format} : (nar format).tanH = nar format

Hyperbolic tangent propagates NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcTanH_nar {format : Format} : (nar format).arcTanH = nar format

Inverse hyperbolic tangent propagates NaR.

theorem FloatLib.Floats.Formats.Posit.Model.arcTanH_eq_nar_of_outside {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (houtside : q ≤ -1 ∨ 1 ≤ q) : value.arcTanH = nar format

Inverse hyperbolic tangent returns NaR at and beyond either endpoint.

theorem FloatLib.Floats.Formats.Posit.Model.sinH_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.sinH = RealRounding.round format (Real.sinh ↑q)

Finite hyperbolic sine rounds its exact real value on its real domain.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.sinH_nar {format : Format} : (nar format).sinH = nar format

Hyperbolic sine propagates NaR.

theorem FloatLib.Floats.Formats.Posit.Model.cosH_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.cosH = RealRounding.round format (Real.cosh ↑q)

Finite hyperbolic cosine rounds its exact real value on its real domain.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.cosH_nar {format : Format} : (nar format).cosH = nar format

Hyperbolic cosine propagates NaR.

theorem FloatLib.Floats.Formats.Posit.Model.arcSinH_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.arcSinH = RealRounding.round format (Real.arsinh ↑q)

Finite inverse hyperbolic sine rounds its exact real value on its real domain.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcSinH_nar {format : Format} : (nar format).arcSinH = nar format

Inverse hyperbolic sine propagates NaR.

theorem FloatLib.Floats.Formats.Posit.Model.arcCosH_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hdomain : 1 ≤ q) : value.arcCosH = RealRounding.round format (Real.arcosh ↑q)

Finite inverse hyperbolic cosine rounds its exact real value on its real domain.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcCosH_nar {format : Format} : (nar format).arcCosH = nar format

Inverse hyperbolic cosine propagates NaR.

theorem FloatLib.Floats.Formats.Posit.Model.arcCosH_eq_nar_of_lt_one {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (houtside : q < 1) : value.arcCosH = nar format

Inverse hyperbolic cosine rejects finite inputs below one.