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