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
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.pi) (real.arcsin ((-x).im / complex.abs x) - real.pi))
@[simp]
theorem
complex.abs_mul_exp_arg_mul_I
(x : ℂ) :
↑(complex.abs x) * complex.exp (↑(x.arg) * complex.I) = x
@[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
@[simp]
theorem
complex.range_exp_mul_I
:
set.range (λ (x : ℝ), complex.exp (↑x * complex.I)) = metric.sphere 0 1
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_re_nonneg
{x : ℂ}
(hx : 0 ≤ x.re) :
x.arg = real.arcsin (x.im / complex.abs x)
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)
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)
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
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
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)
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)
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))
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 (nhds_within z {z : ℂ | 0 ≤ z.im}) (nhds real.pi)