completedCosZeta₀ — Mathlib

English

HurwitzEvenFEPair is the defined WeakFEPair associated to a, constructed from evenKernel and cosKernel with appropriate analytic data.

Русский

HurwitzEvenFEPair — это определённая слабая ФЕ-пара, связанная с a, построенная из evenKernel и cosKernel с соответствующими аналитическими данными.

LaTeX

$$$$ \\text{HurwitzEvenFEPair}(a) = \\text{(f,g) with } f = \\text{Real}(\\text{evenKernel}(a)), \\ g = \\text{Real}(\\text{cosKernel}(a)). $$$$

Lean4

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

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