Complex arctangent

This file defines the complex arctangent Complex.arctan as $$\arctan z=-\frac{i}{2}\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

• z.arctan = -Complex.I / 2 * Complex.log ((1 + z * Complex.I) / (1 - z * Complex.I))

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

theorem Complex.hasSum_arctan_aux {z : ℂ} (hz : ‖z‖ < 1) : Complex.log (1 + z * Complex.I) + -Complex.log (1 - z * Complex.I) = Complex.log ((1 + z * Complex.I) / (1 - z * Complex.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)) (Real.arctan x)

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