The argument of a complex number.

We define arg : ℂ → ℝ, returning a real number in the range $(-π, π]$, such that for x ≠ 0, sin (arg x) = x.im / x.abs and cos (arg x) = x.re / x.abs, while arg 0 defaults to 0

noncomputable def Complex.arg (x : ℂ) : ℝ

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, arg 0 defaults to 0

theorem Complex.sin_arg (x : ℂ) : Real.sin x.arg = x.im / ‖x‖

theorem Complex.cos_arg {x : ℂ} (hx : x ≠ 0) : Real.cos x.arg = x.re / ‖x‖

@[simp]

theorem Complex.norm_mul_exp_arg_mul_I (x : ℂ) : ↑‖x‖ * exp (↑x.arg * I) = x

@[simp]

theorem Complex.norm_mul_cos_add_sin_mul_I (x : ℂ) : ↑‖x‖ * (cos ↑x.arg + sin ↑x.arg * I) = x

@[simp]

theorem Complex.norm_mul_cos_arg (x : ℂ) : ‖x‖ * Real.cos x.arg = x.re

@[simp]

theorem Complex.norm_mul_sin_arg (x : ℂ) : ‖x‖ * Real.sin x.arg = x.im

theorem Complex.norm_eq_one_iff (z : ℂ) : ‖z‖ = 1 ↔ ∃ (θ : ℝ), exp (↑θ * I) = z

@[simp]

theorem Complex.range_exp_mul_I : (Set.range fun (x : ℝ) => exp (↑x * I)) = Metric.sphere 0 1

theorem Complex.arg_mul_cos_add_sin_mul_I {r : ℝ} (hr : 0 < r) {θ : ℝ} (hθ : θ ∈ Set.Ioc (-Real.pi) Real.pi) : (↑r * (cos ↑θ + sin ↑θ * I)).arg = θ

theorem Complex.arg_cos_add_sin_mul_I {θ : ℝ} (hθ : θ ∈ Set.Ioc (-Real.pi) Real.pi) : (cos ↑θ + sin ↑θ * I).arg = θ

theorem Complex.arg_exp (z : ℂ) : (exp z).arg = toIocMod Real.two_pi_pos (-Real.pi) z.im

theorem Complex.arg_exp_mul_I (θ : ℝ) : (exp (↑θ * I)).arg = toIocMod Real.two_pi_pos (-Real.pi) θ

@[simp]

theorem Complex.arg_zero : arg 0 = 0

theorem Complex.ext_norm_arg {x y : ℂ} (h₁ : ‖x‖ = ‖y‖) (h₂ : x.arg = y.arg) : x = y

theorem Complex.ext_norm_arg_iff {x y : ℂ} : x = y ↔ ‖x‖ = ‖y‖ ∧ x.arg = y.arg

theorem Complex.arg_mem_Ioc (z : ℂ) : z.arg ∈ Set.Ioc (-Real.pi) Real.pi

@[simp]

theorem Complex.toIocMod_arg (z : ℂ) : toIocMod Real.two_pi_pos (-Real.pi) z.arg = z.arg

@[simp]

theorem Complex.range_arg : Set.range arg = Set.Ioc (-Real.pi) Real.pi

theorem Complex.arg_le_pi (x : ℂ) : x.arg ≤ Real.pi

theorem Complex.neg_pi_lt_arg (x : ℂ) : -Real.pi < x.arg

theorem Complex.abs_arg_le_pi (z : ℂ) : |z.arg| ≤ Real.pi

@[simp]

theorem Complex.arg_nonneg_iff {z : ℂ} : 0 ≤ z.arg ↔ 0 ≤ z.im

@[simp]

theorem Complex.arg_neg_iff {z : ℂ} : z.arg < 0 ↔ z.im < 0

theorem Complex.arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) : (↑r * x).arg = x.arg

theorem Complex.arg_mul_real {r : ℝ} (hr : 0 < r) (x : ℂ) : (x * ↑r).arg = x.arg

theorem Complex.arg_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : x.arg = y.arg ↔ ↑‖y‖ / ↑‖x‖ * x = y

@[simp]

theorem Complex.arg_one : arg 1 = 0

@[simp]

theorem Complex.arg_div_self (x : ℂ) : (x / x).arg = 0

This holds true for all x : ℂ because of the junk values 0 / 0 = 0 and arg 0 = 0.

@[simp]

theorem Complex.arg_neg_one : (-1).arg = Real.pi

@[simp]

theorem Complex.arg_I : I.arg = Real.pi / 2

@[simp]

theorem Complex.arg_neg_I : (-I).arg = -(Real.pi / 2)

@[simp]

theorem Complex.tan_arg (x : ℂ) : Real.tan x.arg = x.im / x.re

theorem Complex.arg_ofReal_of_nonneg {x : ℝ} (hx : 0 ≤ x) : (↑x).arg = 0

@[simp]

theorem Complex.natCast_arg {n : ℕ} : (↑n).arg = 0

@[simp]

theorem Complex.ofNat_arg {n : ℕ} [n.AtLeastTwo] : (OfNat.ofNat n).arg = 0

