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
Instances For
    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
    @[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.abs_mul_cos_arg (x : ) :
    Complex.abs x * Real.cos x.arg = x.re
    @[simp]
    theorem Complex.abs_mul_sin_arg (x : ) :
    Complex.abs x * Real.sin x.arg = x.im
    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) :
    (r * (Complex.cos θ + Complex.sin θ * Complex.I)).arg = θ
    theorem Complex.arg_exp_mul_I (θ : ) :
    (Complex.exp (θ * Complex.I)).arg = toIocMod (-Real.pi) θ
    @[simp]
    theorem Complex.ext_abs_arg {x : } {y : } (h₁ : Complex.abs x = Complex.abs y) (h₂ : x.arg = y.arg) :
    x = y
    theorem Complex.ext_abs_arg_iff {x : } {y : } :
    x = y Complex.abs x = Complex.abs y x.arg = y.arg
    theorem Complex.arg_le_pi (x : ) :
    x.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 (Complex.abs y) / (Complex.abs x) * x = y
    @[simp]
    @[simp]
    theorem Complex.arg_neg_one :
    (-1).arg = Real.pi
    @[simp]
    @[simp]
    @[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_pi_iff {z : } :
    z.arg = Real.pi z.re < 0 z.im = 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 / Complex.abs 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 / Complex.abs 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 / Complex.abs 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 / Complex.abs z)
    theorem Complex.arg_of_im_pos {z : } (hz : 0 < z.im) :
    z.arg = Real.arccos (z.re / Complex.abs z)
    theorem Complex.arg_of_im_neg {z : } (hz : z.im < 0) :
    z.arg = -Real.arccos (z.re / Complex.abs 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.abs_eq_one_iff' {x : } :
    Complex.abs x = 1 θSet.Ioc (-Real.pi) Real.pi, Complex.exp (θ * Complex.I) = x
    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_sub {r : } (hr : 0 < r) (θ : ) :
    (r * (Complex.cos θ + Complex.sin θ * Complex.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 * Complex.I)).arg = θ
    theorem Complex.arg_cos_add_sin_mul_I_coe_angle (θ : Real.Angle) :
    (θ.cos + θ.sin * Complex.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.

    An alternative description of the slit plane as consisting of nonzero complex numbers whose argument is not π.

    theorem Complex.arg_eq_nhds_of_re_pos {x : } (hx : 0 < x.re) :
    Complex.arg =ᶠ[nhds x] fun (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] fun (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] fun (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] fun (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] fun (x : ) => -Real.arccos (x.re / Complex.abs x)
    theorem Complex.continuousWithinAt_arg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :