completedSinZeta — Mathlib

English

The completed sine zeta is odd in the first argument: completedSinZeta(-a, s) = - completedSinZeta(a, s).

Русский

Функция completedSinZeta по аргументу a нечетна: completedSinZeta(-a, s) = - completedSinZeta(a, s).

LaTeX

$$$$ completedSinZeta(-a, s) = -\, completedSinZeta(a, s). $$$$

Lean4

/-- The entire function of `s` which agrees with
` Gamma ((s + 1) / 2) * π ^ (-(s + 1) / 2) * ∑' (n : ℕ), sin (2 * π * a * n) / n ^ s`
for `1 < re s`.
-/
def completedSinZeta (a : UnitAddCircle) (s : ℂ) : ℂ :=
  ((hurwitzOddFEPair a).symm.Λ ((s + 1) / 2)) / 2

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