English
A meromorphic L-function associated to Φ is defined as a linear combination of Hurwitz zeta functions: LFunction(Φ)(s) = N^{−s} ∑_{j ∈ ZMod N} Φ(j) HurwitzZeta(toAddCircle j)(s).
Русский
Мероморфная L-функция, связанная с Φ, задаётся как линейная комбинация функций Хурвизаты: LFunction(Φ)(s) = N^{−s} ∑_{j ∈ ZMod N} Φ(j) HurwitzZeta(toAddCircle j)(s).
LaTeX
$$$\\\\mathsf{LFunction}(\\\\Phi)(s) = N^{-s} \\\\sum_{j \\\\in ZMod N} \\\\Phi(j) \\\\mathrm{hurwitzZeta}(toAddCircle(j), s)$$$
Lean4
/-- The unique meromorphic function `ℂ → ℂ` which agrees with `∑' n : ℕ, Φ n / n ^ s` wherever the
latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions.
Note that this is not the same as `LSeries Φ`: they agree in the convergence range, but
`LSeries Φ s` is defined to be `0` if `re s ≤ 1`.
-/
noncomputable def LFunction (Φ : ZMod N → ℂ) (s : ℂ) : ℂ :=
N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZeta (toAddCircle j) s
