Angle between complex numbers

This file relates the Euclidean geometric notion of angle between complex numbers to the argument of their quotient.

TODO

Prove the corresponding results for oriented angles.

Tags

arc-length, arc-distance

theorem Complex.angle_eq_abs_arg {x : ℂ} {y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : InnerProductGeometry.angle x y = |Complex.arg (x / y)|

The angle between two non-zero complex numbers is the absolute value of the argument of their quotient.

Note that this does not hold when x or y is 0 as the LHS is π / 2 while the RHS is 0.

theorem Complex.angle_one_left {y : ℂ} (hy : y ≠ 0) : InnerProductGeometry.angle 1 y = |Complex.arg y|

theorem Complex.angle_one_right {x : ℂ} (hx : x ≠ 0) : InnerProductGeometry.angle x 1 = |Complex.arg x|

@[simp]

theorem Complex.angle_mul_left {a : ℂ} (ha : a ≠ 0) (x : ℂ) (y : ℂ) : InnerProductGeometry.angle (a * x) (a * y) = InnerProductGeometry.angle x y

@[simp]

theorem Complex.angle_mul_right {a : ℂ} (ha : a ≠ 0) (x : ℂ) (y : ℂ) : InnerProductGeometry.angle (x * a) (y * a) = InnerProductGeometry.angle x y

theorem Complex.angle_div_left_eq_angle_mul_right (a : ℂ) (x : ℂ) (y : ℂ) : InnerProductGeometry.angle (x / a) y = InnerProductGeometry.angle x (y * a)

theorem Complex.angle_div_right_eq_angle_mul_left (a : ℂ) (x : ℂ) (y : ℂ) : InnerProductGeometry.angle x (y / a) = InnerProductGeometry.angle (x * a) y

theorem Complex.angle_exp_exp (x : ℝ) (y : ℝ) : InnerProductGeometry.angle (Complex.exp (↑x * Complex.I)) (Complex.exp (↑y * Complex.I)) = |toIocMod Real.two_pi_pos (-Real.pi) (x - y)|

theorem Complex.angle_exp_one (x : ℝ) : InnerProductGeometry.angle (Complex.exp (↑x * Complex.I)) 1 = |toIocMod Real.two_pi_pos (-Real.pi) x|