Documentation

Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Complex arctangent #

This file defines the complex arctangent Complex.arctan as $$\arctan z = -\frac i2 \log \frac{1 + zi}{1 - zi}$$ and shows that it extends Real.arctan to the complex plane. Its Taylor series expansion $$\arctan z = \frac{(-1)^n}{2n + 1} z^{2n + 1},\ |z|<1$$ is proved in Complex.hasSum_arctan.

noncomputable def Complex.arctan (z : ) :

The complex arctangent, defined via the complex logarithm.

Equations
Instances For
    theorem Complex.tan_arctan {z : } (h₁ : z Complex.I) (h₂ : z -Complex.I) :
    Complex.tan z.arctan = z
    theorem Complex.cos_ne_zero_of_arctan_bounds {z : } (h₀ : z Real.pi / 2) (h₁ : -(Real.pi / 2) < z.re) (h₂ : z.re Real.pi / 2) :

    cos z is nonzero when the bounds in arctan_tan are met (z lies in the vertical strip -π / 2 < z.re < π / 2 and z ≠ π / 2).

    theorem Complex.arctan_tan {z : } (h₀ : z Real.pi / 2) (h₁ : -(Real.pi / 2) < z.re) (h₂ : z.re Real.pi / 2) :
    (Complex.tan z).arctan = z
    @[simp]
    theorem Complex.ofReal_arctan (x : ) :
    (Real.arctan x) = (↑x).arctan
    theorem Complex.arg_one_add_mem_Ioo {z : } (hz : z < 1) :
    (1 + z).arg Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)

    The argument of 1 + z for z in the open unit disc is always in (-π / 2, π / 2).

    We can combine the logs in log (1 + z * I) + -log (1 - z * I) into one. This is only used in hasSum_arctan.

    theorem Complex.hasSum_arctan {z : } (hz : z < 1) :
    HasSum (fun (n : ) => (-1) ^ n * z ^ (2 * n + 1) / (2 * n + 1)) z.arctan

    The power series expansion of Complex.arctan, valid on the open unit disc.

    theorem Real.hasSum_arctan {x : } (hx : x < 1) :
    HasSum (fun (n : ) => (-1) ^ n * x ^ (2 * n + 1) / (2 * n + 1)) (Real.arctan x)

    The power series expansion of Real.arctan, valid on -1 < x < 1.