English
The auxiliary completed L-function with even/odd Hurwitz zeta terms: completedLFunction₀(Φ) s = N^(−s) ∑ Φ(j) completedHurwitzZetaEven₀(toAddCircle j) s + N^(−s) ∑ Φ(j) completedHurwitzZetaOdd(toAddCircle j) s.
Русский
Вспомогательная завершенная L-функция с членами Hurwitz Zeta: completedLFunction₀(Φ) s = N^(−s)∑ Φ(j) completedHurwitzZetaEven₀(toAddCircle j) s + N^(−s)∑ Φ(j) completedHurwitzZetaOdd(toAddCircle j) s.
LaTeX
$$$$\mathrm{completedLFunction}_{0}(\Phi, s) = N^{-s} \sum_j \Phi(j) \mathrm{completedHurwitzZetaEven}_{0}(toAddCircle(j), s) + N^{-s} \sum_j \Phi(j) \mathrm{completedHurwitzZetaOdd}(toAddCircle(j), s).$$$$
Lean4
/-- The completed L-function of a function `ZMod N → ℂ`, modified by adding multiples of `N ^ (-s) / s`
and `N ^ (-s) / (1 - s)` to make it entire.
-/
noncomputable def completedLFunction₀ (Φ : ZMod N → ℂ) (s : ℂ) : ℂ :=
N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaEven₀ (toAddCircle j) s +
N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s
