Principal-branch identities for the complex argument

The tangent inverse is applied only after locating the argument in its open principal branch. These identities include the real and imaginary axes and Mathlib's totalization at the origin.

theorem FloatLib.Numerics.TrigonometricComparison.arg_of_pos (x y : ℝ) (hx : 0 < x) : { re := x, im := y }.arg = Real.arctan (y / x)

A positive real component places the argument in the open arctangent branch.

theorem FloatLib.Numerics.TrigonometricComparison.arg_of_neg_nonneg (x y : ℝ) (hx : x < 0) (hy : 0 ≤ y) : { re := x, im := y }.arg = Real.arctan (y / x) + Real.pi

The upper left quadrant, including the negative real axis, adds π to the arctangent.

theorem FloatLib.Numerics.TrigonometricComparison.arg_of_neg_neg (x y : ℝ) (hx : x < 0) (hy : y < 0) : { re := x, im := y }.arg = Real.arctan (y / x) - Real.pi

The lower left quadrant subtracts π from the arctangent.

theorem FloatLib.Numerics.TrigonometricComparison.arg_formula (x y : ℝ) : { re := x, im := y }.arg = if 0 < x then Real.arctan (y / x) else if x < 0 then if 0 ≤ y then Real.arctan (y / x) + Real.pi else Real.arctan (y / x) - Real.pi else if 0 < y then Real.pi / 2 else if y < 0 then -(Real.pi / 2) else 0

The arctangent formula for the principal argument, including both axes and the origin.

theorem FloatLib.Numerics.TrigonometricComparison.atan2Reduction_eq_arg (x y : ℚ) : Real.arctan ↑(atan2Reduction x y).1 + ↑(atan2Reduction x y).2 * (Real.pi / 4) = { re := ↑x, im := ↑y }.arg

Rational quadrant reduction equals the exact principal complex argument.