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
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Complex.cos_arg {x : } (hx : x 0) :
    theorem Complex.abs_eq_one_iff (z : ) :
    Complex.abs z = 1 θ, Complex.exp (θ * Complex.I) = z
    theorem Complex.arg_mul_cos_add_sin_mul_I {r : } (hr : 0 < r) {θ : } (hθ : θ Set.Ioc (-Real.pi) Real.pi) :
    Complex.arg (r * (Complex.cos θ + Complex.sin θ * Complex.I)) = θ
    @[simp]
    theorem Complex.ext_abs_arg {x : } {y : } (h₁ : Complex.abs x = Complex.abs y) (h₂ : Complex.arg x = Complex.arg y) :
    x = y
    @[simp]
    theorem Complex.arg_nonneg_iff {z : } :
    0 Complex.arg z 0 z.im
    @[simp]
    theorem Complex.arg_neg_iff {z : } :
    Complex.arg z < 0 z.im < 0
    theorem Complex.arg_real_mul (x : ) {r : } (hr : 0 < r) :
    theorem Complex.arg_eq_arg_iff {x : } {y : } (hx : x 0) (hy : y 0) :
    Complex.arg x = Complex.arg y ↑(Complex.abs y) / ↑(Complex.abs x) * x = y
    @[simp]
    @[simp]
    theorem Complex.tan_arg (x : ) :
    Real.tan (Complex.arg x) = x.im / x.re
    theorem Complex.arg_ofReal_of_nonneg {x : } (hx : 0 x) :
    Complex.arg x = 0
    theorem Complex.arg_eq_zero_iff {z : } :
    Complex.arg z = 0 0 z.re z.im = 0
    theorem Complex.arg_eq_pi_iff {z : } :
    Complex.arg z = Real.pi z.re < 0 z.im = 0
    theorem Complex.arg_ofReal_of_neg {x : } (hx : x < 0) :
    theorem Complex.arg_of_re_nonneg {x : } (hx : 0 x.re) :
    theorem Complex.arg_of_re_neg_of_im_nonneg {x : } (hx_re : x.re < 0) (hx_im : 0 x.im) :
    theorem Complex.arg_of_re_neg_of_im_neg {x : } (hx_re : x.re < 0) (hx_im : x.im < 0) :
    theorem Complex.arg_of_im_nonneg_of_ne_zero {z : } (h₁ : 0 z.im) (h₂ : z 0) :
    theorem Complex.arg_of_im_pos {z : } (hz : 0 < z.im) :
    theorem Complex.arg_of_im_neg {z : } (hz : z.im < 0) :
    @[simp]
    theorem Complex.arg_neg_coe_angle {x : } (hx : x 0) :
    ↑(Complex.arg (-x)) = ↑(Complex.arg x) + Real.pi
    theorem Complex.arg_mul_cos_add_sin_mul_I_sub {r : } (hr : 0 < r) (θ : ) :
    Complex.arg (r * (Complex.cos θ + Complex.sin θ * Complex.I)) - θ = 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) :
    ↑(Complex.arg (r * (↑(Real.Angle.cos θ) + ↑(Real.Angle.sin θ) * Complex.I))) = θ
    theorem Complex.arg_mul_coe_angle {x : } {y : } (hx : x 0) (hy : y 0) :
    ↑(Complex.arg (x * y)) = ↑(Complex.arg x) + ↑(Complex.arg y)
    theorem Complex.arg_div_coe_angle {x : } {y : } (hx : x 0) (hy : y 0) :
    ↑(Complex.arg (x / y)) = ↑(Complex.arg x) - ↑(Complex.arg y)
    theorem Complex.arg_eq_nhds_of_re_pos {x : } (hx : 0 < x.re) :
    theorem Complex.arg_eq_nhds_of_re_neg_of_im_pos {x : } (hx_re : x.re < 0) (hx_im : 0 < x.im) :
    theorem Complex.arg_eq_nhds_of_re_neg_of_im_neg {x : } (hx_re : x.re < 0) (hx_im : x.im < 0) :
    theorem Complex.arg_eq_nhds_of_im_pos {z : } (hz : 0 < z.im) :
    theorem Complex.arg_eq_nhds_of_im_neg {z : } (hz : z.im < 0) :
    theorem Complex.continuousAt_arg {x : } (h : 0 < x.re x.im 0) :
    theorem Complex.continuousWithinAt_arg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :