English
The completed L-function of a function Φ: ZMod 1 → C is a scalar multiple of the completed Riemann zeta function: completedLFunction Φ s = Φ 1 · completedRiemannZeta s.
Русский
Завершенная L-функция Φ: ZMod 1 → ℂ равна Λ · completedRiemannZeta(s), где Λ = Φ(1).
LaTeX
$$$$\mathrm{completedLFunction}(\Phi, s) = \Phi(1) \cdot \mathrm{completedRiemannZeta}(s).$$$$
Lean4
/-- The completed L-function of a function `ZMod 1 → ℂ` is a scalar multiple of the completed Riemann
zeta function.
-/
theorem completedLFunction_modOne_eq (Φ : ZMod 1 → ℂ) (s : ℂ) : completedLFunction Φ s = Φ 1 * completedRiemannZeta s :=
by
rw [completedLFunction_def_even (show Φ.Even from fun _ ↦ congr_arg Φ (Subsingleton.elim ..)), Nat.cast_one, one_cpow,
one_mul, ← singleton_eq_univ 0, sum_singleton, map_zero, completedHurwitzZetaEven_zero, Subsingleton.elim 0 1]
