Documentation

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

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

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

@[deprecated Complex.norm_mul_exp_arg_mul_I (since := "2025-02-16")]

theorem Complex.abs_mul_exp_arg_mul_I (x : ℂ) :

↑‖x‖ * exp (↑x.arg * I) = x

Alias of Complex.norm_mul_exp_arg_mul_I.

@[deprecated Complex.norm_mul_cos_add_sin_mul_I (since := "2025-02-16")]

theorem Complex.abs_mul_cos_add_sin_mul_I (x : ℂ) :

↑‖x‖ * (cos ↑x.arg + sin ↑x.arg * I) = x

Alias of Complex.norm_mul_cos_add_sin_mul_I.

@[deprecated Complex.norm_mul_cos_arg (since := "2025-02-16")]

theorem Complex.abs_mul_cos_arg (x : ℂ) :

‖x‖ * Real.cos x.arg = x.re

Alias of Complex.norm_mul_cos_arg.

@[deprecated Complex.norm_mul_sin_arg (since := "2025-02-16")]

theorem Complex.abs_mul_sin_arg (x : ℂ) :

‖x‖ * Real.sin x.arg = x.im

Alias of Complex.norm_mul_sin_arg.

@[deprecated Complex.norm_eq_one_iff (since := "2025-02-16")]

theorem Complex.abs_eq_one_iff (z : ℂ) :

‖z‖ = 1 ↔ ∃ (θ : ℝ), exp (↑θ * I) = z

Alias of Complex.norm_eq_one_iff.

@[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_mul_I (θ : ℝ) :

(exp (↑θ * I)).arg = toIocMod ⋯ (-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

@[deprecated Complex.ext_norm_arg (since := "2025-02-16")]

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

x = y

Alias of Complex.ext_norm_arg.

@[deprecated Complex.ext_norm_arg_iff (since := "2025-02-16")]

theorem Complex.ext_abs_arg_iff {x y : ℂ} :

x = y ↔ ‖x‖ = ‖y‖ ∧ x.arg = y.arg

Alias of Complex.ext_norm_arg_iff.

theorem Complex.arg_mem_Ioc (z : ℂ) :

z.arg ∈ Set.Ioc (-Real.pi) Real.pi

@[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

@[deprecated Complex.norm_eq_one_iff' (since := "2025-02-16")]

theorem Complex.abs_eq_one_iff' {x : ℂ} :

‖x‖ = 1 ↔ ∃ θ ∈ Set.Ioc (-Real.pi) Real.pi, exp (↑θ * I) = x

Alias of Complex.norm_eq_one_iff'.

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

@[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.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.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