theorem Complex.arg_eq_zero_iff {z : ℂ} : z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0

theorem Complex.arg_eq_zero_iff_zero_le {z : ℂ} : z.arg = 0 ↔ 0 ≤ z

theorem Complex.arg_eq_pi_iff {z : ℂ} : z.arg = Real.pi ↔ z.re < 0 ∧ z.im = 0

theorem Complex.arg_eq_pi_iff_lt_zero {z : ℂ} : z.arg = Real.pi ↔ z < 0

theorem Complex.arg_lt_pi_iff {z : ℂ} : z.arg < Real.pi ↔ 0 ≤ z.re ∨ z.im ≠ 0

theorem Complex.arg_ofReal_of_neg {x : ℝ} (hx : x < 0) : (↑x).arg = Real.pi

theorem Complex.arg_eq_pi_div_two_iff {z : ℂ} : z.arg = Real.pi / 2 ↔ z.re = 0 ∧ 0 < z.im

theorem Complex.arg_eq_neg_pi_div_two_iff {z : ℂ} : z.arg = -(Real.pi / 2) ↔ z.re = 0 ∧ z.im < 0

theorem Complex.arg_of_re_nonneg {x : ℂ} (hx : 0 ≤ x.re) : x.arg = Real.arcsin (x.im / ‖x‖)

theorem Complex.arg_of_re_neg_of_im_nonneg {x : ℂ} (hx_re : x.re < 0) (hx_im : 0 ≤ x.im) : x.arg = Real.arcsin ((-x).im / ‖x‖) + Real.pi

theorem Complex.arg_of_re_neg_of_im_neg {x : ℂ} (hx_re : x.re < 0) (hx_im : x.im < 0) : x.arg = Real.arcsin ((-x).im / ‖x‖) - Real.pi

theorem Complex.arg_of_im_nonneg_of_ne_zero {z : ℂ} (h₁ : 0 ≤ z.im) (h₂ : z ≠ 0) : z.arg = Real.arccos (z.re / ‖z‖)

theorem Complex.arg_of_im_pos {z : ℂ} (hz : 0 < z.im) : z.arg = Real.arccos (z.re / ‖z‖)

theorem Complex.arg_of_im_neg {z : ℂ} (hz : z.im < 0) : z.arg = -Real.arccos (z.re / ‖z‖)

theorem Complex.arg_conj (x : ℂ) : ((starRingEnd ℂ) x).arg = if x.arg = Real.pi then Real.pi else -x.arg

theorem Complex.arg_inv (x : ℂ) : x⁻¹.arg = if x.arg = Real.pi then Real.pi else -x.arg

@[simp]

theorem Complex.abs_arg_inv (x : ℂ) : |x⁻¹.arg| = |x.arg|

theorem Complex.norm_eq_one_iff' {x : ℂ} : ‖x‖ = 1 ↔ ∃ θ ∈ Set.Ioc (-Real.pi) Real.pi, exp (↑θ * I) = x

theorem Complex.image_exp_Ioc_eq_sphere : (fun (θ : ℝ) => exp (↑θ * I)) '' Set.Ioc (-Real.pi) Real.pi = Metric.sphere 0 1

theorem Complex.arg_le_pi_div_two_iff {z : ℂ} : z.arg ≤ Real.pi / 2 ↔ 0 ≤ z.re ∨ z.im < 0

