LSeries_vonMangoldt_eq — Mathlib

English

The L-series of von Mangoldt Λ equals the negative derivative of the L-series of the constant function 1: L((↗Λ), s) = -d/ds L(1) s / L(1) s, for Re(s) > 1.

Русский

L-ряд Λ равен отрицательной производной от L-ряды константы 1: L((↗Λ), s) = - L'(1,s) / L(1,s), при Re(s) > 1.

LaTeX

$$L(↑Λ) s = - deriv(L 1) s / L 1 s$$

Lean4

/-- The L-series of the von Mangoldt function `Λ` equals the negative logarithmic derivative
of the L-series of the constant sequence `1` on its domain of convergence `re s > 1`. -/
theorem LSeries_vonMangoldt_eq {s : ℂ} (hs : 1 < s.re) : L (↗Λ) s = -deriv (L 1) s / L 1 s :=
  by
  refine (LSeries_congr (fun {n} _ ↦ ?_) s).trans <| LSeries_modOne_eq ▸ LSeries_twist_vonMangoldt_eq χ₁ hs
  simp [Subsingleton.eq_one (n : ZMod 1)]

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