mathlib documentation

analysis.special_functions.complex.arg

The argument of a complex number. #

We define arg : ℂ → ℝ, returing 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

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 = ite (0 ≤ x.re) (real.arcsin (x.im / complex.abs x)) (ite (0 ≤ x.im) (real.arcsin ((-x).im / complex.abs x) + π) (real.arcsin ((-x).im / complex.abs x) - π))

theorem complex.arg_le_pi (x : ℂ) :

theorem complex.neg_pi_lt_arg (x : ℂ) :

theorem complex.arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg {x : ℂ} (hxr : x.re < 0) (hxi : 0 ≤ x.im) :

x.arg = (-x).arg + π

theorem complex.arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg {x : ℂ} (hxr : x.re < 0) (hxi : x.im < 0) :

x.arg = (-x).arg - π

@[simp]

theorem complex.arg_zero :

0.arg = 0

@[simp]

theorem complex.arg_one :

1.arg = 0

@[simp]

theorem complex.arg_neg_one :

(-1).arg = π

@[simp]

theorem complex.arg_I :

complex.I.arg = π / 2

@[simp]

theorem complex.arg_neg_I :

(-complex.I).arg = -(π / 2)

theorem complex.sin_arg (x : ℂ) :

real.sin x.arg = x.im / complex.abs x

theorem complex.cos_arg {x : ℂ} (hx : x ≠ 0) :

real.cos x.arg = x.re / complex.abs x

theorem complex.tan_arg {x : ℂ} :

real.tan x.arg = x.im / x.re

theorem complex.arg_cos_add_sin_mul_I {x : ℝ} (hx₁ : -π < x) (hx₂ : x ≤ π) :

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

theorem complex.arg_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :

x.arg = y.arg ↔ (↑(complex.abs y) / ↑(complex.abs x)) * x = y

theorem complex.arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) :

((↑r) * x).arg = x.arg

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

x = y

theorem complex.arg_of_real_of_nonneg {x : ℝ} (hx : 0 ≤ x) :

theorem complex.arg_eq_pi_iff {z : ℂ} :

z.arg = π ↔ z.re < 0 ∧ z.im = 0

theorem complex.arg_of_real_of_neg {x : ℝ} (hx : x < 0) :

theorem complex.tendsto_arg_nhds_within_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :

filter.tendsto complex.arg (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (-π))

theorem complex.continuous_within_at_arg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :

continuous_within_at complex.arg {z : ℂ | 0 ≤ z.im} z

theorem complex.tendsto_arg_nhds_within_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :

filter.tendsto complex.arg (𝓝[{z : ℂ | 0 ≤ z.im}] z) (𝓝 π)