expZeta — Mathlib

English

ExpZeta is defined as the complex combination cosZeta + i sinZeta; it provides a meromorphic continuation of the Dirichlet-type series.

Русский

ExpZeta задаётся как комбинация cosZeta и i sinZeta; она задаёт мероморфное продолжение ряда типа Дирихле.

LaTeX

$$$\\displaystyle \\expZeta(a,s) = \\cosZeta(a,s) + i\,\\sinZeta(a,s).$$$

Lean4

/-- Meromorphic continuation of the series `∑' (n : ℕ), exp (2 * π * I * a * n) / n ^ s`.  See
`hasSum_expZeta_of_one_lt_re` for the relation to the Dirichlet series. -/
noncomputable def expZeta (a : UnitAddCircle) (s : ℂ) :=
  cosZeta a s + I * sinZeta a s

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