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.

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_mul_ne_zero {x : ℂ} (hx : x ∈ Complex.integerComplement) : Complex.sin (↑Real.pi * x) ≠ 0

sin π z is non vanishing on the complement of the integers in ℂ.

theorem cot_pi_mul_contDiffWithinAt {x : ℂ} (k : ℕ∞) (hx : x ∈ Complex.integerComplement) : ContDiffWithinAt ℂ (↑k) (fun (x : ℂ) => (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet x

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.

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

@[deprecated summable_cotTerm (since := "2026-01-28")]

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

Alias of summable_cotTerm.

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.

theorem eqOn_iteratedDeriv_cotTerm (k d : ℕ) : Set.EqOn (iteratedDeriv k fun (z : ℂ) => cotTerm z d) (fun (z : ℂ) => (-1) ^ k * ↑k.factorial * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) Complex.integerComplement

theorem eqOn_iteratedDerivWithin_cotTerm_integerComplement (k d : ℕ) : Set.EqOn (iteratedDerivWithin k (fun (z : ℂ) => cotTerm z d) Complex.integerComplement) (fun (z : ℂ) => (-1) ^ k * ↑k.factorial * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) Complex.integerComplement

theorem eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet (k d : ℕ) : Set.EqOn (iteratedDerivWithin k (fun (z : ℂ) => cotTerm z d) UpperHalfPlane.upperHalfPlaneSet) (fun (z : ℂ) => (-1) ^ k * ↑k.factorial * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) UpperHalfPlane.upperHalfPlaneSet

theorem summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm {k : ℕ} (hk : 1 ≤ k) : SummableLocallyUniformlyOn (fun (n : ℕ) => iteratedDerivWithin k (fun (z : ℂ) => cotTerm z n) UpperHalfPlane.upperHalfPlaneSet) UpperHalfPlane.upperHalfPlaneSet

theorem differentiableOn_iteratedDerivWithin_cotTerm (n l : ℕ) : DifferentiableOn ℂ (iteratedDerivWithin l (fun (z : ℂ) => cotTerm z n) UpperHalfPlane.upperHalfPlaneSet) UpperHalfPlane.upperHalfPlaneSet

theorem iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum {z : ℂ} {k : ℕ} (hk : 1 ≤ k) (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : iteratedDerivWithin k (fun (x : ℂ) => ↑Real.pi * (↑Real.pi * x).cot - 1 / x) UpperHalfPlane.upperHalfPlaneSet z = -(-1) ^ k * ↑k.factorial * z ^ (-1 - ↑k) + (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

theorem iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow {k : ℕ} (hk : 1 ≤ k) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : iteratedDerivWithin k (fun (x : ℂ) => ↑Real.pi * (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet z = (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

theorem iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow {k : ℕ} (hk : 1 ≤ k) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : iteratedDerivWithin k (fun (x : ℂ) => ↑Real.pi * (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet z = (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), 1 / (z + ↑n) ^ (k + 1)

The series expansion of the iterated derivative of π cot (π z).