English
For each a on the unit circle, the cosine Hurwitz zeta function cosZeta(a) is the meromorphic function of a complex variable s which agrees with the Dirichlet series sum_{n≥1} cos(2π a n)/n^s for Re(s) > 1 and extends meromorphically to the entire complex plane, with cosZeta(a)(s) = completedCosZeta(a, s)/Γ(s) and cosZeta(a)(0) = -1/2.
Русский
Для каждого a на единичной окрестности косинусная зета-функция cosZeta(a) является мероморфной функцией от комплексной переменной s, которая совпадает с рядами Дирихле cos(2πa n)/n^s при Re(s) > 1 и далее продолжается мероморфно на всю плоскость, при этом cosZeta(a)(s) = completedCosZeta(a, s)/Γ(s) и cosZeta(a)(0) = -1/2.
LaTeX
$$$$$\\cosZeta(a)(s) = \\frac{\\mathrm{completedCosZeta}(a,s)}{\\Gamma(s)} \\quad (s \\ne 0), \\quad \\cosZeta(a)(0) = -\\frac{1}{2}.$$$$$
Lean4
/-- The cosine zeta function, i.e. the meromorphic function of `s` which agrees
with `∑' (n : ℕ), cos (2 * π * a * n) / n ^ s` for `1 < re s`. -/
noncomputable def cosZeta (a : UnitAddCircle) :=
Function.update (fun s : ℂ ↦ completedCosZeta a s / Gammaℝ s) 0 (-1 / 2)
