English
For even Φ and s with s ≠ 0 or Φ(0) = 0, we have LFunction Φ s = completedLFunction Φ s / Γℝ(s).
Русский
Для чётной Φ и |s|, выполняется LFunction Φ s = completedLFunction Φ s / Γℝ(s) при s ≠ 0 или Φ(0) = 0.
LaTeX
$$$$L(\Phi, s) = \frac{\mathrm{completedLFunction}(\Phi, s)}{\Gamma_{\mathbb{R}}(s)}$$$$
Lean4
/-- Relation between the completed L-function and the usual one (even case).
We state it this way around so it holds at the poles of the gamma factor as well
(except at `s = 0`, where it is genuinely false if `N > 1` and `Φ 0 ≠ 0`).
-/
theorem LFunction_eq_completed_div_gammaFactor_even (hΦ : Φ.Even) (s : ℂ) (hs : s ≠ 0 ∨ Φ 0 = 0) :
LFunction Φ s = completedLFunction Φ s / Gammaℝ s :=
by
simp only [completedLFunction_def_even hΦ, LFunction_def_even hΦ, mul_div_assoc, sum_div]
congr 2 with i
rcases ne_or_eq i 0 with hi | rfl
· rw [hurwitzZetaEven_def_of_ne_or_ne (.inl (hi ∘ toAddCircle_eq_zero.mp))]
· rcases hs with hs | hΦ'
· rw [hurwitzZetaEven_def_of_ne_or_ne (.inr hs)]
· simp only [hΦ', map_zero, zero_mul]
