Correct rounding of configured posit two-coordinate arctangent

The configured operations inherit the model's principal-branch rounding and exceptional-value rules for every lawful storage carrier and valid posit width.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcTan2 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (arcTan2 x y) = (toModel x).arcTan2 (toModel y)

Configured arcTan2 refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan2_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) {a b : ℚ} (hx : toRat? x = some a) (hy : toRat? y = some b) (horigin : ¬(a = 0 ∧ b = 0)) : toModel (arcTan2 x y) = Formats.Posit.Model.RealRounding.round format { re := ↑a, im := ↑b }.arg

Configured arcTan2 rounds the exact principal argument.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan2_eq_nar_left {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hx : toModel x = Formats.Posit.Model.nar format) : toModel (arcTan2 x y) = Formats.Posit.Model.nar format

Configured arcTan2 propagates a NaR first coordinate.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan2_eq_nar_right {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hy : toModel y = Formats.Posit.Model.nar format) : toModel (arcTan2 x y) = Formats.Posit.Model.nar format

Configured arcTan2 propagates a NaR second coordinate.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan2_eq_nar_of_origin {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hx : toModel x = Formats.Posit.Model.zero format) (hy : toModel y = Formats.Posit.Model.zero format) : toModel (arcTan2 x y) = Formats.Posit.Model.nar format

Configured arcTan2 rejects the origin.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcTan2Pi {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (arcTan2Pi x y) = (toModel x).arcTan2Pi (toModel y)

Configured arcTan2Pi refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan2Pi_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) {a b : ℚ} (hx : toRat? x = some a) (hy : toRat? y = some b) (horigin : ¬(a = 0 ∧ b = 0)) : toModel (arcTan2Pi x y) = Formats.Posit.Model.RealRounding.round format ({ re := ↑a, im := ↑b }.arg / Real.pi)

Configured arcTan2Pi rounds the exact principal argument divided by pi.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan2Pi_eq_nar_left {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hx : toModel x = Formats.Posit.Model.nar format) : toModel (arcTan2Pi x y) = Formats.Posit.Model.nar format

Configured arcTan2Pi propagates a NaR first coordinate.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan2Pi_eq_nar_right {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hy : toModel y = Formats.Posit.Model.nar format) : toModel (arcTan2Pi x y) = Formats.Posit.Model.nar format

Configured arcTan2Pi propagates a NaR second coordinate.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan2Pi_eq_nar_of_origin {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (x y : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hx : toModel x = Formats.Posit.Model.zero format) (hy : toModel y = Formats.Posit.Model.zero format) : toModel (arcTan2Pi x y) = Formats.Posit.Model.nar format

Configured arcTan2Pi rejects the origin.