English
If Φ is even, then L(Φ, s) equals N^(−s) times the sum over j of Φ(j) times HurwitzZetaEven(toAddCircle j, s).
Русский
Если Φ нечетно-четная (четная), тогда L(Φ, s) равно N^(−s) умножить на сумму Φ(j)·HurwitzZetaEven(toAddCircle j, s).
LaTeX
$$$$L(\Phi, s) = N^{-s} \sum_{j \in ZMod N} \Phi(j) \; \mathrm{HurwitzZetaEven}(toAddCircle(j), s).$$$$
Lean4
theorem LFunction_def_even (hΦ : Φ.Even) (s : ℂ) :
LFunction Φ s = N ^ (-s) * ∑ j : ZMod N, Φ j * hurwitzZetaEven (toAddCircle j) s :=
by
simp only [LFunction, hurwitzZeta, mul_add (Φ _), sum_add_distrib]
congr 1
simp only [add_eq_left, ← neg_eq_self ℂ, ← sum_neg_distrib]
refine Fintype.sum_equiv (.neg _) _ _ fun i ↦ ?_
simp only [Equiv.neg_apply, hΦ i, map_neg, hurwitzZetaOdd_neg, mul_neg]
