completedLFunction_def_odd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem completedLFunction_def_odd (hΦ : Φ.Odd) (s : ℂ) :
    completedLFunction Φ s = N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s :=
  by
  suffices ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0 by
    rw [completedLFunction, this, mul_zero, zero_add]
  refine (hΦ.mul_even fun j ↦ ?_).sum_eq_zero
  rw [map_neg, completedHurwitzZetaEven_neg]

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