Documentation

Mathlib.Analysis.Complex.Angle

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

source
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.

source
theorem Complex.angle_one_left {y : ℂ} (hy : y ≠ 0) :
InnerProductGeometry.angle 1 y = |y.arg|
source
theorem Complex.angle_one_right {x : ℂ} (hx : x ≠ 0) :
InnerProductGeometry.angle x 1 = |x.arg|
source
@[simp]
theorem Complex.angle_mul_left {a : ℂ} (ha : a ≠ 0) (x : ℂ) (y : ℂ) :
InnerProductGeometry.angle (a * x) (a * y) = InnerProductGeometry.angle x y
source
@[simp]
theorem Complex.angle_mul_right {a : ℂ} (ha : a ≠ 0) (x : ℂ) (y : ℂ) :
InnerProductGeometry.angle (x * a) (y * a) = InnerProductGeometry.angle x y
source
theorem Complex.angle_div_left_eq_angle_mul_right (a : ℂ) (x : ℂ) (y : ℂ) :
InnerProductGeometry.angle (x / a) y = InnerProductGeometry.angle x (y * a)
source
theorem Complex.angle_div_right_eq_angle_mul_left (a : ℂ) (x : ℂ) (y : ℂ) :
InnerProductGeometry.angle x (y / a) = InnerProductGeometry.angle (x * a) y
source
theorem Complex.angle_exp_exp (x : ℝ) (y : ℝ) :
InnerProductGeometry.angle (↑x * Complex.I).exp (↑y * Complex.I).exp = |toIocMod Real.two_pi_pos (-Real.pi) (x - y)|
source
theorem Complex.angle_exp_one (x : ℝ) :
InnerProductGeometry.angle (↑x * Complex.I).exp 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.

source
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.

source
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.

source
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.

source
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.