mathlib3 documentation

analysis.special_functions.complex.arg

The argument of a complex number. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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
source
theorem complex.sin_arg (x : ℂ) :
real.sin x.arg = x.im / ⇑complex.abs x
source
theorem complex.cos_arg {x : ℂ} (hx : x ≠ 0) :
real.cos x.arg = x.re / ⇑complex.abs x
source
@[simp]
theorem complex.abs_mul_exp_arg_mul_I (x : ℂ) :
↑(⇑complex.abs x) * complex.exp (↑(x.arg) * complex.I) = x
source
@[simp]
theorem complex.abs_mul_cos_add_sin_mul_I (x : ℂ) :
↑(⇑complex.abs x) * (complex.cos ↑(x.arg) + complex.sin ↑(x.arg) * complex.I) = x
source
theorem complex.abs_eq_one_iff (z : ℂ) :
⇑complex.abs z = 1 ↔ ∃ (θ : ℝ), complex.exp (↑θ * complex.I) = z
source
@[simp]
theorem complex.range_exp_mul_I  :
set.range (λ (x : ℝ), complex.exp (↑x * complex.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 * (complex.cos ↑θ + complex.sin ↑θ * complex.I)).arg = θ
source
theorem complex.arg_cos_add_sin_mul_I {θ : ℝ} (hθ : θ ∈ set.Ioc (-real.pi) real.pi) :
(complex.cos ↑θ + complex.sin ↑θ * complex.I).arg = θ
source
@[simp]
theorem complex.arg_zero  :
0.arg = 0
source
theorem complex.ext_abs_arg {x y : ℂ} (h₁ : ⇑complex.abs x = ⇑complex.abs y) (h₂ : x.arg = y.arg) :
x = y
source
theorem complex.ext_abs_arg_iff {x y : ℂ} :
x = y ↔ ⇑complex.abs x = ⇑complex.abs 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 complex.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_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
x.arg = y.arg ↔ ↑(⇑complex.abs y) / ↑(⇑complex.abs x) * x = y
source
@[simp]
theorem complex.arg_one  :
1.arg = 0
source
@[simp]
theorem complex.arg_neg_one  :
(-1).arg = real.pi
source
@[simp]
theorem complex.arg_I  :
complex.I.arg = real.pi / 2
source
@[simp]
theorem complex.arg_neg_I  :
(-complex.I).arg = -(real.pi / 2)
source
@[simp]
theorem complex.tan_arg (x : ℂ) :
real.tan x.arg = x.im / x.re
source
theorem complex.arg_of_real_of_nonneg {x : ℝ} (hx : 0 ≤ x) :
↑x.arg = 0
source
theorem complex.arg_eq_zero_iff {z : ℂ} :
z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0
source
theorem complex.arg_eq_pi_iff {z : ℂ} :
z.arg = real.pi ↔ z.re < 0 ∧ z.im = 0
source
theorem complex.arg_lt_pi_iff {z : ℂ} :
z.arg < real.pi ↔ 0 ≤ z.re ∨ z.im ≠ 0
source
theorem complex.arg_of_real_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 / ⇑complex.abs 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 / ⇑complex.abs 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 / ⇑complex.abs 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 / ⇑complex.abs z)
source
theorem complex.arg_of_im_pos {z : ℂ} (hz : 0 < z.im) :
z.arg = real.arccos (z.re / ⇑complex.abs z)
source
theorem complex.arg_of_im_neg {z : ℂ} (hz : z.im < 0) :
z.arg = -real.arccos (z.re / ⇑complex.abs z)
source
theorem complex.arg_conj (x : ℂ) :
(⇑(star_ring_end ℂ) x).arg = ite (x.arg = real.pi) real.pi (-x.arg)
source
theorem complex.arg_inv (x : ℂ) :
x⁻¹.arg = ite (x.arg = real.pi) real.pi (-x.arg)
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
@[simp]
theorem complex.abs_arg_le_pi_div_two_iff {z : ℂ} :
|z.arg| ≤ real.pi / 2 ↔ 0 ≤ z.re
source
@[simp]
theorem complex.arg_conj_coe_angle (x : ℂ) :
↑((⇑(star_ring_end ℂ) 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_to_Ioc_mod {r : ℝ} (hr : 0 < r) (θ : ℝ) :
(↑r * (complex.cos ↑θ + complex.sin ↑θ * complex.I)).arg = to_Ioc_mod real.two_pi_pos (-real.pi) θ
source
theorem complex.arg_cos_add_sin_mul_I_eq_to_Ioc_mod (θ : ℝ) :
(complex.cos ↑θ + complex.sin ↑θ * complex.I).arg = to_Ioc_mod real.two_pi_pos (-real.pi) θ
source
theorem complex.arg_mul_cos_add_sin_mul_I_sub {r : ℝ} (hr : 0 < r) (θ : ℝ) :
(↑r * (complex.cos ↑θ + complex.sin ↑θ * complex.I)).arg - θ = 2 * real.pi * ↑⌊(real.pi - θ) / (2 * real.pi)⌋
source
theorem complex.arg_cos_add_sin_mul_I_sub (θ : ℝ) :
(complex.cos ↑θ + complex.sin ↑θ * complex.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) * complex.I)).arg) = θ
source
theorem complex.arg_cos_add_sin_mul_I_coe_angle (θ : real.angle) :
↑((↑(θ.cos) + ↑(θ.sin) * complex.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
@[simp]
theorem complex.arg_coe_angle_to_real_eq_arg (z : ℂ) :
↑(z.arg).to_real = z.arg
source
theorem complex.arg_coe_angle_eq_iff_eq_to_real {z : ℂ} {θ : real.angle} :
↑(z.arg) = θ ↔ z.arg = θ.to_real
source
@[simp]
theorem complex.arg_coe_angle_eq_iff {x y : ℂ} :
↑(x.arg) = ↑(y.arg) ↔ x.arg = y.arg
source
theorem complex.arg_eq_nhds_of_re_pos {x : ℂ} (hx : 0 < x.re) :
complex.arg =ᶠ[nhds x] λ (x : ℂ), real.arcsin (x.im / ⇑complex.abs x)
source
theorem complex.arg_eq_nhds_of_re_neg_of_im_pos {x : ℂ} (hx_re : x.re < 0) (hx_im : 0 < x.im) :
complex.arg =ᶠ[nhds x] λ (x : ℂ), real.arcsin ((-x).im / ⇑complex.abs 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) :
complex.arg =ᶠ[nhds x] λ (x : ℂ), real.arcsin ((-x).im / ⇑complex.abs x) - real.pi
source
theorem complex.arg_eq_nhds_of_im_pos {z : ℂ} (hz : 0 < z.im) :
complex.arg =ᶠ[nhds z] λ (x : ℂ), real.arccos (x.re / ⇑complex.abs x)
source
theorem complex.arg_eq_nhds_of_im_neg {z : ℂ} (hz : z.im < 0) :
complex.arg =ᶠ[nhds z] λ (x : ℂ), -real.arccos (x.re / ⇑complex.abs x)
source
theorem complex.continuous_at_arg {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) :
continuous_at complex.arg x
source
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 (nhds_within z {z : ℂ | z.im < 0}) (nhds (-real.pi))
source
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
source
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 (nhds_within z {z : ℂ | 0 ≤ z.im}) (nhds real.pi)
source
theorem complex.continuous_at_arg_coe_angle {x : ℂ} (h : x ≠ 0) :
continuous_at (coe ∘ complex.arg) x