theorem Complex.neg_pi_div_two_le_arg_iff {z : ℂ} : -(Real.pi / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

theorem Complex.neg_pi_div_two_lt_arg_iff {z : ℂ} : -(Real.pi / 2) < z.arg ↔ 0 < z.re ∨ 0 ≤ z.im

theorem Complex.arg_lt_pi_div_two_iff {z : ℂ} : z.arg < Real.pi / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

@[simp]

theorem Complex.abs_arg_le_pi_div_two_iff {z : ℂ} : |z.arg| ≤ Real.pi / 2 ↔ 0 ≤ z.re

@[simp]

theorem Complex.abs_arg_lt_pi_div_two_iff {z : ℂ} : |z.arg| < Real.pi / 2 ↔ 0 < z.re ∨ z = 0

@[simp]

theorem Complex.arg_conj_coe_angle (x : ℂ) : ↑((starRingEnd ℂ) x).arg = -↑x.arg

@[simp]

theorem Complex.arg_inv_coe_angle (x : ℂ) : ↑x⁻¹.arg = -↑x.arg

theorem Complex.arg_neg_eq_arg_sub_pi_of_im_pos {x : ℂ} (hi : 0 < x.im) : (-x).arg = x.arg - Real.pi

theorem Complex.arg_neg_eq_arg_add_pi_of_im_neg {x : ℂ} (hi : x.im < 0) : (-x).arg = x.arg + Real.pi

theorem Complex.arg_neg_eq_arg_sub_pi_iff {x : ℂ} : (-x).arg = x.arg - Real.pi ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

theorem Complex.arg_neg_eq_arg_add_pi_iff {x : ℂ} : (-x).arg = x.arg + Real.pi ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re

theorem Complex.arg_neg_coe_angle {x : ℂ} (hx : x ≠ 0) : ↑(-x).arg = ↑x.arg + ↑Real.pi

theorem Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod {r : ℝ} (hr : 0 < r) (θ : ℝ) : (↑r * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-Real.pi) θ

theorem Complex.arg_cos_add_sin_mul_I_eq_toIocMod (θ : ℝ) : (cos ↑θ + sin ↑θ * I).arg = toIocMod Real.two_pi_pos (-Real.pi) θ

theorem Complex.arg_mul_cos_add_sin_mul_I_sub {r : ℝ} (hr : 0 < r) (θ : ℝ) : (↑r * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋

theorem Complex.arg_cos_add_sin_mul_I_sub (θ : ℝ) : (cos ↑θ + sin ↑θ * I).arg - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋

theorem Complex.arg_mul_cos_add_sin_mul_I_coe_angle {r : ℝ} (hr : 0 < r) (θ : Real.Angle) : ↑(↑r * (↑θ.cos + ↑θ.sin * I)).arg = θ

theorem Complex.arg_cos_add_sin_mul_I_coe_angle (θ : Real.Angle) : ↑(↑θ.cos + ↑θ.sin * I).arg = θ

theorem Complex.arg_mul_coe_angle {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : ↑(x * y).arg = ↑x.arg + ↑y.arg

theorem Complex.arg_div_coe_angle {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) : ↑(x / y).arg = ↑x.arg - ↑y.arg

theorem Complex.arg_pow_coe_angle (x : ℂ) (n : ℕ) : ↑(x ^ n).arg = n • ↑x.arg

theorem Complex.arg_zpow_coe_angle (x : ℂ) (n : ℤ) : ↑(x ^ n).arg = n • ↑x.arg

@[simp]

theorem Complex.arg_coe_angle_toReal_eq_arg (z : ℂ) : (↑z.arg).toReal = z.arg

theorem Complex.arg_coe_angle_eq_iff_eq_toReal {z : ℂ} {θ : Real.Angle} : ↑z.arg = θ ↔ z.arg = θ.toReal

@[simp]

theorem Complex.arg_coe_angle_eq_iff {x y : ℂ} : ↑x.arg = ↑y.arg ↔ x.arg = y.arg

theorem Complex.arg_mul_eq_add_arg_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) : (x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi

theorem Complex.arg_mul {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) : x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi → (x * y).arg = x.arg + y.arg

Alias of the reverse direction of Complex.arg_mul_eq_add_arg_iff.

theorem Complex.mem_slitPlane_iff_arg {z : ℂ} : z ∈ slitPlane ↔ z.arg ≠ Real.pi ∧ z ≠ 0

An alternative description of the slit plane as consisting of nonzero complex numbers whose argument is not π.

theorem Complex.slitPlane_arg_ne_pi {z : ℂ} (hz : z ∈ slitPlane) : z.arg ≠ Real.pi

theorem Complex.exp_mem_slitPlane {z : ℂ} : exp z ∈ slitPlane ↔ toIocMod Real.two_pi_pos (-Real.pi) z.im ≠ Real.pi

theorem Complex.arg_eq_nhds_of_re_pos {x : ℂ} (hx : 0 < x.re) : arg =ᶠ[nhds x] fun (x : ℂ) => Real.arcsin (x.im / ‖x‖)

theorem Complex.arg_eq_nhds_of_re_neg_of_im_pos {x : ℂ} (hx_re : x.re < 0) (hx_im : 0 < x.im) : arg =ᶠ[nhds x] fun (x : ℂ) => Real.arcsin ((-x).im / ‖x‖) + Real.pi

theorem Complex.arg_eq_nhds_of_re_neg_of_im_neg {x : ℂ} (hx_re : x.re < 0) (hx_im : x.im < 0) : arg =ᶠ[nhds x] fun (x : ℂ) => Real.arcsin ((-x).im / ‖x‖) - Real.pi

theorem Complex.arg_eq_nhds_of_im_pos {z : ℂ} (hz : 0 < z.im) : arg =ᶠ[nhds z] fun (x : ℂ) => Real.arccos (x.re / ‖x‖)

theorem Complex.arg_eq_nhds_of_im_neg {z : ℂ} (hz : z.im < 0) : arg =ᶠ[nhds z] fun (x : ℂ) => -Real.arccos (x.re / ‖x‖)

theorem Complex.continuousAt_arg {x : ℂ} (h : x ∈ slitPlane) : ContinuousAt arg x

theorem Complex.continuousOn_arg : ContinuousOn arg slitPlane

theorem Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : Filter.Tendsto arg (nhdsWithin z {z : ℂ | z.im < 0}) (nhds (-Real.pi))

theorem Complex.continuousWithinAt_arg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : ContinuousWithinAt arg {z : ℂ | 0 ≤ z.im} z

theorem Complex.tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : Filter.Tendsto arg (nhdsWithin z {z : ℂ | 0 ≤ z.im}) (nhds Real.pi)

theorem Complex.continuousAt_arg_coe_angle {x : ℂ} (h : x ≠ 0) : ContinuousAt (Real.Angle.coe ∘ arg) x