Real rounding and exceptional cases for posit two-coordinate arctangent

The operations round the exact principal complex argument, in radians or divided by pi, including its value on the negative real axis. NaR and the origin are rejected before the comparison search.

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateArgument_eq_real (prepare : ℚ → ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) (function : ℝ → ℝ → ℝ) (hprepare : ∀ (a b : ℚ) (levels : ℕ) (boundary : ℚ), (prepare a b levels).compare boundary = cmp (function ↑a ↑b) ↑boundary) {format : Format} (x y : Model format) {a b : ℚ} (hx : x.toRat? = some a) (hy : y.toRat? = some b) (horigin : ¬(a = 0 ∧ b = 0)) : evaluateArgument prepare x y = RealRounding.round format (function ↑a ↑b)

An exact two-coordinate comparator gives the standard rounding away from the origin.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateArgument_nar_left (prepare : ℚ → ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) {format : Format} (y : Model format) : evaluateArgument prepare (nar format) y = nar format

A NaR first coordinate propagates.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateArgument_nar_right (prepare : ℚ → ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) {format : Format} (x : Model format) : evaluateArgument prepare x (nar format) = nar format

A NaR second coordinate propagates.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateArgument_origin (prepare : ℚ → ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) {format : Format} : evaluateArgument prepare (zero format) (zero format) = nar format

The origin is outside the posit operation's domain.

theorem FloatLib.Floats.Formats.Posit.Model.arcTan2_eq_real {format : Format} (x y : Model format) {a b : ℚ} (hx : x.toRat? = some a) (hy : y.toRat? = some b) (horigin : ¬(a = 0 ∧ b = 0)) : x.arcTan2 y = RealRounding.round format { re := ↑a, im := ↑b }.arg

Two-coordinate arctangent rounds the exact principal angle of a + i*b.

theorem FloatLib.Floats.Formats.Posit.Model.arcTan2Pi_eq_real {format : Format} (x y : Model format) {a b : ℚ} (hx : x.toRat? = some a) (hy : y.toRat? = some b) (horigin : ¬(a = 0 ∧ b = 0)) : x.arcTan2Pi y = RealRounding.round format ({ re := ↑a, im := ↑b }.arg / Real.pi)

Pi-scaled two-coordinate arctangent divides the exact angle before rounding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcTan2_nar_left {format : Format} (y : Model format) : (nar format).arcTan2 y = nar format

arcTan2 propagates a NaR first coordinate.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcTan2_nar_right {format : Format} (x : Model format) : x.arcTan2 (nar format) = nar format

arcTan2 propagates a NaR second coordinate.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcTan2_origin {format : Format} : (zero format).arcTan2 (zero format) = nar format

arcTan2 rejects the origin.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcTan2Pi_nar_left {format : Format} (y : Model format) : (nar format).arcTan2Pi y = nar format

arcTan2Pi propagates a NaR first coordinate.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcTan2Pi_nar_right {format : Format} (x : Model format) : x.arcTan2Pi (nar format) = nar format

arcTan2Pi propagates a NaR second coordinate.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcTan2Pi_origin {format : Format} : (zero format).arcTan2Pi (zero format) = nar format

arcTan2Pi rejects the origin.