Cotangent

This file contains lemmas about the cotangent function, including useful series expansions.

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

noncomputable def sinTerm (x : ℂ) (n : ℕ) : ℂ

The term in the infinite product for sine.

Equations

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

theorem sinTerm_ne_zero {x : ℂ} (hx : x ∈ Complex.integerComplement) (n : ℕ) : sinTerm x n ≠ 0

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

theorem multipliable_sinTerm (x : ℂ) : Multipliable fun (i : ℕ) => sinTerm x i

theorem euler_sin_tprod (x : ℂ) (hx : x ∈ Complex.integerComplement) : ∏' (i : ℕ), sinTerm x i = Complex.sin (↑Real.pi * x) / (↑Real.pi * x)

theorem tendstoUniformlyOn_compact_euler_sin_prod (Z : Set ↑Complex.integerComplement) (hZ : IsCompact Z) : TendstoUniformlyOn (fun (n : ℕ) (z : ↑Complex.integerComplement) => ∏ j ∈ Finset.range n, sinTerm (↑z) j) (fun (x : ↑Complex.integerComplement) => Complex.sin (↑Real.pi * ↑x) / (↑Real.pi * ↑x)) Filter.atTop Z

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

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

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

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

The term in the infinite series expansion of cot.

Equations

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

theorem logDeriv_sinTerm_eq_cotTerm (x : ℂ) (hx : x ∈ Complex.integerComplement) (i : ℕ) : logDeriv (fun (z : ℂ) => sinTerm z i) x = cotTerm x i

theorem logDeriv_of_prod {x : ℂ} (hx : x ∈ Complex.integerComplement) (n : ℕ) : logDeriv (fun (z : ℂ) => ∏ j ∈ Finset.range n, sinTerm 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 (z : ℂ) (hz : z ∈ Complex.integerComplement) (n : ℕ) : cotTerm z n = 2 * z * (1 / (z ^ 2 - (↑n + 1) ^ 2))

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

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

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