Correct rounding of configured posit hyperbolic functions

Refinement holds for every lawful codec. The real-rounding and exceptional-domain theorems therefore apply to every configured width and carrier.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_tanH {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (tanH value) = (toModel value).tanH

Configured hyperbolic tangent refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcTanH {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (arcTanH value) = (toModel value).arcTanH

Configured inverse hyperbolic tangent refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.tanH_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (tanH value) = Formats.Posit.Model.RealRounding.round format (Real.tanh ↑q)

Finite configured hyperbolic tangent rounds its exact real value once.

theorem FloatLib.Floats.ExecFloat.Posit.arcTanH_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (hlower : -1 < q) (hupper : q < 1) : toModel (arcTanH value) = Formats.Posit.Model.RealRounding.round format (Real.artanh ↑q)

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

theorem FloatLib.Floats.ExecFloat.Posit.tanH_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (tanH value) = Formats.Posit.Model.nar format

NaR inputs propagate through configured hyperbolic tangent.

theorem FloatLib.Floats.ExecFloat.Posit.arcTanH_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (arcTanH value) = Formats.Posit.Model.nar format

NaR inputs propagate through configured inverse hyperbolic tangent.

theorem FloatLib.Floats.ExecFloat.Posit.arcTanH_eq_nar_of_outside {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (houtside : q ≤ -1 ∨ 1 ≤ q) : toModel (arcTanH value) = Formats.Posit.Model.nar format

The configured inverse hyperbolic tangent rejects both endpoints and the exterior.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_sinH {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (sinH value) = (toModel value).sinH

Configured hyperbolic sine refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.sinH_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (sinH value) = Formats.Posit.Model.RealRounding.round format (Real.sinh ↑q)

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

theorem FloatLib.Floats.ExecFloat.Posit.sinH_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (sinH value) = Formats.Posit.Model.nar format

NaR inputs propagate through configured hyperbolic sine.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_cosH {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (cosH value) = (toModel value).cosH

Configured hyperbolic cosine refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.cosH_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (cosH value) = Formats.Posit.Model.RealRounding.round format (Real.cosh ↑q)

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

theorem FloatLib.Floats.ExecFloat.Posit.cosH_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (cosH value) = Formats.Posit.Model.nar format

NaR inputs propagate through configured hyperbolic cosine.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcSinH {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (arcSinH value) = (toModel value).arcSinH

Configured inverse hyperbolic sine refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.arcSinH_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (arcSinH value) = Formats.Posit.Model.RealRounding.round format (Real.arsinh ↑q)

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

theorem FloatLib.Floats.ExecFloat.Posit.arcSinH_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (arcSinH value) = Formats.Posit.Model.nar format

NaR inputs propagate through configured inverse hyperbolic sine.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcCosH {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (arcCosH value) = (toModel value).arcCosH

Configured inverse hyperbolic cosine refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.arcCosH_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (hdomain : 1 ≤ q) : toModel (arcCosH value) = Formats.Posit.Model.RealRounding.round format (Real.arcosh ↑q)

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

theorem FloatLib.Floats.ExecFloat.Posit.arcCosH_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (arcCosH value) = Formats.Posit.Model.nar format

NaR inputs propagate through configured inverse hyperbolic cosine.

theorem FloatLib.Floats.ExecFloat.Posit.arcCosH_eq_nar_of_lt_one {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (houtside : q < 1) : toModel (arcCosH value) = Formats.Posit.Model.nar format

Configured inverse hyperbolic cosine rejects finite inputs below one.