LFunction_modOne_eq — Mathlib

English

For every function Φ: ZMod 1 → C, the L-function is a scalar multiple of the Riemann zeta function: L(Φ, s) = Φ(0) ζ(s).

Русский

Для любой функции Φ: ZMod 1 → ℂ выполняется: L(Φ, s) = Φ(0) ζ(s).

LaTeX

$$$$L(\Phi, s) = \Phi(0) \zeta(s).$$$$

Lean4

/-- The L-function of a function on `ZMod 1` is a scalar multiple of the Riemann zeta function. -/
theorem LFunction_modOne_eq (Φ : ZMod 1 → ℂ) (s : ℂ) : LFunction Φ s = Φ 0 * riemannZeta s := by
  simp only [LFunction, Nat.cast_one, one_cpow, ← singleton_eq_univ (0 : ZMod 1), sum_singleton, map_zero,
    hurwitzZeta_zero, one_mul]

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