cot_series_rep — Mathlib

English

For x not an integer, the cotangent expansion can be written with a sum over positive integers

Русский

Для x, не являющегося целым, разложение котангенса записывается как сумма по положительным натуральным числам

LaTeX

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

Lean4

/-- The cotangent infinite sum representation. -/
theorem cot_series_rep (hz : x ∈ ℂ_ℤ) : π * cot (π * x) = 1 / x + ∑' n : ℕ+, (1 / (x - n) + 1 / (x + n)) :=
  by
  have h0 := tsum_pnat_eq_tsum_succ (f := fun n ↦ 1 / (x - n) + 1 / (x + n))
  have h1 := cot_series_rep' hz
  simp only [one_div, Nat.cast_add, Nat.cast_one] at *
  rw [h0, ← h1]
  ring

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