feat: port Analysis.Complex.Arg (#4355)

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Author: riccardobrasca

Mathlib.lean

@@ -413,6 +413,7 @@ import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 import Mathlib.Analysis.Calculus.FDeriv.Star
 import Mathlib.Analysis.Calculus.FormalMultilinearSeries
 import Mathlib.Analysis.Calculus.TangentCone
+import Mathlib.Analysis.Complex.Arg
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Complex.Circle
 import Mathlib.Analysis.Complex.Conformal

Mathlib/Analysis/Complex/Arg.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2022 Eric Rodriguez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Rodriguez
+
+! This file was ported from Lean 3 source module analysis.complex.arg
+! leanprover-community/mathlib commit 45a46f4f03f8ae41491bf3605e8e0e363ba192fd
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+
+/-!
+# Rays in the complex numbers
+
+This file links the definition `SameRay ℝ x y` with the equality of arguments of complex numbers,
+the usual way this is considered.
+
+## Main statements
+
+* `Complex.sameRay_iff` : Two complex numbers are on the same ray iff one of them is zero, or they
+  have the same argument.
+* `Complex.abs_add_eq/Complex.abs_sub_eq`: If two non zero complex numbers have the same argument,
+  then the triangle inequality is an equality.
+
+-/
+
+
+variable {x y : ℂ}
+
+namespace Complex
+
+theorem sameRay_iff : SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg := by
+  rcases eq_or_ne x 0 with (rfl | hx)
+  · simp
+  rcases eq_or_ne y 0 with (rfl | hy)
+  · simp
+  simp only [hx, hy, false_or_iff, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]
+  field_simp [hx, hy]
+  rw [mul_comm, eq_comm]
+#align complex.same_ray_iff Complex.sameRay_iff
+
+theorem sameRay_iff_arg_div_eq_zero : SameRay ℝ x y ↔ arg (x / y) = 0 := by
+  rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]
+  by_cases hx : x = 0; · simp [hx]
+  by_cases hy : y = 0; · simp [hy]
+  simp [hx, hy, arg_div_coe_angle, sub_eq_zero]
+#align complex.same_ray_iff_arg_div_eq_zero Complex.sameRay_iff_arg_div_eq_zero
+
+-- Porting note: `(x + y).abs` stopped working.
+theorem abs_add_eq_iff : abs (x + y) = abs x + abs y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
+  sameRay_iff_norm_add.symm.trans sameRay_iff
+#align complex.abs_add_eq_iff Complex.abs_add_eq_iff
+
+theorem abs_sub_eq_iff : abs (x - y) = |abs x - abs y| ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
+  sameRay_iff_norm_sub.symm.trans sameRay_iff
+#align complex.abs_sub_eq_iff Complex.abs_sub_eq_iff
+
+theorem sameRay_of_arg_eq (h : x.arg = y.arg) : SameRay ℝ x y :=
+  sameRay_iff.mpr <| Or.inr <| Or.inr h
+#align complex.same_ray_of_arg_eq Complex.sameRay_of_arg_eq
+
+theorem abs_add_eq (h : x.arg = y.arg) : abs (x + y) = abs x + abs y :=
+  (sameRay_of_arg_eq h).norm_add
+#align complex.abs_add_eq Complex.abs_add_eq
+
+theorem abs_sub_eq (h : x.arg = y.arg) : abs (x - y) = ‖abs x - abs y‖ :=
+  (sameRay_of_arg_eq h).norm_sub
+#align complex.abs_sub_eq Complex.abs_sub_eq
+
+end Complex

Mathlib/Analysis/Convex/StrictConvexSpace.lean

@@ -224,7 +224,7 @@ theorem not_sameRay_iff_norm_add_lt : ¬SameRay ℝ x y ↔ ‖x + y‖ < ‖x
 #align not_same_ray_iff_norm_add_lt not_sameRay_iff_norm_add_lt
 
 theorem sameRay_iff_norm_sub : SameRay ℝ x y ↔ ‖x - y‖ = |‖x‖ - ‖y‖| :=
-  ⟨SameRay.norm_sub (F := E), fun h =>
+  ⟨SameRay.norm_sub, fun h =>
     Classical.not_not.1 fun h' => (abs_lt_norm_sub_of_not_sameRay h').ne' h⟩
 #align same_ray_iff_norm_sub sameRay_iff_norm_sub
 

Mathlib/Analysis/NormedSpace/Ray.lean

@@ -43,7 +43,7 @@ theorem norm_sub (h : SameRay ℝ x y) : ‖x - y‖ = |‖x‖ - ‖y‖| := by
   wlog hab : b ≤ a with H
   · rw [SameRay.sameRay_comm] at h
     rw [norm_sub_rev, abs_sub_comm]
-    have := @H E _ _ F
+    have := @H E _ _ ℝ
     exact this u b a hb ha h (le_of_not_le hab)
   rw [← sub_nonneg] at hab
   rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, ←