English
The completed L-function is the sum of the even and odd parts, scaled by N^(−s).
Русский
Завершенная L-функция есть сумма четной и нечетной частей, умноженная на N^(−s).
LaTeX
$$$$\mathrm{completedLFunction}(\Phi, s) = N^{-s} \sum_j \Phi(j) \mathrm{completedHurwitzZetaEven}(toAddCircle(j), s) + N^{-s} \sum_j \Phi(j) \mathrm{completedHurwitzZetaOdd}(toAddCircle(j), s).$$$$
Lean4
/-- The completed L-function of a function `Φ : ZMod N → ℂ`.
This is only mathematically meaningful if `Φ` is either even, or odd; here we extend this to all `Φ`
by linearity.
-/
noncomputable def completedLFunction (Φ : ZMod N → ℂ) (s : ℂ) : ℂ :=
N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s +
N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s
