Documentation

Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Complex arctangent #

This file defines the complex arctangent Complex.arctan as arctanz=i2log1+zi1zi and shows that it extends Real.arctan to the complex plane. Its Taylor series expansion arctanz=(1)n2n+1z2n+1, |z|<1 is proved in Complex.hasSum_arctan.

noncomputable def Complex.arctan (z : ) :

The complex arctangent, defined via the complex logarithm.

Equations
theorem Complex.tan_arctan {z : } (h₁ : z I) (h₂ : z -I) :
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 0

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) :
(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).

theorem Complex.hasSum_arctan_aux {z : } (hz : z < 1) :
log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))

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)) (arctan x)

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