completedHurwitzZetaEven — Mathlib

English

CompletedHurwitzZetaEven(a,s) is defined as one half of the Λ-transform of the WeakFEPair evaluated at s/2.

Русский

CompletedHurwitzZetaEven(a,s) задаётся как половина Λ-преобразования пары WeakFEPair в точке s/2.

LaTeX

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

Lean4

/-- The meromorphic function of `s` which agrees with
`1 / 2 * Gamma (s / 2) * π ^ (-s / 2) * ∑' (n : ℤ), 1 / |n + a| ^ s` for `1 < re s`.
-/
def completedHurwitzZetaEven (a : UnitAddCircle) (s : ℂ) : ℂ :=
  ((hurwitzEvenFEPair a).Λ (s / 2)) / 2

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