completedRiemannZeta — Mathlib

English

The completed Riemann zeta function Λ(s) is defined as the completed Hurwitz zeta at zero offset; i.e., Λ(s) = completedHurwitzZetaEven 0 s.

Русский

Завершённая функция Римана Λ(s) определяется как завершённая функция Хёрвитца при нуле: Λ(s) = completedHurwitzZetaEven 0 s.

LaTeX

$$$\\mathrm{completedRiemannZeta}(s) = \\mathrm{completedHurwitzZetaEven}(0,s)$$$

Lean4

/-- The completed Riemann zeta function, `Λ(s)`, which satisfies
`Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s)` (up to a minor correction at `s = 0`). -/
def completedRiemannZeta (s : ℂ) : ℂ :=
  completedHurwitzZetaEven 0 s

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