completedCosZeta_residue_zero — Mathlib

English

The residue of completedCosZeta a s at s = 0 is -1, uniformly in a.

Русский

Положение вычета в точке s = 0 для completedCosZeta a s равно -1 для всех a.

LaTeX

$$$\\forall a:\\text{UnitAddCircle},\\ \\mathrm{Tendsto}\\bigl(s \\mapsto s\\cdot\\mathrm{completedCosZeta}(a,s),\\ 0\\bigr) = -1.$$$

Lean4

theorem completedCosZeta_residue_zero (a : UnitAddCircle) :
    Tendsto (fun s ↦ s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1)) :=
  by
  have h1 : Tendsto (fun s : ℂ ↦ s * _) (𝓝[≠] 0) (𝓝 (-1)) := (hurwitzEvenFEPair a).symm.Λ_residue_zero
  refine (h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)
  simp [completedCosZeta, div_mul_eq_mul_div, mul_div_assoc]

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