# 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`

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

Equations

- x.arg = if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖) else if 0 ≤ x.im then Real.arcsin ((-x).im / ‖x‖) + Real.pi else Real.arcsin ((-x).im / ‖x‖) - Real.pi

Instances For

source
theorem Complex.sin_arg (x : ℂ) :
Real.sin x.arg = x.im / ‖x‖
source
theorem Complex.cos_arg {x : ℂ} (hx : x ≠ 0) :
Real.cos x.arg = x.re / ‖x‖
source
@[simp]
theorem Complex.norm_mul_exp_arg_mul_I (x : ℂ) :
↑‖x‖ * exp (↑x.arg * I) = x
source
@[simp]
theorem Complex.norm_mul_cos_add_sin_mul_I (x : ℂ) :
↑‖x‖ * (cos ↑x.arg + sin ↑x.arg * I) = x
source
@[simp]
theorem Complex.norm_mul_cos_arg (x : ℂ) :
‖x‖ * Real.cos x.arg = x.re
source
@[simp]
theorem Complex.norm_mul_sin_arg (x : ℂ) :
‖x‖ * Real.sin x.arg = x.im
source
theorem Complex.norm_eq_one_iff (z : ℂ) :
‖z‖ = 1 ↔ ∃ (θ : ℝ), exp (↑θ * I) = z
source
@[simp]
theorem Complex.range_exp_mul_I :
(Set.range fun (x : ℝ) => exp (↑x * I)) = Metric.sphere 0 1
source
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 = θ
source
theorem Complex.arg_cos_add_sin_mul_I {θ : ℝ} (hθ : θ ∈ Set.Ioc (-Real.pi) Real.pi) :
(cos ↑θ + sin ↑θ * I).arg = θ
source
theorem Complex.arg_exp_mul_I (θ : ℝ) :
(exp (↑θ * I)).arg = toIocMod ⋯ (-Real.pi) θ
source
@[simp]
theorem Complex.arg_zero :
arg 0 = 0
source
theorem Complex.ext_norm_arg {x y : ℂ} (h₁ : ‖x‖ = ‖y‖) (h₂ : x.arg = y.arg) :
x = y
source
theorem Complex.ext_norm_arg_iff {x y : ℂ} :
x = y ↔ ‖x‖ = ‖y‖ ∧ x.arg = y.arg
source
theorem Complex.arg_mem_Ioc (z : ℂ) :
z.arg ∈ Set.Ioc (-Real.pi) Real.pi
source
@[simp]
theorem Complex.range_arg :
Set.range arg = Set.Ioc (-Real.pi) Real.pi
source
theorem Complex.arg_le_pi (x : ℂ) :
x.arg ≤ Real.pi
source
theorem Complex.neg_pi_lt_arg (x : ℂ) :
-Real.pi < x.arg
source
theorem Complex.abs_arg_le_pi (z : ℂ) :
|z.arg| ≤ Real.pi
source
@[simp]
theorem Complex.arg_nonneg_iff {z : ℂ} :
0 ≤ z.arg ↔ 0 ≤ z.im
source
@[simp]
theorem Complex.arg_neg_iff {z : ℂ} :
z.arg < 0 ↔ z.im < 0
source
theorem Complex.arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) :
(↑r * x).arg = x.arg
source
theorem Complex.arg_mul_real {r : ℝ} (hr : 0 < r) (x : ℂ) :
(x * ↑r).arg = x.arg
source
theorem Complex.arg_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
x.arg = y.arg ↔ ↑‖y‖ / ↑‖x‖ * x = y
source
@[simp]
theorem Complex.arg_one :
arg 1 = 0
source
@[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`.

source
@[simp]
theorem Complex.arg_neg_one :
(-1).arg = Real.pi
source
@[simp]
theorem Complex.arg_I :
I.arg = Real.pi / 2
source
@[simp]
theorem Complex.arg_neg_I :
(-I).arg = -(Real.pi / 2)
source
@[simp]
theorem Complex.tan_arg (x : ℂ) :
Real.tan x.arg = x.im / x.re
source
theorem Complex.arg_ofReal_of_nonneg {x : ℝ} (hx : 0 ≤ x) :
(↑x).arg = 0
source
@[simp]
theorem Complex.natCast_arg {n : ℕ} :
(↑n).arg = 0
source
@[simp]
theorem Complex.ofNat_arg {n : ℕ} [n.AtLeastTwo] :
(OfNat.ofNat n).arg = 0
source
theorem Complex.arg_eq_zero_iff {z : ℂ} :
z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0
source
theorem Complex.arg_eq_zero_iff_zero_le {z : ℂ} :
z.arg = 0 ↔ 0 ≤ z
source
theorem Complex.arg_eq_pi_iff {z : ℂ} :
z.arg = Real.pi ↔ z.re < 0 ∧ z.im = 0
source
theorem Complex.arg_eq_pi_iff_lt_zero {z : ℂ} :
z.arg = Real.pi ↔ z < 0
source
theorem Complex.arg_lt_pi_iff {z : ℂ} :
z.arg < Real.pi ↔ 0 ≤ z.re ∨ z.im ≠ 0
source
theorem Complex.arg_ofReal_of_neg {x : ℝ} (hx : x < 0) :
(↑x).arg = Real.pi
source
theorem Complex.arg_eq_pi_div_two_iff {z : ℂ} :
z.arg = Real.pi / 2 ↔ z.re = 0 ∧ 0 < z.im
source
theorem Complex.arg_eq_neg_pi_div_two_iff {z : ℂ} :
z.arg = -(Real.pi / 2) ↔ z.re = 0 ∧ z.im < 0
source
theorem Complex.arg_of_re_nonneg {x : ℂ} (hx : 0 ≤ x.re) :
x.arg = Real.arcsin (x.im / ‖x‖)
source
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
source
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
source
theorem Complex.arg_of_im_nonneg_of_ne_zero {z : ℂ} (h₁ : 0 ≤ z.im) (h₂ : z ≠ 0) :
z.arg = Real.arccos (z.re / ‖z‖)
source
theorem Complex.arg_of_im_pos {z : ℂ} (hz : 0 < z.im) :
z.arg = Real.arccos (z.re / ‖z‖)
source
theorem Complex.arg_of_im_neg {z : ℂ} (hz : z.im < 0) :
z.arg = -Real.arccos (z.re / ‖z‖)
source
theorem Complex.arg_conj (x : ℂ) :
((starRingEnd ℂ) x).arg = if x.arg = Real.pi then Real.pi else -x.arg
source
theorem Complex.arg_inv (x : ℂ) :
x⁻¹.arg = if x.arg = Real.pi then Real.pi else -x.arg
source
@[simp]
theorem Complex.abs_arg_inv (x : ℂ) :
|x⁻¹.arg| = |x.arg|
source
theorem Complex.norm_eq_one_iff' {x : ℂ} :
‖x‖ = 1 ↔ ∃ θ ∈ Set.Ioc (-Real.pi) Real.pi, exp (↑θ * I) = x
source
theorem Complex.image_exp_Ioc_eq_sphere :
(fun (θ : ℝ) => exp (↑θ * I)) '' Set.Ioc (-Real.pi) Real.pi = Metric.sphere 0 1
source
theorem Complex.arg_le_pi_div_two_iff {z : ℂ} :
z.arg ≤ Real.pi / 2 ↔ 0 ≤ z.re ∨ z.im < 0
source
theorem Complex.neg_pi_div_two_le_arg_iff {z : ℂ} :
-(Real.pi / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
source
theorem Complex.neg_pi_div_two_lt_arg_iff {z : ℂ} :
-(Real.pi / 2) < z.arg ↔ 0 < z.re ∨ 0 ≤ z.im
source
theorem Complex.arg_lt_pi_div_two_iff {z : ℂ} :
z.arg < Real.pi / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
source
@[simp]
theorem Complex.abs_arg_le_pi_div_two_iff {z : ℂ} :
|z.arg| ≤ Real.pi / 2 ↔ 0 ≤ z.re
source
@[simp]
theorem Complex.abs_arg_lt_pi_div_two_iff {z : ℂ} :
|z.arg| < Real.pi / 2 ↔ 0 < z.re ∨ z = 0
source
@[simp]
theorem Complex.arg_conj_coe_angle (x : ℂ) :
↑((starRingEnd ℂ) x).arg = -↑x.arg
source
@[simp]
theorem Complex.arg_inv_coe_angle (x : ℂ) :
↑x⁻¹.arg = -↑x.arg
source
theorem Complex.arg_neg_eq_arg_sub_pi_of_im_pos {x : ℂ} (hi : 0 < x.im) :
(-x).arg = x.arg - Real.pi
source
theorem Complex.arg_neg_eq_arg_add_pi_of_im_neg {x : ℂ} (hi : x.im < 0) :
(-x).arg = x.arg + Real.pi
source
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
source
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
source
theorem Complex.arg_neg_coe_angle {x : ℂ} (hx : x ≠ 0) :
↑(-x).arg = ↑x.arg + ↑Real.pi
source
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) θ
source
theorem Complex.arg_cos_add_sin_mul_I_eq_toIocMod (θ : ℝ) :
(cos ↑θ + sin ↑θ * I).arg = toIocMod Real.two_pi_pos (-Real.pi) θ
source
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)⌋
source
theorem Complex.arg_cos_add_sin_mul_I_sub (θ : ℝ) :
(cos ↑θ + sin ↑θ * I).arg - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋
source
theorem Complex.arg_mul_cos_add_sin_mul_I_coe_angle {r : ℝ} (hr : 0 < r) (θ : Real.Angle) :
↑(↑r * (↑θ.cos + ↑θ.sin * I)).arg = θ
source
theorem Complex.arg_cos_add_sin_mul_I_coe_angle (θ : Real.Angle) :
↑(↑θ.cos + ↑θ.sin * I).arg = θ
source
theorem Complex.arg_mul_coe_angle {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
↑(x * y).arg = ↑x.arg + ↑y.arg
source
theorem Complex.arg_div_coe_angle {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
↑(x / y).arg = ↑x.arg - ↑y.arg
source
theorem Complex.arg_pow_coe_angle (x : ℂ) (n : ℕ) :
↑(x ^ n).arg = n • ↑x.arg
source
theorem Complex.arg_zpow_coe_angle (x : ℂ) (n : ℤ) :
↑(x ^ n).arg = n • ↑x.arg
source
@[simp]
theorem Complex.arg_coe_angle_toReal_eq_arg (z : ℂ) :
(↑z.arg).toReal = z.arg
source
theorem Complex.arg_coe_angle_eq_iff_eq_toReal {z : ℂ} {θ : Real.Angle} :
↑z.arg = θ ↔ z.arg = θ.toReal
source
@[simp]
theorem Complex.arg_coe_angle_eq_iff {x y : ℂ} :
↑x.arg = ↑y.arg ↔ x.arg = y.arg
source
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
source
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`.

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

source
theorem Complex.slitPlane_arg_ne_pi {z : ℂ} (hz : z ∈ slitPlane) :
z.arg ≠ Real.pi
source
theorem Complex.arg_eq_nhds_of_re_pos {x : ℂ} (hx : 0 < x.re) :
arg =ᶠ[nhds x] fun (x : ℂ) => Real.arcsin (x.im / ‖x‖)
source
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
source
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
source
theorem Complex.arg_eq_nhds_of_im_pos {z : ℂ} (hz : 0 < z.im) :
arg =ᶠ[nhds z] fun (x : ℂ) => Real.arccos (x.re / ‖x‖)
source
theorem Complex.arg_eq_nhds_of_im_neg {z : ℂ} (hz : z.im < 0) :
arg =ᶠ[nhds z] fun (x : ℂ) => -Real.arccos (x.re / ‖x‖)
source
theorem Complex.continuousAt_arg {x : ℂ} (h : x ∈ slitPlane) :
ContinuousAt arg x
source
theorem Complex.continuousOn_arg :
ContinuousOn arg slitPlane
source
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))
source
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
source
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)
source
theorem Complex.continuousAt_arg_coe_angle {x : ℂ} (h : x ≠ 0) :
ContinuousAt (Real.Angle.coe ∘ arg) x