completedLFunction_def_even — Mathlib

English

If Φ is even, then completedLFunction Φ s equals N^(−s) times the sum of Φ_j times completedHurwitzZetaEven(toAddCircle j) s.

Русский

Если Φ четная, то completedLFunction Φ s = N^(−s)∑ Φ_j completedHurwitzZetaEven(toAddCircle j) s.

LaTeX

$$$$\mathrm{completedLFunction}(\Phi, s) = N^{-s} \sum_j \Phi(j) \mathrm{completedHurwitzZetaEven}(toAddCircle(j), s).$$$$

Lean4

theorem completedLFunction_def_even (hΦ : Φ.Even) (s : ℂ) :
    completedLFunction Φ s = N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s :=
  by
  suffices ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0 by rw [completedLFunction, this, mul_zero, add_zero]
  refine (hΦ.mul_odd fun j ↦ ?_).sum_eq_zero
  rw [map_neg, completedHurwitzZetaOdd_neg]

Похожие утверждения