cot_series_rep' — Mathlib

English

Let x be a complex number not an integer. Then π cot(π x) has the Mittag-Leffler expansion

Русский

Пусть x — комплексное число, не являющееся целым. Тогда котангенс имеет разложение Миттаг-Леффлера

LaTeX

$$$$\;x \in \mathbb{C} \setminus \mathbb{Z} \;\Longrightarrow\; \pi \cot(\pi x) - \frac{1}{x} = \sum_{n=0}^{\infty} \left( \frac{1}{x - (n+1)} + \frac{1}{x + (n+1)} \right).$$$$

Lean4

theorem cot_series_rep' (hz : x ∈ ℂ_ℤ) : π * cot (π * x) - 1 / x = ∑' n : ℕ, (1 / (x - (n + 1)) + 1 / (x + (n + 1))) :=
  by
  rw [HasSum.tsum_eq]
  apply (Summable.hasSum_iff_tendsto_nat (Summable_cotTerm hz)).mpr (tendsto_logDeriv_euler_cot_sub hz)

Похожие утверждения