Summable_cotTerm — Mathlib

English

The sequence of cotTerm terms is summable along the integers provided x is not an integer.

Русский

Последовательность cotTerm по целым индексам суммируема, если x не целое.

LaTeX

$$$$\forall x \in \mathbb{C}_{\mathbb{Z}}, \; \sum_{n=0}^{\infty} \cotTerm(x,n) \text{ сходится}.$$$$

Lean4

theorem Summable_cotTerm (hz : x ∈ ℂ_ℤ) : Summable fun n ↦ cotTerm x n :=
  by
  rw [funext fun n ↦ cotTerm_identity hz n]
  apply Summable.mul_left
  suffices Summable fun i : ℕ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
    by
    rw [← summable_nat_add_iff 1] at this
    simpa using this
  suffices Summable fun i : ℤ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by apply this.comp_injective CharZero.cast_injective
  apply (EisensteinSeries.summable_linear_sub_mul_linear_add x 1 1).congr
  simp [mul_comm]

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