The cotangent over ℤ and away from the real axis #
Mathlib's partial-fraction expansion of the cotangent (cot_series_rep) pairs the poles at ± n.
Pairing each pole n instead with the constant 1 / n gives an absolutely convergent series over
ℤ (TauCeti.hasSum_one_div_sub_intCast_add_one_div_intCast):
π cot (π w) = ∑_{n ∈ ℤ} (1 / (w - n) + 1 / n) for w ∉ ℤ,
the term at n = 0 being 1 / w. This is the form in which the cotangent appears as a row of the
lattice series of the Weierstrass ζ function.
Away from the real axis, π cot (π u) tends to -π i as Im u → ∞, and to π i as
Im u → -∞, exponentially fast: with q = e^(2π i u), π cot (π u) + π i = 2π q / (i (1 - q))
(TauCeti.norm_pi_mul_cot_pi_mul_add_pi_mul_I_le,
TauCeti.norm_pi_mul_cot_pi_mul_sub_pi_mul_I_le). Correcting by these limits, the cotangents
π cot (π m w) + sign(m) π i are odd in m ∈ ℤ and sum to 0; at the division points
(c z + b) / M the q-expansion is a series in e(z / M) = e^(2π i z / M) with coefficients
e(k b / M).
Main results #
Complex.cot_neg,Complex.cot_zero: the cotangent is odd, with junk value0at0.TauCeti.hasSum_one_div_sub_intCast_add_one_div_intCast: the expansion overℤ.TauCeti.hasSum_pi_mul_cot_pi_mul_add_pi_mul_I: theq-expansion in the upper half-plane.TauCeti.hasSum_pi_mul_cot_pi_mul_div_add_pi_mul_I,TauCeti.hasSum_ite_pi_mul_cot_pi_mul_div_add_pi_mul_I: theq-expansion at the division points(c z + b) / M, for onec ≥ 1and summed over a residue class ofcmoduloM.TauCeti.hasSum_pi_mul_cot_pi_mul_intCast_mul_add_sign: the corrected cotangentsπ cot (π m w) + sign(m) π isum to0overm ∈ ℤ.TauCeti.hasSum_ite_pi_mul_cot_pi_mul_intCast_div_add_sign: the corrected cotangentsπ cot (π (n z + b) / M) + sign(n) π isummed over a residue class ofn ∈ ℤmoduloM.TauCeti.hasSum_pi_mul_cot_pi_mul_div_sub_intCast_mul_add_pi_mul_cot: the cotangent rowsπ cot (π (x - m z)) + π cot (π m z)at a division pointx = (b₀ z + b) / M, summed overm ∈ ℤ, as aq-expansion ine(z / M).TauCeti.pi_mul_cot_pi_mul_val_div_eq_sum: the finite Fourier expansion ofπ cot (π j / M)at the nonzero residuesjmoduloM.TauCeti.sum_pi_mul_cot_pi_mul_val_div_mul_stdAddChar: the finite Fourier transform ofj ↦ π cot (π j / M), the sawtoothx ↦ π i (M - 2 x)vanishing atx = 0.TauCeti.norm_pi_mul_cot_pi_mul_add_pi_mul_I_le,TauCeti.norm_pi_mul_cot_pi_mul_sub_pi_mul_I_le: the exponential approach to∓ π i.
The junk value of the cotangent at its pole 0 is 0.
The partial-fraction expansion of the cotangent over ℤ. For w ∉ ℤ,
π cot (π w) = ∑_{n ∈ ℤ} (1 / (w - n) + 1 / n), the series converging absolutely; its term at
n = 0 is 1 / w.
The q-expansion of the cotangent in the upper half-plane: if 0 < Im w, then
π cot (π w) + π i = -2π i ∑_{k ≥ 1} e^(2π i k w). This is Mathlib's pi_mul_cot_pi_q_exp with
the constant term separated from the series.
The sum of π cot (π u) and π cot (π v), for u in the upper and v in the lower
half-plane, at imaginary distance at least t > 0 from the real axis and r from it, is at most
2 (2π / (1 - e^(-2π t))) e^(-2π r): the two cotangents approach -π i and π i.
The q-expansion of the cotangent at a division point: if 0 < Im z, c ≥ 1 and
b ∈ ℤ, then π cot (π (c z + b) / M) + π i = -2π i ∑_{k ≥ 1} e(k b / M) e(z / M)^(c k), where
e(k b / M) = ZMod.stdAddChar (k b) and e(z / M) = e^(2π i z / M).
The q-expansion of the cotangents at the division points of a residue class: if
0 < Im z, the cotangents π cot (π (c z + b) / M) + π i with c ≥ 1 and c ≡ d modulo M sum
to the absolutely convergent double series -2π i ∑_{c ≡ d, k ≥ 1} e(k b / M) e(z / M)^(c k).
The corrected cotangents over ℤ sum to zero: if 0 < Im w, the terms
π cot (π m w) + sign(m) π i are odd in m ∈ ℤ, decay geometrically, and sum to 0.
The corrected cotangents along a residue class of ℤ: if 0 < Im z, the cotangents
π cot (π (n z + b) / M) + sign(n) π i over n ≡ d modulo M sum to the absolutely convergent
double series -2π i ∑_{c, k ≥ 1} D(c, k) e(z / M)^(c k), plus the term π cot (π b / M) at
n = 0 if d = 0. Here D(c, k) is e(k b / M) if c ≡ d minus e(-k b / M) if c ≡ -d:
the classes n = c ≥ 1 and n = -c ≤ -1 give its two parts.
The cotangent rows at a division point, as a q-expansion. If 0 < Im z and
0 ≤ b₀ < M, the rows π cot (π (x - m z)) + π cot (π m z) at x = (b₀ z + b) / M sum over
m ∈ ℤ to -2π i ∑_{c, k ≥ 1} D(c, k) e(z / M)^(c k), plus the constant π cot (π b / M) if
b₀ = 0 and -π i otherwise, with D as in
TauCeti.hasSum_ite_pi_mul_cot_pi_mul_intCast_div_add_sign. Write x - m z = (n z + b) / M with
n = b₀ - m M, which runs over the residue class of b₀; the signs of n and m cancel except
at m = 0, and the remaining cotangents π cot (π m z) + sign(m) π i cancel in pairs.
The finite Fourier expansion of the cotangent at the division points. For a nonzero
residue j modulo M, π cot (π j / M) = π i + (2π i / M) ∑_{m mod M} m e(m j / M), with
0 ≤ m < M the representative of m and e(x) = e^(2π i x). With ζ = e(j / M) ≠ 1, the sum
∑_{m < M} m ζ^m is M / (ζ - 1).
The finite Fourier transform of the cotangent at the division points. For a residue x
modulo M, ∑_{j mod M} π cot (π j / M) e(x j / M) is π i (M - 2 x) if x ≠ 0, with
0 ≤ x < M the representative of x, and 0 if x = 0. The term at j = 0 is cot 0 = 0.