completedHurwitzZetaEven₀ — Mathlib

English

The pole-removed entire function is defined by one half of the Λ-transform of the HurwitzEvenFEPair evaluated at s/2.

Русский

Полюс-удалённая целая функция определяется как половина Λ-преобразования HurwitzEvenFEPair в точке s/2.

LaTeX

$$$$ \\operatorname{completedHurwitzZetaEven}_0(a,s) = \\frac{1}{2} \\Lambda_0((\\mathrm{hurwitzEvenFEPair}(a)))(s/2). $$$$

Lean4

/-- The entire function differing from `completedHurwitzZetaEven a s` by a linear combination of
`1 / s` and `1 / (1 - s)`. -/
def completedHurwitzZetaEven₀ (a : UnitAddCircle) (s : ℂ) : ℂ :=
  ((hurwitzEvenFEPair a).Λ₀ (s / 2)) / 2

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