Angle between complex numbers

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

It also shows that the arc and chord distances between two unit complex numbers are equivalent up to a factor of π / 2.

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 = |(x / y).arg|

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 = |y.arg|

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

@[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 (exp (↑x * I)) (exp (↑y * I)) = |toIocMod Real.two_pi_pos (-Real.pi) (x - y)|

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

Arc-length and chord-length are equivalent

This section shows that the arc and chord distances between two unit complex numbers are equivalent up to a factor of π / 2.

theorem Complex.norm_sub_mem_Icc_angle {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ‖x - y‖ ∈ Set.Icc (2 / Real.pi * InnerProductGeometry.angle x y) (InnerProductGeometry.angle x y)

Chord-length is a multiple of arc-length up to constants.

theorem Complex.norm_sub_le_angle {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : ‖x - y‖ ≤ InnerProductGeometry.angle x y

Chord-length is always less than arc-length.

theorem Complex.mul_angle_le_norm_sub {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : 2 / Real.pi * InnerProductGeometry.angle x y ≤ ‖x - y‖

Chord-length is always greater than a multiple of arc-length.

theorem Complex.angle_le_mul_norm_sub {x y : ℂ} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : InnerProductGeometry.angle x y ≤ Real.pi / 2 * ‖x - y‖

Arc-length is always less than a multiple of chord-length.