Cotangent

This file contains lemmas about the cotangent function, including useful series expansions. In particular, we prove that π * cot (π * z) = π * I - 2 * π * I * ∑' n : ℕ, Complex.exp (2 * π * I * z) ^ n as well as the infinite sum representation of cotangent (also known as the Mittag-Leffler expansion): π * cot (π * z) = 1 / z + ∑' n : ℕ+, (1 / ((z : ℂ) - n) + 1 / (z + n)).

theorem Complex.cot_eq_exp_ratio (z : ℂ) : z.cot = (exp (2 * I * z) + 1) / (I * (1 - exp (2 * I * z)))

theorem Complex.cot_pi_eq_exp_ratio (z : ℂ) : (↑Real.pi * z).cot = (exp (2 * ↑Real.pi * I * z) + 1) / (I * (1 - exp (2 * ↑Real.pi * I * z)))

theorem pi_mul_cot_pi_q_exp (z : UpperHalfPlane) : ↑Real.pi * (↑Real.pi * ↑z).cot = ↑Real.pi * Complex.I - 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n

@[reducible, inline]

noncomputable abbrev sineTerm (x : ℂ) (n : ℕ) : ℂ

The main term in the infinite product for sine.

Equations

• sineTerm x n = -x ^ 2 / (↑n + 1) ^ 2

theorem sineTerm_ne_zero {x : ℂ} (hx : x ∈ Complex.integerComplement) (n : ℕ) : 1 + sineTerm x n ≠ 0

theorem tendsto_euler_sin_prod' {x : ℂ} (h0 : x ≠ 0) : Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range n, (1 + sineTerm x i)) Filter.atTop (nhds (Complex.sin (↑Real.pi * x) / (↑Real.pi * x)))

theorem multipliable_sineTerm (x : ℂ) : Multipliable fun (i : ℕ) => 1 + sineTerm x i

theorem euler_sineTerm_tprod {x : ℂ} (hx : x ∈ Complex.integerComplement) : ∏' (i : ℕ), (1 + sineTerm x i) = Complex.sin (↑Real.pi * x) / (↑Real.pi * x)

theorem multipliableUniformlyOn_euler_sin_prod_on_compact {Z : Set ℂ} (hZC : IsCompact Z) : MultipliableUniformlyOn (fun (n : ℕ) (z : ℂ) => 1 + sineTerm z n) {Z}

theorem HasProdUniformlyOn_sineTerm_prod_on_compact {Z : Set ℂ} (hZ2 : Z ⊆ Complex.integerComplement) (hZC : IsCompact Z) : HasProdUniformlyOn (fun (n : ℕ) (z : ℂ) => 1 + sineTerm z n) (fun (x : ℂ) => Complex.sin (↑Real.pi * x) / (↑Real.pi * x)) {Z}

theorem HasProdLocallyUniformlyOn_euler_sin_prod : HasProdLocallyUniformlyOn (fun (n : ℕ) (z : ℂ) => 1 + sineTerm z n) (fun (x : ℂ) => Complex.sin (↑Real.pi * x) / (↑Real.pi * x)) Complex.integerComplement

theorem sin_pi_z_ne_zero {x : ℂ} (hz : x ∈ Complex.integerComplement) : Complex.sin (↑Real.pi * x) ≠ 0

theorem tendsto_logDeriv_euler_sin_div {x : ℂ} (hx : x ∈ Complex.integerComplement) : Filter.Tendsto (fun (n : ℕ) => logDeriv (fun (z : ℂ) => ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) Filter.atTop (nhds (logDeriv (fun (t : ℂ) => Complex.sin (↑Real.pi * t) / (↑Real.pi * t)) x))

theorem logDeriv_sin_div_eq_cot {x : ℂ} (hz : x ∈ Complex.integerComplement) : logDeriv (fun (t : ℂ) => Complex.sin (↑Real.pi * t) / (↑Real.pi * t)) x = ↑Real.pi * (↑Real.pi * x).cot - 1 / x

@[reducible, inline]

noncomputable abbrev cotTerm (x : ℂ) (n : ℕ) : ℂ

The term in the infinite sum expansion of cot.

Equations

• cotTerm x n = 1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1))

theorem logDeriv_sineTerm_eq_cotTerm {x : ℂ} (hx : x ∈ Complex.integerComplement) (i : ℕ) : logDeriv (fun (z : ℂ) => 1 + sineTerm z i) x = cotTerm x i

theorem logDeriv_prod_sineTerm_eq_sum_cotTerm {x : ℂ} (hx : x ∈ Complex.integerComplement) (n : ℕ) : logDeriv (fun (z : ℂ) => ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x = ∑ j ∈ Finset.range n, cotTerm x j

theorem tendsto_logDeriv_euler_cot_sub {x : ℂ} (hx : x ∈ Complex.integerComplement) : Filter.Tendsto (fun (n : ℕ) => ∑ j ∈ Finset.range n, cotTerm x j) Filter.atTop (nhds (↑Real.pi * (↑Real.pi * x).cot - 1 / x))

theorem cotTerm_identity {x : ℂ} (hz : x ∈ Complex.integerComplement) (n : ℕ) : cotTerm x n = 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))

theorem Summable_cotTerm {x : ℂ} (hz : x ∈ Complex.integerComplement) : Summable fun (n : ℕ) => cotTerm x n

theorem cot_series_rep' {x : ℂ} (hz : x ∈ Complex.integerComplement) : ↑Real.pi * (↑Real.pi * x).cot - 1 / x = ∑' (n : ℕ), (1 / (x - (↑n + 1)) + 1 / (x + (↑n + 1)))

theorem cot_series_rep {x : ℂ} (hz : x ∈ Complex.integerComplement) : ↑Real.pi * (↑Real.pi * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - ↑↑n) + 1 / (x + ↑↑n))

The cotangent infinite sum representation.