The partial-fraction expansion of the hyperbolic tangent

The hyperbolic tangent has simple poles at the odd multiples of i π / 2, and its Mittag-Leffler expansion runs over the odd integers: for every real y,

(π / 2) tanh (π y / 2) = ∑_{n ≥ 0} 2 y / (y² + (2 n + 1)²).

This file derives it from Mathlib's partial-fraction expansion of the cotangent (cot_series_rep'), whose terms cotTerm z n = 1 / (z - (n + 1)) + 1 / (z + (n + 1)) collect the poles at ± (n + 1). Halving the argument keeps exactly the poles at even integers (TauCeti.cotTerm_div_two), so subtracting the two expansions isolates the odd poles (TauCeti.hasSum_cotTerm_two_mul):

π cot (π z) - (π / 2) cot (π z / 2) = ∑_{n ≥ 0} (1 / (z - (2 n + 1)) + 1 / (z + (2 n + 1)))

for every non-integer z. Evaluating at z = i y turns cotangents into hyperbolic cotangents, and coth (2 u) - coth u / 2 = tanh u / 2 gives the expansion of the hyperbolic tangent (TauCeti.hasSum_pi_div_two_mul_tanh).

Main results

• TauCeti.cot_ofReal_mul_I: the cotangent at an imaginary argument;
• TauCeti.hasSum_cotTerm_two_mul: the odd-pole part of the cotangent expansion;
• TauCeti.hasSum_pi_div_two_mul_tanh: the partial-fraction expansion of tanh (π y / 2).

theorem TauCeti.cot_ofReal_mul_I (x : ℝ) : Complex.cot (↑x * Complex.I) = -↑(Real.cosh x / Real.sinh x) * Complex.I

The cotangent at an imaginary argument is a hyperbolic cotangent: cot (x i) = -(cosh x / sinh x) i for every real x (both sides vanish at x = 0).

theorem TauCeti.cotTerm_div_two (z : ℂ) (n : ℕ) : cotTerm (z / 2) n = 2 * cotTerm z (2 * n + 1)

Halving the argument of the cotangent term doubles the pole index: cotTerm (z / 2) n = 2 cotTerm z (2 n + 1), both sides collecting the poles at ± (2 n + 2).

theorem TauCeti.hasSum_cotTerm_two_mul {z : ℂ} (hz : z ∈ Complex.integerComplement) : HasSum (fun (n : ℕ) => cotTerm z (2 * n)) (↑Real.pi * Complex.cot (↑Real.pi * z) - ↑Real.pi / 2 * Complex.cot (↑Real.pi * (z / 2)))

The odd-pole part of the cotangent expansion. For z ∉ ℤ, π cot (π z) - (π / 2) cot (π z / 2) = ∑_{n ≥ 0} (1 / (z - (2 n + 1)) + 1 / (z + (2 n + 1))). The full expansion of π cot (π z) collects all integer poles, and that of π cot (π z / 2) exactly the even ones (cotTerm_div_two).

theorem TauCeti.hasSum_pi_div_two_mul_tanh (y : ℝ) : HasSum (fun (n : ℕ) => 2 * y / (y ^ 2 + (2 * ↑n + 1) ^ 2)) (Real.pi / 2 * Real.tanh (Real.pi * y / 2))

The partial-fraction expansion of the hyperbolic tangent. For every real y, (π / 2) tanh (π y / 2) = ∑_{n ≥ 0} 2 y / (y² + (2 n + 1)²).