English
For a point z in the upper half-plane, π cot(π z) can be written as π i minus a geometric-series term involving exp(2π i z).
Русский
Для точки z в верхней полуплоскости число π cot(π z) выражается через π i минус ряд геометрической прогрессии, содержащий exp(2π i z).
LaTeX
$$$$\forall z \in \mathbb{H}, \; \pi \cot(\pi z) = \pi i - 2\pi i \sum_{n \ge 0} e^{2\pi i z n}.$$$$
Lean4
theorem pi_mul_cot_pi_q_exp (z : ℍ) : π * cot (π * z) = π * I - 2 * π * I * ∑' n : ℕ, Complex.exp (2 * π * I * z) ^ n :=
by
have h1 :
π * ((exp (2 * π * I * z) + 1) / (I * (1 - exp (2 * π * I * z)))) =
-π * I * ((exp (2 * π * I * z) + 1) * (1 / (1 - exp (2 * π * I * z)))) :=
by
simp only [div_mul_eq_div_mul_one_div, div_I, one_div, neg_mul, mul_neg, neg_inj]
ring
rw [cot_pi_eq_exp_ratio, h1, one_div,
(tsum_geometric_of_norm_lt_one (UpperHalfPlane.norm_exp_two_pi_I_lt_one z)).symm, add_comm,
geom_series_mul_one_add (Complex.exp (2 * π * I * (z : ℂ))) (UpperHalfPlane.norm_exp_two_pi_I_lt_one _)]
ring
