completedCosZeta — Mathlib

English

The functional equation in one-sub form states that completedHurwitzZetaEven(a, 1 - s) equals completedCosZeta(a, s).

Русский

Функциональное уравнение в форме «один минус s»: completedHurwitzZetaEven(a, 1 - s) = completedCosZeta(a, s).

LaTeX

$$$$ \\operatorname{completedHurwitzZetaEven}(a, 1 - s) = \\operatorname{completedCosZeta}(a, s). $$$$

Lean4

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

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