tendsto_logDeriv_euler_cot_sub — Mathlib

English

The sum of cotTerm tends to the log derivative expression π cot(π x) − 1/x as n → ∞.

Русский

Сумма cotTerm стремится к выражению логарифмической производной: π cot(π x) − 1/x при n → ∞.

LaTeX

$$$$\forall x \in \mathbb{C}, x \in \mathbb{C}_{\mathbb{Z}} \Rightarrow \\ \mathrm{Tendsto}\left( n \mapsto \sum_{j=0}^{n-1} \cotTerm(x,j) \right)\;\text{atTop} \; (\mathcal{N}) = \pi \cot(\pi x) - \frac{1}{x}.$$$$

Lean4

theorem tendsto_logDeriv_euler_cot_sub (hx : x ∈ ℂ_ℤ) :
    Tendsto (fun n : ℕ => ∑ j ∈ Finset.range n, cotTerm x j) atTop (𝓝 <| π * cot (π * x) - 1 / x) :=
  by
  simp_rw [← logDeriv_sin_div_eq_cot hx, ← logDeriv_prod_sineTerm_eq_sum_cotTerm hx]
  simpa using tendsto_logDeriv_euler_sin_div hx

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