English
Let Φ be an odd additive character modulo N. Then the L-function attached to Φ satisfies a simple relation with the completed L-function: LFunction(Φ, s) = completedLFunction(Φ, s) / Γ(s+1) for all s ∈ ℂ where the gamma factor has poles (i.e., in the odd case).
Русский
Пусть Φ — нечеткая (нечётная) аддитивная характеристика по модулю N. Тогда L-функция, ассоциированная с Φ, удовлетворяет соотношению с завершённой L-функцией: LFunction(Φ, s) = completedLFunction(Φ, s) / Γ(s+1) для всех комплексных s (учитывая полюса гамма-фактора).
LaTeX
$$$L(\Phi,s) = \dfrac{\mathrm{completedLFunction}(\Phi,s)}{\Gamma(s+1)}$$$
Lean4
/-- Relation between the completed L-function and the usual one (odd case).
We state it this way around so it holds at the poles of the gamma factor as well.
-/
theorem LFunction_eq_completed_div_gammaFactor_odd (hΦ : Φ.Odd) (s : ℂ) :
LFunction Φ s = completedLFunction Φ s / Gammaℝ (s + 1) := by
simp only [LFunction_def_odd hΦ, completedLFunction_def_odd hΦ, hurwitzZetaOdd, mul_div_assoc, sum_div]
