feat: Angle between complex numbers (#10226)

Prove that the angle between two complex numbers is the absolute value of the argument of their quotient.

From LeanAPAP

Mathlib.lean

@@ -697,6 +697,7 @@ import Mathlib.Analysis.Calculus.Taylor
 import Mathlib.Analysis.Calculus.UniformLimitsDeriv
 import Mathlib.Analysis.Complex.AbelLimit
 import Mathlib.Analysis.Complex.AbsMax
+import Mathlib.Analysis.Complex.Angle
 import Mathlib.Analysis.Complex.Arg
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Complex.CauchyIntegral

Mathlib/Analysis/Complex/Angle.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
+
+/-!
+# 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
+-/
+
+open InnerProductGeometry
+open scoped Real
+
+namespace Complex
+variable {a 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`. -/
+lemma angle_eq_abs_arg (hx : x ≠ 0) (hy : y ≠ 0) : angle x y = |(x / y).arg| := by
+  refine Real.arccos_eq_of_eq_cos (abs_nonneg _) (abs_arg_le_pi _) ?_
+  rw [Real.cos_abs, Complex.cos_arg (div_ne_zero hx hy)]
+  have := (map_ne_zero Complex.abs).2 hx
+  have := (map_ne_zero Complex.abs).2 hy
+  simp [div_eq_mul_inv, Complex.normSq_eq_norm_sq]
+  field_simp
+  ring
+
+lemma angle_one_left (hy : y ≠ 0) : angle 1 y = |y.arg| := by simp [angle_eq_abs_arg, hy]
+lemma angle_one_right (hx : x ≠ 0) : angle x 1 = |x.arg| := by simp [angle_eq_abs_arg, hx]
+
+@[simp] lemma angle_mul_left (ha : a ≠ 0) (x y : ℂ) : angle (a * x) (a * y) = angle x y := by
+  obtain rfl | hx := eq_or_ne x 0 <;> obtain rfl | hy := eq_or_ne y 0 <;>
+    simp [angle_eq_abs_arg, mul_div_mul_left, *]
+
+@[simp] lemma angle_mul_right (ha : a ≠ 0) (x y : ℂ) : angle (x * a) (y * a) = angle x y := by
+  simp [mul_comm, angle_mul_left ha]
+
+lemma angle_div_left_eq_angle_mul_right (a x y : ℂ) : angle (x / a) y = angle x (y * a) := by
+  obtain rfl | ha := eq_or_ne a 0
+  · simp
+  · rw [← angle_mul_right ha, div_mul_cancel _ ha]
+
+lemma angle_div_right_eq_angle_mul_left (a x y : ℂ) : angle x (y / a) = angle (x * a) y := by
+  rw [angle_comm, angle_div_left_eq_angle_mul_right, angle_comm]
+
+lemma angle_exp_exp (x y : ℝ) :
+    angle (exp (x * I)) (exp (y * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)| := by
+  simp_rw [angle_eq_abs_arg (exp_ne_zero _) (exp_ne_zero _), ← exp_sub, ← sub_mul, ← ofReal_sub,
+    arg_exp_mul_I]
+
+lemma angle_exp_one (x : ℝ) : angle (exp (x * I)) 1 = |toIocMod Real.two_pi_pos (-π) x| := by
+  simpa using angle_exp_exp x 0
+
+end Complex

Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

@@ -16,14 +16,11 @@ such that for `x ≠ 0`, `sin (arg x) = x.im / x.abs` and `cos (arg x) = x.re /
 while `arg 0` defaults to `0`
 -/
 
-
-noncomputable section
+open Filter Metric Set
+open scoped ComplexConjugate Real Topology
 
 namespace Complex
-
-open ComplexConjugate Real Topology
-
-open Filter Set
+variable {a x z : ℂ}
 
 /-- `arg` returns values in the range (-π, π], such that for `x ≠ 0`,
   `sin (arg x) = x.im / x.abs` and `cos (arg x) = x.re / x.abs`,
@@ -123,6 +120,14 @@ theorem arg_cos_add_sin_mul_I {θ : ℝ} (hθ : θ ∈ Set.Ioc (-π) π) : arg (
 set_option linter.uppercaseLean3 false in
 #align complex.arg_cos_add_sin_mul_I Complex.arg_cos_add_sin_mul_I
 
+lemma arg_exp_mul_I (θ : ℝ) :
+    arg (exp (θ * I)) = toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ := by
+  convert arg_cos_add_sin_mul_I (θ := toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ) _ using 2
+  · rw [← exp_mul_I, eq_sub_of_add_eq $ toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
+      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
+  · convert toIocMod_mem_Ioc _ _ _
+    ring
+
 @[simp]
 theorem arg_zero : arg 0 = 0 := by simp [arg, le_refl]
 #align complex.arg_zero Complex.arg_zero
@@ -347,6 +352,24 @@ theorem arg_inv (x : ℂ) : arg x⁻¹ = if arg x = π then π else -arg x := by
   · exact arg_real_mul (conj x) (by simp [hx])
 #align complex.arg_inv Complex.arg_inv
 
+@[simp] lemma abs_arg_inv (x : ℂ) : |x⁻¹.arg| = |x.arg| := by rw [arg_inv]; split_ifs <;> simp [*]
+
+-- TODO: Replace the next two lemmas by general facts about periodic functions
+lemma abs_eq_one_iff' : abs x = 1 ↔ ∃ θ ∈ Set.Ioc (-π) π, exp (θ * I) = x := by
+  rw [abs_eq_one_iff]
+  constructor
+  · rintro ⟨θ, rfl⟩
+    refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
+    · convert toIocMod_mem_Ioc _ _ _
+      ring
+    · rw [eq_sub_of_add_eq $ toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
+      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
+  · rintro ⟨θ, _, rfl⟩
+    exact ⟨θ, rfl⟩
+
+lemma image_exp_Ioc_eq_sphere : (fun θ : ℝ ↦ exp (θ * I)) '' Set.Ioc (-π) π = sphere 0 1 := by
+  ext; simpa using abs_eq_one_iff'.symm
+
 theorem arg_le_pi_div_two_iff {z : ℂ} : arg z ≤ π / 2 ↔ 0 ≤ re z ∨ im z < 0 := by
   rcases le_or_lt 0 (re z) with hre | hre
   · simp only [hre, arg_of_re_nonneg hre, Real.arcsin_le_pi_div_two, true_or_iff]
@@ -568,8 +591,6 @@ end slitPlane
 
 section Continuity
 
-variable {x z : ℂ}
-
 theorem arg_eq_nhds_of_re_pos (hx : 0 < x.re) : arg =ᶠ[𝓝 x] fun x => Real.arcsin (x.im / abs x) :=
   ((continuous_re.tendsto _).eventually (lt_mem_nhds hx)).mono fun _ hy => arg_of_re_nonneg hy.le
 #align complex.arg_eq_nhds_of_re_pos Complex.arg_eq_nhds_of_re_pos

Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

@@ -27,6 +27,7 @@ open Set Filter
 open Real
 
 namespace Real
+variable {x y : ℝ}
 
 /-- Inverse of the `sin` function, returns values in the range `-π / 2 ≤ arcsin x ≤ π / 2`.
 It defaults to `-π / 2` on `(-∞, -1)` and to `π / 2` to `(1, ∞)`. -/
@@ -363,6 +364,9 @@ theorem arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ π) : arccos (cos
   rw [arccos, ← sin_pi_div_two_sub, arcsin_sin] <;> simp [sub_eq_add_neg] <;> linarith
 #align real.arccos_cos Real.arccos_cos
 
+lemma arccos_eq_of_eq_cos (hy₀ : 0 ≤ y) (hy₁ : y ≤ π) (hxy : x = cos y) : arccos x = y := by
+  rw [hxy, arccos_cos hy₀ hy₁]
+
 theorem strictAntiOn_arccos : StrictAntiOn arccos (Icc (-1) 1) := fun _ hx _ hy h =>
   sub_lt_sub_left (strictMonoOn_arcsin hx hy h) _
 #align real.strict_anti_on_arccos Real.strictAntiOn_arccos

Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean

@@ -20,6 +20,9 @@ This file defines unoriented angles in Euclidean affine spaces.
 * `EuclideanGeometry.angle`, with notation `∠`, is the undirected angle determined by three
   points.
 
+## TODO
+
+Prove the triangle inequality for the angle.
 -/
 
 
@@ -31,8 +34,8 @@ namespace EuclideanGeometry
 
 open InnerProductGeometry
 
-variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
-  [NormedAddTorsor V P]
+variable {V P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
+  [NormedAddTorsor V P] {p p₀ p₁ p₂ : P}
 
 /-- The undirected angle at `p2` between the line segments to `p1` and
 `p3`. If either of those points equals `p2`, this is π/2. Use
@@ -139,21 +142,25 @@ nonrec theorem angle_le_pi (p1 p2 p3 : P) : ∠ p1 p2 p3 ≤ π :=
   angle_le_pi _ _
 #align euclidean_geometry.angle_le_pi EuclideanGeometry.angle_le_pi
 
-/-- The angle ∠AAB at a point. -/
-theorem angle_eq_left (p1 p2 : P) : ∠ p1 p1 p2 = π / 2 := by
+/-- The angle ∠AAB at a point is always `π / 2`. -/
+@[simp] lemma angle_self_left (p₀ p : P) : ∠ p₀ p₀ p = π / 2 := by
   unfold angle
   rw [vsub_self]
   exact angle_zero_left _
-#align euclidean_geometry.angle_eq_left EuclideanGeometry.angle_eq_left
+#align euclidean_geometry.angle_eq_left EuclideanGeometry.angle_self_left
+
+/-- The angle ∠ABB at a point is always `π / 2`. -/
+@[simp] lemma angle_self_right (p₀ p : P) : ∠ p p₀ p₀ = π / 2 := by rw [angle_comm, angle_self_left]
+#align euclidean_geometry.angle_eq_right EuclideanGeometry.angle_self_right
 
-/-- The angle ∠ABB at a point. -/
-theorem angle_eq_right (p1 p2 : P) : ∠ p1 p2 p2 = π / 2 := by rw [angle_comm, angle_eq_left]
-#align euclidean_geometry.angle_eq_right EuclideanGeometry.angle_eq_right
+/-- The angle ∠ABA at a point is `0`, unless `A = B`. -/
+theorem angle_self_of_ne (h : p ≠ p₀) : ∠ p p₀ p = 0 := angle_self $ vsub_ne_zero.2 h
+#align euclidean_geometry.angle_eq_of_ne EuclideanGeometry.angle_self_of_ne
 
-/-- The angle ∠ABA at a point. -/
-theorem angle_eq_of_ne {p1 p2 : P} (h : p1 ≠ p2) : ∠ p1 p2 p1 = 0 :=
-  angle_self fun he => h (vsub_eq_zero_iff_eq.1 he)
-#align euclidean_geometry.angle_eq_of_ne EuclideanGeometry.angle_eq_of_ne
+-- 2024-02-14
+@[deprecated] alias angle_eq_left := angle_self_left
+@[deprecated] alias angle_eq_right := angle_self_right
+@[deprecated] alias angle_eq_of_ne := angle_self_of_ne
 
 /-- If the angle ∠ABC at a point is π, the angle ∠BAC is 0. -/
 theorem angle_eq_zero_of_angle_eq_pi_left {p1 p2 p3 : P} (h : ∠ p1 p2 p3 = π) : ∠ p2 p1 p3 = 0 := by
@@ -207,7 +214,7 @@ theorem angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi {p1 p2 p3 p4 p5 : P} (hapc
 theorem left_dist_ne_zero_of_angle_eq_pi {p1 p2 p3 : P} (h : ∠ p1 p2 p3 = π) : dist p1 p2 ≠ 0 := by
   by_contra heq
   rw [dist_eq_zero] at heq
-  rw [heq, angle_eq_left] at h
+  rw [heq, angle_self_left] at h
   exact Real.pi_ne_zero (by linarith)
 #align euclidean_geometry.left_dist_ne_zero_of_angle_eq_pi EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi
 

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

@@ -17,6 +17,9 @@ This file defines unoriented angles in real inner product spaces.
 
 * `InnerProductGeometry.angle` is the undirected angle between two vectors.
 
+## TODO
+
+Prove the triangle inequality for the angle.
 -/
 
 
@@ -112,6 +115,8 @@ theorem angle_neg_left (x y : V) : angle (-x) y = π - angle x y := by
   rw [← angle_neg_neg, neg_neg, angle_neg_right]
 #align inner_product_geometry.angle_neg_left InnerProductGeometry.angle_neg_left
 
+proof_wanted angle_triangle (x y z : V) : angle x z ≤ angle x y + angle y z
+
 /-- The angle between the zero vector and a vector. -/
 @[simp]
 theorem angle_zero_left (x : V) : angle 0 x = π / 2 := by